問題タブ [spin]

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

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

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

以下のようなコードを使用して、検証モードでスピンを実行しています。「never」という関数に問題があります。実行中に、関数 inc()、dec()、reset() が完了していないというエラーが表示されます。しかし、サイクルを追加すると、うまく機能します。ドキュメントでは、「決して」すべてのステップで変数をチェックしません。では、なぜサイクルがないと機能しないのでしょうか。

「決して」ブロックしないと、警告が表示されます

実際には、これはエラーではなく、一種の警告であり、proctype Inc、Dec、Reset、Init で unreached が表示されます。完全な警告ログは以下のとおりです。

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

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

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

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

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

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

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

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

私は得る

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

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

基本的に、モデル チェックでは、モデル 'm' (システムの動作記述) と、システムが満たすプロパティ 'p' を扱います。どちらのアーティファクトでも、モデル チェッカーはモデルがプロパティを満たすかどうかを判断します。

私の質問は、モデル 'm' を LTL 式として指定し、LTL 'm' としてのモデルがプロパティ 'p' を満たすかどうかを確認できるかどうかです。

理論的には、LTL 式 'p' 用とモデル 'm' を記述する LTL プロパティ用の 2 つの Büchi オートマトンを生成できるため、このアプローチはうまくいくと思います。2 つの非決定性オートマトンの共通部分が空の場合、LTL としてのモデル 'm' はプロパティを満たします。

誰かが私にヒントを与えることができますか？出来ますか？

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

エイドリアンよろしく

私の設計では、N 個のグローバル変数と、状態に応じて、前述のパラメーターのいくつかをパラメーターとして受け取るメソッドがあります。

グローバル変数を参照渡しのパラメーターとして渡すことはできますか?

この論文は、結論の部分で明示的に次のように述べています。

「Spin がサポートしていない参照渡しパラメータの特別な形式」

これを行うことができる他の方法はありますか？(つまり、変数名を渡す)

構造を以下に示します

PS たとえば、使用できません：

AProcess は他の変数の存在を認識できないため、どの変数が渡されたかを確認します。