CONST
 bsize : 16;
 bsize_1 : bsize-1;

TYPE
 byteT : 0..bsize_1;

VAR
 c1, c2 : byteT;

STARTSTATE
 c1 := 0;
 c2 := 0;
ENDSTARTSTATE;

STARTSTATE
 c1 := bsize_1;
 c2 := bsize_1;
ENDSTARTSTATE;

RULE "up c1"
 true ==> c1 := (c1+1) % bsize;
ENDRULE;

RULE "down c1"
-- Murphi's mod is broken - does not know that -1%bsize is bsize_1.
 true ==> if c1=0 then c1 := bsize_1 else c1 := c1-1 endif; -- (c1-1) % bsize;
ENDRULE;

RULE "up c2"
 true ==> c2 := (c2+1) % bsize;
ENDRULE;

RULE "down c2"
-- Murphi's mod is broken - does not know that -1%bsize is bsize_1.
 true ==> if c2=0 then c2 := bsize_1 else c2 := c2-1 endif; -- (c2-1) % bsize;
ENDRULE;

-->1 INVARIANT
-->1 true
-->1 ;

-- mu -b -c two-bytes.m
-- make two-bytes
-- mkdir two-bytes-trace
-- two-bytes -vbfs -b40 -tv -ndl -m200 -p4 -d two-bytes-trace

INVARIANT
 ! ( (c1 = 13) &  (c2 = 2) )
 ;