問題タブ [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.
file - NuSMV でファイルを読み取る
NuSMV にトランジション システムを実装したいと考えています。このトランジション システムは .txt ファイルで指定されており、ツールで読み取り、そこから TS をビルドします。ファイル形式は次のとおりです。
6
1 2
2 3
3 4
4 5
5 6
これは、頂点/ノードの総数が 6 で、その後にそれらの間のエッジを指定するタプルが続く特定の例です。NuSMV でいくつかの例を見てきましたが、遷移システムを記述したファイルを読み取るための適切な例が得られません。誰でも助けることができますか？
verification - クリプキの建造物に警備員を配置できますか?
私は単純な kripke 構造を持っています。ここには 3 つの状態があり、次の遷移があります。
s1 は唯一の初期状態です。ループ s1 から s2 を一定量以上 (たとえば 2 回) 繰り返したくありません。他のトランジション システムでは、トランジションにガードを追加できます。
Q1: Kripke 構造はトランジションにガードを付けることができますか?
Q2: はいの場合、NuSmv でモデル化するにはどうすればよいですか?
ありがとう