NuSMV Simulation Using Random Traces

I am attempting to run "random" or non-deterministic simulations of a NuSMV model I have created. However between subsequent runs the trace that is produced is exactly the same.

Here is the model:

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);

I am running this using the following commands in the interactive shell:

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

Perhaps I have a mistake in my model? Or I am not running the correct commands in the shell.

Thanks in advance!

Solution

As far as I can tell after playing around with the tool, I would say that what you experience is a common behaviour due to using pseudo-random generators in a certain way.

Basically, I posit that each time one starts NuSMV void srand(unsigned int seed) is initialised with the same seed value. The obvious result is that NuSMV performs the exact same non-deterministic choices among independent runs, provided that you load the exact same model and perform exactly the same sequence of commands.

This kind of design is common among model checkers because it allows to reproduce potential bug traces reported by users more easily.

After looking at NuSMV -help and NuSMV documentation, it appears to me that the program has no option to manually set an arbitrary seed for the pseudo-random generator. (Note: you might want to contact NuSMV mailing list about this, it may be possible that there exists some internal variable to configure the random seed with the aid of the set command)

Therefore, I would like to propose the following work-around to help you achieving your goal of collecting different, non-deterministic execution traces from the same model. Try:

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

Basically, the idea is to exploit the first simulation in order to move forward the pseudo-random generator to an arbitrary point in the pseudo-random chain. Each time you execute this script, you change the value of RANDOM_SEED, so that any two executions of NuSMV have a different starting-point in the pseudo-random generator for the second trace. In this way, NuSMV no longer repeats the same choices it has done in other executions for the second trace, unless that happens by pure chance.

Alternatively, you may obtain all the non-deterministic execution traces you want from a single run of the NuSMV solver:

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

Note 1: your model has only one initial state, so pick_state -r always chooses the same initial state.

Note 2: your model reports the following error on my system:

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

when I type pick_state -i.

Note 3: since NuSMV source code is available, another possible solution is to patch it so as to accept a novel option for setting an arbitrary seed to initialise the pseudo-random generator.