原文地址：http://www.cnblogs.com/Rainday/p/cmurphi_prime_1.html
本來以為自己會是一個搞技術的人的，沒想到現在徹底變成一個搞科研的人了。搞的東西，現在自己也不是很懂。摸着石頭過河吧。
Murphi驗證系統由Murphi編譯器和Murphi描述性語言組成。
- Murphi編譯器根據Murphi描述生成一個特定目的的驗證器。這個驗證器可以用來檢查系統的特性，比如錯誤斷言，不變量和死鎖。
- Murphi描述語言是一個高級描述語言，針對狀態有限的異步並行系統。Murphi在某些特性上是高級的，這些特性可以在很多高級編程語言如Pascal或者C中找到，同時這些特性也是Murphi的一部分。例如，Murphi擁有用戶定義的數據類型，過程，以及描述的參數化方法。
1. Murphi描述的結構
Murphi描述由以下部分組成：
- 常量，類型，全局變量和過程的定義；
- 狀態遷移規則的集合；
- 初始狀態的描述；
- 不變量集。
Murphi的行為部分，是一個狀態遷移規則的集合。每一條規則都是一條保護命令，其由一個條件（全局變量上的布爾表達式）和一個動作（一條可以修改變量的值的語句）組成。條件和動作均以類Pascal的風格書寫。動作可以是包含循環和條件的任意復合語句，但不論其多么復雜，動作的執行都是原子的——沒有其他的規則可以改變變量或者說，當它正在執行的時候，沒有其他的接口。
2. 使用Murphi驗證一個系統的簡單四步
a) 編寫Murphi語言程序，命名如pingpong.m。
b) 在其上邊運行Murphi編譯器，其命令行：
1 $(murphipath)/mu pingpong.m
這樣會生成一個文件pingpong.C。
c) 在pingpong.C中運行C++編譯器，其命令行：
1 $(g++path)/g++ pingpong.C -I$(includepath)
記住說明所有包含文件的路徑。
d) 最終，你可以通過調用a.out運行一個模擬過程或者驗證過程。可以通過下邊的命令查看命令行開關的列表：
1 a.out -h
事實上，這整個過程以后可以通過使用Makefile簡化，這個文件在ex文件夾中提供。然而，你必須分別對變量CPLUSPLUS，MURPHIPATH和INCLUDEPATH進行設置。
3. Murphi的執行模型
Murphi狀態，是對描述中的所有全局變量的賦值。描述的執行可以由下邊的無限循環生成。
無限循環：
- 尋找當前狀態下所有的規則，這些規則的條件值均為true。也就是說，條件表達式的值為true，可以為全局變量賦當前值。
- 任意選擇一個規則並且執行其動作，進入另一個狀態。
注意，Murphi描述是非確定性的，因為在上邊的第2步中進行了任意的選擇。用戶無法控制這個選擇的過程，所以不管那條規則被選擇，“正確”的Murphi程序必須能夠做正確的事情。然而，一旦一條規則被選擇，動作就是確定的了（有確定的下一個狀態）。
這個執行模型對描述通過共享變量交互的異步系統（以不同的速度運行不同的進程）是有好處的，這種系統中，進程A通過寫一個進程B將會讀取的變量來影響進程B。信息傳遞可以通過讀寫緩沖區變量或者數組來進行建模。
Murphi模擬器在所有的規則中任意選擇一條來進入新的狀態。另一方面，驗證器決定所有可能的選擇的結果。當前的驗證器通過廣度優先搜索或者深度優先搜索來做到這個，這兩種方法都在一個巨大的哈希表中存儲狀態，這樣就可以在遇到一個曾經遇到過的狀態時中斷搜索。
當驗證器生成狀態時，會檢查各種條件。有時會出現運行時錯誤，大部分都是賦值或者數組索引出界。有顯式"assert"和"error"語句可以在一個動作中調用。如果這些語句中的一個發生了，驗證器就會中止並且打印出診斷信息，包含導致由初始狀態運行到錯誤狀態的重新排序的狀態列表。驗證器也會在不變量表達式（用戶給出的描述中的一部分）對當前狀態的值為false或者當前狀態“死鎖”（無法成功跳出當前狀態）的時候這么做（打印診斷信息）。
4. Murphi編譯器的選項
Murphi編譯器擁有幾個命令行選項：
- -h 幫助
- -l 打印許可信息
- -b 使用位壓縮狀態
- -c 使用哈希壓縮
默認情況下，Murphi將所有狀態變量按字節對齊。結果就是狀態的描述會是在每個位都被使用的情況（即位壓縮，選項-b）下的2~4倍大。然而，Murphi的運行速度大約會快25%。
當使用哈希壓縮（選項-c）時，通常被壓縮為40bit大小的值會保存在哈希表中，而不是完整的狀態描述。以后會更加詳細地討論。當完整的狀態描述必須要使用的時候，哈希壓縮可以和位壓縮結合使用來減小活動狀態隊列對存儲的需求。
5. 使用已生成的特殊目的的驗證器
Murphi編譯器為特殊的Murphi描述生成了特殊目的的驗證器。下面的列表是相應的命令行選項：
1） 一般：
- -h 幫助
- -l 打印許可信息
2） 驗證策略（默認-v）：
- -s 模擬器
- -v或者-vbfs 使用廣度優先搜索驗證
- -vdfs 使用深度優先搜索驗證
- -ndl 不檢查死鎖
3） 其他選項（默認-m8， -p3， -loop1000）
- -m<n> 哈希表的存儲數量，單位是Mb
- -k<n> 同上，單位是Kb
- -loop<n> 允許循環最多執行n次
- -p 使模擬或者驗證轉為冗余模式（verbose）
- -p<n> 每10^n次事件報告一次進展，n的值為1~5
- -pn 不打印進展報告
- -pr 打印規則信息
4） 錯誤跟蹤操縱（默認-tn）
- -tv 寫出違反跟蹤（默認與-td一起使用）
- -td 只寫出與前一個狀態的不同（在模擬模式下，只寫出冗余模式下的不同）
- -tf 在跟蹤中寫完整的狀態
- -ta 寫所有生成的狀態至少一次
- -tn 不寫跟蹤
5）壓縮技術（默認-sym3和-permlimit 10，使用multiset壓縮）
- -nosym 不使用對齊壓縮（multiset壓縮仍然有效）
- -nomultiset 不使用multiset壓縮
- -sym<n> 使用對齊壓縮
- -permlimit<n> 在alg 3中檢查的序列的最大數目（設為0來標准化）
| n | 方法 |
| 1 | 徹底標准化 |
| 2 | 試探快速標准化（可能會比alg 3標准化慢或者快，對大數量集使用很多附加存儲） |
| 3 | 試探低存儲標准化（依賴於-permlimit） |
| 4 | 試探快速標准化（alg 3和-permlimit 1同時使用） |
6） Hash壓縮（默認使用40位的哈希壓縮）
- -b<n> 用來存儲的位的數目
- -d dir 將跟蹤信息寫入文件dir/sci.trace中
命令行選項"-s"將驗證器轉換為Murphi的模擬器，將會任意選擇規則。不使用"-s"，驗證器決定所有可能選擇的結果。當前的驗證器通過BFS（默認）或者DFS（通過選項"-vdfs"）來這么做。
一個巨大的哈希表被用來存儲能夠達到的狀態。哈希表的大小通過"-m"和"-k"確定。默認的存儲使用是8MB。文件"mu_prolog.inc"中的常量"gPercentActiveStates"可以修改，來改變BFS或者DFS中驗證時使用的隊列的容量。
這一部分算是結束了，其實好好看一遍手冊，發現自己上次看的幾遍都有理解錯誤或者遺漏的東西。。
傳送門：