1

考虑这个片段：

chan sel = [0] of {int};

active proctype Selector(){
    int not_me;

    endselector:
    do
    ::  sel ? not_me;
        if
        :: 0 != not_me -> sel ! 0;
        :: 1 != not_me -> sel ! 1;
        :: 2 != not_me -> sel ! 2;
        :: 3 != not_me -> sel ! 3;
        :: else -> -1;
        fi

    od
}

proctype H(){
    int i = -1;
    int count = 1000;
    do
    :: sel ! i; sel ? i; printf("currently selected: %d\n",i); count = count -1;
    :: count < 0 -> break;
    od

    assert(false);
}

init{
    atomic{
        run H();
    }
}

您希望这可以任意打印漂亮的值 0..3，直到计数器低于 0，此时它可以打印另一个数字，也可以终止。

然而，情况似乎并非如此。

返回的唯一值是 0，然后是 1，然后是 0，然后是 1，然后是 0，然后是 1，...

我是否以某种方式误解了 if/fi 语句的“非确定性”？

（如果重要的话，在 ubuntu 上使用 ispin）。

4

2 回答 2

1

语言规范的相关部分。对我来说似乎不确定。

如果您只查看系统的（一些）痕迹，那么您将受到（伪）随机生成器的支配。

我认为 SPIN 的主要目的是证明属性。因此，您可以编写一个公式 F 来描述您想要的跟踪，然后让 SPIN 检查“系统和 F”是否有模型。

于 2016-02-05T18:39:09.260 回答
0

如果您在“模拟”模式下运行 Spin，那么else我相信这些选项会被确定性地访问。因此，在Selectorproctype 中，if通过检查以下选项进行模拟：0 ~= not_me，然后是 1、2、3 选项。对于您的执行，您因此在 0 和 1 之间进行 ping pong。

您可以通过将您的if声明替换为以下内容来确认这一点：

if
:: 0 != not_me -> sel ! 0;
:: 1 != not_me -> sel ! 1;
:: else -> assert(false)
fi

你的模拟永远不会达到断言。

Spin 也可以在“验证”模式下运行——生成一个pan可执行文件并执行它。然后，将访问所有案例（内存和时间的模限制）。然而，在“验证”模式下，什么都不会打印出来——所以你可能很难看到其他情况！

于 2016-02-10T23:09:11.130 回答