問題タブ [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.

0 投票する
1 に答える
374 参照

model-checking - SMV の CTL 仕様を確認する

SMV で「EG (!s11included & !s10included)」をチェックしようとすると、false と報告され、次のように反例が示されます。これは、逆にこの CTL 仕様をサポートしていると思います。CTL 仕様に何か問題がありますか?

0 投票する
1 に答える
446 参照

random - ランダム トレースを使用した NuSMV シミュレーション

作成した NuSMV モデルの「ランダム」または非決定論的シミュレーションを実行しようとしています。ただし、後続の実行間で生成されるトレースはまったく同じです。

モデルは次のとおりです。

対話型シェルで次のコマンドを使用してこれを実行しています。

おそらく私のモデルに間違いがありますか?または、シェルで正しいコマンドを実行していません。

前もって感謝します!