1

我正在尝试对我创建的 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 中运行正确的命令。

提前致谢！

4

1 回答 1

2

据我在使用该工具后所知道的，我会说您所经历的是由于以某种方式使用伪随机生成器而导致的常见行为。

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

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

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

因此，我想提出以下解决方法，以帮助您实现从同一模型中收集不同的、非确定性的执行跟踪的目标。尝试：

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

基本上，这个想法是利用第一个模拟，以便将伪随机生成器向前移动到伪随机链中的任意点。每次执行此脚本时，都会更改 的值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 源代码可用，另一种可能的解决方案是对其进行修补，以便接受设置任意种子以初始化伪随机生成器的新颖选项。

于 2017-07-30T16:06:42.253 回答