問題タブ [spin]

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

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

SPINモデルチェッカーで調べました。ただし、動的割り当ての機能はありません。動的割り当てに使用できるモデル チェッカーは他にありますか?

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

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

私は現在、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 を超えるプロセスを処理できない場合、どのようにして最終出力を得ることができますか?

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

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

Windows7-64 で SPIN モデル チェッカーを使用したいのですが、その前提条件をすべてインストールしました。以下は私がそれをした手順です

1. cygwin で gcc コンパイラをインストールしました。コマンド プロンプトで更新されたパスを確認すると、バージョン 4.9.2 が表示されます
2. インストールされた Active Tcl .. 更新されたパス .. ispin を開くと正常に動作します。
3. ispin ディレクトリのパスも更新されました。
4. ちょっとしたトリックですが、ispin ファイル内の gcc.exe の正確なパスを指定して確認してください。しかし、エラーは同じままでした。

しかし、あらかじめ含まれているサンプル ファイル (例: Leader.pml) をコンパイルしようとすると、エラーが発生します。

誰かが私が間違っていることや欠けていることを教えてもらえますか? どうすればこれを修正できますか？

ありがとう。

iSpin/Promela に慣れようとしています。私は使っている：

Spin バージョン 6.4.3 -- 2014 年 12 月 16 日、iSpin バージョン 1.1.4 -- 2014 年 11 月 27 日、TclTk バージョン 8.6/8.6、Windows 8.1。

これは、LTL を使用しようとする例です。for ループの 2 つのステップがアトミックでない場合、LTL プロパティの検証でエラーが発生するはずです。

検証タップでは、LTL プロパティをテストしたいだけなので、すべての安全プロパティを無効にして、「使用クレーム」を有効にします。クレーム名は「alwaysten」です。

しかし、「アサーション違反」をアクティブにすると、LTL プロパティが評価されるだけのようです。なんで？同僚が iSpin v1.1.0 を使用していますが、これを有効にする必要はありませんか? 私は何を間違っていますか？アサーションと LTL プロパティを独立して証明したい...

トレースは次のとおりです。