Nusmv 中的 Digicode

Question

我是 NUSMV 的新手，我正在尝试为 reconize 41708 建模数字代码，但用户不能再犯 3 个错误。如果您输入更多 3 个错误，当您输入要解锁的特殊代码时，系统会进入阻塞状态等待。如果您不能帮助我提出想法并建议完成代码，那就是我的代码。

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;

Image of Model

Answer 1

一个可能的解决方案是：

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;

解决方案假设一次只能输入一个数字，通过输入 in_digit，并且有一个单独的控制信号 in_signal 来重置设备。

设备有三种可能的状态：

RUN：设备从in_digit读取一个输入数字，并与固定密码序列
OK: 设备在过去某个时候识别了输入序列，现在忽略任何进一步的输入
ERROR：用户输入错误次数过多，设备忽略任何输入数字，直到 in_signal 变为 true。

在模型的末尾，我添加了三个 INVAR 约束，其中 p运行e 从与我们不相关的边缘过渡 space，因为一些输入被忽略了在某些时刻。忽略这些输入可以更容易地手动模拟系统。

运行例子，使用NuSMV:

~$ NuSMV -int
~$ reset; read_model -i digicode.smv; go; pick_state -iv; simulate -iv -k 30
~$ quit

另一种更简单的方法是一次性向 digicode 提供 5 个输入数字。这样一来，就可以把模型中的idx和pwd去掉，就简单多了。

Nusmv 中的 Digicode

Digicode in Nusmv

nusmv