SPIN：解释错误跟踪

我试图解决与农民，狼，山羊和卷心菜有关的任务。SPIN：解释错误跟踪

所以，我发现了如下因素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 {<>鳍& & []（WG & & GC）} 验证，狼不会吃山羊，山羊不会吃白菜。我想要举一个例子，农民如何运输他所有的需求（w-g-c）而不损失。

当运行验证时，得到以下结果：状态矢量20字节，深度达到59，错误：1 64个状态，存储 23个州，匹配 87转变（=存储+匹配） 0原子步骤散列冲突：0（已解决）

这意味着该程序为我生成了一个示例。但我无法解释它。 * .pml.trial文件的内容是：enter image description here

请帮我解释。

来源

2017-01-03 julitta_94

为了“解释”它，你可以使每一个采取行动的东西intellegibile时间打印在标准输出修改你的源代码。

例如为：

  :: (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 -t file_name.pml

选项-t重播的最新trail发现旋在违反一些断言/财产。

来源

2017-01-03 12:31:18

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

使用iSpin：
- 去模拟/在播放模式
- ，选择引导并输入您的跟踪文件的名称
- 运行

这将逐步显示每个进程所采取的行动，包括诸如进程号，实例类型名称，行号麻烦等信息执行指令，执行指令代码。

做同样的旋转：
使用命令

spin -t -p xyz.pml

理解跟踪文件的语法：
在文件中的每个行是一个一步由模拟器采取。第一栏只是序号。第二列是进程号（pids）。（例如，init将为0，它启动/运行的第一个进程将为1，依此类推。）第三列是转换编号。如果你只想知道发生了什么，你可以看看pid，然后阅读说明书

来源

2017-10-03 10:56:40

SPIN：解释错误跟踪

回答

相关问题