問題タブ [spin]

SPIN で計算された状態空間を出力して、その視覚化を行い、手動で調査できるようにしたいと考えています。それは可能ですか？

私はすでに -DCHECK や -DVERBOSE などのフラグをチェックしましたが、それらは私が探しているものではないと思います...

次のLTLプロパティの単純なPromelaモデルをモデルチェックしようとしています:

そして、エラーが発生しました。エラートレイルのガイド付きシミュレーションでは、次の出力が得られます。

ここで、「M[0] until M[1]」がどこで違反されているのかわかりません。M[0] は init プロセスで 1 に設定され、M[1] が 1 になるまでそのままです。トレースが非常に早く終了するか、「stronguntil」のセマンティクスを完全に誤解している可能性があります。私はこれが事実であると確信しています...しかし、私は何が間違っていますか? Promela ファイル内の LTL の指定は大丈夫ですか?

問題のモデルは次のとおりです (単純なペトリネット)。

スピン ガイドを読みましたが、次の質問に対する回答がありません。

コードに次のような行があります。

ここで、Ch はチャネル、x はチャネル タイプ (MSG を受信するため) です。Ch が空の場合はどうなりますか? MSG が到着するのを待ちますか? Ch が空でないかどうかを最初に確認する必要がありますか?

基本的に私が望むのは、Chが空の場合、MSGが到着するまで待ち、到着したら続行することです...

Spin でモデルを書きました。モデルの LTL を確認したい。例えば：

[検証] ウィンドウで、[クレームを使用] オプションを選択し、[実行] をクリックします。

この時点で、私は次に何をすべきかわかりません...？Google で答えを探してみましたが、Spin の使用方法に関するガイドはありません....

複数のステートメントを無限に頻繁に実行する必要があるという公平性の制約があるプログラムで、LTL プロパティを検証できるかどうか疑問に思っています。

例えば：

このプログラムは、最終的にno_flipフラグが trueに flagなり、true になった場合に正しいです。

ただし、'pan -a' と 'pan -a -f' (弱い公平性) の両方を実行すると、no_flip=1ステートメントと受け入れ状態 (LTL 式から) を循環します。

進行状況ラベルは、実行が無限に頻繁に通過することを強制すると思っていましたが、そうではないようです。では、そのような公平性制約を追加することは可能ですか?

ありがとう、ヌーノ

Spin を使用してベーカリー ロックを作成しました

テストすると、次のエラーが表示されます: pan:1: アサーション違反 - 無効な配列インデックス (深さ 5)

トレイルを走ると、これが戻ってきます

この行をスキップする理由を誰か教えてください (i == n) -> break; ?

グローバル変数のデフォルト値はありますか? または、モデル チェッカーは可能なすべてのインターリービングをチェックします。つまり、この場合、 と の両方(x==0)で可能なすべての状態を使用し(x>0)ます。