2

次の単純な PROMELA モデルを検討してください。

#define p (x!=4)

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

私は、spin -f を使用して生成された次の単純な主張で、このモデルを検証したかったのです。

never {    /* []p */
accept_init:
T0_init:
    do
    :: ((p)) -> goto T0_init
    od;
}

ただし、これを使用した検証は

spin -a model.pml
cc -o pan pan.c
./pan

結果が出ません。-a オプションを試しても結果は得られません。任意のランダム シミュレーションは、ある時点で明らかに p が false であることを示しています。

基本的な何かが欠けていますか？

4

2 に答える 2

1

を確認したい場合は、 のクレーム[]pを作成する必要があります。never![]p

参照から：

LTL 式を Never Claim に変換するには、式が正のプロパティを表すか負のプロパティを表すかを最初に考慮する必要があります。正のプロパティは、システムに望んでいる良い動作を表します。負のプロパティは、システムにはないと主張する悪い動作を表します。never クレームは、通常、ネガティブ プロパティ (決して発生してはならない動作) を形式化するためにのみ使用されます。つまり、ポジティブ プロパティは、クレームに変換される前に否定する必要があります。

于 2016-02-16T10:17:34.083 に答える
1

クレームをソースコードに入れます（たとえば、check.pml）

int x = 0;

init {
    do
    :: x < 10 ->
        x++;
    od
}

ltl  { [] (x != 4) }

それから

spin -a check.pml
cc     pan.c   -o pan
./pan -a

これは与える

pan:1: assertion violated  !( !((x!=4))) (at depth 16)
pan: wrote check.pml.trail

あなたはトレイルを見ることができます

./pan -r -v

私見ですが、追加のツールを使用してクレームからオートマトンを構築することは、非常に不便であり、しばしば混乱を招きます。

于 2016-02-17T20:34:35.183 に答える