2

我尝试通过旋转来解决有关农夫、狼、山羊和卷心菜的任务。

所以，我找到了以下 promela 描述：

#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

3

有几种方法可以解释跟踪。

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

这将逐步显示每个进程执行的操作，包括进程号、proctype 名称、执行的指令行号、执行的指令代码等信息。

  1. 对 spin 执行相同操作：
    使用命令

    spin -t -p xyz.pml

  2. 了解跟踪文件语法：文件
    中的每一行都是模拟器执行的一个步骤。第一列只是序列号。第二列是进程号（pids）。（例如 init 将是 0，它启动/运行的第一个进程将是 1 等等。）第三列是转换编号。如果您只想了解正在发生的事情，可以查看 pid 并查看说明

于 2017-10-03T10:56:40.977 回答
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来查看反例中发生的情况

~$ spin -t file_name.pml

该选项在违反某些assertion/property-t时重播spintrail发现的最新消息。

于 2017-01-03T12:31:18.023 回答