i am new with NUSMV i am trying to modelise a digicode for reconize 41708 but user can't do more 3 error. if you enter more 3 error the system go to state bloked to wait when you enter special code to be unblocked. it is my code if you cant help me with idea and suggest code to finish .
MODULE main
VAR
val1 : {0,1,2,3,4,5,6,7,8};
location : {E1,E2,E3,E4,E5,succes,blocked,unblocked,verified};
cpt : 0..3;
block : boolean;
NumberEnter : 0..5 ;
ASSIGN
init(cpt):=0;
init(block):=FALSE;
init(location):=E1;
next(location):= case
(location=E1) &(cpt!=3) & (block!=TRUE) :E2 ;
(location=E2) & (cpt!=3) & (block!=TRUE) :{E3,E1,blocked};
(location=E3) & (cpt!=3) & (block!=TRUE) :{E2,E1,blocked} ;
(location=E4) & (cpt!=3) & (block!=TRUE) :{E1,E5,blocked} ;
(location=E5) & (cpt!=3) & (block!=TRUE) :{E1,blocked} ;
TRUE:blocked;
esac;
next(pas):= case
NumberEnter<5 :NumberEnter+ 1 ;
TRUE:0;
esac;
One possible solution is:
MODULE main()
VAR
in_digit : 0 .. 9;
in_signal : boolean;
dc : digicode(in_digit, in_signal);
MODULE digicode(in_digit, in_signal)
VAR
state : { RUN, OK, ERROR };
idx : 0 .. 4;
counter : 0 .. 3;
DEFINE
pwd := [4, 1, 7, 0, 8];
INIT state = RUN & idx = 0 & counter = 0;
ASSIGN
next(state) := case
state = RUN & pwd[idx] = in_digit & idx < 4 : RUN;
state = RUN & pwd[idx] = in_digit : OK;
state = RUN & pwd[idx] != in_digit & counter < 3 : RUN;
state = RUN & pwd[idx] != in_digit : ERROR;
state = ERROR & in_signal : RUN;
TRUE : state;
esac;
next(counter) := case
state = RUN & pwd[idx] != in_digit & counter < 3 : counter + 1;
state = RUN & pwd[idx] = in_digit : counter;
TRUE : 0;
esac;
next(idx) := case
state = RUN & pwd[idx] = in_digit & idx < 4 : idx + 1;
state = RUN & pwd[idx] != in_digit : 0;
TRUE : 0;
esac;
--
-- the following invariants nicely restrict the set of viable
-- transitions when inputs can be ignored
--
INVAR
in_signal -> state = ERROR;
INVAR
state = ERROR -> in_digit = 0;
INVAR
state = OK -> in_digit = 0;
The solutions assumes that one can only enter one digit at a time, through input in_digit
, and that there is a separate control signal in_signal
to reset the device.
The device has three possible states:
RUN
: the device reads an input digit from in_digit
, and compares it with a fixed password sequenceOK
: the device recognized the input sequence some time in the past, and it is now ignoring any further inputERROR
: the user made too many incorrect input attempts, and the device is ignoring any input digit until in_signal
is true
.At the end of the model, I added three INVAR
constraints which prune the transition space from edges that are not relevant to us because of some inputs being ignored at certain moments. Ignoring those inputs makes it much easier to simulate the system by hand.
The run the example, use NuSMV
:
~$ NuSMV -int
~$ reset; read_model -i digicode.smv; go; pick_state -iv; simulate -iv -k 30
~$ quit
An alternative, and much simpler approach, would be to provide digicode
with 5 input digits all at once. In this way, one can remove idx
and pwd
from the model, making it much simpler.