1

以下のようなコードを使用して、検証モードでスピンを実行しています。「never」という関数に問題があります。実行中に、関数 inc()、dec()、reset() が完了していないというエラーが表示されます。しかし、サイクルを追加すると、うまく機能します。ドキュメントでは、「決して」すべてのステップで変数をチェックしません。では、なぜサイクルがないと機能しないのでしょうか。

int x=0
proctype Inc(){
 do
  ::true ->
    if
      ::x<10->x=x+1
    fi
 od
}

proctype Dec(){
 do
  ::true ->
    if
      ::x>0->x=x-1
    fi
 od
}

proctype Reset(){
 do
  ::true ->
   if
    ::x==10->x=0
   fi
 od
}


never {       // if I need this to work, i have to add
  To_Init:    //  this line
    if 
      :: (x<0) || (10<x) -> goto accept
      :: else -> goto To_Init      //  and that line
    fi;
  accept:
}

init{
  run Inc();
  run Dec();
  run Reset();
}

「決して」ブロックしないと、警告が表示されます

never { 
    if 
        :: (x<0) || (10<x) -> goto accept
    fi;
    accept:
}

実際には、これはエラーではなく、一種の警告であり、proctype Inc、Dec、Reset、Init で unreached が表示されます。完全な警告ログは以下のとおりです。

warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.2.7 — 2 March 2014)
+ Partial Order Reduction

Full statespace search for:
never claim + (never_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 28 byte, depth reached 0, errors: 0
1 states, stored
0 states, matched
1 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.289 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage

unreached in proctype Inc
l31never-no-cycle:6, state 3, "x = (x+1)"
l31never-no-cycle:6, state 4, "((x<10))"
l31never-no-cycle:4, state 6, "(1)"
l31never-no-cycle:9, state 9, "-end-"
(4 of 9 states)
unreached in proctype Dec
l31never-no-cycle:15, state 3, "x = (x-1)"
l31never-no-cycle:15, state 4, "((x>0))"
l31never-no-cycle:13, state 6, "(1)"
l31never-no-cycle:18, state 9, "-end-"
(4 of 9 states)
unreached in proctype Reset
l31never-no-cycle:24, state 3, "x = 0"
l31never-no-cycle:24, state 4, "((x==10))"
l31never-no-cycle:22, state 6, "(1)"
l31never-no-cycle:27, state 9, "-end-"
(4 of 9 states)
unreached in claim never_0
l31never-no-cycle:35, state 6, "-end-"
(1 of 6 states)
unreached in init
l31never-no-cycle:39, state 2, "(run Dec())"
l31never-no-cycle:40, state 3, "(run Reset())"
l31never-no-cycle:41, state 4, "-end-"
(3 of 4 states)
4

1 に答える 1

5

クレームは、次のnever2 つのケースでエラーを報告します: 1) 'accept' サイクルが検出された場合、または 2) 決してクレームが完了しない場合。3 つ目の可能性は、neverクレームが一歩踏み出せない場合です。この 3 番目の可能性は、コードが生成する可能性です

あなたの主張が次の場合:

never { 
    if 
    :: (x<0) || (10<x) -> goto accept
    fi;
    accept:
}

初期状態には可能なステップはありません。つまり、クレーム開始状態は;neverの直前です。次の一歩が踏み出せないif状態から。x==0

クレームに可能なステップがない場合never、検証者はステップを実行できる状態に戻ります。あなたの場合、バックアップする場所がなく、これ以上何もすることがないため、検証は終了します。その後、検証者は、多くのコードが実行されなかったことを認識します (実際には、モデルで何も実行されていないためです)。

実行されていないコードがすべてあるため、これは予期したものではないことがわかります。しかし、それはエラーとして報告されていません。

その後のケースでは、else. この場合、検証者はneverクレームの手順を実行できるため、検証が続行されます。

于 2014-04-09T14:28:30.537 に答える