問題タブ [promela]

私はスピンモデルのチェックにかなり慣れていないので、このエラーの意味を知りたいと思っていました:

ここに私のコードがあります:

実際に終了する必要はありません。これは、2 つのプロセスが一緒にクリティカル セクションにないかどうかをチェックする相互排除プログラムです。エラーはプログラムが終了しないことを意味しますか? ありがとう！

私が教えるコースでは、並行性のモデリングに Promela と Spin を使用しています。私はjspinフロントエンドも使用しています。Windows 8 にツールをインストールしようとしている学生がいますが、彼らは苦労しています。それが 64 ビットと 32 ビットの問題なのか、使用している gcc のバージョンなのか、それとも完全に別のものなのかはわかりません。

そのため、Windows 8 でこれらのツールの動作構成を持っていて、ツール チェーンの使用方法などについて助けてくれる人を探しています。

さて、私はこれを持っています（これはコードの一部です）：

/////////////でスタックし（書き込みタイムアウト）、たとえばステップ40に進む方法はありません。

これは、Ricart-Agrawala アルゴリズムの一部です。ここでは次のようになります。

私は何を間違っていますか？前もって感謝します

PS クリティカル - クリティカル セクションの「シミュレーター」です。このアルゴリズムは分散システム用です...

たとえば、私は次のものを持っているとしましょう

私は得る

私が理解しているのは、基になる変数が char 型であるためです。ただし、その文字の mtype を取得したいのですが、文字をその mtype に相互参照する方法はありますか?

sプロセスがセットからランダムに要素を選択する必要があるモデルがありますS。選択部分は単一の操作です。UPPAAL で私が知っている唯一の同様のデータ構造は配列です。

UPPAAL には一定のデータ構造が存在しますか? そうでない場合は、どうすれば作成できますか?

私のモデル チェック コードでは、特定の変数の最大値を見つけることにのみ関心があります。私が今採用している手順は、assert ステートメントを持ちassert( var < MAX_VALUE )、MAX_VALUE を二分探索方式で変更し続けることです。ただし、SPIN が実際に 1 回の実行で変数の最大可能値を与える方法を持っていれば、はるかに優れています。supUPPAALにはそのためのオペレーターがあることを知っています。SPINに同等のものはありますか?

私は非常に単純な送信者 - 受信者プロトコルを持っています:

4 つのパケットを送信してから受信します。次に、プロパティを証明しようとします: 常に送信は最終的に受信を意味します:

ltl pr { [] ( (送信 == 1) -> (<> (受信 == 1)) }

...そして何も起こりません: SPIN は、このプロパティの証明とその否定の両方を見つけません。

なんで？

モデル チェックに Promela を使用して Spin を評価していますが、処理時間が問題になります。マルチコアを使用して計算を改善できることを見てきましたが、計算を高速化するための GPU/Cuda サポートについてはどうですか? 私はこれを行うことができますか？

エイドリアンよろしく