SPIN:解释错误跟踪

Question

我试图用旋转的任务来解决农民，狼，山羊和卷心菜的问题。

所以，我找到了关于狩猎的描述：

#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 }来验证，比狼不吃山羊，山羊不吃卷心菜。我想举个例子，农民如何能够不受损失地运送他所有的需求(W)。

当我运行验证时，得到以下结果:状态向量20字节，深度达到59，错误:1 64状态，存储23状态，匹配87次转换(= stored+matched) 0原子步骤哈希冲突:0(已解决)

这意味着程序已经为我生成了一个示例。但我无法解释。*.pml.trial文件的内容是：在这里输入图像描述

请帮我解释一下。

Answer 1

你可以用几种方法来解释痕迹。

1. 使用iSpin：
   • 去模拟/玩
   • 在模式中，选择“引导”并输入跟踪文件的名称。
   • 跑

​

这将一步一步地显示每个进程所采取的行动，包括进程号、proctype名称、已执行指令的行号、执行指令代码等信息。

1. 对旋转也要这样做： 使用以下命令 spin -t -p xyz.pml
2. 了解跟踪文件语法： 文件上的每一行都是模拟器执行的一个步骤。第一列只是序列号。第二列是进程号(pids)。(例如init为0，它启动/运行的第一个进程为1，依此类推。)第三列是转换号。如果您只想了解正在发生的事情，可以查看pids并查看说明。

Answer 2

为了“解释”它，您可以修改源代码，以便每次执行某个操作时，都会在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);，如果您记住0意味着left，1意味着right，则可以使用它来解释反示例。不过，我更喜欢更详细的跟踪。

在完成了每个可能的转换之后，您可以通过以以下方式运行spin来查看反例中发生了什么。

~$ spin -t file_name.pml

选项-t在违反某些断言/属性时重放spin找到的最新trail。