問題タブ [spin]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
spin - PROMELA/SPIN で「任意の」チャネルからメッセージを受信する方法
Spin でアルゴリズムをモデリングしています。複数のチャネルを持つプロセスがあり、ある時点で、メッセージが送信されることはわかっていますが、どのチャネルから送信されるかわかりません。そのため、いずれかのチャネルからメッセージが来るまでプロセスを待機 (ブロック) したいと考えています。どうやってやるの?
model-checking - Spin Modelchecker からのエラー トレイルの理解
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 プロパティが間違っていました。私はそれを次のように変更しました:
しかし、私はまだまったく同じエラートレイルを取得しています。
spin - Promelaで別のプロセスからあるプロセスのローカル変数にアクセスする
あるプロセスのローカル変数の値に別のプロセスからアクセスすることは可能ですか? たとえば、以下のプログラムでは、マネージャーから my_id の値を読み取りたいとします。
verification - Promela/SPIN のタイムアウトの原因は何ですか?
私は次のpromelaコードを持っています:
レベル (0-9) 情報をチャネルに送信し、このレベルに応じてセンサー出力を low|normal|high にすることを期待しています。とてもシンプルです。しかし、なぜ SPIN はいつもタイムアウトを言っているのでしょうか?
do ループの反復を 1 回しか実行していないように見えるのはなぜですか?
spin - Promela: typedef 型の配列に for ループを使用する方法
以下に示すように、for ループを使用して typedef 値の配列をループできるようにしたいと考えています。
Spin で次のエラーが発生します。
インデックス ポインターで for ループを使用する代わりに、この形式で for ループを使用して配列をループすることは可能ですか?
model-checking - SpinおよびPromela構文を使用したLTLモデル検査
ダイクストラが「シーケンシャルプロセスの協調」というタイトルの論文で書いたALGOL60コードを再現しようとしています。このコードは、ミューテックス問題を解決する最初の試みです。構文は次のとおりです。
だから私はPromelaで上記のコードを再現しようとしました、そしてここに私のコードがあります:
私がやろうとしているのは、ラベルL1が無限に実行されているため、公平性プロパティが保持されないことを確認することです。
ここでの問題は、neverclaimブロックがエラーを生成していないことです。取得した出力は、単に私のステートメントに到達しなかったことを示しています。
これがiSpinからの実際の出力です
ブロックのスピンに関するすべてのドキュメントを読みましたnever{..}
が、答えが見つかりませんでした(ここにリンクがあります)。また、ltl{..}
ブロックを使用してみました(リンク)が、明示的には構文エラーが発生しました。ドキュメントに、init
およびの外部にある可能性があると記載されていますがproctypes
、誰かがこのコードを修正するのを手伝ってもらえますか?
ありがとうございました
gcc - 「ロングロングロング」はgccには長すぎますか?
ispinを使用してモデルを検証しようとすると、「long long long is toolongforgcc」というエラーが表示されます。gccに問題はありますか?
timeout - Spin/Promelaを使用するとタイムアウトします
誰かが私に次のコードでタイムアウトが発生する理由を説明できれば、それは素晴らしいことです。私はタイムアウトの考えを理解している、または少なくとも私は理解していると思いますが、doループを使用すると、これでこれが止まると思いました。アドバイスをいただければ幸いです。