問題タブ [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.
model-checking - 決定木が不変条件を満たしているかどうかを確認する方法は?
私は決定木と不変条件が何であるかを知っています (それが正しい用語であれば)。使用される他のすべての定義 ( UsingTor、UsingProxyなどは何でもかまいません)。TLA+ を使用して、ディシジョン ツリーのすべての葉が不変条件を満たしているかどうかを確認するにはどうすればよいですか?
決定木が状態のシーケンスである場合、これを行う方法を知っています。この不変条件を満たす状態になるかどうかを常に確認します。ただし、これを行う方法がわかりません。
formal-verification - Coffee Can TLA+ の問題 : タスクを表現できない
David Gries の Coffee Can Problemを TLA+ でモデル化しようとしていますが、この部分で行き詰っています。
「最初に缶に入っていた黒豆と白豆の数の関数として、最終的に残った豆の色について何が言えますか?」
これにアプローチする方法がわかりません。アドバイスやヒントを教えてください。（方法論も大歓迎です）
これは TLA+ の私のコードです:
specifications - TLA+ エラー: 不変不変式は状態述語ではありません
私の仕様では、シーケンスの変更が -1、0、または 1 のいずれかであるかどうかを確認しようとしています。
この不変式を次のように説明しました。
TLC モデル チェッカーは次のように出力します。