vendredi 28 juillet 2017

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!




Aucun commentaire:

Enregistrer un commentaire