問題タブ [spin]

Promela共有変数を操作する次の 2 つのプロセスのモデルを考えてみましょうN。

両方のプロセスが終了したときにLTL formula変数が持つことができる最小値を見つけるためにどのように使用できますか?N

このシステム (単なる例) は、リーダーがフレームの特定のスパンを要求するリーダー/ライター キューをモデル化する必要が[rq_begin,rq_end]あり、ライターは少なくともこのスパンを利用可能にする必要があります。[av_begin,av_end]利用可能なフレームのスパンです。

4 つの値は絶対フレーム インデックスでrq_beginあり、リーダーがフレームの次のスパンを読み取ると、無限にインクリメントされます。

値が範囲外であるため、システムを直接検証することはできません (無限に多くの状態が生成されます)。Promela/Spin (または同様のソフトウェア) は、このようなシステムを検証し、有限になるように自動的に変換する機能をサポートしていますか?

たとえば、4 つの値がすべて同じ量だけ増分された場合でも、状況は同じです。または、代わりにこれらの値の差の変数を持つモデルに再定式化することもできますav_end - rq_end。

私は Promela/Spin を使用して、このような絶対フレーム インデックスを使用するより複雑なキューイング システムを検証しています。

農夫、オオカミ、ヤギ、キャベツに関するタスクをスピンして解決しようとします。

それで、私は次のプロメラの説明を見つけました：

そこに LTL 式を追加します: ltl ltl_0 { <> fin && [] ( wg && gc ) } 検証するために、オオカミはヤギを食べず、ヤギはキャベツを食べません。農家がすべてのニーズ (wgc) を損失なく輸送する方法の例を取得したいと思います。

検証を実行すると、次の結果が得られます: 状態ベクトル 20 バイト、深度が 59 に到達、エラー: 1 64 状態、保存された 23 状態、一致した 87 遷移 (= 保存 + 一致) 0 アトミック ステップ ハッシュ競合: 0 (解決済み)

これは、プログラムが私の例を生成したことを意味します。しかし、私はそれを解釈することはできません。*.pml.trial ファイルの内容:ここに画像の説明を入力

解釈を手伝ってください。

ここhttp://spinroot.com/spin/Man/Manual.htmlに、次のように書かれています。

Promela には、テストとセットの問題を回避する別の方法もあります: アトミック シーケンスです。中かっこで囲まれたステートメントのシーケンスの前にキーワードatomicを付けることで、ユーザーは、シーケンスが他のプロセスとインターリーブされずに、分割できない1つの単位として実行されることを示すことができます。最初のステートメント以外のステートメントがアトミック シーケンスでブロックされると、実行時エラーが発生します。これは、アトミック シーケンスを使用して、前の例でグローバル変数状態への同時アクセスを保護する方法です。

そして、ここhttp://spinroot.com/spin/Man/atomic.htmlには、次のように書かれています。

アトミック シーケンス ブロック内のいずれかのステートメントが失われると、原子性が失われます。ブロックされたステートメントが再び実行可能になると、アトミック シーケンスの実行はいつでも再開できますが、すぐに再開できるとは限りません。プロセスがシーケンスの残りのアトミックな実行を再開する前に、プロセスはまずシステム内の他のすべてのアクティブなプロセスと競合して制御を取り戻す必要があります。つまり、最初に実行をスケジュールする必要があります。

それで、本当は何ですか？最初の引用から、atomic でブロックすることは許可されていないことがわかります (最初のステートメントではありません)。

2 番目の引用から、atomic でブロックしても問題ないことがわかります。原子性を失うだけで、それだけです。