問題タブ [promela]

私は次のpromelaコードを持っています:

レベル (0-9) 情報をチャネルに送信し、このレベルに応じてセンサー出力を low|normal|high にすることを期待しています。とてもシンプルです。しかし、なぜ SPIN はいつもタイムアウトを言っているのでしょうか?

do ループの反復を 1 回しか実行していないように見えるのはなぜですか?

以下に示すように、for ループを使用して typedef 値の配列をループできるようにしたいと考えています。

Spin で次のエラーが発生します。

インデックス ポインターで for ループを使用する代わりに、この形式で for ループを使用して配列をループすることは可能ですか?

ダイクストラが「シーケンシャルプロセスの協調」というタイトルの論文で書いたALGOL60コードを再現しようとしています。このコードは、ミューテックス問題を解決する最初の試みです。構文は次のとおりです。

だから私はPromelaで上記のコードを再現しようとしました、そしてここに私のコードがあります：

私がやろうとしているのは、ラベルL1が無限に実行されているため、公平性プロパティが保持されないことを確認することです。

ここでの問題は、neverclaimブロックがエラーを生成していないことです。取得した出力は、単に私のステートメントに到達しなかったことを示しています。

これがiSpinからの実際の出力です

ブロックのスピンに関するすべてのドキュメントを読みましたnever{..}が、答えが見つかりませんでした（ここにリンクがあります）。また、ltl{..}ブロックを使用してみました（リンク）が、明示的には構文エラーが発生しました。ドキュメントに、initおよびの外部にある可能性があると記載されていますがproctypes、誰かがこのコードを修正するのを手伝ってもらえますか？

ありがとうございました

ispinを使用してモデルを検証しようとすると、「long long long is toolongforgcc」というエラーが表示されます。gccに問題はありますか？

誰かが私に次のコードでタイムアウトが発生する理由を説明できれば、それは素晴らしいことです。私はタイムアウトの考えを理解している、または少なくとも私は理解していると思いますが、doループを使用すると、これでこれが止まると思いました。アドバイスをいただければ幸いです。

SPIN で計算された状態空間を出力して、その視覚化を行い、手動で調査できるようにしたいと考えています。それは可能ですか？

私はすでに -DCHECK や -DVERBOSE などのフラグをチェックしましたが、それらは私が探しているものではないと思います...

次のLTLプロパティの単純なPromelaモデルをモデルチェックしようとしています:

そして、エラーが発生しました。エラートレイルのガイド付きシミュレーションでは、次の出力が得られます。

ここで、「M[0] until M[1]」がどこで違反されているのかわかりません。M[0] は init プロセスで 1 に設定され、M[1] が 1 になるまでそのままです。トレースが非常に早く終了するか、「stronguntil」のセマンティクスを完全に誤解している可能性があります。私はこれが事実であると確信しています...しかし、私は何が間違っていますか? Promela ファイル内の LTL の指定は大丈夫ですか?

問題のモデルは次のとおりです (単純なペトリネット)。

スピン ガイドを読みましたが、次の質問に対する回答がありません。

コードに次のような行があります。

ここで、Ch はチャネル、x はチャネル タイプ (MSG を受信するため) です。Ch が空の場合はどうなりますか? MSG が到着するのを待ちますか? Ch が空でないかどうかを最初に確認する必要がありますか?

基本的に私が望むのは、Chが空の場合、MSGが到着するまで待ち、到着したら続行することです...

Spin でモデルを書きました。モデルの LTL を確認したい。例えば：

[検証] ウィンドウで、[クレームを使用] オプションを選択し、[実行] をクリックします。

この時点で、私は次に何をすべきかわかりません...？Google で答えを探してみましたが、Spin の使用方法に関するガイドはありません....