这是一个鸽了很久的系列，本来是要记录完成本科毕设《状态机自动生成与图形化仿真系统研究与实现》的过程，因为使用的JavaBDD算是一个很老的包了，文档很少，而且这个领域的资料也很少，所以想着整理一下，方便后来人使用。但写了前三篇《开端》、《探索 Graphviz》和《探索 JavaBDD》之后，因为各种事情搁置了。
时光飞逝，到现在已经过了一年半的时间，从当时的本科毕设，到现在都开始做研究生毕设了😂本来是打算弃坑的，因为觉得它的价值随着时代变化已经越来越少了，但仍然偶尔能看到有朋友私信问我相关的问题。我意识到，虽然关注这个领域的人并不多，但可能一直都会有人怀着相同的疑问而无处寻得解答。因此，我决定用这一篇作为毕设记录的完结。
这里假设读者对JavaBDD、Graphviz已经有基本的了解，也已经看过前文了。本篇文章继续讲解JavaBDD的应用，布尔表达式的运算、CTL公式解析和模型检验。当然，还有不少其他的应用，但这里主要关注这三个。
1. 布尔表达式的运算
与其说是运算，不如说是让布尔表达式为真时，取值的情况。比如布尔表达式：A or B or C，计算的输出是<0:0, 1:0, 2:1><0:0, 1:1><0:1>，这里冒号前的 0、1 和 2 分别对应着 A、B 和 C，冒号后的 0 和 1 代表着真和假，每对尖括号意味着一种取值情况。因此，输出的意思是有三种情况使该布尔表达式成立：一是 A 和 B 为假，C 为真；二是 A 为假，B 为真，C真或假都可以；三是 A 为真，B 和 C 为真或假都可以。
如果不使用JavaBDD，怎么得到结果？可能有人说我肉眼看就能看出来。这样的话稍微复杂点，眼就要看花，比如(A or C)and ((B or not A) and (D or C))，估计得看几分钟才能得到结果。还有人说我让每个值取 0 和 1 两种情况，遍历所有结果。这比第一种方法好，但这样的复杂度是 O(2^n)，太慢了，而且输出也比较复杂。
以布尔函数result = (A or C)and(B or A)为例，它包含 A、B 和 C 三个布尔变量输入，result 一个布尔变量输出。当使用电路验证模块处理这个例子时，会得到下表中的结果：
| 序号 | A | B | C | result |
|---|---|---|---|---|
| 1 | 0 | 0 | 0 | 0 |
| 2 | 0 | 0 | 1 | 0 |
| 3 | 0 | 1 | 0 | 0 |
| 4 | 0 | 1 | 1 | 1 |
| 5 | 1 | 0 | 0 | 1 |
| 6 | 1 | 0 | 1 | 1 |
| 7 | 1 | 1 | 0 | 1 |
| 8 | 1 | 1 | 1 | 1 |
但是当使用布尔运算模块处理时，就会得到下图的结果了。仔细观察，会发现它们并不冲突，图中描述的情况与表中相吻合。前者将 result 和布尔变量输入的取值变化详细地展现出来了，而后者则以一种更简洁的情况描述了 result 取真值的情况，且情况 2 只需要 A 为真即可，对其他的变量取值没有要求。通过检查布尔函数可知，这也是符合逻辑的。
布尔运算模块的输出
1.1 逆波兰表达式
接下来说明对于布尔函数的运算是如何实现的。首先需要明确的是，其本质还是需要将结果布尔变量转化成BDD变量，然后通过JavaBDD来求取结果。但是，由于输入的布尔表达式可能会很复杂，比如包含一些空格和括号，无法被很容易地转化前文中的JavaBDD的形式。因此，首先需要考虑如何对原始的布尔函数进行处理，使其变成计算机能够理解的形式。
在这一点上，我从算术表达式求解的过程中得到了启发。日常生活中出现的算术表达式，如1+2-3*4/5，属于中序表达式的范畴，其中的运算符是在第一个和第二个操作数中间的。有一种求解它的思路是，先将其转化为逆波兰表达式（也称为后序表达式），然后再进行求解。
例如中序表达式(a+b)*c转化成逆波兰表达式后就是ab+c*，转化过程需要两个栈分别存放着变量和运算符，从左往右读入中序表达式，并将元素压入对应的栈。但运算符栈顶元素的优先级必须小于要压栈的运算符的优先级，否则在压栈前需要将运算符出栈并压入变量栈，直到满足要求。（需要注意的是，括号需要压入运算符栈，当遇到右括号时，重复将运算符栈的元素出栈并压入变量栈，直到遇到左括号，此时将左括号出栈即可。）当结束读入表达式时，再将运算符栈的元素依次出栈并压入变量栈。最终变量栈从栈底到栈顶的内容即为逆波兰表达式。
可能你读完上面这段话已经晕了，那么就看下面的动图吧😄
逆波兰表达式的转换
逆波兰表达式求值的步骤也很简单。准备一个空栈，从左至右读入表达式，遇到变量则压栈，遇到运算符则依次从栈中弹出两个变量，运算后继续入栈，直到最后栈中只剩下唯一的值，即为表达式的结果。 这部分实现的代码在网上有很多了。
像这样对表达式进行处理，算法的实现并不难，而且还能取出括号，更易于计算机理解。那么布尔表达式是否也能像这样被处理呢？答案是肯定的。每个布尔变量就像是算术表达式中的一个数字，每个逻辑运算符则像是加减乘除之类的运算符，使用JavaBDD对出栈的BDD变量进行运算，并将结果BDD变量压栈，就相当于对表达式进行计算的过程。流程图如下所示。
算法流程示意图
1.2 布尔表达式求值算法的设计与实现
布尔函数求值的算法主要分为三部分：第一部分对输入的字符串预处理，如去除多余的空格等，最终转化成List<String>类型的中序表达式；第二部分是对中序表达式处理，得到List<String>类型的逆波兰表达式；第三部分则是由逆波兰表达式得到布尔函数对应的 BDD 变量。第二部分的处理算法如下所示：
public static List<String> toReversePolishExpression
(List<String> middleOrderExpression) {
Stack<String> symbolStack = new Stack<>(); // 存放符号的栈
// 使用List来作为存放变量和符号的栈，更加灵活
List<String> num_sym_list = new ArrayList<>();
for (String element : middleOrderExpression) {
if (element.equals("(")) { symbolStack.push(element); }// 若为左括号则入栈
else if (element.equals(")")) {
while (!symbolStack.peek().equals("(")) {
num_sym_list.add(symbolStack.pop());}
symbolStack.pop();}// 将符号出栈直到栈顶是左括号，也将其出栈
else if (isBooleanSymbol(element)) {
while (symbolStack.size() != 0 && Operation.getValue(symbolStack.peek()) >= Operation.getValue(element)) {
num_sym_list.add(symbolStack.pop());}
symbolStack.push(element);}
else {num_sym_list.add(element); // 如果是变量的情况
//注意var_list是专门存放变量的，之后会对变量出现的次数进行统计
var_list.add(element);}}
// 处理完中序表达式后，若符号栈还有元素则将其插入变量栈
while (symbolStack.size() != 0) { num_sym_list.add(symbolStack.pop());}
return num_sym_list;
}
其中用到了isBooleanSymbol方法，该方法的作用是判断 String 类型的变量是否属于布尔运算符之一，使用正则表达式进行判断。具体代码如下：
public static Boolean isBooleanSymbol(String input) {
// 正则表达式的意思是匹配11种运算符号
if (input.matches("(?:and|or|not|diff|imp|biimp|invimp|less|nand|nor|xor)")) {
return true;
} else {return false;}
}
另外，其中还用到了Operation类，这个类中定义了各类操作的权重，在处理的时候优先级高的操作符会被先处理，比如从下面的代码中可以看到，非操作的优先级是最高的，还有几种操作的优先级是同等的。
public class Operation {
private static int NOTOP=10;//非
private static int ANDOP=9;//与
private static int NANDOP=9;//与非
private static int DIFFOP=9;//P∧非Q
private static int LESSOP=9;//非P∧Q
private static int OROP=8;//或
private static int NOROP=8;//或非
private static int IMPOP=7;//蕴含, ->
private static int INVIMPOP=7;//反蕴含, <-
private static int BIIMPOP=6;//同或, <-> ,相同就是1,不同就是0
private static int XOROP=6;//异或,相同就是0,不同就是1
public static int getValue(String operation){
int result;
switch (operation){
case "not":
result=NOTOP;
break;
case "and":
result=ANDOP;
break;
case "or":
result=OROP;
break;
case "diff":
result=DIFFOP;
break;
case "imp":
result=IMPOP;
break;
case "biimp":
result=BIIMPOP;
break;
case "invimp":
result=INVIMPOP;
break;
case "less":
result=LESSOP;
break;
case "nand":
result=NANDOP;
break;
case "nor":
result=NOROP;
break;
case "xor":
result=XOROP;
break;
default:
System.out.println("不存在该运算符");
result=0;
}
return result;
}
}
接下来是最关键的对逆波兰表达式求值的部分。但在求值之前还需要处理一下，因为有可能输入的布尔表达式中含有重复的布尔变量。看似这并不是个问题，因为算数表达式可能也会出现很多重复的数字，也没关系，逐一计算就好了，但是在这种情况下我们是将每个数字都看成是独立的、和别的数字是无关的。然而当涉及到布尔函数的时候这样就行不通了，因为对于一个布尔变量来说，它可能并不是独立的，而是会重复出现和计算的，就比如在前面提到过的布尔函数result = (A or C)and(B or A)，其中 A 出现了两次，这说明这两个A的取值必须是一样的，而不能像算术表达式那样是独立的。因此这里需要建立一个 HashMap，存放着每个布尔变量和其对应的 BDD 变量，当布尔函数出现了这个布尔变量，就使用这个对应的 BDD 变量进行运算，这样就可以保证运算的一致性了。下面的handleRepeatedVar方法保证了这一点，同时也有统计变量个数的作用：
public static void handleRepeatedVar() {
for(String element:var_list){
Integer i = var_counter_map.get(element);
// 如果HashMap中没有对应的变量，则新建一项并将次数置1
if(i == null){ var_counter_map.put(element, 1);}
else{ var_counter_map.put(element, i+1);}}// 如果有，则将次数加一
}
接下来是对逆波兰表达式进行求值的方法：
public static BDD getBddDotOutput(List<String> input) {
int size = input.size();
BDDFactory factory = BDDFactory.init(1024, 1024);
factory.setVarNum(size);
Stack<BDD> bddStack = new Stack<>();// 存放BDD变量的栈
//将各个变量的BDD都提前生成好，存放在fixedBDDList中
int tempCounter = 0;
for (String a : var_counter_map.()) {
BDD tempBDD = factory.ithVar(tempCounter);
fixedBDDList.put(a, tempBDD);
tempCounter++;}
// j的作用是从前往后初始化变量BDD
int j = 0;
for (int i = 0; i < input.size(); i++) {
String element = input.get(i);
// 如果是变量，就从fixedBDDList取出事先生成好的BDD并压栈
if (!isBooleanSymbol(element)) {
bddStack.push(fixedBDDList.get(element));}
else {// 如果是运算符，则将两个元素出栈再运算，注意它们的顺序
BDD b = bddStack.pop();
BDD a = bddStack.pop();
BDD result = factory.ithVar(j);
j++;
if (element.equals("not")) {
result = b.not();
} else if (element.equals("and")) {
result = a.apply(b, BDDFactory.and);
} else if (element.equals("or")) {
result = a.apply(b, BDDFactory.or);
} else if (element.equals("diff")) {
result = a.apply(b, BDDFactory.diff);
} else if (element.equals("imp")) {
result = a.apply(b, BDDFactory.imp);
} else if (element.equals("biimp")) {
result = a.apply(b, BDDFactory.biimp);
} else if (element.equals("invimp")) {
result = a.apply(b, BDDFactory.invimp);
} else if (element.equals("less")) {
result = a.apply(b, BDDFactory.less);
} else if (element.equals("nand")) {
result = a.apply(b, BDDFactory.nand);
} else if (element.equals("nor")) {
result = a.apply(b, BDDFactory.nor);
} else if (element.equals("xor")) {
result = a.apply(b, BDDFactory.xor);}
bddStack.push(result);}}// 将结果BDD压栈，直到遍历结束
return bddStack.pop();
}
这基本就是布尔函数运算的整个过程了。实际上仔细观察会发现，其中有一个很重要的细节值得注意，这就是关于布尔运算符 not（也就是逻辑非）的处理。这个运算符特殊的地方在于它是一元运算符，而算术表达式中的符号和别的布尔运算符都是二元运算符。这意味着需要单独处理遇到 not 的情况，但是这样又会更加程序的复杂度，可能会带来一些额外的麻烦。
更好的方式是把它转化成二元运算符，然后就可以和别的运算符一样地处理了。具体的实现方式是，在对输入的布尔函数字符串进行预处理时，如果遇到了 not，就先在结果的字符串列表中插入一个特殊的字符（比如*），当计算逆波兰表达式时，如果遇到 not，也还是让两个元素出栈，但是只处理其中第一个元素，因为第二个元素就是那个用来占位的特殊字符，只需要简单地让其出栈，不做其他处理即可。这一点也可以从代码中处理 not 情况的逻辑看到。
以上算法返回的是一个 BDD 对象，实际上它就是所求的布尔表达式转化成图的形式。借助在前文中介绍过的printSet方法，就可以由该对象得到一些初步的输出了，之前作为例子的表达式A or B or C的输出是<0:0, 1:0, 2:1><0:0, 1:1><0:1>，另外一个较复杂的布尔表达式(A or C)and ((B or not A) and (D or C))，得到的输出为<1:0, 3:1><1:1, 2:1, 3:0, 4:1><1:1, 2:1, 3:1>，这表示在三种情况下该表达式为真：一是 A 为假，C 为真；二是 A、B 和 D 为真，C 为假；三是 A、B 和 C 为真，D 的取值不影响。经过验证发现，这是完全正确的。
所以，当得到了布尔函数对应的 BDD 变量后，我们就可以知道它在什么情况下取值为真了。对BDD对象调用printSet方法，获取其用尖括号隔开的输出，然后进行二次处理，拆分成若干种情况，并将每种情况中的数字序号替换成布尔变量的名字，最后输出即可。另外也可以给定布尔变量的值，快速得到布尔函数的结果。求的方式也不难，如果某变量为 0，则对 BDD 调用low()方法得到 0-分支对应的子 BDD，反之如果为 1 则调用high()方法得到 1-分支对应的子 BDD。
2. 基于语义树的CTL公式解析
CTL 也就是计算树逻辑，关于这个东西是啥，如果不知道请自行百度。。。下面的 2.2 节也有讲。
为什么要讲这个？因为对于一个状态机系统，如果要检验这个系统的工作方式是否符合要求，就可以用 CTL 公式来描述一种状态转换过程。比如说电梯的开关门和上下楼，微波炉的开关门和加热食物，都是一个状态机的转换的过程，见下图。为了检查电梯在上下楼途中不会开门，微波炉开门时不能加热食物，就需要看这个状态机是否符合一些 CTL 描述。
微波炉的状态转换图
2.1 SemanticTree语义树结构
在解析 CTL 公式时，之所以要使用 SemanticTree，是为了在之后的模型检验过程中更好地计算出满足条件的状态。刚开始时笔者也考虑过使用逆波兰表达式的方式来完成 CTL 公式的计算，后来还是选择了更优的树的方式，一是因为逆波兰表达式的操作元素都是原子变量，而CTL公式中可能会出现复合变量，这正是树结构所擅长解决的。而且 CTL 公式的多数操作符都是一元运算符而非二元运算符，增加了直接计算的难度。下面给出 SemanticTree 类的定义：
public class SemanticTree {
String nodeValue;
//如果是AU之类的双操作数符号，则为2；
//如果是AX、非之类的单操作符号，则为1，如果是纯变量，则为0
int childNum;
SemanticTree leftChild;
SemanticTree rightChild;
//默认有左右两个子树，当成二叉树处理。
//若为单操作符，则右子树为空，只看左节点
public SemanticTree(String input){ nodeValue = input; }
public SemanticTree() {}
}
可以看到，该类的定义和二叉树的定义很类似，都是使用了一种递归定义的方式。每个 SemanticTree 变量都包含着两个 SemanticTree 类型的变量代表左右子树，同时还有一个 String 类型的变量存放着节点的内容，可以是操作符或者布尔变量。最后还有一个 int 类型的变量 childNum 代表着该节点的有效子树个数。当某个节点是 and、or 之类的二元操作符时，左子树和右子树分别代表着它的两个操作数，childNum 的值为 2；当该节点是 not 这样的一元操作数时，左子树存放着唯一的操作数，右子树为空，childNum 为 1；当该节点是布尔变量时，往往都意味着这个节点是叶子结点，它的左右子树都为空，childNum 的值也为 0。
2.2 CTL公式解析算法设计与实现
接下来给出将 String 类型的 CTL 公式转为 SemanticTree 类型的方法。该方法的思路主要是通过正则表达式匹配和递归来完成的，正则表达式可以作为 If 语句的条件快速判定操作符的类型；递归则能够简洁而优雅地将一长串复杂的CTL公式迭代处理。
CTL公式中需要处理的描述符一共有八种（AX、EX、AF、EF、AG、EG、AU和EU），描述符由路径量词和时态逻辑运算符构成，前者包含 A 和 E，A 的意思是“对于所有的状态路径”，E 的意思是“对于至少一条状态路径”。注意它们并不是对立的，E 至少包含一条路径，至多包含所有路径。后者包含 X、F、G 和 U，X 的意思是“下一个状态”，F 的意思是“将来某个状态”，G 的意思是“之后的所有状态”，U 的意思是“直到某个状态”。将路径量词和时态逻辑运算符组合，就能表示很多逻辑描述了。在解析为 SemanticTree 的过程中，并不需要对这些描述符进行逻辑操作，而是依据它们的子树个数来决定下一步的操作，因此下面的代码中不会给出完整的代码，而是仅列出不同子树个数的情况。
CTL 语义示例
public static SemanticTree CTL_formula_parser(String input) {
SemanticTree result = new SemanticTree();
if (Pattern.matches("A\\[.*", input)) { //二元操作符的情况
result.nodeValue = "AU";
result.childNum = 2;
String[] substrings = AU_or_EU_get_two_substring(input.substring(2));
result.leftChild = CTL_formula_parser(substrings[0]);
result.rightChild = CTL_formula_parser(substrings[1]);
return result;}
... ... // EU、→、∨和∧的情况和上面类似，只是在求子字符串时不同
else if (Pattern.matches("AX.*", input)) { //一元操作符的情况
result.nodeValue = "AX";
result.childNum = 1;
result.leftChild = CTL_formula_parser(input.substring(2));
return result;}
... ... // EX、AF、EF、AG、EG和¬的情况和上面类似
else if (Pattern.matches("\\(.*", input)) {
return CTL_formula_parser(get_string_between_brackets(input));}
else if (Pattern.matches("⊤|⊥|\\w*", input)) { //非操作符的情况
result.nodeValue = input;
result.childNum = 0;
return result;}
return null;
}
算法的流程图如下所示：
算法流程图
其中有几点需要说明，一是在对一元操作符进行处理时，默认只是给左子树赋值，对右子树不进行操作，从而得到图2-3中那种只有一个子节点的效果。二是在遇到左括号时，说明遇到了复合的布尔变量，此时调用了get_string_between_brackets方法，得到括号之间的CTL子公式再将其变成一段 SemanticTree。该方法实现比较简单，需要维护一个括号计数器，因为一对括号之间可能还会出现若干对括号。当找到与左括号匹配的右括号时，即返回两括号之间的子字符串。
最后需要注意非操作符可能有三种情况，就是永真、永假和布尔变量。它们自己本身表示的就是某些状态而非逻辑描述符，因此它们是没有子树的，对其左右子树都不处理。
通过该算法，就可以将复杂的 CTL 公式转化成 SemanticTree 语义树的形式，再使用类似的递归函数，结合前文提到的 Graphviz 的 API 就可以输出 svg 格式的图像。比如，当将字符串E[AF(pvq)UE[AX¬rU¬s]]作为输入，将得到的 svg 输出在浏览器中打开，即能看到下图所示的结果。
CTL 公式解析的例子
3. 模型检验
在将 CTL 公式转换成了抽象的语义树结构后，就到了最核心的一部分，即借助 JavaBDD 库来求取模型检验算法。
什么是模型检验？还是以第 2 节中的微波炉举例子，给出微波炉的各种状态以及它们之间的转换（迁移）情况，来检验这个状态机系统是否符合 CTL 公式的描述。
这部分有三点最为关键，一是用 BDD 表示状态集和迁移关系，二是求出某个状态的前驱状态，三是编写求取满足条件的状态的方法。第一点的具体实现在前文已经介绍了，主要难在思维的转换上，使用BDD解决状态相关问题是一个新的视角，需要对 BDD 有较深刻的理解；第二点则是一个基础算法，在模型检验算法中处理大部分 CTL 公式都需要用到该算法；第三点则是通过最小集和三个核心求取状态集的算法 EX、EU 和 EG 完成整体的算法。下面分别对后两点进行介绍。
3.1 前驱状态的求取
在求解系统中有哪些状态满足CTL公式的过程中，大多数情况都是需要先求出满足某布尔变量的状态集合，然后由这些状态一步步推出最终的结果状态集。在这个过程中，很重要的一个步骤就是求解某个或某些状态的前驱状态。前驱状态更准确的定义是，能发生一次迁移为X的状态集合，其中X表示系统状态的子集。设X的前驱状态为pre∃(X)，则有如下的表达式：
pre∃(X) = {s∈S|∃s’,(s→s’且s’∈X)}
对于前驱状态的求取来说，一共存在三种情况，即一对一、一对多和多对一，如下图所示。第一种情况很简单，前面的状态就是后面状态的前驱状态；第二种情况下，对后面任意一个状态，前面的状态就是其前驱状态；第三种情况下，前面的所有状态都是后面状态的前驱状态。要注意的是，在实际应用中，是要对许多状态同时求它们的前驱状态的，这一并行问题可以由BDD通过状态集合的方式来更有效地解决。
前驱状态的三种情况
下面给出求前驱状态的具体算法。该方法接收一个用 BDD 形式表示的状态集合（编序为奇数，即1，3，5，...，表示迁移关系的终点），返回这些状态的前驱状态的 BDD 形式（编序为偶数，即0，2，4，...，表示迁移关系的起点）。
算法的整体思路是根据传入的 BDD 的情况进行不同的处理，如果 BDD 是永假，不包括任何状态，则返回永假；如果 BDD 与系统包含的布尔变量数目一致，则只需要调用restrict方法，将传入的 BDD 包含的状态约束为真，即能得到前驱状态的 BDD。这是因为对于迁移关系的路径来说，约束了迁移关系的终点（编序为奇数），那么剩下的就只有编序为偶数的节点，它们实际上就是迁移关系的起点。如果 BDD 的节点数目少于系统包含的布尔变量数目，这就说明 BDD 存在被约减的节点。此时不能再直接调用restrict方法，因为有可能造成遗漏的情况。这里采取了逐个判断的做法。
private static BDD get_pre_states(BDD input) {
int nodeCount = input.nodeCount();
if (nodeCount == 0) {
// 该情况下，传入的BDD为永假，对应的状态集合是⊥
return B.zero();}
else if (nodeCount == booleanVector.length) {
// 该情况下，传入的BDD包含的布尔变量数目与系统的布尔变量数目一致
// 这意味着所有到终点1节点的每条路径都只包含一种情况，没有约减节点
return TRANS_bdd.restrict(input);} // TRANS_bdd表示迁移关系的BDD
else {
// 该情况下，存在某条到达终点1节点的路径包含多种取值情况，
// 有节点被约减，如图3-4。这时采取一个特殊的策略：遍历所有的状态
// 看它是否有可能属于前驱状态
BDD result = B.zero();
// 遍历形参BDD的每一条到终点1的路径
for (Object object : input.allsat()) {
if (object instanceof byte[]) {
BDD anAssignment = fromByteListToBDD((byte[]) object);
for (int i = 0; i < state_bdds.length; i++) {
BDD temp = state_bdds[i].replace(adjustEvenOrder);
BDD restricted = TRANS_bdd.restrict(anAssignment).restrict(temp);
if (restricted.pathCount() > 0.0 || restricted.equals(B.one())) {
result = result.or(temp);}}}
else { System.err.println("allsat()转化成byte[]时出错！");}}
return result;}
}
其中有两点需要说明，一是allsat方法，该方法以List的形式返回一个 BDD 所有到达终点 1 节点的路径。经过查看源码，得知List中的元素类型是 byte 数组，数组中的元素个数为系统的布尔变量的个数，有三种取值：1，0 和 -1。1 对应着布尔变量取真，0 对应着布尔变量取假，-1 对应着路径上不包含该变量。二是fromByteListToBDD方法的作用是将一条到达终点1的路径转换成 BDD 的形式。程序中还出现了若干 restrict 方法，主要作用是调整 BDD 的编序以更方便地计算迁移状态的起点。
3.2 模型检验算法的设计与实现
有了之前的铺垫，现在实现具体的模型检验算法就不是那么难了。虽然 CTL 运算符有很多（本项目中能识别的有８种），但是我们并不需要对每个CTL运算符都进行处理，因为大部分 CTL 运算符可以转化成一小部分的CTL运算符，也就是说只需要实现CTL的最小集就可以了。
一个最小集包含的运算符有：⊤（永真），∨，¬，EG，EU 和 EX。下面是一些其他的运算符转化成最小集包含的运算符的公式：
- EFφ == E[⊤U(φ)]（因为Fφ == [⊤U(φ)]）
- AXφ == ¬EX(¬φ)
- AGφ == ¬EF(¬φ) == ¬ E[⊤U(¬φ)]
- AFφ == A[⊤Uφ] == ¬EG(¬φ)
- A[φUψ] == ¬(E[(¬ψ)U¬(φ∨ψ)]∨EG(¬ψ))
接下来讨论这样一个算法，接收 CTL 系统模型的输入和 CTL 公式，输出满足该公式的状态集合。整体思路是，首先将 CTL 公式转化成 SemanticTree 语义树形式的变量，然后将公式中的运算符都转化成最小集中的运算符，接着先求出满足 CTL 一些子公式的状态，再逐步扩展到整个 CTL 公式。在此之前，需要说明如何通过最小集中的运算符得到满足它们的状态。考虑以下几种情况：
- 若公式为 ⊤，则返回系统的状态集 S 对应的 BDD，表示所有状态都满足；
- 若公式为某个特定的布尔变量 ψ，则返回所有满足 ψ 的状态集合的 BDD；
- 若公式为 ψ１∨ψ２，则先分别求出 ψ１和 ψ２ 对应的 BDD，再调用 or 方法求状态集的并集。
同理若公式为 ψ１∧ψ２，则对两个 BDD 调用 and 方法求交集。 - 若公式为 EXψ，则先求出满足 ψ 的状态集合的 BDD，然后对它们调用求前驱状态的算法，即可得到存在一个后继状态满足 ψ 的状态集合，如下图；
求取满足 EX 公式的状态
- 若公式为 E[ψ１Uψ２]，则先求出满足 ψ２ 的状态集合 A，再观察满足 ψ1 的所以状态，看其是否存在后继状态属于 A，若是则将其加入 A。重复这种操作直到没有新的变化为止，A 对应的 BDD 就是最终的结果，如下图；
求取满足 EU 公式的状态
- 若公式为 EGψ，则首先假设所有的状态都满足，将系统状态集 S 作为初始值，接下来从中去除不满足布尔变量 ψ 的状态，然后再去掉某些状态，它们的后继状态集中不存在满足布尔变量 ψ 的状态。重复这种操作直到没有新的变化为止，最终的状态集合对应的 BDD 就是最终的结果，如下图。
求取满足 EG 公式的状态
下面给出求解满足EX、EU和EG的状态的算法，这是整个模型检验算法的核心部分，对CTL其他运算符的处理几乎都会转化为这三个算法。它们的输出是满足条件的状态集的BDD。上面的图6-2、图6-3和图6-4也可以作为算法的图解。
private static BDD SAT_EX(BDD input) {//传入的BDD相当于EXψ中ψ对应的状态集
BDD X = input;
// 调整编序，比如说如果X的BDD有3个节点，调整为[1,3,5]
// 注意这里先变成了奇数编序，最后又调整回来，是为了方便求前驱状态集
// 奇数编序在迁移关系中意味着终点节点，迁移关系调用restrict方法后
// 剩下的节点编序为偶数，对应着起点节点。EU和EG两个算法同理
X = X.replace(adjustOddOrder);
BDD result = get_pre_states(X);
return result.replace(adjustEvenOrderBack);// 把编序调整成初始的[0,1,2]
}
private static BDD SAT_EU(BDD input1, BDD input2) {
// 传入的两个BDD相当于E[ψ１Uψ２]中满足ψ１和ψ２的状态集
BDD W, X, Y;
W = input1;
X = S_bdd.id();// 复制一份，免得产生的修改影响了代表S的BDD
Y = input2;
if (X.equals(Y)) { return Y;}
while (!X.equals(Y.replace(adjustOddOrder))) {
// 调整编序，比如说如果X的BDD有3个节点，调整为[1,3,5]
X = Y.replace(adjustOddOrder);
BDD pre_states = get_pre_states(X);//此时pre_states的编序为0,2,4,...
Y = bdd_OR(Y, bdd_AND(W, pre_states.replace(adjustEvenOrderBack)));}
return Y;
}
private static BDD SAT_EG(BDD input) {
BDD X, Y;
Y = input;
X = B.zero();
if (X.equals(Y)) { return Y; }
while (!(X.equals(Y.replace(adjustOddOrder)))) {
// 调整编序，比如说如果X的BDD有3个节点，调整为[1,3,5]
X = Y.replace(adjustOddOrder);
BDD pre_states = get_pre_states(X);//此时pre_states的编序为0,2,4,...
Y = bdd_AND(Y, pre_states.replace(adjustEvenOrderBack));}
return Y;
}
需要说明的是，算法中会用到三个辅助方法，分别是bdd_OR、bdd_AND和bdd_SUB。前面两个其实就是调用or和and方法，第三个是求两个BDD的差集的，原理是将求差集转化成了求交集。如bdd1 - bdd2 = bdd1.and(bdd2.not())。
有了这三个算法，就能实现求满足CTL公式的状态集了。下面的算法接收一个SemanticTree类型的参数，通过递归调用求解，将其他类型的CTL描述符都转化成了EX、EU和EG这三种形式再求解，最终返回满足该语义树的状态集对应的BDD。其中S_bdd表示系统的状态集对应的BDD。
public static BDD getSatStates(SemanticTree sTree) {
// sTree可能有三种情况：1.左右子树都存在；2.左子树存在；3.不存在子树
SemanticTree left = sTree.leftChild;
SemanticTree right = sTree.rightChild;
if (sTree.childNum == 2) {
if (sTree.nodeValue.equals("AU")) {
// A[φ1Uφ2] == ¬(E[(¬φ2)U¬(φ1∨φ2)]∨EG(¬φ2))
return bdd_SUB(S_bdd,bdd_OR(SAT_EU(bdd_SUB(S_bdd,getSatStates(right)),bdd_AND(
bdd_SUB(S_bdd,getSatStates(left)),bdd_SUB(S_bdd,getSatStates(right)))),
SAT_EG(bdd_SUB(S_bdd,getSatStates(right)))));}
else if (sTree.nodeValue.equals("EU")) {
return SAT_EU(getSatStates(left),getSatStates(right));}
else if (sTree.nodeValue.equals("→")) {
// φ1→φ2 == ¬φ1∨φ2
return bdd_OR(bdd_SUB(S_bdd, getSatStates(left)), getSatStates(right));}
else if (sTree.nodeValue.equals("∨")) {
return bdd_OR(getSatStates(left),getSatStates(right));}
else if (sTree.nodeValue.equals("∧")) {
return bdd_AND(getSatStates(left),getSatStates(right));}}
else if (sTree.childNum == 1) {
if (sTree.nodeValue.equals("AX")) {
// AXφ == ¬EX¬φ
return bdd_SUB(S_bdd, SAT_EX(bdd_SUB(S_bdd,getSatStates(left))));}
else if (sTree.nodeValue.equals("EX")) {
return SAT_EX(getSatStates(left));}
else if (sTree.nodeValue.equals("AF")) {
// AFφ == ¬EG¬φ
return bdd_SUB(S_bdd, SAT_EG(bdd_SUB(S_bdd,getSatStates(left))));}
else if (sTree.nodeValue.equals("EF")) {
// EFφ == E(⊤Uφ)
return SAT_EU(S_bdd,getSatStates(left));}
else if (sTree.nodeValue.equals("AG")) {
// AGφ == ¬EF¬φ
return bdd_SUB(S_bdd,SAT_EU(S_bdd,bdd_SUB(S_bdd,getSatStates(left))));}
else if (sTree.nodeValue.equals("EG")) {
return SAT_EG(getSatStates(left));}
else if (sTree.nodeValue.equals("¬")) {
return getSatStates(left).not();}}
else {// 子树的数目为0
if (sTree.nodeValue.equals("⊤")) { return S_bdd;}
else if (sTree.nodeValue.equals("⊥")) { return S_bdd.not();}
else if (Pattern.matches("\\w*", sTree.nodeValue)) {
// get_atomic_bdd方法会遍历所有状态，找到满足该布尔变量的状态集
return get_atomic_bdd(sTree.nodeValue);}}
return S_bdd.not();
}
以上就是模型检验算法的主要部分。可以看到，当最开始输入一个 CTL 公式字符串时，首先会通过递归函数将其解析成 SemanticTree 语义树类型，接下来会再次调用递归函数，从语义树的叶子节点开始，逐步向上推出符合 CTL 公式的状态集合。在求解过程中，主要会使用 EX、EU 和 EG 三种算法，而在这三种算法中又会用到求解前驱状态的算法。最后，遍历所有的状态对应的 BDD，对getSatStates返回的 BDD 调用restrict方法约束这些状态对应的 BDD，并判断结果是否为永真，即可达到判断状态是否满足 CTL 公式的目的。
那么总结一下模型检验的流程，如下图所示：
模型检验算法流程图
4. 实例应用——微波炉操作模型
又见到了微波炉~~作为一个经典的例子，该操作模型描述了微波炉运行过程中的状态转换关系。
再贴一遍之前的图：
微波炉的状态转换图
图中每个圆圈代表一种微波炉的状态，操作模型一共包括四个布尔变量，分别表示电源是否开启、箱门是否关闭、是否正在加热，以及是否出错。比如在第一个圆圈表示的状态中，四种布尔变量都是不被满足的，对应的就是微波炉没通电、箱门开着、未加热和未出错的状态。微波炉的状态通过不同的动作实现转换。
首先需要模型进行抽象化。将七个状态用 s0-s6 来表示，四个布尔变量分别用 a、b、c、d来表示。每个状态中只保留其满足的布尔变量，不满足的就不显示。比如在第一个状态中，四个条件都是不满足的，因此抽象后 s0 不含任何布尔变量。而处于烹饪中状态的微波炉满足箱门关闭和正在加热的条件，因此抽象后对应的 s3 满足 b 和 c 两个布尔变量。最终抽象后的微波炉模型如下图：
抽象后的对比
此时，微波炉模型的状态和迁移关系就可以转化成布尔函数的形式，如s1 = a∧¬b∧¬c∧d，s1—>s4 = a∧¬b∧¬c∧d∧a’∧b’∧¬c’∧d。对应到 JavaBDD 中，状态的表示需要对 BDDFactory 调用setVarNum方法，传入的参数为 4，从而生成四个BDD 变量，则 s1 对应的 BDD 表达式就是a.and(b.not).and(c.not).and(d)，其中a = BDDFactory.ithVar(0)，表示 a 是 BDDFactory 的第 0 个变量。b、c 和 d 同理，对应的序号分别为 1、2 和 3。其他的状态也可以被这样表示。最终得到的 BDD 状态集的 DOT 输出对应的图像如下：
微波炉状态集的表示
s1 到 s4 的迁移关系的表示则需要对 BDDFactory 调用extDomain方法，传入一个包含两个元素的 int 数组，每个元素的大小都是 24。该方法会返回一个包含两个元素的 BDDDomain 数组，使用第一个 BDDDomain 包含的 BDD 表示迁移关系的起点（BDD 的序号为 0，2，4 和 6），第二个包含的 BDD 表示迁移关系的终点（BDD 的序号为 1，3，5 和 7）。最后将所有的迁移关系取并集（或者说对所有迁移关系对应的 BDD 调用 or 方法），即可得到下图所示的总迁移关系。
微波炉迁移关系的表示，状态多就是这样，不要被吓到哈
虽然上面给出了状态集和迁移关系的 BDD，但是实际上在模型检验的过程中用户是接触不到的，它相当于一个黑盒，遮盖了复杂的原理和计算过程，最终给出一个简洁的结果。这也让本系统的易用性得到了提升。
接下来对微波炉模型进行模型检验。比如要验证这样一个属性：当微波炉的箱门没有关上时，微波炉无法进行加热操作。首先需要把这样一个描述转化成CTL公式，方便计算机理解。这里需要用到 AU 描述符。之前说过，A[pUq]表示在从当前状态出发的每一条计算路径上，都存在一个状态使得 q 成立，并且对这些路径上的所有以前状态 p 成立。因此，我们需要验证A[¬c U b]这个公式对于上面抽象出来的 CTL 模型是不是成立的。
构造一个 CTL 描述
可能有同学会有疑问，这个微波炉的模型是怎么输入的。为了方便操作，我用 SpringBoot 写了个简单的网页，输入布尔变量、状态变量和迁移关系，以及要检验的 CTL 公式，就相当于是输入了模型了。界面如下图所示：
通过网页操作，请忽略要输入的超多参数...
接下来点击生成结果的按钮开始模型检验部分的计算，在1-2s内即可得到系统生成的结果。结果包含三部分，一是满足CTL公式的状态集，二是根据输入生成的模型示意图，如下图 1 所示。三是对 CTL 公式解析得到的语法树，如下图 2 所示。模型检验计算得到的结果是 [s0, s1, s2, s3, s4, s5, s6]，说明所有七个状态都满足这个 CTL 公式，这从第一个图中可以验证，也意味着微波炉模型是满足这个性质的。除此之外，还可以对模型示意图和 CTL 公式的语法树图像进行缩放、移动、tooltip 提示以及突出显示路径的操作，便于进一步的观察。
系统生成的模型示意图
系统生成的 CTL 语义树
总结一下步骤就是，首先根据输入，生成系统模型示意图和待验证的 CTL 公式的语义树，随后将状态集和迁移关系转化成 BDD 进行后续的验证和计算。这样就以一种可视化的形式表现了状态机运行和迁移的逻辑、CTL公式的结构以及布尔函数运算的结果。
当然，由于个人的时间精力等原因，本系统仍有可提升的空间，具体有两个方面。一是在用 BDD 表示状态集和迁移关系时，通过选择性地整合未使用的布尔矢量可以进一步简化最终的 BDD 表示，关键在于如何选择合适的布尔矢量用于化简。二是在设计实现求取前驱状态集的算法的过程中，当路径中存在被化简的状态节点时，采取的遍历策略效率不是很高，所以此处的策略还有进一步优化的可能。这些问题就留给后来研究Java BDD的同学们解决吧（如果有人的话）... ...
Last Words
这篇文章到这里就结束了✨文中介绍的几种应用，对大多数人来说，可能计算布尔表达式的部分比较有参考价值，另外两种比较小众，只有了解数理逻辑、状态机转换等领域的同学才用得上。
对于使用JavaBDD的同学，现在应该有更多的选择了。我之前在 GitHub 上找到了一个项目列表，用各种语言实现了BDD，感兴趣的可以看看：johnyf/tool_lists
而且，如果要检验一个状态机系统的转换逻辑是否有漏洞，现在应该也有很多方式了，比如用 Petri 网描述，然后用模拟软件去验证，还有很多别的方式。此处不禁感叹一句，大人，时代变了！😭
最后，本文所描述的这些，更多地是将几种工具结合，进行状态机转换的理论性探索。如有错误和纰漏，请多多指出，还望海涵。最后的最后，感谢你能读到这里！😜
网友评论