0

複数のステートメントを無限に頻繁に実行する必要があるという公平性の制約があるプログラムで、LTL プロパティを検証できるかどうか疑問に思っています。

例えば：

bool no_flip;
bool flag;

active[1] proctype node()
{
  do
  :: skip -> progress00: no_flip = 1
  :: skip -> progress01: flag = 1
  :: !no_flip -> flag = 0
  od;
}

// eventually we have flag==1 forever
ltl p0  { <> ([] (flag == 1)) }

このプログラムは、最終的にno_flipフラグが trueに flagなり、true になった場合に正しいです。

ただし、'pan -a' と 'pan -a -f' (弱い公平性) の両方を実行すると、no_flip=1ステートメントと受け入れ状態 (LTL 式から) を循環します。

進行状況ラベルは、実行が無限に頻繁に通過することを強制すると思っていましたが、そうではないようです。では、そのような公平性制約を追加することは可能ですか?

ありがとう、ヌーノ

4

2 に答える 2

2

進行状況ラベル自体を含めるだけでは、実行が進行状況以外のケースに限定されることは保証されません。ltlまたはneverクレームのどこかに「非進行」を追加する必要があります。

never進行状況を強制するクレームとして<>[](np_)( spin -p '<>[](np_)'never クレーム自体を生成するために使用)。確認の可能なltl形式は次のとおりです。

ltl { []<>!(np_) && <>[](flag==1) }

また、「進行」することは、各進行状況ラベルを無限に頻繁に訪問することを意味するわけではないことに注意してください。これは、進行状況ラベルに無限に頻繁にアクセスすることを意味します。したがって、進行状況を強制する場合、コードを介した実行可能なパスが最初のdoオプションになりますが、これは期待したものではありません。

于 2013-10-14T22:40:31.180 に答える