2

農夫、オオカミ、ヤギ、キャベツに関するタスクをスピンして解決しようとします。

それで、私は次のプロメラの説明を見つけました：

#define fin (all_right_side == true)
#define wg  (g_and_w == false)
#define gc  (g_and_c == false)

ltl ltl_0 { <> fin && [] ( wg && gc ) } 

bool all_right_side, g_and_w, g_and_c;
active proctype river()
{
 bit f = 0, 
 w = 0, 
 g = 0, 
 c = 0; 

 all_right_side = false;
 g_and_w = false;
 g_and_c = false;
 printf("MSC: f %c w %c g %c c %c \n", f, w, g, c);

 do
 :: (f==1) && (f == w) && (f ==g) && (f == c) -> 
        all_right_side = true; 
        break;
 :: else ->
        if
            :: (f == w) ->
                    f =  1 - f;
                    w =  1 - w;
            :: (f == c) ->
                    f =  1 - f;
                    w =  1 - c;
            :: (f == g) ->
                    f =  1 - f;
                    w =  1 - g;
            :: (true) ->
                    f =  1 - f;
        fi;

        printf("M f %c w %c g %c c %c \n",  f, w, g, c);

        if
            :: (f != g && g == c) ->
                    g_and_c = true;
            :: (f != g && g == w) ->
                    g_and_w = true;
            ::else ->
                    skip
        fi
 od;

 printf ("MSC: OK!\n")
}

そこに LTL 式を追加します: ltl ltl_0 { <> fin && [] ( wg && gc ) } 検証するために、オオカミはヤギを食べず、ヤギはキャベツを食べません。農家がすべてのニーズ (wgc) を損失なく輸送する方法の例を取得したいと思います。

検証を実行すると、次の結果が得られます: 状態ベクトル 20 バイト、深度が 59 に到達、エラー: 1 64 状態、保存された 23 状態、一致した 87 遷移 (= 保存 + 一致) 0 アトミック ステップ ハッシュ競合: 0 (解決済み)

これは、プログラムが私の例を生成したことを意味します。しかし、私はそれを解釈することはできません。*.pml.trial ファイルの内容:ここに画像の説明を入力

解釈を手伝ってください。

4

2 に答える 2

0

それを「解釈」するために、ソースコードを変更して、アクションが実行されるたびに何か分かりやすいものがstdoutに出力されるようにすることができます。

例えば：

            :: (f == w) ->
                    if
                       :: f == 0 -> printf("LEFT ---[farmer, wolf]--> RIGHT\n");
                       :: f == 1 -> printf("LEFT <--[farmer, wolf]--- RIGHT\n");
                       :: else -> skip;
                    fi;
                    f =  1 - f;
                    w =  1 - w;

+ (f == c)、(f == g)および(true).

注:ソース コードには既に が用意printf("M f %c w %c g %c c %c \n", f, w, g, c);されています。ただし、より詳細なトレースを希望します。0left1right

可能な遷移ごとにこれを行った後、次の方法でスピンを実行することにより、反例内で何が起こるかを確認できます

~$ spin -t file_name.pml

このオプションは、いくつかのアサーション/プロパティの違反時にスピンによって見つかっ-tた最新のものを再生します。trail

于 2017-01-03T12:31:18.023 に答える