問題タブ [spin]

次のコードでは、

次のエラーが表示されます。

どうしてこんなことに？Promela は cond1 のすべての値 (cond1 == 0 と cond1 != 0 の両方) に対して実行すべきではありません。少なくともこれはここに書かれているものです。

このモードでは、実際にはすべての動作オプションが一度に 1 つずつ探索されるため、検証中にそのような呼び出しは行われません。

キャッシュの一貫性を含め、マルチコア プロセッサのキャッシュをモデル化しようとしています。そのような PROMELA 実装は既に存在しますか? 私はそれを検索しようとしましたが、何も見つかりませんでした。次に、自分で実装する必要がある場合、PROMELA でキャッシュ構造を表すために非常に大きな配列を宣言することは可能ですか?

だから私が望むのは、プロセスAがプロセスBからDにメッセージをブロードキャストすることです.これはどのように行うことができますか? これを行う正しい方法は、次のように、A とプロセス B から D の間にチャネルを持ち、B から D までの各プロセスに同じメッセージを送信するだけのようです。

これは PROMELA で放送を模倣する正しい方法ですか、それともそうするための適切なオペレーターはいますか?

英語で申し訳ありません、ウクライナ出身です) スピンシステムの検証を勉強し始めたばかりです。次の問題を出題しました: 「LTL 式の下の形式で提示: マーシャを愛しているなら、ダーシャを愛することはできません」。私はそれを行う方法を理解できません。これが私が得たものです: p - マーシャが取得した Gp のように、[] p コードの形式で表されます (ただし、書き方はわかりません):

これがナンセンスであることは理解していますが、あなたの助けを求めます。

私は Promela と SPIN を使用しようとしている初心者です。簡単な Promela 仕様を作成しているので、printf() を使用してプログラム内の変数の値を確認したいと考えています。このマニュアル ページを読み、単純な hello world プログラムを実行しようとしていますが、出力テキストが表示されません。サンプルの hello world ファイルは次のとおりです。

コンパイルと実行に使用する手順は次のとおりです。

実行からの出力は

では、printf ステートメントからの出力はどこにありますか? より複雑な promela ファイルでも printf ステートメントを試してみましたが、明らかに、最初に単純なケースで機能させたいと考えています。任意の洞察をいただければ幸いです。ありがとう！

Promela と Spin を学習しましたが、モデルを検証しようとすると、これらの行が返されます。

彼らはどういう意味ですか？

ありがとう