A simple example in SMV

You should see a short program in the window below. (If not, then you probably can not use this demo with your browser.) This example is taken from the SMV guided tour. You may run it as it is, or you may try to change it and find out how SMV responds to the changes.

You can read more about SMV input language in the SMV manual (compressed postscript, 56K).

Please, do not run big programs on this server. This page is intended for demonstration, and any abuse will force me to close or severely restrict this service. At this point you are given 4Mb of RAM + 2Mb of stack and 1 minute of user CPU time on Pentium II 450MHz.

Although these seem to be quite modest resources for a model checker, they are a way more than enough for any demonstration. In fact, using a proper variable ordering, I was able to verify a (nontrivial!) part of the digital autopilot of the Space Shuttle using up less than a quater of the resources provided.

If you want to use SMV in your project, download the SMV software to your local machine.

To write your own program, use an SMV Trial form.

Write your program here:

MODULE main
 VAR
   s0: {noncritical, trying, critical, ready};
   s1: {noncritical, trying, critical, ready};
   turn: boolean;
   pr0: process prc(s0, s1, turn, 0);
   pr1: process prc(s1, s0, turn, 1);

ASSIGN init(turn) := 0;

FAIRNESS !(s0 = critical)
 FAIRNESS !(s1 = critical)

SPEC AG((s0 = critical) -> !(s1 = critical))
 SPEC AG((s1 = critical) -> !(s0 = critical))

SPEC AG((s0 = trying) -> AF(s0 = critical))
 SPEC AG((s1 = trying) -> AF(s1 = critical))

MODULE prc(state0, state1, turn, turn0)

ASSIGN
 init(state0) := noncritical;
 next(state0) := 
 case
    (state0 = noncritical) : {trying,noncritical};
    (state0 = trying) & ((state1 = noncritical) | 
                         (state1 = trying) |
                         (state1 = ready)): ready;
    (state0 = ready): critical;
    (state0 = trying) & (state1 = trying) 
                      & (turn = turn0):  critical;
    (state0 = critical) : {critical,noncritical};
    1: state0;
 esac;

next(turn) :=
 case
    turn = turn0 & state0 = critical: !turn;
    1: turn;
 esac;
 FAIRNESS running

Cache size: Key Table size:

Forward search Report number of states Output the variable ordering (not avail. yet)
Verbose level: None 1 2

Number of runs is 19 (before Feb. 12)

CMU-SCS Model Checking home page

Sergey Berezin / berez+@cs.cmu.edu

Please send any comments and suggestions to Nishant Sinha - (nishants) at cs dot cmu dot edu.