1 约束式建模

前面学习的建模方式都是赋值式（Assignment Style） 的，可以将这些模型转换成一种约束式（Constraint Style） 的，多数时候都会让模型的表达更方便。

例如，下面的模型表达的是某种机器在就绪（ready）时，如果有请求来了，就会开始忙碌（busy），否则接下来既可以就绪也可以忙碌：

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

重写这个next()转换，可以将其变成约束式的（注意ASSIGN被拆成了INIT和TRANS两块）：

MODULE main
VAR
    request : boolean;
    state : {ready, busy};
INIT
    state := ready;
TRANS
    (state = ready & request) -> next(state) = busy;

约束式建模，其核心在于一个模型可以用若干个如下约束来表达：

• 不变性状态：INVAR <simple_expression>
• 初始状态：INIT <simple_expression>
• 转移关系：TRANS <simple_expression>

约束可以和赋值ASSIGN混合使用，约束可以是任何合法的命题公式，使用约束往往是更加精简的，并不是所有的约束都能方便的使用赋值ASSIGN来表达。

2 赋值式和约束式的比较

赋值式的建模在构造时，至少有一个初始状态，所有的状态都至少有一个后继状态，并且模型中的非确定性是非常明显的（未赋值的变量、集合赋值等）。

约束式的建模在构造时，因为写约束写的有问题可能带来一些坑。如果初始状态的约束是前后矛盾的，那么就会导致没有初始状态；如果转移的约束是前后矛盾的，那么就会导致发生死锁（可以用check_fsm来检查模型中的死锁）。另外，因为约束本身的不易理解，模型中的非确定性可能非常难以察觉（例如上面的例子）。

3 约束式建模的例子

这里两个例子演示了建模中比较容易踩坑的地方。

3.1 关于case的例子

MODULE main()
VAR
    state : {S0, S1, S2};
DEFINE
    go_s1 := state != S2;
    go_s2 := state != S1;
INIT
    state = S0;
TRANS
    case
        go_s1 : next(state) = S1;
        go_s2 : next(state) = S2;
    esac;

这个例子里需要注意因为case是逐条执行的，是有先后顺序的，一旦某一条的条件满足了，后面的就不再执行了，所以实际上是没有从S0向S2的迁移的，其状态机模型：

3.2 关于next的例子

MODULE main()
VAR
    arr: array 0..1 of {1,2};
    i : 0..1;
ASSIGN
    init(arr[0]) := 1;
    init(arr[1]) := 2;
    init(i) := 0;
    next(i) := 1-i;
TRANS
    next(arr[i]) = arr[1-i] & next(arr[1-i]) = arr[i];

这个例子里需要注意next的语义，在next()操作符中的所有内容都会先计算其后继状态的情况，包括数组的下标，所以这里的TRANS里的next(arr[i])中的下标i会被计算成1-i，同理next(arr[1-i])中的下标1-i会被计算成i，因此这个模型并不能完成数组arr中的两个数交换的操作，其状态机模型：

如果想要完成交换，最后一行要改成next(arr[1-i]) = arr[1-i] & next(arr[i]) = arr[i]，虽然这个语义很别扭。

4 多模块定义

模型里应当有一个主模块main和若干其它模块，模块（MODULE）可以在其他模块的VAR中被例化成一个变量，然后使用.操作符来访问例化的模块中的变量。例如，下面定义了从0到9的循环计数器的模块，然后在主模块中例化了两个该模块并进行加法运算：

MODULE counter
VAR
    out: 0..9;
ASSIGN
    next(out) := (out + 1) mod 10;

MODULE main
VAR
    m1 : counter;
    m2 : counter;
    sum: 0..18;
ASSIGN
    sum := m1.out + m2.out;

这个例化结构的概念图如下：

模块就可以理解成进程模板的概念，所以是可以有构造结构的，在模块声明的地方可以写构造器（比如可以写MODULE counter(in)），然后模块例化时候可以传参数（比如可以写VAR m1 : counter(m2.out);），参数是以引用的形式传递到模块内部的。

5 多模块构型

这里的构型（Composition） 指的是不同的例化模块之间“向后继转移”这件事是同步的还是异步的。

5.1 同步

下面是一个红绿蓝三色轮换的模型：

MODULE cell(input)
VAR
    val : {red, green, blue};
ASSIGN
    next(val) := input;

MODULE main
VAR
    c1 : cell(c3.val);
    c2 : cell(c1.val);
    c3 : cell(c2.val)

这个例化结构的概念图如下：

在默认情况下，所有的例化模块之间是同步的，也就是说所有的模块都会一起往后转移一步。

上面的例子每一步执行完的状态trace如下：

5.2 异步

如果要让不同的例化模块的转移动作是异步进行的，可以用关键字来指明一下，比如对于上面的模型，要改成：

MODULE cell(input)
VAR
    val : {red, green, blue};
ASSIGN
    next(val) := input;
FAIRNESS running

MODULE main
VAR
    c1 : process cell(c3.val);
    c2 : process cell(c1.val);
    c3 : process cell(c2.val);

异步模型关键就是要在例化的地方加上process标记，每个process在运行时都会有一个独立的运行时布尔变量，仅当这个布尔变量置为TRUE时这个process才会向后执行。

注意模型里的FAIRNESS running，这表示采用公平调度策略，保证其process获得运行的机会是公平的。

上面的例子每一步执行完的可能的状态trace如下（加粗的地方process发生了状态转移）：

注意，process标记在nuXmv里已经弃用了，不会再维护了。

6 例子：四位加法器

四位加法器模型定义如下：

-- 一位加法器模块（位1，位2，进位输入）
MODULE bit-adder(in1, in2, cin)
VAR
    sum : boolean; -- 加法结果
    cout : boolean; -- 进位输出
ASSIGN
    next(sum) := (in1 xor in2) xor cin; -- 异或就是不进位加法
    next(cout) := (in1 & in2) | ((in1 | in2) & cin); -- 求进位，其实就是看in1/in2/cin里有没有两个TRUE

-- 四位加法器模块（位数组1，位数组2）
MODULE adder(in1, in2)
VAR
    -- 最低位，就是两个最低位组成的一加法器模块，因为是最低位，所以来自上一位的进位是FALSE
    bit[0] : bit-adder(in1[0], in2[0], FALSE);
    -- 只要不是最低位，都要把上一位的进位输出搞进来
    bit[1] : bit-adder(in1[1], in2[1], bit[0].cout);
    bit[2] : bit-adder(in1[2], in2[2], bit[1].cout);
    bit[3] : bit-adder(in1[3], in2[3], bit[2].cout);
DEFINE
    -- 这里的sum和overflow只计算不声明，是输出变量
    sum[0] := bit[0].sum;
    sum[1] := bit[1].sum;
    sum[2] := bit[2].sum;
    sum[3] := bit[3].sum;
    overflow := bit[3].cout;

-- 主模块
MODULE main
VAR
    -- 给四位加法器用的两个四位比特数组
    in1 : array 0..3 of boolean;
    in2 : array 0..3 of boolean;
    -- 四位加法器模块例化
    a : adder(in1, in2);
ASSIGN
    -- 因为模块例化的构造器是传引用的，所以结果会自己算和更新，这里的next还是自己
    next(in1[0]) := in1[0];
    next(in1[1]) := in1[1];
    next(in1[2]) := in1[2];
    next(in1[3]) := in1[3];
    next(in2[0]) := in2[0];
    next(in2[1]) := in2[1];
    next(in2[2]) := in2[2];
    next(in2[3]) := in2[3];
DEFINE
    -- 这三个是输出变量，op1是操作数1的十进制值，op2是操作数2的十进制值，sum是经过四位加法器加法后的十进制值
    op1 := toint(in1[0]) + 2*toint(in1[1]) + 4*toint(in1[2]) + 8*toint(in1[3]);
    op2 := toint(in2[0]) + 2*toint(in2[1]) + 4*toint(in2[2]) + 8*toint(in2[3]);
    sum := toint(a.sum[0]) + 2*toint(a.sum[1]) + 4*toint(a.sum[2]) + 8*toint(a.sum[3]) + 16*toint(a.overflow);

进入nuXmv的交互Shell：

nuxmv -int

读取模型文件：

nuXmv > read_model -i addr.smv

将模型展平：

nuXmv > flatten_hierarchy

对变量编码：

nuXmv > encode_variables

构建模型：

nuXmv > build_model

随机选取模型的初始状态，并显示详细信息：

nuXmv > pick_state -v -r
Trace Description: Simulation Trace 
Trace Type: Simulation
  -> State: 1.1 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = FALSE
    a.bit[1].cout = TRUE
    a.bit[2].sum = FALSE
    a.bit[2].cout = TRUE
    a.bit[3].sum = FALSE
    a.bit[3].cout = TRUE
    sum = 16
    op2 = 4
    op1 = 10
    a.overflow = TRUE
    a.sum[3] = FALSE
    a.sum[2] = FALSE
    a.sum[1] = FALSE
    a.sum[0] = FALSE

模拟执行，设定只转移5次（所以trace上有6个状态），并显示详细信息：

nuXmv > simulate -v -k 5
********  Simulation Starting From State 1.1   ********
Trace Description: Simulation Trace
Trace Type: Simulation
  -> State: 1.1 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = FALSE
    a.bit[1].cout = TRUE
    a.bit[2].sum = FALSE
    a.bit[2].cout = TRUE
    a.bit[3].sum = FALSE
    a.bit[3].cout = TRUE
    sum = 16
    op2 = 4
    op1 = 10
    a.overflow = TRUE
    a.sum[3] = FALSE
    a.sum[2] = FALSE
    a.sum[1] = FALSE
    a.sum[0] = FALSE
  -> State: 1.2 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = TRUE
    a.bit[1].cout = FALSE
    a.bit[2].sum = FALSE
    a.bit[2].cout = TRUE
    a.bit[3].sum = FALSE
    a.bit[3].cout = TRUE
    sum = 18
    op2 = 4
    op1 = 10
    a.overflow = TRUE
    a.sum[3] = FALSE
    a.sum[2] = FALSE
    a.sum[1] = TRUE
    a.sum[0] = FALSE
  -> State: 1.3 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = TRUE
    a.bit[1].cout = FALSE
    a.bit[2].sum = TRUE
    a.bit[2].cout = FALSE
    a.bit[3].sum = FALSE
    a.bit[3].cout = TRUE
    sum = 22
    op2 = 4
    op1 = 10
    a.overflow = TRUE
    a.sum[3] = FALSE
    a.sum[2] = TRUE
    a.sum[1] = TRUE
    a.sum[0] = FALSE
  -> State: 1.4 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = TRUE
    a.bit[1].cout = FALSE
    a.bit[2].sum = TRUE
    a.bit[2].cout = FALSE
    a.bit[3].sum = TRUE
    a.bit[3].cout = FALSE
    sum = 14
    op2 = 4
    op1 = 10
    a.overflow = FALSE
    a.sum[3] = TRUE
    a.sum[2] = TRUE
    a.sum[1] = TRUE
    a.sum[0] = FALSE
  -> State: 1.5 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = TRUE
    a.bit[1].cout = FALSE
    a.bit[2].sum = TRUE
    a.bit[2].cout = FALSE
    a.bit[3].sum = TRUE
    a.bit[3].cout = FALSE
    sum = 14
    op2 = 4
    op1 = 10
    a.overflow = FALSE
    a.sum[3] = TRUE
    a.sum[2] = TRUE
    a.sum[1] = TRUE
    a.sum[0] = FALSE
  -> State: 1.6 <-
    in1[0] = FALSE
    in1[1] = TRUE
    in1[2] = FALSE
    in1[3] = TRUE
    in2[0] = FALSE
    in2[1] = FALSE
    in2[2] = TRUE
    in2[3] = FALSE
    a.bit[0].sum = FALSE
    a.bit[0].cout = FALSE
    a.bit[1].sum = TRUE
    a.bit[1].cout = FALSE
    a.bit[2].sum = TRUE
    a.bit[2].cout = FALSE
    a.bit[3].sum = TRUE
    a.bit[3].cout = FALSE
    sum = 14
    op2 = 4
    op1 = 10
    a.overflow = FALSE
    a.sum[3] = TRUE
    a.sum[2] = TRUE
    a.sum[1] = TRUE
    a.sum[0] = FALSE