2

Spin Model Checker を使用して、2 つのオブジェクト (A と B) 間のゲームをモデルチェックしようとしています。オブジェクトはボード上を移動し、各位置はその (x,y) 座標によって定義されます。2 つのオブジェクトは衝突しないはずです。init、A Model、B Model の 3 つのプロセスがあります。私は ltl プロパティをチェックするモデルです: (2 つのオブジェクトが同じ場所を占有するかどうかをチェックする liveness プロパティ)

ltl prop1 { [] (!(x_a == x_b) && !(y_a == y_b)) }

私が得るエラートレイルは次のとおりです: init -> A Model -> B Model -> init

ただし、表示されているデータに基づいてエラー トレイル (反例) を取得する必要はありません: x_a=2、x_b=1、y_a=1、y_b=1。

また、最初の init は init プロセスのすべての行を通過しますが、2 番目の init はその最後の行までしか表示されません。

また、私の A モデルと B モデルは、以下に示すように、「do」ブロック内のガードとアクションのみで構成されています。ただし、それらはより複雑で、'->' の右側に if ブロックがあります。

active proctype AModel(){
do
:: someValue == 1 -> go North
:: someValue == 2 -> go South
:: someValue == 3 -> go East
:: someValue == 4 -> go West
:: else -> skip;
od
}

アトミックブロックに何かを入れる必要はありますか? 私が質問している理由は、エラー トレイルが示している行が 'do' ブロックにも入っておらず、2 つのモデルの最初の行に過ぎないからです。

編集: LTL プロパティが間違っていました。私はそれを次のように変更しました：

ltl prop1 { [] (!((x_a == x_b) && (y_a == y_b))) }

しかし、私はまだまったく同じエラートレイルを取得しています。

4

1 に答える 1

2

LTL プロパティが正しく実装されていません。基本的に、SPIN が見つけた反例は、前述の LTL の真の反例です。

[] ( !(x_a == x_b) && !(y_z == y_b) )   =>
[] ( !(2 == 1) && !(1 == 1) )  =>
[] ( !0 && !1) =>
[] ( 1 && 0)   =>
[] 0  =>
false

LTL は次のようになります。

always not (same location) =>
[] (! ((x_a == x_b) && (y_a == y_b))) =>
[] (! ((2 == 1) && (1 == 1))) =>
[] (! (0 && 1) =>
[] (! 0) =>
[] 1 =>
true

あなたの初期化とタスクについて。タスクを開始するときは、タスクを実行する前に初期化が完了していることを確認する必要があります。次の 2 つの方法のいずれかを使用します。

init { ... atomic { run taskA(); run taskB() } where tasks are spawned once all initialization is complete`

また

bool init_complete = false;
init { ...;  init_complete = true }
proctype taskA () { /* init local stuff */ ...; init-complete -> /* begin real works */ ... }

初期化中に LTL が失敗している可能性があります。

あなたの問題に基づいて、x または y を変更した場合は、atomic{} で両方を一度に変更することをお勧めします。

于 2012-04-15T03:57:24.533 に答える