NuSMV

Today I have installed NuSMV, which is one of the SMV model checker.

SMV, Simbol Model Verification, is a famous Model checking way.

Professor. Ammann gave students an assignment which I have to grade next week.
The assignment was about SMV which I don't have enough knowledge.

I have heard SMV can represent finite automata.
It is very interesting that somebody made a tool that we can use freely.
There are several SMV checkers and NuSMV is one of them: Cadence SMV, VCEGAR.

For a backup, I refer professor's example here:

-- SMV Specification for simple EW,NS intersection
-- Paul Ammann

MODULE main
VAR
EW       : direction; NS : direction;

EWGreen  : process ToGreen(EW, NS);
NSGreen  : process ToGreen(NS, EW);

EWYellow : process ToYellow(EW);
NSYellow : process ToYellow(NS);

EWRed    : process ToRed(EW);
NSRed    : process ToRed(NS);

--ASSIGN

-- (EW, NS) check for P1
SPEC
 AG((EW.light = red | NS.light = red))
SPEC
 AG((NS.light = green ) -> AX (EW.light = red))

-- spec for test generation
--SPEC
--   AG((NS.light = green ) -> (AG !(NS.light = red)))


MODULE direction
VAR
 light : {red, yellow, green};
ASSIGN
 init(light) := red;

MODULE ToGreen(dir1, cdir1)

ASSIGN
 next(dir1.light) :=
    case
     (dir1.light = red) & (cdir1.light = red) : green;
     1 : dir1.light;
    esac;

MODULE ToYellow(dir1)

ASSIGN
 next(dir1.light) :=
    case
     (dir1.light = green) : yellow;
     1 : dir1.light;
    esac;

MODULE ToRed(dir1)

ASSIGN
 next(dir1.light) :=
    case
     (dir1.light = yellow) : red;
     1 : dir1.light;
    esac;

This seems complex, but it will be very powerful if we can have formal specification using these kind of Model Checking.