-1

我是 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;

模型图像

4

1 回答 1

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;

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

该设备具有三种可能的状态：

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

在模型的最后，我添加了三个INVAR约束，它们从与我们不相关的边缘中修剪过渡空间，因为某些输入在某些时刻被忽略了。忽略这些输入可以更容易地手动模拟系统。

运行示例，使用NuSMV：

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

另一种更简单的方法是digicode一次提供 5 个输入数字。通过这种方式，可以从模型中移除idx和移除pwd模型，使其更简单。

于 2018-02-23T12:54:23.600 回答