問題タブ [model-checking]

私は、CBMC (C 境界モデル チェッカー) で「正確に 1 回」のプロパティを記述するためのより良い解決策を思いつくために一生懸命努力しています。つまり、行内の 1 つの要素の位置が値 1 (またはブール値 true としてチェックできる任意の正の数) を持つ必要があり、残りはすべてゼロでなければなりません。

M = 4 の場合

それ以上のMは大問題です。M = 8 としましょう。次のようなことをしなければなりません:

違反を 1 回だけチェックするのは簡単ですが、それを述べるのは簡単ではありません。もう 1 つのオプションがあります。2 次元配列の問題を 1 次元のビットベクトルの問題に記述してから、スマート xor を実行することです。しかし、私は現在それについて確信が持てません。

誰にも問題のより良い解決策がありますか?

SPIN モデル チェッカー GUI - iSPIN を使用しています。GUI には便利なオートマトン ビュー ジェネレーターが付属していますが、完全なオートマトンを表示するにはズームイン/ズームアウトする必要があります。また、可能であれば、そのオートマトンを素敵な画像で保存したいと思います（印刷画面の使用は避けてください）。Promela モデルに基づいて、SPIN またはオートマトンを生成できる別のツールから生成されたオートマトン イメージを保存する方法はありますか?

PS 以下は、保存したい生成された Automaton 画像を示す画像です。もちろん、プリントスクリーンだけでは再現できません。

次のような状況をモデル化するための適切な形式 (つまり時相論理) を探しています。

1. 時間内に個別のイベントでイベントが発生する可能性があります (以下に詳述する条件に従います)。
2. 状態あります。この状態は一定数の変数では表現できません。ただし、各エントリが有限数の変数で構成される線形リスト/配列で表現することは可能です。
3. イベントが発生する前に、状態は修正されます。
4. いつでも、イベントが可能です。それらは固定された構造を持っています (いくつかの変数があります)。発生する可能性のあるイベントは、現在の状態によって制限されます。
5. イベントは、状態の即時変更を引き起こします。
6. イベントによって、状態が継続的に変化することもあります。たとえば、(上記の配列のエントリの 1 つの) 変数は、その値を 0 から 1 に一定時間 (すぐに、または指定された遅延の後に) 変更します。
7. また、「ある条件 C が成立するイベント E の後の最も早い時点」という形式で離散的な時点を指定し、そのような時点で連続的な状態変化を開始することも可能である必要があります。

このようなものをモデル化するための既存の時相論理はありますか?

次のように、希望する条件を表現することも可能である必要があります。

1. 特定の時点の参照: 配列のすべてのエントリの特定の変数の合計は、特定のしきい値を超えることはできません。
2. 時間の経過に伴う変化の参照: すべての可能な時間間隔について、特定の変数の値 (再び、前述の配列の各エントリから) [現実的には、各エントリに対して計算された算術式ではなく] は、指定されたしきい値よりも速く変化してはなりません。

考えられるすべてのシナリオについて、すべての条件が満たされているかどうかをチェックできるモデル チェッカーが存在する必要があります。そうでない場合は、考えられるシナリオを 1 つ出力し、どの条件が満たされていないかを通知する必要があります。つまり、可能性のあるシナリオを説明する条件と、それらのシナリオで満たされなければならない条件を区別する必要があり、単に「不可能」とだけ言うのではありません。

NuSMV で信号機システムの実装を作成しようとしています。現在、NS/EW 赤、黄、緑の 6 つのブール値があります。ただし、将来の状態でそれぞれが常に true であると指定すると、false が返されます。誰かが私のコードにエラーを見つけたら、助けていただければ幸いです。ありがとう。

NuSMV ツールを使用して CTL が正しいかどうかを検証すると、混乱する問題に遭遇します。

私のモデルは

NuSMVコードは次のとおりです。

私のCTL式は次のとおりです。

1. "AG( A1 -> AX ( A [ B1 U ( D1 -> EX ( F1) ) ] ) )"
2. "AG( A1 -> AX ( A [ B1 U ( F1 -> EX ( C1) ) ] ) )"
3. "AG( A1 -> AX ( A [ M1 U ( F1 -> EX ( C1) ) ] ) )"

NuSMV は上記の 3 つの公式を検証し、すべてが真であることが判明しました。

では、私の質問は、なぜ式 2 と式 3 が真になるのかということです。

Windows7-64 で SPIN モデル チェッカーを使用したいのですが、その前提条件をすべてインストールしました。以下は私がそれをした手順です

1. cygwin で gcc コンパイラをインストールしました。コマンド プロンプトで更新されたパスを確認すると、バージョン 4.9.2 が表示されます
2. インストールされた Active Tcl .. 更新されたパス .. ispin を開くと正常に動作します。
3. ispin ディレクトリのパスも更新されました。
4. ちょっとしたトリックですが、ispin ファイル内の gcc.exe の正確なパスを指定して確認してください。しかし、エラーは同じままでした。

しかし、あらかじめ含まれているサンプル ファイル (例: Leader.pml) をコンパイルしようとすると、エラーが発生します。

誰かが私が間違っていることや欠けていることを教えてもらえますか? どうすればこれを修正できますか？

ありがとう。

ubuntu マシンに NuSMV 2.5.4 をインストールしました。コマンド NuSMV -int first.smv を使用して対話モードで実行すると、次の応答が表示され、入力ファイル first.smv を開けません。何故ですか？smv ファイル (first.smv) を bin フォルダーに配置しました。