問題タブ [nusmv]

次の構造 M = (S, R, L) があるとします。ここで、S = {s0, s1, s2} は可能な状態のセットであり、R は次のような遷移関係です: s0 -> s1, s0 -> s2, s1 -> s0、s1 -> s2、および s2 -> s2、および L は、L(s0) = {p, q}、L(s1) = {q, r}、およびL(s2) = {r}。Huth と Ryan による Logic in Computer Science の教科書に記載されている表記法を使用しています。

明らかに、このようなモデルから、s1 と s2 で r が満たされているため、s0 (初期状態) で X r が満たされていることがわかります。Kripke 構造の NuSMV コードは次のとおりです (ここで説明)。

しかし、NuSMV は仕様 X r が false であることを返し、反例を生成します。

私は NuSMV を初めて使用し、この単純なターン制ゲームをモデル化しようとしています。山には10個のレンガがあり、各プレイヤーは1ターンに1〜3個のレンガを取ることができ、最後のレンガを取った人がゲームに勝ちます. プレイヤー A が最初に行くと仮定すると、これが私の試みです。「最終的に勝者がいる」と表現したいのですが、brick=0 の後にプレーヤーがブロックを取得することを妨げないため、私のコードは機能せず、最終的にプレーヤー a,b の両方が勝者になります。

ここに私のコードがあります:

そして、これが私の要点を説明するための SPEC AF (勝者 = a | 勝者 = なし) での私の出力です。

ご覧のとおり、モデルは、プレイヤー a がすでに勝った後にプレイヤー b がゲームに勝つという反例を提供します。

提供された readme を使用して NuSMV をインストールしましたが、NuSMV コマンドを使用しようとすると、次のメッセージが表示されます: -bash: NuSMV: command not found

これについてはネット上にあまり情報がありませんので、お役に立てれば幸いです

私は NuSMV を初めて使用します。Kripke 構造から自動販売機の実装を作成しようとしています。3 つのブール値 (コイン、選択、醸造) と 3 つの状態があります。しかし、コードをコンパイルすると、"Line 25: at token ":": 構文エラー" 誰かが私のコードにエラーを見つけたら、助けていただければ幸いです。

クリプキ構造

コードを記述しようとする私の試みは次のとおりです。

NuSMV を使用して Dekker アルゴリズムを検証します。私のコードは次のとおりです。

しかし、フィードバックは写真のようなもので、「:」の不正な左オペランド型を示しています。ブール値にする必要があります。どうしてか分かりません。助けてください... コードの何が問題なの NuSMV フィードバック