本文共 815 字，大约阅读时间需要 2 分钟。

NuSMV(New Symbolic Model Verifier)新符号模型检测工具

1、安装方法

win64下，下载二进制文件：

CMD进入bin文件夹运行 NuSMV， 得到以下结果

2、数据类型：

　　Boolean（布尔）=FALSE / TRUE;

　　Int类型与C语言中范围相同；

　　Enumeration Types（枚举类型）：

　　　　symbolic enum type（符号枚举类）：{stopped, running, waiting}；

　　　　integers-and-symbolic enum type（整数-符号枚举类）：{-1, 1, waiting}, {0, 1, OK}；

　　　　integer enum（整数枚举类）：{2, 4, -2, 0}；

　　Enum不能包含boolean值,例如{FALSE,TRUE}。

　　word类：word[3]表示3bit向量，unsigned word[N]范围是0 到 2^(N − 1), signed word[N]范围是−2^(N−1) 到 2^(N−1) − 1

　　Array（数组）：

　　　　array 0..3 of boolean

　　　　array 10..20 of {OK, y, z}

　　　　array 1..8 of array -1..2 of unsigned word[5] 一个包含8个元素(从1到8)的数组，每个元素是包含4个元素(从-1到2)的数组，这些元素是5位长的无符号单词。

　　数组类型与集合类型不兼容，即数组元素不能为集合类型。

　　Set（集和）：四类：布尔集合、整数集合、符号集合、整数-符号集合。变量不可以是集合类。

3、运算符

　　逻辑运算符：

　　& (与), | (或), xor (异或), xnor = !xor, -> (蕴含),  <-> (当且仅当) , !(非)

转载地址：https://www.cnblogs.com/aidenchen8/p/13943338.html 如侵犯您的版权，请留言回复原文章的地址，我们会给您删除此文章，给您带来不便请您谅解！