問題タブ [spin]

誰かがこのツールSPINを使ったモデル検査、さらにモデル検査の情報（並行プログラム）に触れたことはありますか

Spin でアルゴリズムをモデリングしています。複数のチャネルを持つプロセスがあり、ある時点で、メッセージが送信されることはわかっていますが、どのチャネルから送信されるかわかりません。そのため、いずれかのチャネルからメッセージが来るまでプロセスを待機 (ブロック) したいと考えています。どうやってやるの？

Spin Model Checker を使用して、2 つのオブジェクト (A と B) 間のゲームをモデルチェックしようとしています。オブジェクトはボード上を移動し、各位置はその (x,y) 座標によって定義されます。2 つのオブジェクトは衝突しないはずです。init、A Model、B Model の 3 つのプロセスがあります。私は ltl プロパティをチェックするモデルです: (2 つのオブジェクトが同じ場所を占有するかどうかをチェックする liveness プロパティ)

私が得るエラートレイルは次のとおりです: init -> A Model -> B Model -> init

ただし、表示されているデータに基づいてエラー トレイル (反例) を取得する必要はありません: x_a=2、x_b=1、y_a=1、y_b=1。

また、最初の init は init プロセスのすべての行を通過しますが、2 番目の init はその最後の行までしか表示されません。

また、私の A モデルと B モデルは、以下に示すように、「do」ブロック内のガードとアクションのみで構成されています。ただし、それらはより複雑で、'->' の右側に if ブロックがあります。

アトミックブロックに何かを入れる必要はありますか? 私が質問している理由は、エラー トレイルが示している行が 'do' ブロックにも入っておらず、2 つのモデルの最初の行に過ぎないからです。

編集: LTL プロパティが間違っていました。私はそれを次のように変更しました：

しかし、私はまだまったく同じエラートレイルを取得しています。

あるプロセスのローカル変数の値に別のプロセスからアクセスすることは可能ですか? たとえば、以下のプログラムでは、マネージャーから my_id の値を読み取りたいとします。

私は次のpromelaコードを持っています:

レベル (0-9) 情報をチャネルに送信し、このレベルに応じてセンサー出力を low|normal|high にすることを期待しています。とてもシンプルです。しかし、なぜ SPIN はいつもタイムアウトを言っているのでしょうか?

do ループの反復を 1 回しか実行していないように見えるのはなぜですか?

以下に示すように、for ループを使用して typedef 値の配列をループできるようにしたいと考えています。

Spin で次のエラーが発生します。

インデックス ポインターで for ループを使用する代わりに、この形式で for ループを使用して配列をループすることは可能ですか?

ダイクストラが「シーケンシャルプロセスの協調」というタイトルの論文で書いたALGOL60コードを再現しようとしています。このコードは、ミューテックス問題を解決する最初の試みです。構文は次のとおりです。

だから私はPromelaで上記のコードを再現しようとしました、そしてここに私のコードがあります：

私がやろうとしているのは、ラベルL1が無限に実行されているため、公平性プロパティが保持されないことを確認することです。

ここでの問題は、neverclaimブロックがエラーを生成していないことです。取得した出力は、単に私のステートメントに到達しなかったことを示しています。

これがiSpinからの実際の出力です

ブロックのスピンに関するすべてのドキュメントを読みましたnever{..}が、答えが見つかりませんでした（ここにリンクがあります）。また、ltl{..}ブロックを使用してみました（リンク）が、明示的には構文エラーが発生しました。ドキュメントに、initおよびの外部にある可能性があると記載されていますがproctypes、誰かがこのコードを修正するのを手伝ってもらえますか？

ありがとうございました

ispinを使用してモデルを検証しようとすると、「long long long is toolongforgcc」というエラーが表示されます。gccに問題はありますか？

誰かが私に次のコードでタイムアウトが発生する理由を説明できれば、それは素晴らしいことです。私はタイムアウトの考えを理解している、または少なくとも私は理解していると思いますが、doループを使用すると、これでこれが止まると思いました。アドバイスをいただければ幸いです。