問題タブ [tla+]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
graph - TLA+ 状態グラフを視覚化する方法
私は新しいTLA+ユーザーです。TLAツールボックスを使用すると、モデル チェックの完了後に状態グラフを視覚化できると読みました。
そのためには、私が行ったようにドットをインストールする必要があります。しかし、ビジュアライゼーションを起動する方法がわかりませんでした。GUI を使用して購入できますか、それとも専用のコマンド ラインを使用する必要がありますか?
ありがとう
tla+ - TLA+ 要素の削除に関する問題
現在 TLA+ を学習しており、この簡単な登録簿から人を削除する方法に行き詰まっています。問題は、私が見ることができる許可状態にあるようです。
私の TLA+ 関数は次のようになり、許可と共に登録者から人を削除します。
チェックしているtypeokには次の制約があります
typeOK に違反しているというモデル エラーが発生します。スタックトレースでは、エラーは次のようになります
洞察をありがとう
編集：
以前の状態は、何らかの用途に役立つ可能性があります。
tla+ - モジュールのオーバーロードを使用して TLA+ でハッシュ関数を実装する
モジュールのオーバーロード メカニズムは、こちらのハノイの塔のサンプルで説明されています。モデルチェックのパフォーマンスを向上させるために、Java で TLA+ 演算子を実装できます。
私はしばらくの間、TLA+ で便利なハッシュ関数を定義するのに苦労してきました (いいえ、ID 関数は私の目的では機能しません)。モジュールのオーバーロードがそれを行う方法かもしれないと考えています。ハッシュ関数は、TLA+ オブジェクト (レコードなど) を受け入れ、hashCode()オブジェクトの文字列表現に対して Java のメソッドを使用して、決定論的にそのハッシュ値を導き出します。この値は TLA+ 仕様に戻されます。
これは可能ですか？Java オーバーライド コードはどのようになりますか? 他のモジュール オーバーライド コード サンプルはありますか?