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!
Aucun commentaire:
Enregistrer un commentaire