使用随机轨迹的 NuSMV 模拟

Question

我正在尝试运行 "random" 或我创建的 NuSMV 模型的非确定性模拟。然而，在随后的运行秒之间，产生的轨迹完全相同。

这是模型：

MODULE main
VAR x : 0..4;
VAR clk : 0..10;

DEFINE next_x :=
    case
        x = 0 : {0,1};
        x = 1 : {1,2};
        x = 2 : {1,0};
        TRUE : {0};
    esac;

DEFINE next_clk :=
    case
        (clk < 10) : (clk+1);
        TRUE : clk;
    esac;

INIT (x = 0);
INIT (clk = 0);

TRANS (next(x) in next_x);
TRANS next(clk) = next_clk;

CTLSPEC AG(clk < 10);

我正在运行在交互式 shell 中使用以下命令进行此操作：

go
pick_state -r
simulate -k -r 30
show_traces 1
quit

也许我的模型有误？或者我没有运行在 shell.

中使用正确的命令

提前致谢！

Answer 1

据我所知 在试用该工具后，我会说您遇到的是常见行为，由于以某种方式使用 伪随机 生成器。

基本上，我假设每次启动 NuSMV void srand(unsigned int seed) 时都使用相同的 seed 值进行初始化。显而易见的结果是 NuSMV 在独立的运行中执行完全相同的 non-deterministic 选择，前提是您加载完全相同的建模并执行完全相同的命令序列。

这种设计在模型检查器中很常见，因为它可以更轻松地重现用户报告的潜在错误痕迹。

查看 NuSMV -help 和 NuSMV 文档后，在我看来该程序没有手动设置的选项伪随机生成器的 任意种子 。 (注意： 你可能想联系 NuSMV 邮件列表，可能存在一些内部变量来借助 set命令)

因此，我想提出以下解决方法来帮助您实现收集不同的、不确定的执行痕迹[=82]的目标=] 来自同一型号。尝试：

go pick_state -r simulate -r RANDOM_SEED pick_state -r simulate -r 30 show_traces 2 quit

基本上，这个想法是利用第一个模拟，以便将伪随机生成器向前移动到 伪随机链 中的任意点。每次执行此 script 时，都会更改 RANDOM_SEED 的值，因此 NuSMV 的任何两次执行都有不同的开始-指向第二条轨迹的伪随机生成器。通过这种方式，NuSMV 不再重复它在第二次跟踪的其他执行中所做的相同选择，除非那是纯属偶然。

或者， 您可以从单个运行 NuSMV 求解器：

go pick_state -r simulate -r 30 show_traces 1 pick_sate -r simulate -r 30 show_traces 2 ... pick_state -r simulate -r 30 show_traces N quit

注1：你的模型只有一个初始状态，所以pick_state -r总是选择相同的初始状态。

注2：您的模型在我的系统上报如下错误：

TYPE ERROR file test.smv: line 23 : illegal operand types of "=" : integer-set and integer

当我输入 pick_state -i 时。

注释 3：由于 NuSMV 源代码 可用，另一种可能的解决方案是对其进行修补，以便接受新的选项设置任意种子以初始化伪随机生成器。

使用随机轨迹的 NuSMV 模拟

NuSMV Simulation Using Random Traces

random

model-checking

nusmv