問題タブ [promela]

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

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

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

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

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

構造を以下に示します

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

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

Promela でオブジェクトの発射体の軌道をモデル化し、モデルのいくつかのプロパティを検証したいと考えています。しかし、Promela には浮動小数点データ型がありません。したがって、たとえば、発射体のモーション パラメータを計算することはできません。たとえば、正弦/余弦などの三角関数を計算できないため、発射体の動きをモデル化できません。

この問題の回避策は何ですか? そのようなシステムを Promela でモデル化するにはどうすればよいでしょうか?

私は理想的には次のようなものが欲しいです:

しかし、私が知る限り、それはうまくいきません。これを行う方法はありますか？

私は現在、Promela/Spin を学んでいます。私が抱えている問題は、プログラムを検証できないことです。

私は自分の pan ファイルを次のように作成します: spin_64bits.exe -a x.pr --- ここまでは問題ありません。

今、gcc pan.c (gcc -o pan pan.c など) を介して pan.c をコンパイルしようとすると、srandom と random への未定義の参照があるというエラーが表示されます。

注: これらを srand() と rand() でそれぞれ交換すると機能しますが、正直なところ、検証を実行するたびに pan.c を開いて編集したくありません。

おそらく別のコンパイラを使用する必要がありますか？MinGWを使用しています。

複数のプロセスを作成し、それらが順番に他のプロセスを生成しています。したがって、SPIN モデルは「Too many processes (Max 255)」を出力し続けます。ただし、それでも最終的な出力が得られます。255 を超えるプロセスを処理できない場合、どのようにして最終出力を得ることができますか?

ispin を使用していますが、spin: Trails end after 10 steps and transition fails というエラーが表示されます。

このエラーの発生を防ぐにはどうすればよいですか?

メッセージのサイズを指定する方法はありますか? たとえば、チャネル AB を介してメッセージ データを送信したい場合、PROMELA 言語でデータのサイズを指定するにはどうすればよいですか?

SPIN モデル チェッカー GUI - iSPIN を使用しています。GUI には便利なオートマトン ビュー ジェネレーターが付属していますが、完全なオートマトンを表示するにはズームイン/ズームアウトする必要があります。また、可能であれば、そのオートマトンを素敵な画像で保存したいと思います（印刷画面の使用は避けてください）。Promela モデルに基づいて、SPIN またはオートマトンを生成できる別のツールから生成されたオートマトン イメージを保存する方法はありますか?

PS 以下は、保存したい生成された Automaton 画像を示す画像です。もちろん、プリントスクリーンだけでは再現できません。

Promela モデリング言語で ABP モデルを用意しました。しかし、別のモデリング言語である mCRL で書き直すには、助けが必要です。私はその経験がありません。誰かが開始方法を教えてくれますか、または mCRL の良いチュートリアルを教えてくれませんか? とにかく、 mCRL と mCRL2 のコードに違いはありますか?

プロメラの私のコード: