nuXmv是一种基于NuSMV开发的符号模型检测器，能够在有限状态系统上使用SAT的一些算法做验证，能够在无限状态系统上（比如含有实数或者整数变量的系统）使用SMT技术做验证。nuXmv支持同步系统，对异步系统不再支持。

1 nuXmv交互式Shell

在官网下载nuXmv后直接就能拿到一个可执行文件，Windows上就是nuXmv.exe。主要使用的方式就是用它的交互式Shell，使用nuxmv -int即可进入（这里int是interactive的意思）。

交互式Shell里有很多命令，使用help可以查看所有的命令。对于一个指定的命令，后跟-h就能够查看这个命令的具体使用方法。

使用reset命令可以重置整个系统，也就是和刚打开交互式Shell的时候一样，当需要加载另一个模型之前应当执行这个命令。

使用read_model [-i filename]命令可以把指定的文件里的模型读入进来。

使用go、go_bmc、go_msat等命令可以初始化nuXmv的验证（Verification）或者模拟执行（Simulation）使用指定的后端引擎。

使用pick_state [-v] [-a] [-r | -i]命令可以从初始状态集合中选取一个状态：

• -v用于打印选取的状态
• -r用于从初始状态集合中随机选取一个状态
• -i用于交互式地选取一个指定的状态
• -a用于显示所有的状态变量（需要配合-i使用）

使用simulate [-p | -v] [-a] [-r | -i] -k N可以进行模拟执行，从当前状态开始，最多执行N次转移：

• -p用于在生成的trace中打印有变化的变量
• -v用于在生成的trace中打印所有变量（包括有变化的和未变化的）
• -a用于输出所有状态变量（需要配合-i使用）
• -r用于在任何状态随机选择下一个状态
• -i用于在任何状态交互式地选择下一个状态

使用print_current_state [-h] [-v]输出当前的状态：

• -v用于输出所有的变量

使用goto_state state_label跳转到state_label所指示的状态，可以用来在trace上导航。

使用show_traces [-t] [-v] [-a | TN [.FS[:[TS]]]定位到traceTN，从FS状态出发，到TS状态结束。

• -t输出已经存储的trace的总数
• -v输出trace的详细内容
• -a打印所有当前已经存储的trace

使用show_vars [-s] [-f] [-i] [-t] [-v]打印变量内容和类型。

• -s输出状态变量
• -f输出冻结的变量
• -i输出输入的变量
• -t打印变量的数目
• -v启动详细打印

使用quit退出交互式Shell程序。

2 nuXmv建模元素

nuXmv的模型文件是.smv类型的，它可以组织多个模块，每个模块包含：

• 状态变量声明
• 可用的初始状态的赋值式声明
• 转移关系的赋值式声明

例如：

MODULE main
VAR b0 : boolean;ASSIGNinit(b0) := FALSE;next(b0) := !b0;

程序中只有一个状态变量b0，它的后继状态就是它取反。

2.1 基本类型

形如x : boolean;声明布尔值，取值可以为TRUE或者FALSE。

形如s : {ready, busy, waiting, stopped};声明枚举值。

形如n : 1..8;声明有界整数。

形如n : integer;声明整数，其取值范围在C/C++定义的INT_MIN和INT_MAX之间。

形如r : real;定义实数，取值可以是1.66、f'2/3、2e3、10e-1等形式。

形如unsigned word[3];或signed word[7];定义比特数组，可以支持按位运算和算数运算。

形如x : array -1..10 of T;定义T类型的数组，需要指定数组的下界和上界，例如：

VARx : array 0..10 of boolean; -- 11个元素的布尔数组y : array -1..1 of {red, green, orange}; -- 3个元素的枚举数组z : array 1..10 of array 1..5 of boolean; -- 以数组作为元素的数组
ASSIGNinit(x[5]) := bool(1); -- 给数组某个值赋初始值init(y[0]) := {red, green}; -- 这表示它的初始值可以是集合里的任何一个init(z[3][2]) := TRUE; -- 二维数组的访问

注意数组索引必须是常量。

对这节开头给出的例子添加一个变量b1，得到：

MODULE main
VARb0 : boolean;b1 : boolean;
ASSIGNinit(b0) := FALSE;next(b0) := !b0;

对应的状态机模型是：

整个有限状态机模型是所有的变量自己的状态迁移模型的同步积（Synchronized Product），而新的状态空间的每个状态都取自所有的状态变量的笛卡尔积。

2.2 初始状态

初始状态的设置形如：
$$init(⟨variable⟩):=⟨simple\_expression⟩;$$

表示某个变量的初始值受右侧的简单表达式限制，比如init(x) := FALSE;。简单表达式还可以是一个集合，例如init(y) := {1,2,3};表示变量y的初始值可以是这个集合中的任何一个。如果一个变量没有用这样的方式约束，那么它的初始值可以是它的取值范围里的任何一个值。

初始状态集合：满足所有的init()约束的状态的集合，每个状态是所有变量具体取值后的笛卡尔积。

如果在2.1的例子里加一句init(b1) := FALSE;，那么这个模型的初始状态就被约束到了<!b0, !b1>，所以上面的图里的左下角的状态上不再具有初始状态标记。

2.3 表达式

算术运算符有：+、-、*、/、mod、-(unary)。

比较运算符有：=、!=、>、<、<=、>=。

逻辑运算符有：&、|、xor、!(not)、->、<->。

位运算符有：>>、<<。

集合算子形如：{v1, v2, ..., vn}。其上的运算符in用来测试一个元素是否在指定的集合中，union用来计算两个集合的并集。

计数算子形如：count(b1 + b2 + ... + bn)，用来计算布尔表达式为TRUE的数目。

case表达式形如：

casec1 : e1;c2 : e2;...TRUE : en;
esac;

其语义是如果c1成立就取用e1，否则，如果c2成立就取用e2，……，全都不成立时，取用en。

条件分支表达式形如：cond_expr ? basic_expr1 : basic_expr2，即相当于C/C++里的三目运算符。

转型操作符，常见的有toint、bool、floor。还有swconst和uwconst分别用来将int转换为signed word和unsigned word；word1用来将boolean转换成一个仅有一位的word；unsigned和signed用来实现signed word和unsigned word的互相转换。

表达式不是一定需要计算成一个单个的值，也可以是表达一组可能的取值，即集合，例如：

init(var) := {a, b, c} union {x, y, z};

就是两个集合的并运算，表达式的结果也是一个集合，不是单个值。如果表达式是单个值c，那其实就是集合{c}的缩写。

赋值中的:=操作表示左值可以被非确定地用右值集合中的值来赋值。

2.4 转移关系

转移关系给出了变量在下一个状态上的取值的约束限制，形如：
$$next(⟨variable⟩):=⟨next\_expression⟩;$$

其中，表达下一状态的表达式next_expression可以依赖于当前状态的取值和下一状态的取值：

next(a) := {a, a + 1};
next(b) := b + (next(a) - a);

转移关系一定是能从变量的取值计算出来值的，对于不带约束的变量，其next取值也一定是非确定的。

下面是一个0~3的二进制计数器的例子，其中b0表示低位，b1表示高位，当低位变成1之后下一步高位就翻转，否则高位不变：

MODULE main
VARb0 : boolean;b1 : boolean;
ASSIGNinit(b0) := FALSE;next(b0) := !b0;init(b1) := FALSE;next(b1) :=caseb0 : !b1;TRUE : b1;esac;

对应的状态机模型：

2.5 输出变量

输出变量是没有init()约束也没有next()约束，仅依赖于其它状态变量的当前值的变量，用于建模系统的输出，形如：
$$⟨variable⟩:=⟨simple\_expression⟩$$

例如，为2.4中的计数器加上一个输出变量out，用来输出计数器的当前值的十进制表示，只要在VAR声明部分加上：

out : 0..3;

再在ASSIGN赋值部分加上：

out := toint(b0) + 2 * toint(b1);

2.6 赋值规则

单变量规则：每个变量只能被赋值一次，不能有同一变量的多次init()或者多次next()。

循环依赖规则：多条赋值动作里不能有循环依赖。

2.7 DEFINE声明

类似于C/C++中的宏定义，在DEFINE中定义的标识的每次出现都会被替换为DEFINE体。DEFINE声明提供了一种定义输出变量的新方式。比如2.5中的输出变量用DEFINE的话就不用VAR声明了，直接在最下面加个DEFINE声明：

DEFINEout := toint(b0) + 2 * toint(b1);

2.8 外部控制信号

在模型中可以定义一个既没有init()，也没有next()，也不是输出变量，但是却参与了其它变量的计算的变量。这个变量对模型自己来说是没法控制的，但是可以作为一种外部控制信号。例如，下面是对前面的计数器的例子，加上了一个重置信号，每当重置信号来临（变量reset置为TRUE）的时候，下一个状态一定是回到<0,0>，即计数器的两个位都置为FALSE，达到计数器重置的效果：

MODULE main
VARb0 : boolean; -- 计数器的低位b1 : boolean; -- 计数器的高位reset : boolean; -- 指示计数器的充值，是模型本身无法控制的外部信号
ASSIGNinit(b0) := FALSE; -- 低位初始是0init(b1) := FALSE; -- 高位初始是0next(b0) :=casereset = TRUE : FALSE; -- 如果有重置信号，即要变到00，所以低位置0reset = FALSE : !b0; -- 没有重置信号，正常工作esac;next(b1) :=casereset : FALSE; -- 如果有重置信号（这里reset即是reset = TRUE），即要变到00，所以高位置0TRUE : ((!b0 & b1) | (b0 & !b1)); -- 没有重置信号，正常工作esac;
DEFINEout := toint(b0) + 2 * toint(b1); -- 定义输出变量，是计数器的当前值的十进制表示

对应的状态机（绿色是重置导致的转移）：