1

次のコードでは、

proctype A() 
{ 
byte cond1;

time = time + 1;
time = time + 2;
t[0] = 3;
a[0] = 2;
do
:: (a[0] == 0)->break;
:: else -> a[0] = a[0] - 1;
    do
    :: (t[0] <= t[1])->break;
    od;
    if 
        :: (cond1 != 0) ->
           lock(mutex);
           time = time + 1;
           time = time + 2;
           t[0] = t[0] + 3;
           unlock(mutex);
        :: (cond1 == 0) -> time = time + 1;
    fi
od;
t[0] = 1000;
}

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

unreached in proctype A
code.pml:15, state 20, "time = (time+1)"
code.pml:14, state 23, "((mutex==0))"
code.pml:14, state 23, "else"
code.pml:18, state 25, "time = (time+1)"
code.pml:12, state 26, "((mutex==0))"
code.pml:12, state 26, "((mutex==1))"
code.pml:12, state 29, "((mutex==0))"
code.pml:12, state 29, "((mutex==1))"
code.pml:45, state 31, "time = (time+2)"
code.pml:46, state 32, "t[0] = (t[0]+3)"
(7 of 43 states)

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

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

4

2 に答える 2

1

の初期値cond1はゼロであり、Spin またはコードによって変更されることはありません。したがって、条件cond1 != 0が真になることはありません。そのオプションを実行するには、検証をセットアップして、cond1使用する他の/追加の値を生成する必要があります。次に例を示します。

proctype A() 
{ 
  byte cond1;
  if
  :: cond1 = 0;
  :: cond1 = 1;
  /* … */
  fi;

  …
}
于 2014-02-03T00:51:50.413 に答える
1

このように、selectステートメントを使用して解決しました。

select (cond1 : 0..1);
于 2014-01-14T17:10:52.910 に答える