モジュールのオーバーロード メカニズムは、こちらのハノイの塔のサンプルで説明されています。モデルチェックのパフォーマンスを向上させるために、Java で TLA+ 演算子を実装できます。
私はしばらくの間、TLA+ で便利なハッシュ関数を定義するのに苦労してきました (いいえ、ID 関数は私の目的では機能しません)。モジュールのオーバーロードがそれを行う方法かもしれないと考えています。ハッシュ関数は、TLA+ オブジェクト (レコードなど) を受け入れ、hashCode()オブジェクトの文字列表現に対して Java のメソッドを使用して、決定論的にそのハッシュ値を導き出します。この値は TLA+ 仕様に戻されます。
これは可能ですか？Java オーバーライド コードはどのようになりますか? 他のモジュール オーバーライド コード サンプルはありますか?