問題タブ [model-checking]

次の構造 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 であることを返し、反例を生成します。

次の単純な PROMELA モデルを検討してください。

私は、spin -f を使用して生成された次の単純な主張で、このモデルを検証したかったのです。

ただし、これを使用した検証は

結果が出ません。-a オプションを試しても結果は得られません。任意のランダム シミュレーションは、ある時点で明らかに p が false であることを示しています。

基本的な何かが欠けていますか？

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

したがって、2 人の Patron が現在同じ本を持つことはできないという主張を追加したいと思います。これが私が持ってきた主張です：

したがって、アサーションを次のようにチェックします。

Alloyは反例を見つけません。しかし、run コマンドを使用すると、Alloy は多くの反例を示します。

また、有効なアサーションを否定して事実を追加しても、インスタンスが得られないことになっていることを読みました。私はそれを追加しました：

モデルを実行すると、Alloy は有効なインスタンスを見つけます。

私は何を間違っていますか？ありがとうございました。

私は Windows OS を使用しており、Cygwin i で次のように入力wish -f ispin.tclして ispin インターフェイスを開きます。test.pml以下を含むファイルを開きます。

その後、シード = 123 でランダムな方法を使用して実行します。結果は問題なく出力に出力されます。

このモデルを検証しようとすると、問題が発生します。検証の結果は次のとおりです。

どうすればこれを解決できますか? インターネットで検索しましたが、役立つ情報が見つかりませんでした。

注：検証プロパティは変更していません：

C と C++ の両方のプログラムに対して、Ubuntu でCBMC Bounded Model Checkerを使用しようとしています。gcc (4.9 v) および g++ (4.9 v) コンパイラをダウンロードし、端末から CBMC をインストールしました。

C プログラムを検証でき、以下の手順を使用しても問題は発生しません。

Α .c ファイルの名前file2.c:

端末タイプ:

出力：

次の .cpp ファイルを実行しようとすると、エラーが発生します。

sum_num.cppファイル：

ターミナルに次のように入力します。

出力 - エラー:

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

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

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

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