model-checking - 了解 Spin Modelchecker 的错误轨迹

Question

我正在尝试使用旋转模型检查器对两个对象(A 和 B)之间的游戏进行模型检查。对象在板上移动，每个位置由其 (x,y) 坐标定义。两个物体应该不会碰撞。我有三个进程:init、A Model、B Model。我正在模型检查 ltl 属性:( active 属性来检查两个对象是否占据相同的位置)

ltl prop1 { [] (!(x_a == x_b) && !(y_a == y_b)) }

我得到的错误轨迹是: 初始化 -> A 模型 -> B 模型 -> 初始化

但是，根据显示的数据，我不应该得到错误线索(反例):x_a=2、x_b=1、y_a=1、y_b=1。

第一个 init 确实会遍历 init 进程的所有行，但第二个 init 只显示到它的最后一行。

此外，我的 A 模型和 B 模型仅包含“do” block 中的防护和操作，如下所示。然而它们更复杂，并且在“->”右侧有 if block

active proctype AModel(){
do
:: someValue == 1 -> go North
:: someValue == 2 -> go South
:: someValue == 3 -> go East
:: someValue == 4 -> go West
:: else -> skip;
od
}

我需要在原子 block 中放入任何东西吗？我问的原因是错误跟踪显示的行甚至没有进入“do” block ，它只是两个模型的第一行。

编辑: LTL 属性错误。我将其更改为:

ltl prop1 { [] (!((x_a == x_b) && (y_a == y_b))) }

但是，我仍然得到完全相同的错误线索。

Answer 1

您的 LTL 属性实现错误。本质上，SPIN 发现的反例是上述 LTL 的真实反例。

[] ( !(x_a == x_b) && !(y_z == y_b) )   =>
[] ( !(2 == 1) && !(1 == 1) )  =>
[] ( !0 && !1) =>
[] ( 1 && 0)   =>
[] 0  =>
false

零担应该是:

always not (same location) =>
[] (! ((x_a == x_b) && (y_a == y_b))) =>
[] (! ((2 == 1) && (1 == 1))) =>
[] (! (0 && 1) =>
[] (! 0) =>
[] 1 =>
true

关于您的初始化和任务。启动任务时，您需要确保在任务运行之前完成初始化。我将使用两种方法之一:

init { ... atomic { run taskA(); run taskB() } where tasks are spawned once all initialization is complete`

或

bool init_complete = false;
init { ...;  init_complete = true }
proctype taskA () { /* init local stuff */ ...; init-complete -> /* begin real works */ ... }

您的 LTL 在初始化期间可能会失败。

根据您的问题，如果您更改了 x 或 y，您最好在原子{}中同时更改这两个值。