3

次のLTLプロパティの単純なPromelaモデルをモデルチェックしようとしています:

ltl { M[0] U M[1] }

そして、エラーが発生しました。エラートレイルのガイド付きシミュレーションでは、次の出力が得られます。

ltl ltl_0: (M[0]) U (M[1])
spin: couldn't find claim 2 (ignored) 
0 :init ini M[0] = 1             
Process Statement                M[0]       M[1]       
0 :init ini M[1] = 0             1          0          
Starting net with pid 2
0 :init ini run net()            1          0          
spin: trail ends after 4 steps
#processes: 2
  4:    proc  1 (net) petri:11 (state 13)
  4:    proc  0 (:init:) petri:25 (state 5)
2 processes created
Exit-Status 0

ここで、「M[0] until M[1]」がどこで違反されているのかわかりません。M[0] は init プロセスで 1 に設定され、M[1] が 1 になるまでそのままです。トレースが非常に早く終了するか、「stronguntil」のセマンティクスを完全に誤解している可能性があります。私はこれが事実であると確信しています...しかし、私は何が間違っていますか? Promela ファイル内の LTL の指定は大丈夫ですか?

問題のモデルは次のとおりです (単純なペトリネット)。

#define nPlaces 2
#define nTransitions 2
#define inp1(x1) (x1>0) -> x1--
#define out1(x1) x1++

int M[nPlaces];
int T[nTransitions];

proctype net()
{
    do
    ::  d_step{inp1(M[0])->T[0]++;out1(M[1]);skip}
    ::  d_step{inp1(M[1])->T[1]++;out1(M[0]);skip}
    od
}
init
{
    atomic 
    {
        M[0] = 1;
        M[1] = 0;
    }
    run net();
}

ltl { M[0] U M[1] }
4

2 に答える 2

2

あなたの主張は、初期状態 ( のinit使用前atomic) で違反されています。pan -a次に示すのは、証跡ファイルからの出力を含む SPIN 検証の実行 ( ) です。

ebg@ebg$ spin -a foo.pml
ltl ltl_0: (M[0]) U (M[1])
ebg@ebg$ gcc -o pan pan.c
ebg@ebg$ ./pan -a
pan:1: assertion violated  !(( !(M[0])&& !(M[1]))) (at depth 0)
pan: wrote foo.pml.trail

(Spin Version 6.2.4 -- 21 November 2012)
Warning: Search not completed
    + Partial Order Reduction

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

State-vector 36 byte, depth reached 6, errors: 1
        4 states, stored (7 visited)
        1 states, matched
        8 transitions (= visited+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.290   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



pan: elapsed time 0 seconds
ebg@ebg$ spin -p -t foo.pml
ltl ltl_0: (M[0]) U (M[1])
starting claim 2
using statement merging
spin: _spin_nvr.tmp:5, Error: assertion violated
spin: text of failed assertion: assert(!((!(M[0])&&!(M[1]))))
Never claim moves to line 5 [D_STEP]
spin: trail ends after 1 steps
#processes: 1
        M[0] = 0
        M[1] = 0
        T[0] = 0
        T[1] = 0
  1:    proc  0 (:init:) foo.pml:18 (state 3)
  1:    proc  - (ltl_0) _spin_nvr.tmp:3 (state 6)
1 processes created

ltlが次のように翻訳されたことがわかりますassert(!(( !(M[0])&& !(M[1])))):

  !(( !0 && !0))
  !((  1 &&  1))
  !((  1 ))
  0

したがって、アサーションは違反されます。

この問題を回避する最も簡単な方法は、配列を個別の変数に変更することです。配列のサイズはちょうど 2 であるため、簡単に実行できます。

int M0 = 1;
int M1 = 0;
int T0 = 0;
int T1 = 0;
/* then use as appropriate. */

これにより、をスキップしinitて、netproctype を次のように宣言することができます。active proctype net ()

于 2013-06-18T14:21:48.600 に答える
1

あなたのltl式はうまく配置されています。ispin を使用してプログラムを検証する (シミュレートしない) 場合は、「use claim」オプションが選択されていることを確認してください。注意: デフォルトは「never claim または ltl プロパティを使用しない」です。

于 2013-06-17T13:33:24.903 に答える