NuSMV教程(一)

简单示例
仿真

本章主要是简单介绍几个例子，熟悉一下NuSMV的表达方式。

Exapmles

同步系统

Single Process Example

MODULE main
VAR
    request : boolean;
    state   : {ready, busy};
ASSIGN
    init(state) := ready;
    next(state) := case
                        state = ready & request = TRUE : busy;
                        TRUE : {ready, busy}; 
                   esac;

Var 为变量的声明，冒号后面是它们能够取的值或者变量类型，这里不用过多解释。下面的赋值操作中有对状态的操作，init是对state初始化，为其初始化为ready；而request变量并没有为它初始化，因此它可以取false，也可以去true；而对于有限状态机的状态转移，可通过定义变量next状态下的值来描述，也就是说next后的参数是当前状态的值，当前state变量的下一个状态的定义就用next(state)来表示，这里是一个case判断。

Binary Counter

这一个程序使用了表达式与module的复用，这是一个三位的电流计数器。Module的顺序不会影响。

MODULE counter_cell(carry_in)
VAR
   value : boolean;
ASSIGN
   init(value) := FALSE;
   next(value) := value xor carry_in;
DEFINE
  carry_out := value & carry_in;

MODULE main
VAR
   bit0 : counter_cell(TRUE);
   bit1 : counter_cell(bit0.carry_out);
   bit2 : counter_cell(bit1.carry_out);

通过在main中实例化三次counter_cell，分别为它们取名为bit0、bit1、bit2。而ccounter_cell有一个输入参数carry_in，而bit0.carry_in这种取值方式应该很常见；而DEFINE则是用来将等式右边的表达式赋值给符号carry_out；因此一个的definition定义，可以理解为根据当前其他变量的值获得此要定义变量的值。当然需要注意的是，其他变量的当前值是通过ASSIGN得到的，而不是next的值。

定义符号Symbol不需要引入新的变量，因此这样也不会增加有限状态机的状态空间，另一方面，不可能非确定性地给定义的符号赋值。还有就是定义变量会去声明其类型，而定义符号不用。

异步系统

Inverter Ring

MODULE inverter(input)
VAR
   output : boolean;
ASSIGN
   init(output) := FALSE;
   next(output) := !input;

MODULE main
VAR
   gate1 : process inverter(gate3.output);
   gate2 : process inverter(gate1.output);
   gate3 : process inverter(gate2.output);

实例化中有关键词```Process``，执行它们是不确定的，并且在process中的语句执行是并行的。那么如果一个process没有为一给定的变量赋值，那么这个变量的值肯定是不变的。由于下一个process的执行是不确定的，该程序门的速度逆变器环进行独立地建模。

为了强制一个给定的process能够经常无限次地执行，我们使用fairness限制。每一个process都有一个特殊的变量叫做running，当且仅当该process在执行时为TRUE。

FAIRNESS
  running

Mutual Exclusion

使用信号量semaphore在两个异步进程中实现互斥。每一个进程process都有四个状态：idle, entering, critical 和 exiting。

entering 代表process想要进入临界区；
如果信号量变量semaphore为false，那么它进入临界状态，并设置semaphore为TRUE。
一旦从临界区exiting，那么process就设置为FALSE。

MODULE main
VAR
   semaphore : boolean;
   proc1     : process user(semaphore);
   proc2     : process user(semaphore);
ASSIGN
   init(semaphore) := FALSE;

MODULE user(semaphore)
VAR
    state : {idle, entering, critical, exiting};
ASSIGN
    init(state) := idle;
    next(state) :=
        case
            state = idle                  : {idle, entering}; 
            state = entering & !semaphore : critical;
            state = critical              : {critical, exiting};
            state = exiting               : idle;
            TRUE                          : state;
        esac;
    next(semaphore) :=
        case
            state = entering : TRUE;
            state = exiting  : FALSE;
            TRUE             : semaphore;
        esac;
FAIRNESS
    running

直接的规范

NuSMV可以通过命题逻辑公式直接描述一个有限状态机FSM。初始状态集合可以以一个当前状态变量表示的公式来规范定义。满足该公式的状态即是初始状态。

一个转移关系可以直接以一个命题公式来表示，该命题公式是状态变量的当前值与下一个值。满足该公式的都是当前状态与下一个状态的转移关系对。

这两个功能用INIT和TRANS来表示。

MODULE main
VAR
   gate1 : inverter(gate3.output);
   gate2 : inverter(gate1.output);
   gate3 : inverter(gate2.output);

MODULE inverter(input)
VAR
   output : boolean;
INIT
   output = FALSE
TRANS
   next(output) = !input | next(output) = output

根据TRANS所定义的，对于每一个inverter，output的下一个值要么是非input，那么是当前的output值。

仿真

仿真使得用户能够对一个NuSMV模型进行一些执行，走一些traces。通过这种方式，用户可以更加熟悉模型，并且能在真正验证程序性质之前能够更有信心保证其正确性。

路径策略 Trace Strategies

为了在模拟阶段能够达到最大的灵活性和自由度，NuSMV采用了三种路径生成策略：确定的、随机的、相互影响的。

确定的 —— 首选集合中的第一个状态
随机的 —— 随便选了，不确定的

在以上两种方式中，都是由NuSMV自动生成路径。用户在一次时间内得到整个路径，而不干预生成方式。

相互影响的 —— 用户能够通过一些操作来影响路径的生成，用户有着完全的控制权。

在第三种模拟方式中，系统会在每一步停顿下，并显示出未来可能的状态列表：用户请求去选择它们其中的一个状态。系统会请求用户进行一些限制，以便能够使得显示的状态数量在一个预先设置的范围以内。当然也要注意一些前后矛盾的输入。

人机交互模式 Interactive Mode

例如使用以下的模型：

MODULE main
VAR
    request : boolean;
    state   : {ready, busy};
ASSIGN
    init(state) := ready;
    next(state) := case
                        state = ready & request = TRUE : busy;
                        TRUE : {ready, busy}; 
                   esac;

在这之前，NuSMV需要将模型读入程序。假设模型名保存为short.smv，那么通过以下命令:

system prompt> NuSMV -int short.smv
NuSMV> go
NuSMV>

那么就得到了显示的结果：

Current state is 1.1
request = FALSE
state = ready

选择一个初始状态

开始模拟之前一般需要指定一个初始状态，这个能够用三种方式办到：

默认使用当前状态作为一个新的仿真的起始状态；当然只有定义过一个当前状态时才有效；
使用goto_state命令的话，用户可以选择任何一存在路径上的状态作为当前状态current state；
使用pick state命令的话，可以在模型的初始状态中选择一个起始状态；这个命令可以在当前状态current state不存在的时候使用（也就是模型还没有开始进展，或者被重置的时候）。

那么在以上的模型中，并没有当前状态current state，系统中也没有当前储存的路径。因此，使用pick_state，使用simulate命令：

system prompt> NuSMV -int short.smv NuSMV> go
NuSMV> pick state -r
NuSMV> print current state -v
NuSMV> simulate -r -k 3
********* Starting Simulation From State 1.1 ********* NuSMV> show traces -t
There is 1 trace currently available.
NuSMV> show traces -v
#################### Trace number: 1 #################### Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 1.1 <-
    request = FALSE
    state = ready
-> State: 1.2 <-
    request = TRUE
    state = busy
-> State: 1.3 <-
    request = TRUE
    state = ready
-> State: 1.4 <-
    request = TRUE
    state = busy

这里面接触到了几个命令：

pick state -r 在模型的初始化状态集合中随机选择起始状态；
simulate -r -k 3 通过随机产生下一步状态来进行三步的仿真；
show traces -v 最后的路径包含了4个状态(初始状态，以及三个由随机仿真增加的状态)；
每一个路径都由一个整型数字定义，每一个状态则由点后面的数字标识；

开始一个新的仿真

接下来可以选择之前的状态1.4作为当前的状态，然后再随机仿真3步；得到如下的结果：

NuSMV> goto state 1.4
The starting state for new trace is: -> State 2.4 <-
    request = TRUE
state = busy
NuSMV> simulate -r -k 3
******** Simulation Starting From State 2.4 ******** NuSMV> show traces 2
################### Trace number: 2 ################### Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 2.1 <-
    request = TRUE
    state = ready
-> State: 2.2 <-
    state = busy
-> State: 2.3 <-
    request = FALSE
-> State: 2.4 <-
request = TRUE
-> State: 2.5 <-
    request = FALSE
-> State: 2.6 <-
    state = ready
-> State: 2.7 <-
NuSMV>

读者可以从前面的例子中看到，新轨迹存储为轨迹2.用户还可以交互式地选择他想要构建的轨迹的状态：交互式仿真示例如下所示：

NuSMV> pick state -i
*************** AVAILABLE STATES *************
================= State =================
0) -------------------------
    request = TRUE
    state = ready
================= State =================
1) -------------------------
    request = FALSE
    state = ready
Choose a state from the above (0-1): 1 <RET>
Chosen state is: 1
NuSMV> simulate -i -k 1
******** Simulation Starting From State 3.1 ********
***************  AVAILABLE FUTURE STATES  *************
================= State =================
0) -------------------------
    request = TRUE
    state = ready
================= State =================
1) -------------------------
    request = TRUE
    state = busy
================= State =================
2) -------------------------
    request = FALSE
    state = ready
================= State =================
3) -------------------------
    request = FALSE
    state = busy

Choose a state from the above (0-3): 0 <RET>
Chosen state is: 0
NuSMV> show traces 3
################### Trace number: 3 ################### Trace Description: Simulation Trace
Trace Type: Simulation
-> State: 3.1 <-
    request = FALSE
    state = ready
-> State: 3.2 <-
    request = TRUE

表述限制Specifying Constraints

pick state和simulate命令都能够使用-C来设置限制条件，

NuSMV> pick state -c "request = TRUE" -i 
*************** AVAILABLE STATES ***************
================= State =================
0) -------------------------
    request = TRUE
    state = ready
There’s only one future state. Press Return to Proceed. <RET>
Chosen state is: 0 NuSMV> quit
system prompt>

-C是对整个生成的路径全局可见的，它包括在了仿真的每一步中；而与之相辅相成的pick_state命令则是局部的，在下一步就好失效。

参考资料

NuSMV 2.6 Tutorial