問題タブ [tla+]

TLA+言語のプロジェクト トピックに関する提案をお願いします。私は言語のコースを受講しています。仕様と検証について学んでいる最初の年であり、2 週間で実装するものを選択する手がかりがありません。何か案は？

私はもう試した

しかし、TLCは私に構文エラーを与えます：

エラー：TLCは、1行目の構成ファイルでエラーを検出しました。=または<-を予期していましたが、検出されませんでした。

Sequencesまた、モジュールを構成ファイルに含めようとしましたが、役に立ちませんでした。

だから...シーケンスを割り当てるために私は何をしなければなりませんか？

TLAで指定されたいくつかのアクションをErlangに翻訳したいと考えています。これを Erlang で直接行う自然な方法や、そのようなことができるフレームワークを思いつきますか? 一言で言えば (非常に小さなものです)、TLA アクションは変数の条件であり、その一部はプライミングされています。つまり、次の状態の変数の値を表します。例えば：

このアクションは、システムの状態がPredicateAvariable に対してtrue であり、に対して trueまたはtrue のxいずれかである場合は常に、システムはその状態を変更して、現在の値に 1 を加えた値に変更されることを除いてすべてが同じままになることを意味します。 .PredicateByPredicateCzx

Erlang でそれを表現するには、少なくとも私が見つけた方法では、多くの配管が必要です。たとえば、次のように、条件をトリガーする前に条件を評価するループを作成します。

この配管を非表示にするフレームワークを作成し、関数内にメッセージ パッシングを組み込みget_new_info()、できれば OTP 準拠にすることを考えています。すでにそれを行っているフレームワークを知っている場合、またはこれを実装する簡単な方法を考えられる場合は、それについて聞いていただければ幸いです。

ハノイの塔問題の TLA+ 仕様を書きました。

TEX

アスキー

Invariant数式を不変式として指定すると、TLA モデル チェッカーがパズルを解いてくれます。

理想的には、変更されていない変数を に渡したくありませんが、Move()方法がわかりません。私がやりたいことは、書くことです

それをTLA言語でどのように表現できますか？