這是一個(gè)鴿了很久的系列弦蹂，本來(lái)是要記錄完成本科畢設(shè)《狀態(tài)機(jī)自動(dòng)生成與圖形化仿真系統(tǒng)研究與實(shí)現(xiàn)》的過(guò)程，因?yàn)槭褂玫腏avaBDD算是一個(gè)很老的包了强窖，文檔很少凸椿，而且這個(gè)領(lǐng)域的資料也很少，所以想著整理一下翅溺，方便后來(lái)人使用脑漫。但寫了前三篇《開(kāi)端》、《探索 Graphviz》和《探索 JavaBDD》之后咙崎，因?yàn)楦鞣N事情擱置了窿撬。
時(shí)光飛逝，到現(xiàn)在已經(jīng)過(guò)了一年半的時(shí)間叙凡，從當(dāng)時(shí)的本科畢設(shè)劈伴，到現(xiàn)在都開(kāi)始做研究生畢設(shè)了??本來(lái)是打算棄坑的，因?yàn)橛X(jué)得它的價(jià)值隨著時(shí)代變化已經(jīng)越來(lái)越少了握爷，但仍然偶爾能看到有朋友私信問(wèn)我相關(guān)的問(wèn)題跛璧。我意識(shí)到，雖然關(guān)注這個(gè)領(lǐng)域的人并不多新啼，但可能一直都會(huì)有人懷著相同的疑問(wèn)而無(wú)處尋得解答追城。因此，我決定用這一篇作為畢設(shè)記錄的完結(jié)燥撞。

這里假設(shè)讀者對(duì)JavaBDD座柱、Graphviz已經(jīng)有基本的了解，也已經(jīng)看過(guò)前文了物舒。本篇文章繼續(xù)講解JavaBDD的應(yīng)用色洞，布爾表達(dá)式的運(yùn)算、CTL公式解析和模型檢驗(yàn)冠胯。當(dāng)然火诸，還有不少其他的應(yīng)用，但這里主要關(guān)注這三個(gè)荠察。

1. 布爾表達(dá)式的運(yùn)算

與其說(shuō)是運(yùn)算置蜀，不如說(shuō)是讓布爾表達(dá)式為真時(shí)，取值的情況悉盆。比如布爾表達(dá)式：A or B or C盯荤，計(jì)算的輸出是<0:0, 1:0, 2:1><0:0, 1:1><0:1>，這里冒號(hào)前的 0焕盟、1 和 2 分別對(duì)應(yīng)著 A秋秤、B 和 C，冒號(hào)后的 0 和 1 代表著真和假，每對(duì)尖括號(hào)意味著一種取值情況航缀。因此商架，輸出的意思是有三種情況使該布爾表達(dá)式成立：一是 A 和 B 為假，C 為真芥玉；二是 A 為假蛇摸，B 為真，C真或假都可以灿巧；三是 A 為真赶袄，B 和 C 為真或假都可以。

如果不使用JavaBDD抠藕，怎么得到結(jié)果饿肺？可能有人說(shuō)我肉眼看就能看出來(lái)。這樣的話稍微復(fù)雜點(diǎn)盾似，眼就要看花敬辣，比如(A or C)and ((B or not A) and (D or C))，估計(jì)得看幾分鐘才能得到結(jié)果零院。還有人說(shuō)我讓每個(gè)值取 0 和 1 兩種情況溉跃，遍歷所有結(jié)果。這比第一種方法好告抄，但這樣的復(fù)雜度是 O(2^n)撰茎，太慢了，而且輸出也比較復(fù)雜打洼。

以布爾函數(shù)result = (A or C)and(B or A)為例龄糊，它包含 A、B 和 C 三個(gè)布爾變量輸入募疮，result 一個(gè)布爾變量輸出炫惩。當(dāng)使用電路驗(yàn)證模塊處理這個(gè)例子時(shí)，會(huì)得到下表中的結(jié)果：

但是當(dāng)使用布爾運(yùn)算模塊處理時(shí)酝锅，就會(huì)得到下圖的結(jié)果了诡必。仔細(xì)觀察，會(huì)發(fā)現(xiàn)它們并不沖突搔扁，圖中描述的情況與表中相吻合。前者將 result 和布爾變量輸入的取值變化詳細(xì)地展現(xiàn)出來(lái)了蟋字，而后者則以一種更簡(jiǎn)潔的情況描述了 result 取真值的情況稿蹲，且情況 2 只需要 A 為真即可，對(duì)其他的變量取值沒(méi)有要求鹊奖。通過(guò)檢查布爾函數(shù)可知苛聘，這也是符合邏輯的。

布爾運(yùn)算模塊的輸出

1.1 逆波蘭表達(dá)式

接下來(lái)說(shuō)明對(duì)于布爾函數(shù)的運(yùn)算是如何實(shí)現(xiàn)的。首先需要明確的是设哗，其本質(zhì)還是需要將結(jié)果布爾變量轉(zhuǎn)化成BDD變量唱捣，然后通過(guò)JavaBDD來(lái)求取結(jié)果。但是网梢，由于輸入的布爾表達(dá)式可能會(huì)很復(fù)雜震缭，比如包含一些空格和括號(hào)，無(wú)法被很容易地轉(zhuǎn)化前文中的JavaBDD的形式战虏。因此拣宰，首先需要考慮如何對(duì)原始的布爾函數(shù)進(jìn)行處理，使其變成計(jì)算機(jī)能夠理解的形式烦感。

在這一點(diǎn)上巡社，我從算術(shù)表達(dá)式求解的過(guò)程中得到了啟發(fā)。日常生活中出現(xiàn)的算術(shù)表達(dá)式手趣，如1+2-3*4/5晌该，屬于中序表達(dá)式的范疇，其中的運(yùn)算符是在第一個(gè)和第二個(gè)操作數(shù)中間的绿渣。有一種求解它的思路是朝群，先將其轉(zhuǎn)化為逆波蘭表達(dá)式（也稱為后序表達(dá)式），然后再進(jìn)行求解怯晕。

例如中序表達(dá)式(a+b)*c轉(zhuǎn)化成逆波蘭表達(dá)式后就是ab+c*潜圃，轉(zhuǎn)化過(guò)程需要兩個(gè)棧分別存放著變量和運(yùn)算符，從左往右讀入中序表達(dá)式舟茶，并將元素壓入對(duì)應(yīng)的棧谭期。但運(yùn)算符棧頂元素的優(yōu)先級(jí)必須小于要壓棧的運(yùn)算符的優(yōu)先級(jí)，否則在壓棧前需要將運(yùn)算符出棧并壓入變量棧吧凉，直到滿足要求隧出。（需要注意的是，括號(hào)需要壓入運(yùn)算符棧阀捅，當(dāng)遇到右括號(hào)時(shí)胀瞪，重復(fù)將運(yùn)算符棧的元素出棧并壓入變量棧，直到遇到左括號(hào)饲鄙，此時(shí)將左括號(hào)出棧即可凄诞。）當(dāng)結(jié)束讀入表達(dá)式時(shí)，再將運(yùn)算符棧的元素依次出棧并壓入變量棧忍级。最終變量棧從棧底到棧頂?shù)膬?nèi)容即為逆波蘭表達(dá)式帆谍。

可能你讀完上面這段話已經(jīng)暈了，那么就看下面的動(dòng)圖吧??

逆波蘭表達(dá)式的轉(zhuǎn)換

逆波蘭表達(dá)式求值的步驟也很簡(jiǎn)單轴咱。準(zhǔn)備一個(gè)空棧汛蝙，從左至右讀入表達(dá)式，遇到變量則壓棧坚洽，遇到運(yùn)算符則依次從棧中彈出兩個(gè)變量讶舰，運(yùn)算后繼續(xù)入棧绘雁，直到最后棧中只剩下唯一的值援所，即為表達(dá)式的結(jié)果庐舟。 這部分實(shí)現(xiàn)的代碼在網(wǎng)上有很多了。

像這樣對(duì)表達(dá)式進(jìn)行處理住拭，算法的實(shí)現(xiàn)并不難挪略，而且還能取出括號(hào)，更易于計(jì)算機(jī)理解滔岳。那么布爾表達(dá)式是否也能像這樣被處理呢杠娱？答案是肯定的。每個(gè)布爾變量就像是算術(shù)表達(dá)式中的一個(gè)數(shù)字谱煤，每個(gè)邏輯運(yùn)算符則像是加減乘除之類的運(yùn)算符摊求，使用JavaBDD對(duì)出棧的BDD變量進(jìn)行運(yùn)算，并將結(jié)果BDD變量壓棧刘离，就相當(dāng)于對(duì)表達(dá)式進(jìn)行計(jì)算的過(guò)程室叉。流程圖如下所示。

算法流程示意圖

1.2 布爾表達(dá)式求值算法的設(shè)計(jì)與實(shí)現(xiàn)

布爾函數(shù)求值的算法主要分為三部分：第一部分對(duì)輸入的字符串預(yù)處理硫惕，如去除多余的空格等茧痕，最終轉(zhuǎn)化成List<String>類型的中序表達(dá)式；第二部分是對(duì)中序表達(dá)式處理恼除，得到List<String>類型的逆波蘭表達(dá)式；第三部分則是由逆波蘭表達(dá)式得到布爾函數(shù)對(duì)應(yīng)的 BDD 變量。第二部分的處理算法如下所示：

public static List<String> toReversePolishExpression
(List<String> middleOrderExpression) {
    Stack<String> symbolStack = new Stack<>(); // 存放符號(hào)的棧
// 使用List來(lái)作為存放變量和符號(hào)的棧，更加靈活
    List<String> num_sym_list = new ArrayList<>();
    for (String element : middleOrderExpression) {
        if (element.equals("(")) { symbolStack.push(element); }// 若為左括號(hào)則入棧
        else if (element.equals(")")) {
           while (!symbolStack.peek().equals("(")) {
            num_sym_list.add(symbolStack.pop());}
            symbolStack.pop();}// 將符號(hào)出棧直到棧頂是左括號(hào)堵幽，也將其出棧
        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是專門存放變量的，之后會(huì)對(duì)變量出現(xiàn)的次數(shù)進(jìn)行統(tǒng)計(jì)        
            var_list.add(element);}}
    // 處理完中序表達(dá)式后，若符號(hào)棧還有元素則將其插入變量棧
    while (symbolStack.size() != 0) { num_sym_list.add(symbolStack.pop());}
    return num_sym_list;
}

其中用到了isBooleanSymbol方法团滥，該方法的作用是判斷 String 類型的變量是否屬于布爾運(yùn)算符之一秉溉，使用正則表達(dá)式進(jìn)行判斷父晶。具體代碼如下：

public static Boolean isBooleanSymbol(String input) {
   // 正則表達(dá)式的意思是匹配11種運(yùn)算符號(hào)
   if (input.matches("(?:and|or|not|diff|imp|biimp|invimp|less|nand|nor|xor)")) {
      return true;
   } else {return false;}
}

另外铛只，其中還用到了Operation類，這個(gè)類中定義了各類操作的權(quán)重谊惭，在處理的時(shí)候優(yōu)先級(jí)高的操作符會(huì)被先處理悄雅，比如從下面的代碼中可以看到握牧，非操作的優(yōu)先級(jí)是最高的，還有幾種操作的優(yōu)先級(jí)是同等的。

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;//蘊(yùn)含, ->
    private static int INVIMPOP=7;//反蘊(yùn)含, <-
    
    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("不存在該運(yùn)算符");
                result=0;
        }
        return result;
    }
}

接下來(lái)是最關(guān)鍵的對(duì)逆波蘭表達(dá)式求值的部分芦缰。但在求值之前還需要處理一下包斑，因?yàn)橛锌赡茌斎氲牟紶柋磉_(dá)式中含有重復(fù)的布爾變量再姑∩芴睿看似這并不是個(gè)問(wèn)題，因?yàn)樗銛?shù)表達(dá)式可能也會(huì)出現(xiàn)很多重復(fù)的數(shù)字，也沒(méi)關(guān)系，逐一計(jì)算就好了旋恼，但是在這種情況下我們是將每個(gè)數(shù)字都看成是獨(dú)立的冬殃、和別的數(shù)字是無(wú)關(guān)的奕谭。然而當(dāng)涉及到布爾函數(shù)的時(shí)候這樣就行不通了，因?yàn)閷?duì)于一個(gè)布爾變量來(lái)說(shuō)，它可能并不是獨(dú)立的，而是會(huì)重復(fù)出現(xiàn)和計(jì)算的介返，就比如在前面提到過(guò)的布爾函數(shù)result = (A or C)and(B or A)徘公，其中 A 出現(xiàn)了兩次哮针，這說(shuō)明這兩個(gè)A的取值必須是一樣的关面，而不能像算術(shù)表達(dá)式那樣是獨(dú)立的。因此這里需要建立一個(gè) HashMap诚撵，存放著每個(gè)布爾變量和其對(duì)應(yīng)的 BDD 變量缭裆，當(dāng)布爾函數(shù)出現(xiàn)了這個(gè)布爾變量，就使用這個(gè)對(duì)應(yīng)的 BDD 變量進(jìn)行運(yùn)算澈驼，這樣就可以保證運(yùn)算的一致性了嘴高。下面的handleRepeatedVar方法保證了這一點(diǎn)绪氛，同時(shí)也有統(tǒng)計(jì)變量個(gè)數(shù)的作用：

public static void handleRepeatedVar() {
    for(String element:var_list){
        Integer i = var_counter_map.get(element);
// 如果HashMap中沒(méi)有對(duì)應(yīng)的變量嘿辟，則新建一項(xiàng)并將次數(shù)置1
    if(i == null){ var_counter_map.put(element, 1);}
    else{ var_counter_map.put(element, i+1);}}// 如果有，則將次數(shù)加一
}

接下來(lái)是對(duì)逆波蘭表達(dá)式進(jìn)行求值的方法：

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變量的棧
   //將各個(gè)變量的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 {// 如果是運(yùn)算符严就，則將兩個(gè)元素出棧再運(yùn)算孽文，注意它們的順序
    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);}}// 將結(jié)果BDD壓棧稚失，直到遍歷結(jié)束
   return bddStack.pop();
}

這基本就是布爾函數(shù)運(yùn)算的整個(gè)過(guò)程了篙螟。實(shí)際上仔細(xì)觀察會(huì)發(fā)現(xiàn)站故，其中有一個(gè)很重要的細(xì)節(jié)值得注意悦即，這就是關(guān)于布爾運(yùn)算符 not（也就是邏輯非）的處理吮成。這個(gè)運(yùn)算符特殊的地方在于它是一元運(yùn)算符，而算術(shù)表達(dá)式中的符號(hào)和別的布爾運(yùn)算符都是二元運(yùn)算符辜梳。這意味著需要單獨(dú)處理遇到 not 的情況赁豆，但是這樣又會(huì)更加程序的復(fù)雜度，可能會(huì)帶來(lái)一些額外的麻煩冗美。

更好的方式是把它轉(zhuǎn)化成二元運(yùn)算符，然后就可以和別的運(yùn)算符一樣地處理了析二。具體的實(shí)現(xiàn)方式是粉洼，在對(duì)輸入的布爾函數(shù)字符串進(jìn)行預(yù)處理時(shí)，如果遇到了 not叶摄，就先在結(jié)果的字符串列表中插入一個(gè)特殊的字符（比如*）属韧，當(dāng)計(jì)算逆波蘭表達(dá)式時(shí)，如果遇到 not蛤吓，也還是讓兩個(gè)元素出棧宵喂，但是只處理其中第一個(gè)元素，因?yàn)榈诙€(gè)元素就是那個(gè)用來(lái)占位的特殊字符会傲，只需要簡(jiǎn)單地讓其出棧锅棕，不做其他處理即可。這一點(diǎn)也可以從代碼中處理 not 情況的邏輯看到淌山。

以上算法返回的是一個(gè) BDD 對(duì)象裸燎，實(shí)際上它就是所求的布爾表達(dá)式轉(zhuǎn)化成圖的形式。借助在前文中介紹過(guò)的printSet方法泼疑，就可以由該對(duì)象得到一些初步的輸出了德绿，之前作為例子的表達(dá)式A or B or C的輸出是<0:0, 1:0, 2:1><0:0, 1:1><0:1>，另外一個(gè)較復(fù)雜的布爾表達(dá)式(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>移稳，這表示在三種情況下該表達(dá)式為真：一是 A 為假蕴纳，C 為真；二是 A个粱、B 和 D 為真古毛，C 為假；三是 A几蜻、B 和 C 為真喇潘，D 的取值不影響。經(jīng)過(guò)驗(yàn)證發(fā)現(xiàn)梭稚，這是完全正確的颖低。

所以，當(dāng)?shù)玫搅瞬紶柡瘮?shù)對(duì)應(yīng)的 BDD 變量后弧烤，我們就可以知道它在什么情況下取值為真了忱屑。對(duì)BDD對(duì)象調(diào)用printSet方法，獲取其用尖括號(hào)隔開(kāi)的輸出暇昂，然后進(jìn)行二次處理莺戒，拆分成若干種情況，并將每種情況中的數(shù)字序號(hào)替換成布爾變量的名字急波，最后輸出即可从铲。另外也可以給定布爾變量的值，快速得到布爾函數(shù)的結(jié)果澄暮。求的方式也不難名段，如果某變量為 0，則對(duì) BDD 調(diào)用low()方法得到 0-分支對(duì)應(yīng)的子 BDD泣懊，反之如果為 1 則調(diào)用high()方法得到 1-分支對(duì)應(yīng)的子 BDD伸辟。

2. 基于語(yǔ)義樹(shù)的CTL公式解析

CTL 也就是計(jì)算樹(shù)邏輯，關(guān)于這個(gè)東西是啥馍刮，如果不知道請(qǐng)自行百度信夫。。卡啰。下面的 2.2 節(jié)也有講静稻。

為什么要講這個(gè)？因?yàn)閷?duì)于一個(gè)狀態(tài)機(jī)系統(tǒng)碎乃，如果要檢驗(yàn)這個(gè)系統(tǒng)的工作方式是否符合要求姊扔，就可以用 CTL 公式來(lái)描述一種狀態(tài)轉(zhuǎn)換過(guò)程绑榴。比如說(shuō)電梯的開(kāi)關(guān)門和上下樓偏瓤，微波爐的開(kāi)關(guān)門和加熱食物坦刀，都是一個(gè)狀態(tài)機(jī)的轉(zhuǎn)換的過(guò)程，見(jiàn)下圖药有。為了檢查電梯在上下樓途中不會(huì)開(kāi)門表牢，微波爐開(kāi)門時(shí)不能加熱食物蝠检，就需要看這個(gè)狀態(tài)機(jī)是否符合一些 CTL 描述辣苏。

微波爐的狀態(tài)轉(zhuǎn)換圖

2.1 SemanticTree語(yǔ)義樹(shù)結(jié)構(gòu)

在解析 CTL 公式時(shí)，之所以要使用 SemanticTree摧茴，是為了在之后的模型檢驗(yàn)過(guò)程中更好地計(jì)算出滿足條件的狀態(tài)绵载。剛開(kāi)始時(shí)筆者也考慮過(guò)使用逆波蘭表達(dá)式的方式來(lái)完成 CTL 公式的計(jì)算，后來(lái)還是選擇了更優(yōu)的樹(shù)的方式苛白，一是因?yàn)槟娌ㄌm表達(dá)式的操作元素都是原子變量娃豹，而CTL公式中可能會(huì)出現(xiàn)復(fù)合變量，這正是樹(shù)結(jié)構(gòu)所擅長(zhǎng)解決的购裙。而且 CTL 公式的多數(shù)操作符都是一元運(yùn)算符而非二元運(yùn)算符懂版，增加了直接計(jì)算的難度。下面給出 SemanticTree 類的定義：

public class SemanticTree {
    String nodeValue;
    //如果是AU之類的雙操作數(shù)符號(hào)躏率，則為2躯畴；
    //如果是AX、非之類的單操作符號(hào)薇芝，則為1蓬抄，如果是純變量，則為0
    int childNum;
    SemanticTree leftChild;
    SemanticTree rightChild;
    //默認(rèn)有左右兩個(gè)子樹(shù)夯到，當(dāng)成二叉樹(shù)處理嚷缭。
    //若為單操作符，則右子樹(shù)為空耍贾，只看左節(jié)點(diǎn)
    public SemanticTree(String input){ nodeValue = input; }
    public SemanticTree() {}
}

可以看到峭状，該類的定義和二叉樹(shù)的定義很類似，都是使用了一種遞歸定義的方式逼争。每個(gè) SemanticTree 變量都包含著兩個(gè) SemanticTree 類型的變量代表左右子樹(shù)，同時(shí)還有一個(gè) String 類型的變量存放著節(jié)點(diǎn)的內(nèi)容劝赔，可以是操作符或者布爾變量誓焦。最后還有一個(gè) int 類型的變量 childNum 代表著該節(jié)點(diǎn)的有效子樹(shù)個(gè)數(shù)。當(dāng)某個(gè)節(jié)點(diǎn)是 and着帽、or 之類的二元操作符時(shí)杂伟，左子樹(shù)和右子樹(shù)分別代表著它的兩個(gè)操作數(shù)，childNum 的值為 2仍翰；當(dāng)該節(jié)點(diǎn)是 not 這樣的一元操作數(shù)時(shí)赫粥，左子樹(shù)存放著唯一的操作數(shù)，右子樹(shù)為空予借，childNum 為 1越平；當(dāng)該節(jié)點(diǎn)是布爾變量時(shí)频蛔，往往都意味著這個(gè)節(jié)點(diǎn)是葉子結(jié)點(diǎn)，它的左右子樹(shù)都為空秦叛，childNum 的值也為 0晦溪。

2.2 CTL公式解析算法設(shè)計(jì)與實(shí)現(xiàn)

接下來(lái)給出將 String 類型的 CTL 公式轉(zhuǎn)為 SemanticTree 類型的方法。該方法的思路主要是通過(guò)正則表達(dá)式匹配和遞歸來(lái)完成的挣跋，正則表達(dá)式可以作為 If 語(yǔ)句的條件快速判定操作符的類型三圆；遞歸則能夠簡(jiǎn)潔而優(yōu)雅地將一長(zhǎng)串復(fù)雜的CTL公式迭代處理。

CTL公式中需要處理的描述符一共有八種（AX避咆、EX舟肉、AF、EF查库、AG路媚、EG、AU和EU）膨报，描述符由路徑量詞和時(shí)態(tài)邏輯運(yùn)算符構(gòu)成磷籍，前者包含 A 和 E，A 的意思是“對(duì)于所有的狀態(tài)路徑”现柠，E 的意思是“對(duì)于至少一條狀態(tài)路徑”院领。注意它們并不是對(duì)立的，E 至少包含一條路徑够吩，至多包含所有路徑比然。后者包含 X、F周循、G 和 U强法，X 的意思是“下一個(gè)狀態(tài)”，F(xiàn) 的意思是“將來(lái)某個(gè)狀態(tài)”湾笛，G 的意思是“之后的所有狀態(tài)”饮怯，U 的意思是“直到某個(gè)狀態(tài)”。將路徑量詞和時(shí)態(tài)邏輯運(yùn)算符組合嚎研，就能表示很多邏輯描述了蓖墅。在解析為 SemanticTree 的過(guò)程中，并不需要對(duì)這些描述符進(jìn)行邏輯操作临扮，而是依據(jù)它們的子樹(shù)個(gè)數(shù)來(lái)決定下一步的操作论矾，因此下面的代碼中不會(huì)給出完整的代碼，而是僅列出不同子樹(shù)個(gè)數(shù)的情況杆勇。

CTL 語(yǔ)義示例

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贪壳、→、∨和∧的情況和上面類似蚜退，只是在求子字符串時(shí)不同
    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;
}

算法的流程圖如下所示：

算法流程圖

其中有幾點(diǎn)需要說(shuō)明杰扫，一是在對(duì)一元操作符進(jìn)行處理時(shí)，默認(rèn)只是給左子樹(shù)賦值膘掰，對(duì)右子樹(shù)不進(jìn)行操作章姓，從而得到圖2-3中那種只有一個(gè)子節(jié)點(diǎn)的效果。二是在遇到左括號(hào)時(shí)识埋，說(shuō)明遇到了復(fù)合的布爾變量凡伊，此時(shí)調(diào)用了get_string_between_brackets方法，得到括號(hào)之間的CTL子公式再將其變成一段 SemanticTree窒舟。該方法實(shí)現(xiàn)比較簡(jiǎn)單系忙，需要維護(hù)一個(gè)括號(hào)計(jì)數(shù)器，因?yàn)橐粚?duì)括號(hào)之間可能還會(huì)出現(xiàn)若干對(duì)括號(hào)惠豺。當(dāng)找到與左括號(hào)匹配的右括號(hào)時(shí)银还，即返回兩括號(hào)之間的子字符串。

最后需要注意非操作符可能有三種情況洁墙，就是永真蛹疯、永假和布爾變量。它們自己本身表示的就是某些狀態(tài)而非邏輯描述符热监，因此它們是沒(méi)有子樹(shù)的捺弦，對(duì)其左右子樹(shù)都不處理。

通過(guò)該算法孝扛，就可以將復(fù)雜的 CTL 公式轉(zhuǎn)化成 SemanticTree 語(yǔ)義樹(shù)的形式列吼，再使用類似的遞歸函數(shù)，結(jié)合前文提到的 Graphviz 的 API 就可以輸出 svg 格式的圖像苦始。比如寞钥，當(dāng)將字符串E[AF(pvq)UE[AX?rU?s]]作為輸入，將得到的 svg 輸出在瀏覽器中打開(kāi)陌选，即能看到下圖所示的結(jié)果凑耻。

CTL 公式解析的例子

3. 模型檢驗(yàn)

在將 CTL 公式轉(zhuǎn)換成了抽象的語(yǔ)義樹(shù)結(jié)構(gòu)后，就到了最核心的一部分柠贤，即借助 JavaBDD 庫(kù)來(lái)求取模型檢驗(yàn)算法。

什么是模型檢驗(yàn)类缤？還是以第 2 節(jié)中的微波爐舉例子臼勉，給出微波爐的各種狀態(tài)以及它們之間的轉(zhuǎn)換（遷移）情況，來(lái)檢驗(yàn)這個(gè)狀態(tài)機(jī)系統(tǒng)是否符合 CTL 公式的描述餐弱。

這部分有三點(diǎn)最為關(guān)鍵宴霸，一是用 BDD 表示狀態(tài)集和遷移關(guān)系囱晴，二是求出某個(gè)狀態(tài)的前驅(qū)狀態(tài)，三是編寫求取滿足條件的狀態(tài)的方法瓢谢。第一點(diǎn)的具體實(shí)現(xiàn)在前文已經(jīng)介紹了畸写，主要難在思維的轉(zhuǎn)換上，使用BDD解決狀態(tài)相關(guān)問(wèn)題是一個(gè)新的視角氓扛，需要對(duì) BDD 有較深刻的理解枯芬；第二點(diǎn)則是一個(gè)基礎(chǔ)算法，在模型檢驗(yàn)算法中處理大部分 CTL 公式都需要用到該算法采郎；第三點(diǎn)則是通過(guò)最小集和三個(gè)核心求取狀態(tài)集的算法 EX千所、EU 和 EG 完成整體的算法。下面分別對(duì)后兩點(diǎn)進(jìn)行介紹蒜埋。

3.1 前驅(qū)狀態(tài)的求取

在求解系統(tǒng)中有哪些狀態(tài)滿足CTL公式的過(guò)程中淫痰，大多數(shù)情況都是需要先求出滿足某布爾變量的狀態(tài)集合，然后由這些狀態(tài)一步步推出最終的結(jié)果狀態(tài)集整份。在這個(gè)過(guò)程中待错，很重要的一個(gè)步驟就是求解某個(gè)或某些狀態(tài)的前驅(qū)狀態(tài)。前驅(qū)狀態(tài)更準(zhǔn)確的定義是烈评，能發(fā)生一次遷移為X的狀態(tài)集合火俄，其中X表示系統(tǒng)狀態(tài)的子集。設(shè)X的前驅(qū)狀態(tài)為pre?(X)础倍，則有如下的表達(dá)式：

pre?(X) = {s∈S|?s’,(s→s’且s’∈X)}

對(duì)于前驅(qū)狀態(tài)的求取來(lái)說(shuō)烛占，一共存在三種情況，即一對(duì)一沟启、一對(duì)多和多對(duì)一忆家，如下圖所示。第一種情況很簡(jiǎn)單德迹，前面的狀態(tài)就是后面狀態(tài)的前驅(qū)狀態(tài)芽卿；第二種情況下，對(duì)后面任意一個(gè)狀態(tài)胳搞，前面的狀態(tài)就是其前驅(qū)狀態(tài)卸例；第三種情況下，前面的所有狀態(tài)都是后面狀態(tài)的前驅(qū)狀態(tài)肌毅。要注意的是筷转，在實(shí)際應(yīng)用中，是要對(duì)許多狀態(tài)同時(shí)求它們的前驅(qū)狀態(tài)的悬而，這一并行問(wèn)題可以由BDD通過(guò)狀態(tài)集合的方式來(lái)更有效地解決呜舒。

前驅(qū)狀態(tài)的三種情況

下面給出求前驅(qū)狀態(tài)的具體算法。該方法接收一個(gè)用 BDD 形式表示的狀態(tài)集合（編序?yàn)槠鏀?shù)笨奠，即1袭蝗，3唤殴，5，...到腥，表示遷移關(guān)系的終點(diǎn)）朵逝，返回這些狀態(tài)的前驅(qū)狀態(tài)的 BDD 形式（編序?yàn)榕紨?shù)，即0乡范，2配名，4，...篓足，表示遷移關(guān)系的起點(diǎn)）段誊。

算法的整體思路是根據(jù)傳入的 BDD 的情況進(jìn)行不同的處理，如果 BDD 是永假栈拖，不包括任何狀態(tài)连舍，則返回永假；如果 BDD 與系統(tǒng)包含的布爾變量數(shù)目一致涩哟，則只需要調(diào)用restrict方法索赏，將傳入的 BDD 包含的狀態(tài)約束為真，即能得到前驅(qū)狀態(tài)的 BDD贴彼。這是因?yàn)閷?duì)于遷移關(guān)系的路徑來(lái)說(shuō)潜腻，約束了遷移關(guān)系的終點(diǎn)（編序?yàn)槠鏀?shù)），那么剩下的就只有編序?yàn)榕紨?shù)的節(jié)點(diǎn)器仗，它們實(shí)際上就是遷移關(guān)系的起點(diǎn)融涣。如果 BDD 的節(jié)點(diǎn)數(shù)目少于系統(tǒng)包含的布爾變量數(shù)目，這就說(shuō)明 BDD 存在被約減的節(jié)點(diǎn)精钮。此時(shí)不能再直接調(diào)用restrict方法威鹿，因?yàn)橛锌赡茉斐蛇z漏的情況。這里采取了逐個(gè)判斷的做法轨香。

private static BDD get_pre_states(BDD input) {
    int nodeCount = input.nodeCount();
    if (nodeCount == 0) { 
// 該情況下忽你，傳入的BDD為永假，對(duì)應(yīng)的狀態(tài)集合是⊥
    return B.zero();}
else if (nodeCount == booleanVector.length) {
// 該情況下臂容，傳入的BDD包含的布爾變量數(shù)目與系統(tǒng)的布爾變量數(shù)目一致
// 這意味著所有到終點(diǎn)1節(jié)點(diǎn)的每條路徑都只包含一種情況科雳，沒(méi)有約減節(jié)點(diǎn)
    return TRANS_bdd.restrict(input);} // TRANS_bdd表示遷移關(guān)系的BDD
else {
// 該情況下，存在某條到達(dá)終點(diǎn)1節(jié)點(diǎn)的路徑包含多種取值情況脓杉，
// 有節(jié)點(diǎn)被約減糟秘，如圖3-4。這時(shí)采取一個(gè)特殊的策略：遍歷所有的狀態(tài)
// 看它是否有可能屬于前驅(qū)狀態(tài)
    BDD result = B.zero();
    // 遍歷形參BDD的每一條到終點(diǎn)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()轉(zhuǎn)化成byte[]時(shí)出錯(cuò)球散！");}}
return result;}
}

其中有兩點(diǎn)需要說(shuō)明尿赚，一是allsat方法，該方法以List的形式返回一個(gè) BDD 所有到達(dá)終點(diǎn) 1 節(jié)點(diǎn)的路徑。經(jīng)過(guò)查看源碼吼畏，得知List中的元素類型是 byte 數(shù)組，數(shù)組中的元素個(gè)數(shù)為系統(tǒng)的布爾變量的個(gè)數(shù)嘁灯，有三種取值：1泻蚊，0 和 -1。1 對(duì)應(yīng)著布爾變量取真丑婿，0 對(duì)應(yīng)著布爾變量取假性雄，-1 對(duì)應(yīng)著路徑上不包含該變量。二是fromByteListToBDD方法的作用是將一條到達(dá)終點(diǎn)1的路徑轉(zhuǎn)換成 BDD 的形式羹奉。程序中還出現(xiàn)了若干 restrict 方法秒旋，主要作用是調(diào)整 BDD 的編序以更方便地計(jì)算遷移狀態(tài)的起點(diǎn)。

3.2 模型檢驗(yàn)算法的設(shè)計(jì)與實(shí)現(xiàn)

有了之前的鋪墊诀拭，現(xiàn)在實(shí)現(xiàn)具體的模型檢驗(yàn)算法就不是那么難了迁筛。雖然 CTL 運(yùn)算符有很多（本項(xiàng)目中能識(shí)別的有８種），但是我們并不需要對(duì)每個(gè)CTL運(yùn)算符都進(jìn)行處理耕挨，因?yàn)榇蟛糠?CTL 運(yùn)算符可以轉(zhuǎn)化成一小部分的CTL運(yùn)算符细卧，也就是說(shuō)只需要實(shí)現(xiàn)CTL的最小集就可以了。

一個(gè)最小集包含的運(yùn)算符有：?（永真）筒占，∨贪庙，?，EG翰苫，EU 和 EX止邮。下面是一些其他的運(yùn)算符轉(zhuǎn)化成最小集包含的運(yùn)算符的公式：

• EFφ == E[?U(φ)]（因?yàn)镕φ == [?U(φ)]）
• AXφ == ?EX(?φ)
• AGφ == ?EF(?φ) == ? E[?U(?φ)]
• AFφ == A[?Uφ] == ?EG(?φ)
• A[φUψ] == ?(E[(?ψ)U?(φ∨ψ)]∨EG(?ψ))

接下來(lái)討論這樣一個(gè)算法，接收 CTL 系統(tǒng)模型的輸入和 CTL 公式奏窑，輸出滿足該公式的狀態(tài)集合导披。整體思路是，首先將 CTL 公式轉(zhuǎn)化成 SemanticTree 語(yǔ)義樹(shù)形式的變量良哲，然后將公式中的運(yùn)算符都轉(zhuǎn)化成最小集中的運(yùn)算符盛卡，接著先求出滿足 CTL 一些子公式的狀態(tài)，再逐步擴(kuò)展到整個(gè) CTL 公式筑凫。在此之前滑沧，需要說(shuō)明如何通過(guò)最小集中的運(yùn)算符得到滿足它們的狀態(tài)∥∈担考慮以下幾種情況：

1. 若公式為 ?滓技，則返回系統(tǒng)的狀態(tài)集 S 對(duì)應(yīng)的 BDD，表示所有狀態(tài)都滿足棚潦；
2. 若公式為某個(gè)特定的布爾變量 ψ令漂，則返回所有滿足 ψ 的狀態(tài)集合的 BDD；
3. 若公式為 ψ１∨ψ２，則先分別求出 ψ１和 ψ２ 對(duì)應(yīng)的 BDD叠必，再調(diào)用 or 方法求狀態(tài)集的并集荚孵。
   同理若公式為 ψ１∧ψ２，則對(duì)兩個(gè) BDD 調(diào)用 and 方法求交集纬朝。
4. 若公式為 EXψ收叶，則先求出滿足 ψ 的狀態(tài)集合的 BDD，然后對(duì)它們調(diào)用求前驅(qū)狀態(tài)的算法共苛，即可得到存在一個(gè)后繼狀態(tài)滿足 ψ 的狀態(tài)集合判没，如下圖；

求取滿足 EX 公式的狀態(tài)

5. 若公式為 E[ψ１Uψ２]隅茎，則先求出滿足 ψ２ 的狀態(tài)集合 A澄峰，再觀察滿足 ψ1 的所以狀態(tài)，看其是否存在后繼狀態(tài)屬于 A辟犀，若是則將其加入 A俏竞。重復(fù)這種操作直到?jīng)]有新的變化為止，A 對(duì)應(yīng)的 BDD 就是最終的結(jié)果踪蹬，如下圖胞此；

求取滿足 EU 公式的狀態(tài)

6. 若公式為 EGψ，則首先假設(shè)所有的狀態(tài)都滿足跃捣，將系統(tǒng)狀態(tài)集 S 作為初始值漱牵，接下來(lái)從中去除不滿足布爾變量 ψ 的狀態(tài)，然后再去掉某些狀態(tài)疚漆，它們的后繼狀態(tài)集中不存在滿足布爾變量 ψ 的狀態(tài)酣胀。重復(fù)這種操作直到?jīng)]有新的變化為止，最終的狀態(tài)集合對(duì)應(yīng)的 BDD 就是最終的結(jié)果娶聘，如下圖闻镶。

求取滿足 EG 公式的狀態(tài)

下面給出求解滿足EX、EU和EG的狀態(tài)的算法丸升，這是整個(gè)模型檢驗(yàn)算法的核心部分铆农，對(duì)CTL其他運(yùn)算符的處理幾乎都會(huì)轉(zhuǎn)化為這三個(gè)算法。它們的輸出是滿足條件的狀態(tài)集的BDD狡耻。上面的圖6-2墩剖、圖6-3和圖6-4也可以作為算法的圖解。

private static BDD SAT_EX(BDD input) {//傳入的BDD相當(dāng)于EXψ中ψ對(duì)應(yīng)的狀態(tài)集
    BDD X = input;
    // 調(diào)整編序夷狰，比如說(shuō)如果X的BDD有3個(gè)節(jié)點(diǎn)岭皂，調(diào)整為[1,3,5]
    // 注意這里先變成了奇數(shù)編序，最后又調(diào)整回來(lái)沼头，是為了方便求前驅(qū)狀態(tài)集
    // 奇數(shù)編序在遷移關(guān)系中意味著終點(diǎn)節(jié)點(diǎn)爷绘，遷移關(guān)系調(diào)用restrict方法后
    // 剩下的節(jié)點(diǎn)編序?yàn)榕紨?shù)书劝，對(duì)應(yīng)著起點(diǎn)節(jié)點(diǎn)。EU和EG兩個(gè)算法同理
    X = X.replace(adjustOddOrder);
    BDD result = get_pre_states(X);
    return result.replace(adjustEvenOrderBack);// 把編序調(diào)整成初始的[0,1,2]
}
private static BDD SAT_EU(BDD input1, BDD input2) {
    // 傳入的兩個(gè)BDD相當(dāng)于E[ψ１Uψ２]中滿足ψ１和ψ２的狀態(tài)集
    BDD W, X, Y;
    W = input1;
    X = S_bdd.id();// 復(fù)制一份土至，免得產(chǎn)生的修改影響了代表S的BDD
    Y = input2;
    if (X.equals(Y)) { return Y;}
    while (!X.equals(Y.replace(adjustOddOrder))) {
        // 調(diào)整編序购对，比如說(shuō)如果X的BDD有3個(gè)節(jié)點(diǎn)，調(diào)整為[1,3,5]
        X = Y.replace(adjustOddOrder);
    BDD pre_states = get_pre_states(X);//此時(shí)pre_states的編序?yàn)?,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)))) {
        // 調(diào)整編序陶因，比如說(shuō)如果X的BDD有3個(gè)節(jié)點(diǎn)洞斯，調(diào)整為[1,3,5]
        X = Y.replace(adjustOddOrder);
    BDD pre_states = get_pre_states(X);//此時(shí)pre_states的編序?yàn)?,2,4,...
    Y = bdd_AND(Y, pre_states.replace(adjustEvenOrderBack));}
    return Y;
}

需要說(shuō)明的是，算法中會(huì)用到三個(gè)輔助方法坑赡，分別是bdd_OR、bdd_AND和bdd_SUB么抗。前面兩個(gè)其實(shí)就是調(diào)用or和and方法毅否，第三個(gè)是求兩個(gè)BDD的差集的，原理是將求差集轉(zhuǎn)化成了求交集蝇刀。如bdd1 - bdd2 = bdd1.and(bdd2.not())螟加。

有了這三個(gè)算法，就能實(shí)現(xiàn)求滿足CTL公式的狀態(tài)集了吞琐。下面的算法接收一個(gè)SemanticTree類型的參數(shù)捆探，通過(guò)遞歸調(diào)用求解，將其他類型的CTL描述符都轉(zhuǎn)化成了EX站粟、EU和EG這三種形式再求解黍图，最終返回滿足該語(yǔ)義樹(shù)的狀態(tài)集對(duì)應(yīng)的BDD。其中S_bdd表示系統(tǒng)的狀態(tài)集對(duì)應(yīng)的BDD奴烙。

public static BDD getSatStates(SemanticTree sTree) {
    // sTree可能有三種情況：1.左右子樹(shù)都存在助被；2.左子樹(shù)存在；3.不存在子樹(shù)
    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 {// 子樹(shù)的數(shù)目為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方法會(huì)遍歷所有狀態(tài)切诀，找到滿足該布爾變量的狀態(tài)集
    return get_atomic_bdd(sTree.nodeValue);}}
    return S_bdd.not();
}

以上就是模型檢驗(yàn)算法的主要部分揩环。可以看到幅虑，當(dāng)最開(kāi)始輸入一個(gè) CTL 公式字符串時(shí)丰滑，首先會(huì)通過(guò)遞歸函數(shù)將其解析成 SemanticTree 語(yǔ)義樹(shù)類型，接下來(lái)會(huì)再次調(diào)用遞歸函數(shù)倒庵，從語(yǔ)義樹(shù)的葉子節(jié)點(diǎn)開(kāi)始褒墨，逐步向上推出符合 CTL 公式的狀態(tài)集合。在求解過(guò)程中哄芜，主要會(huì)使用 EX貌亭、EU 和 EG 三種算法，而在這三種算法中又會(huì)用到求解前驅(qū)狀態(tài)的算法认臊。最后圃庭，遍歷所有的狀態(tài)對(duì)應(yīng)的 BDD，對(duì)getSatStates返回的 BDD 調(diào)用restrict方法約束這些狀態(tài)對(duì)應(yīng)的 BDD，并判斷結(jié)果是否為永真剧腻，即可達(dá)到判斷狀態(tài)是否滿足 CTL 公式的目的拘央。

那么總結(jié)一下模型檢驗(yàn)的流程，如下圖所示：

模型檢驗(yàn)算法流程圖

4. 實(shí)例應(yīng)用——微波爐操作模型

又見(jiàn)到了微波爐~~作為一個(gè)經(jīng)典的例子书在，該操作模型描述了微波爐運(yùn)行過(guò)程中的狀態(tài)轉(zhuǎn)換關(guān)系灰伟。

再貼一遍之前的圖：

微波爐的狀態(tài)轉(zhuǎn)換圖

圖中每個(gè)圓圈代表一種微波爐的狀態(tài)，操作模型一共包括四個(gè)布爾變量儒旬，分別表示電源是否開(kāi)啟栏账、箱門是否關(guān)閉、是否正在加熱栈源，以及是否出錯(cuò)挡爵。比如在第一個(gè)圓圈表示的狀態(tài)中，四種布爾變量都是不被滿足的甚垦，對(duì)應(yīng)的就是微波爐沒(méi)通電晦毙、箱門開(kāi)著微酬、未加熱和未出錯(cuò)的狀態(tài)已骇。微波爐的狀態(tài)通過(guò)不同的動(dòng)作實(shí)現(xiàn)轉(zhuǎn)換误债。

首先需要模型進(jìn)行抽象化。將七個(gè)狀態(tài)用 s0-s6 來(lái)表示迄埃，四個(gè)布爾變量分別用 a疗韵、b、c侄非、d來(lái)表示伶棒。每個(gè)狀態(tài)中只保留其滿足的布爾變量，不滿足的就不顯示彩库。比如在第一個(gè)狀態(tài)中肤无，四個(gè)條件都是不滿足的，因此抽象后 s0 不含任何布爾變量骇钦。而處于烹飪中狀態(tài)的微波爐滿足箱門關(guān)閉和正在加熱的條件宛渐，因此抽象后對(duì)應(yīng)的 s3 滿足 b 和 c 兩個(gè)布爾變量。最終抽象后的微波爐模型如下圖：

抽象后的對(duì)比

此時(shí)眯搭，微波爐模型的狀態(tài)和遷移關(guān)系就可以轉(zhuǎn)化成布爾函數(shù)的形式窥翩，如s1 = a∧?b∧?c∧d，s1—>s4 = a∧?b∧?c∧d∧a’∧b’∧?c’∧d鳞仙。對(duì)應(yīng)到 JavaBDD 中寇蚊，狀態(tài)的表示需要對(duì) BDDFactory 調(diào)用setVarNum方法，傳入的參數(shù)為 4棍好，從而生成四個(gè)BDD 變量仗岸，則 s1 對(duì)應(yīng)的 BDD 表達(dá)式就是a.and(b.not).and(c.not).and(d)允耿，其中a = BDDFactory.ithVar(0)，表示 a 是 BDDFactory 的第 0 個(gè)變量扒怖。b较锡、c 和 d 同理，對(duì)應(yīng)的序號(hào)分別為 1盗痒、2 和 3蚂蕴。其他的狀態(tài)也可以被這樣表示。最終得到的 BDD 狀態(tài)集的 DOT 輸出對(duì)應(yīng)的圖像如下：

微波爐狀態(tài)集的表示

s1 到 s4 的遷移關(guān)系的表示則需要對(duì) BDDFactory 調(diào)用extDomain方法俯邓，傳入一個(gè)包含兩個(gè)元素的 int 數(shù)組骡楼，每個(gè)元素的大小都是 24。該方法會(huì)返回一個(gè)包含兩個(gè)元素的 BDDDomain 數(shù)組稽鞭，使用第一個(gè) BDDDomain 包含的 BDD 表示遷移關(guān)系的起點(diǎn)（BDD 的序號(hào)為 0君编，2，4 和 6）川慌，第二個(gè)包含的 BDD 表示遷移關(guān)系的終點(diǎn)（BDD 的序號(hào)為 1，3祠乃，5 和 7）梦重。最后將所有的遷移關(guān)系取并集（或者說(shuō)對(duì)所有遷移關(guān)系對(duì)應(yīng)的 BDD 調(diào)用 or 方法），即可得到下圖所示的總遷移關(guān)系亮瓷。

微波爐遷移關(guān)系的表示琴拧，狀態(tài)多就是這樣，不要被嚇到哈

雖然上面給出了狀態(tài)集和遷移關(guān)系的 BDD嘱支，但是實(shí)際上在模型檢驗(yàn)的過(guò)程中用戶是接觸不到的蚓胸，它相當(dāng)于一個(gè)黑盒，遮蓋了復(fù)雜的原理和計(jì)算過(guò)程除师，最終給出一個(gè)簡(jiǎn)潔的結(jié)果沛膳。這也讓本系統(tǒng)的易用性得到了提升。

接下來(lái)對(duì)微波爐模型進(jìn)行模型檢驗(yàn)汛聚。比如要驗(yàn)證這樣一個(gè)屬性：當(dāng)微波爐的箱門沒(méi)有關(guān)上時(shí)锹安，微波爐無(wú)法進(jìn)行加熱操作。首先需要把這樣一個(gè)描述轉(zhuǎn)化成CTL公式倚舀，方便計(jì)算機(jī)理解叹哭。這里需要用到 AU 描述符。之前說(shuō)過(guò)痕貌，A[pUq]表示在從當(dāng)前狀態(tài)出發(fā)的每一條計(jì)算路徑上风罩，都存在一個(gè)狀態(tài)使得 q 成立，并且對(duì)這些路徑上的所有以前狀態(tài) p 成立舵稠。因此超升，我們需要驗(yàn)證A[?c U b]這個(gè)公式對(duì)于上面抽象出來(lái)的 CTL 模型是不是成立的入宦。

構(gòu)造一個(gè) CTL 描述

可能有同學(xué)會(huì)有疑問(wèn)，這個(gè)微波爐的模型是怎么輸入的廓俭。為了方便操作云石，我用 SpringBoot 寫了個(gè)簡(jiǎn)單的網(wǎng)頁(yè)，輸入布爾變量研乒、狀態(tài)變量和遷移關(guān)系汹忠，以及要檢驗(yàn)的 CTL 公式，就相當(dāng)于是輸入了模型了雹熬。界面如下圖所示：

通過(guò)網(wǎng)頁(yè)操作宽菜，請(qǐng)忽略要輸入的超多參數(shù)...

接下來(lái)點(diǎn)擊生成結(jié)果的按鈕開(kāi)始模型檢驗(yàn)部分的計(jì)算，在1-2s內(nèi)即可得到系統(tǒng)生成的結(jié)果竿报。結(jié)果包含三部分铅乡，一是滿足CTL公式的狀態(tài)集，二是根據(jù)輸入生成的模型示意圖烈菌，如下圖 1 所示阵幸。三是對(duì) CTL 公式解析得到的語(yǔ)法樹(shù)，如下圖 2 所示芽世。模型檢驗(yàn)計(jì)算得到的結(jié)果是 [s0, s1, s2, s3, s4, s5, s6]挚赊，說(shuō)明所有七個(gè)狀態(tài)都滿足這個(gè) CTL 公式，這從第一個(gè)圖中可以驗(yàn)證济瓢，也意味著微波爐模型是滿足這個(gè)性質(zhì)的荠割。除此之外，還可以對(duì)模型示意圖和 CTL 公式的語(yǔ)法樹(shù)圖像進(jìn)行縮放旺矾、移動(dòng)蔑鹦、tooltip 提示以及突出顯示路徑的操作，便于進(jìn)一步的觀察箕宙。

系統(tǒng)生成的模型示意圖

系統(tǒng)生成的 CTL 語(yǔ)義樹(shù)

總結(jié)一下步驟就是嚎朽，首先根據(jù)輸入，生成系統(tǒng)模型示意圖和待驗(yàn)證的 CTL 公式的語(yǔ)義樹(shù)柬帕，隨后將狀態(tài)集和遷移關(guān)系轉(zhuǎn)化成 BDD 進(jìn)行后續(xù)的驗(yàn)證和計(jì)算火鼻。這樣就以一種可視化的形式表現(xiàn)了狀態(tài)機(jī)運(yùn)行和遷移的邏輯、CTL公式的結(jié)構(gòu)以及布爾函數(shù)運(yùn)算的結(jié)果雕崩。

當(dāng)然魁索，由于個(gè)人的時(shí)間精力等原因，本系統(tǒng)仍有可提升的空間盼铁，具體有兩個(gè)方面粗蔚。一是在用 BDD 表示狀態(tài)集和遷移關(guān)系時(shí)，通過(guò)選擇性地整合未使用的布爾矢量可以進(jìn)一步簡(jiǎn)化最終的 BDD 表示饶火，關(guān)鍵在于如何選擇合適的布爾矢量用于化簡(jiǎn)鹏控。二是在設(shè)計(jì)實(shí)現(xiàn)求取前驅(qū)狀態(tài)集的算法的過(guò)程中致扯，當(dāng)路徑中存在被化簡(jiǎn)的狀態(tài)節(jié)點(diǎn)時(shí)，采取的遍歷策略效率不是很高当辐，所以此處的策略還有進(jìn)一步優(yōu)化的可能抖僵。這些問(wèn)題就留給后來(lái)研究Java BDD的同學(xué)們解決吧（如果有人的話）... ...

Last Words

這篇文章到這里就結(jié)束了?文中介紹的幾種應(yīng)用，對(duì)大多數(shù)人來(lái)說(shuō)缘揪，可能計(jì)算布爾表達(dá)式的部分比較有參考價(jià)值耍群，另外兩種比較小眾，只有了解數(shù)理邏輯找筝、狀態(tài)機(jī)轉(zhuǎn)換等領(lǐng)域的同學(xué)才用得上蹈垢。

對(duì)于使用JavaBDD的同學(xué)，現(xiàn)在應(yīng)該有更多的選擇了袖裕。我之前在 GitHub 上找到了一個(gè)項(xiàng)目列表曹抬，用各種語(yǔ)言實(shí)現(xiàn)了BDD，感興趣的可以看看：johnyf/tool_lists

而且急鳄，如果要檢驗(yàn)一個(gè)狀態(tài)機(jī)系統(tǒng)的轉(zhuǎn)換邏輯是否有漏洞谤民，現(xiàn)在應(yīng)該也有很多方式了，比如用 Petri 網(wǎng)描述疾宏，然后用模擬軟件去驗(yàn)證张足，還有很多別的方式。此處不禁感嘆一句灾锯，大人，時(shí)代變了嗅榕！??

最后顺饮，本文所描述的這些，更多地是將幾種工具結(jié)合凌那，進(jìn)行狀態(tài)機(jī)轉(zhuǎn)換的理論性探索兼雄。如有錯(cuò)誤和紕漏，請(qǐng)多多指出帽蝶，還望海涵赦肋。最后的最后，感謝你能讀到這里励稳！??