問題タブ [nusmv]
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.
logic - NuSMV で再帰的に定義されたエラーを理解する
エラーが発生した NuSMV のコードがあります。コードは次のとおりです。
したがって、これを NuSMV でコンパイルすると、エラーが発生します。recursively defined: x1
x1 の遷移ルールの x2 に関連付けられた次のステートメントを削除することで、このエラーを簡単に処理できx1=d & next(x2)=c : a;ますx1=d : a;。x1=d & x2=d : a;
エラーの原因となっている NuSMV ソフトウェアの仕組みと、上記の修正によってエラーが解決される理由を理解したいと思います。私が理解していない同期実装何とか何とか何とかしていると思います。誰かが正確で詳細な技術的説明をすることができますか?
また、 variable でエラーが発生しない理由も説明してくださいx2。その遷移規則は、次の演算子を使用して定義されています。
model-checking - NuSMV のネストされた NEXT 演算子の構文エラー
NuSMV を使用してモデルをチェックしようとしましたが、コードは次のとおりです。
ただし、NuSMV kernel.smvシェルに入力するとエラーが発生します
私は NuSMV モデル チェッカーの初心者なので、この構文エラーを修正できませんでした。助けてください、ありがとう！