問題タブ [promela]

次のスニペットを検討してください。

これは、カウンターが 0 を下回るまで値 0..3 をかなり恣意的に出力し、その時点で別の数値を出力するか終了することを期待するでしょう。

しかし、そうではないようです。

返される値は、0、次に 1、次に 0、次に 1、次に 0、次に 1 だけです。

if/fi ステートメントの「非決定論」を誤解したのでしょうか?

（問題がある場合は、ubuntuでispinを使用してください）。

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

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

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

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

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

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

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

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

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

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

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 プロパティを検証しようとすると、上記のエラーが発生します。意味がよくわからないのでどうすればいいのかわかりません...

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