問題タブ [spin]

Spin でモデルを作成しました。シミュレーションは期待どおりに実行されています。ただし、ltl プロパティを確認しようとすると、次の結果が得られます。

トレイル ファイルを使用してシミュレーションを実行しても、シミュレーションはすぐに終了するため、多くの情報は得られませんでした (未使用の変数に関連する警告のみが表示されます)。VECTORSZ is too smallそれが問題の原因であると思われます。iSpin を使用してこの値を変更するにはどうすればよいですか?

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

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

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

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

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

2 つのプロセス S が別のプロセス R にメッセージを送信する単純なモデルを Spin で作成しました。次に、プロセス R が両方のプロセスに応答を送信します。以下に示すように、「プロセス x がメッセージを送信した場合、プロセス y が最終的にそれを受信する」というプロパティを定義したいと思います。問題は、シミュレーションが期待どおりに機能しているにもかかわらず、検証がうまくいかないことです。9 行目で定義したプロパティは常にエラーなしで渡されますが、17 行目で検証を失敗させるエラーを挿入しました。ここで何か不足していますか？

Spin Modal Checker の promela 構文を学習しています。この単純なコードに遭遇しました。

私が知っているように、セミコロンはステートメントの終わりを定義するために使用されます。andと after;の両方の最後で使用できますか; プログラムの動作は変わりますか? このセミコロンをクリアしてくれてありがとう。count++count--fi

しばらくグーグルで検索したところ、SPIN の CTL または CTL* モデル チェックを提案している論文がいくつか見つかりました。ただし、Promela のマニュアル ページによると、Promela モデルで CTL を表現する方法はありません。今はちょうど提案レベルですか？

PROMELA で LTL を Automata に変換するにはどうすればよいですか? コマンド SPIN -f "ltl x" を使用すると、LTL を決してクレームに変換できないことはわかっていますが、否定ではなく LTL のオートマトンが必要です。never クレームを生成する前に LTL を否定すれば正しいです。誰でも私を助けることができますか？

Spin を使用してプロパティの複数 (またはすべて) の違反トレースを取得することはできますか?

例として、以下の Promela モデルを作成しました。

単純なミューテックスの実装があります。プロセス A と B が一緒にクリティカル セクションに到達しないことが予想されるので、それをチェックするために LTL 式を書きました。

ランニング

プロパティが有効ではなく、実行中であることを示します

プロパティに違反する一連のステートメントを表示します。

これは、一連のステートメント (ラベルで示される) 'B1' -> 'A1' -> 'B2' -> 'A2' がプロパティに違反していることを示していますが、それにつながる他のインターリーブ オプションがあります (例: 'A1' -> ' B1' -> 'B2' -> 'A2')。

Spin に複数 (またはすべて) のトレースを提供するように依頼できますか?

以下は、私が書いている Promela コードです。

しかし、コードをシミュレートしようとすると、次のようなエラー メッセージが表示されます。

見た: '['、予想される ':' スピン: osek_sp2.pml:507、エラー: 予想される選択 (名前: 定数 .. 定数) 近くの '選択'

しかし、構文定義によると、問題は見つかりません。

SYNTAX
select '(' varref ':' expr '..' expr ')'

varref : 名前 [ '[' any_expr ']' ] [ '.' varref ]

このエラー メッセージの理由は何ですか?

私は SPIN と Promela にかなり慣れていないので、モデルの liveness プロパティを検証しようとしているときにこのエラーに遭遇しました。

エラーコード：

コードは基本的にピーターソンのアルゴリズムの実装であり、安全性をチェックしたところ、有効なようです。しかし、ltl {[]((wait -> <> (cs)))} を使用して liveness プロパティを検証しようとすると、上記のエラーが発生します。意味がよくわからないのでどうすればいいのかわかりません...

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