1

次のスニペットを検討してください。

chan sel = [0] of {int};

active proctype Selector(){
    int not_me;

    endselector:
    do
    ::  sel ? not_me;
        if
        :: 0 != not_me -> sel ! 0;
        :: 1 != not_me -> sel ! 1;
        :: 2 != not_me -> sel ! 2;
        :: 3 != not_me -> sel ! 3;
        :: else -> -1;
        fi

    od
}

proctype H(){
    int i = -1;
    int count = 1000;
    do
    :: sel ! i; sel ? i; printf("currently selected: %d\n",i); count = count -1;
    :: count < 0 -> break;
    od

    assert(false);
}

init{
    atomic{
        run H();
    }
}

これは、カウンターが 0 を下回るまで値 0..3 をかなり恣意的に出力し、その時点で別の数値を出力するか終了することを期待するでしょう。

しかし、そうではないようです。

返される値は、0、次に 1、次に 0、次に 1、次に 0、次に 1 だけです。

if/fi ステートメントの「非決定論」を誤解したのでしょうか?

（問題がある場合は、ubuntuでispinを使用してください）。

4

2 に答える 2

1

言語仕様の関連部分。私には非決定的なようです。

システムの (いくつかの) トレースのみを見ている場合は、(疑似) ランダム ジェネレーターに翻弄されています。

SPIN の主な目的は、プロパティを証明することだと思いました。したがって、必要なトレースを記述する式 F を記述し、「システムと F」にモデルがあることを SPIN チェックさせることができます。

于 2016-02-05T18:39:09.260 に答える
0

Spin を「シミュレーション」モードで実行している場合、elseオプションは確定的にアクセスされると思います。そのため、 proctype では、オプションを 0 ~= not_me としてチェックし、次に 1、2、3 オプションをチェックしてSelector、シミュレーションが進行します。ifしたがって、実行のために、0 と 1 の間でピンポンします。

ifステートメントを次のように置き換えることで、これを確認できます。

if
:: 0 != not_me -> sel ! 0;
:: 1 != not_me -> sel ! 1;
:: else -> assert(false)
fi

シミュレーションがアサートに到達することはありません。

Spin は「検証」モードでも実行できます。実行可能ファイルを生成してpan実行します。次に、すべてのケースが調べられます (メモリと時間のモジュロ制限)。ただし、「検証」モードでは何も出力されません。そのため、他のケースを確認するのが難しい場合があります。

于 2016-02-10T23:09:11.130 に答える