PROMELA（Protocol Meta Language）是一種用于描述和驗證并發系統的形式化建模語言，主要與SPIN（Simple Promela Interpreter）模型檢查器配合使用。本教程將基于JSPIN（SPIN的Java圖形化版本），圍繞順序編程（Sequential Programming）核心知識點展開，通過示例代碼和操作演示，幫助你快速掌握PROMELA的基礎語法與實踐。
1.1 第一個PROMELA程序
PROMELA程序的核心是定義進程（process），通過proctype關鍵字聲明。程序執行從init進程開始（類似C語言的main函數）。
示例1-1：基礎結構與輸出
/* 第一個PROMELA程序：輸出簡單信息 */
proctype HelloWorld() {printf("Hello, PROMELA!\n"); /* 打印輸出 */
}init {run HelloWorld(); /* 啟動HelloWorld進程 */
}
操作步驟（JSPIN工具）：
- 打開JSPIN，新建文件并輸入上述代碼，保存為
hello.pml。 - 點擊
Verify→Parse檢查語法（無錯誤則顯示Parsing completed）。 - 點擊
Simulate→Run啟動模擬，控制臺將輸出Hello, PROMELA!。
示例1-2：變量賦值與輸出
proctype VarDemo() {int x = 5; /* 聲明并初始化int變量 */byte y = 10; /* 聲明byte變量（0-255） */printf("x = %d, y = %d\n", x, y); /* 格式化輸出 */
}init {run VarDemo();
}
示例1-3：簡單計算
proctype CalcDemo() {int a = 10, b = 3;int sum = a + b;int product = a * b;printf("Sum: %d, Product: %d\n", sum, product);
}init {run CalcDemo();
}
關鍵說明：
proctype定義進程模板，init是程序入口。printf支持%d（整數）、%s（字符串）、%c（字符）等格式化符號。
1.2 Random simulation（隨機模擬）
PROMELA支持非確定性（Non-determinism），通過rand()函數或多分支選擇（如if語句）實現隨機行為。JSPIN的模擬功能可展示不同執行路徑。
示例1-4：隨機數生成
proctype RandDemo() {int r = rand() % 10; /* 生成0-9的隨機數 */printf("Random number: %d\n", r);
}init {run RandDemo();
}
操作步驟（觀察隨機結果）：
在JSPIN中多次點擊Simulate → Run，每次輸出的隨機數可能不同（因rand()依賴偽隨機種子）。
示例1-5：多分支隨機選擇
proctype BranchDemo() {if:: printf("執行分支1\n"); /* 分支1 */:: printf("執行分支2\n"); /* 分支2 */fi; /* if結束 */
}init {run BranchDemo();
}
示例1-6：條件隨機選擇
proctype CondRandDemo() {int x = rand() % 2; /* 0或1 */if:: x == 0 -> printf("x是0\n"); /* 條件分支1 */:: x == 1 -> printf("x是1\n"); /* 條件分支2 */fi;
}init {run CondRandDemo();
}
關鍵說明：
if語句的分支用::分隔，JSPIN會隨機選擇一個可執行的分支（若多個分支條件滿足）。->符號表示“僅當條件滿足時執行該分支”（后續1.6節詳細說明）。
1.3 Data types（數據類型）
PROMELA支持以下基礎數據類型，需注意取值范圍和使用場景：
1.3.1 基礎類型對比
| 類型 | 描述 | 取值范圍 | 示例 |
|---|---|---|---|
bool | 布爾值 | true/false | bool flag = true; |
byte | 無符號8位整數 | 0 ~ 255 | byte age = 30; |
int | 有符號32位整數（依賴SPIN配置） | -231 ~ 231-1 | int score = -5; |
mtype | 枚舉類型 | 用戶定義的符號常量集合 | mtype { A, B, C }; |
示例1-7：bool類型使用
proctype BoolDemo() {bool isReady = true;if:: isReady -> printf("準備就緒\n");:: else -> printf("未就緒\n"); /* else分支（僅當isReady為false時執行） */fi;
}init {run BoolDemo();
}
示例1-8：byte與int的取值范圍
proctype OverflowDemo() {byte b = 255;b = b + 1; /* 溢出：255+1=0（模256） */int i = 2147483647; /* int最大值 */i = i + 1; /* 溢出：2147483648（依賴SPIN配置，可能報錯） */printf("b=%d, i=%d\n", b, i);
}init {run OverflowDemo();
}
示例1-9：mtype枚舉類型
mtype { SUCCESS, FAIL, PENDING }; /* 定義枚舉類型 */proctype MtypeDemo() {mtype status = PENDING;if:: status == SUCCESS -> printf("成功\n");:: status == FAIL -> printf("失敗\n");:: status == PENDING -> printf("等待中\n");fi;
}init {run MtypeDemo();
}
關鍵說明：
byte溢出會自動取模（如255+1=0），int溢出可能導致未定義行為（SPIN默認不檢查）。mtype枚舉用于提高代碼可讀性，避免“魔法數值”。
1.3.2 Type conversions（類型轉換）
PROMELA支持隱式轉換（小范圍類型轉大范圍）和顯式轉換（需強制聲明）。
示例1-10：隱式轉換（byte→int）
proctype ImplicitConv() {byte b = 100;int i = b; /* 隱式轉換：byte→int */printf("b=%d, i=%d\n", b, i); /* 輸出：100, 100 */
}init {run ImplicitConv();
}
示例1-11：顯式轉換（int→byte）
proctype ExplicitConv() {int i = 300;byte b = (byte)i; /* 顯式轉換：截斷高位，300 → 300-256=44 */printf("i=%d, b=%d\n", i, b); /* 輸出：300, 44 */
}init {run ExplicitConv();
}
示例1-12：bool與int的轉換
proctype BoolIntConv() {bool flag = true;int x = flag; /* true→1，false→0 */bool y = (bool)0; /* 0→false，非0→true */printf("x=%d, y=%s\n", x, y ? "true" : "false"); /* 輸出：1, false */
}init {run BoolIntConv();
}
關鍵說明：
- 隱式轉換僅允許從低精度到高精度（如
byte→int），反之需顯式轉換。 bool轉int時，true為1，false為0；int轉bool時，0為false，非0為true。
1.4 Operators and expressions（操作符與表達式）
PROMELA支持算術、邏輯、比較等操作符，優先級與C語言類似（()可改變優先級）。
1.4.1 操作符分類
| 類型 | 操作符 | 示例 | 說明 |
|---|---|---|---|
| 算術 | +, -, *, /, % | a + b, c % d | %為取模，結果符號與被除數一致 |
| 邏輯 | &&, ` | , !` | |
| 比較 | ==, !=, <, >, <=, >= | a != b, c <= d | 結果為bool類型 |
示例1-13：算術操作符
proctype ArithmeticOps() {int a = 10, b = 3;printf("a+b=%d, a-b=%d\n", a+b, a-b); /* 13, 7 */printf("a*b=%d, a/b=%d\n", a*b, a/b); /* 30, 3（整數除法取整） */printf("a%%b=%d\n", a%b); /* 1（10%3=1） */
}init {run ArithmeticOps();
}
示例1-14：邏輯與比較操作符
proctype LogicOps() {int x = 5, y = 10;bool cond1 = (x > 0) && (y < 20); /* true */bool cond2 = (x == 5) || (y != 10); /* true */bool cond3 = !cond1; /* false */printf("cond1=%s, cond2=%s, cond3=%s\n", cond1 ? "true" : "false", cond2 ? "true" : "false", cond3 ? "true" : "false");
}init {run LogicOps();
}
示例1-15：表達式優先級
proctype PrecedenceDemo() {int a = 2, b = 3, c = 4;int res1 = a + b * c; /* 2 + (3*4)=14 */int res2 = (a + b) * c;/* (2+3)*4=20 */printf("res1=%d, res2=%d\n", res1, res2);
}init {run PrecedenceDemo();
}
關鍵說明：
- 整數除法
/會截斷小數部分（如10/3=3）。 - 邏輯操作符
&&和||支持短路求值，避免無效計算。
1.4.2 Local variables（局部變量）
PROMELA中變量分為全局變量（聲明在進程外）和局部變量（聲明在進程或init內），局部變量作用域限于所在進程。
示例1-16：全局變量與局部變量對比
int global_var = 10; /* 全局變量 */proctype LocalVarDemo() {int local_var = 20; /* 局部變量 */printf("全局變量: %d, 局部變量: %d\n", global_var, local_var);
}init {run LocalVarDemo();/* 無法訪問LocalVarDemo的local_var（作用域僅限該進程） */
}
示例1-17：局部變量的生命周期
proctype LifeCycleDemo() {int x = 0;x = x + 1; /* x=1 */printf("x=%d\n", x); /* 輸出1 */
} /* 進程結束，x被銷毀 */init {run LifeCycleDemo();run LifeCycleDemo(); /* 再次啟動進程，x重新初始化為0 */
}
示例1-18：同名變量覆蓋
int x = 100; /* 全局變量x */proctype ShadowDemo() {int x = 200; /* 局部變量x覆蓋全局變量 */printf("局部x: %d, 全局x: %d\n", x, ::x); /* ::x訪問全局變量 */
}init {run ShadowDemo();
}
關鍵說明：
- 全局變量可被所有進程訪問，局部變量僅所在進程可見。
- 使用
::x顯式訪問被局部變量覆蓋的全局變量（如示例1-18）。
1.4.3 Symbolic names（符號名）
通過#define定義常量，或typedef定義類型別名，提高代碼可讀性。
示例1-19：#define常量
#define MAX_USERS 10 /* 定義常量 */
#define PI 3.14 /* 注意：PROMELA不支持浮點數，此處僅為示例 */proctype DefineDemo() {int users = MAX_USERS;printf("最大用戶數: %d\n", users);
}init {run DefineDemo();
}
示例1-20：typedef類型別名
typedef Score int; /* 定義Score為int的別名 */proctype TypedefDemo() {Score math = 90; /* 等價于int math=90 */printf("數學成績: %d\n", math);
}init {run TypedefDemo();
}
示例1-21：符號名與枚舉結合
#define SUCCESS 0
#define FAIL 1
mtype { STATUS_SUCCESS=SUCCESS, STATUS_FAIL=FAIL }; /* 枚舉關聯常量 */proctype SymbolDemo() {int result = SUCCESS;if:: result == STATUS_SUCCESS -> printf("操作成功\n");:: result == STATUS_FAIL -> printf("操作失敗\n");fi;
}init {run SymbolDemo();
}
關鍵說明：
#define是預編譯指令，僅替換文本（需注意括號避免優先級問題，如#define ADD(a,b) (a+b)）。typedef用于創建類型別名，提高代碼可維護性。
1.5 Control statements（控制語句）
PROMELA的控制語句用于管理代碼執行順序，包括順序執行、分支（if/alt）、循環（do/for）等。
1.6 Selection statements（選擇語句）
PROMELA提供兩種選擇語句：if（非阻塞選擇）和alt（阻塞選擇），易混淆點在于分支條件不滿足時的行為。
1.6.1 if與alt的對比
| 語句 | 行為 | 示例 |
|---|---|---|
if | 若所有分支條件均不滿足，報錯（invalid end of if） | if :: cond -> ... fi |
alt | 若所有分支條件均不滿足，阻塞（等待條件變化） | alt :: cond -> ... od |
示例1-22：if語句（非阻塞）
proctype IfDemo() {int x = 5;if:: x > 10 -> printf("x>10\n"); /* 條件不滿足 */:: x < 3 -> printf("x<3\n"); /* 條件不滿足 */fi; /* 報錯：所有分支條件均不滿足 */
}init {run IfDemo();
}
示例1-23：alt語句（阻塞）
proctype AltDemo() {int x = 5;alt:: x > 10 -> printf("x>10\n"); /* 條件不滿足，阻塞 */:: x < 3 -> printf("x<3\n"); /* 條件不滿足，阻塞 */od; /* 程序卡住，等待x的值變化 */
}init {run AltDemo();
}
示例1-24：帶else的if語句
proctype IfElseDemo() {int x = 5;if:: x > 10 -> printf("x>10\n");:: else -> printf("x≤10\n"); /* else分支（所有其他情況） */fi; /* 輸出：x≤10 */
}init {run IfElseDemo();
}
關鍵說明：
if必須至少有一個分支條件滿足，否則SPIN會報錯（error: invalid end of if）。alt用于并發場景中等待條件滿足（如進程間同步），單獨使用可能導致死鎖。
1.6.2 Conditional expressions（條件表達式）
條件表達式是if/alt語句的核心，支持復雜邏輯組合。
示例1-25：多條件組合
proctype CondExprDemo() {int a = 5, b = 10;if:: (a > 0) && (b < 20) -> printf("條件1滿足\n"); /* true */:: (a == 5) || (b != 10) -> printf("條件2滿足\n"); /* true */fi; /* 隨機選擇一個滿足的分支執行 */
}init {run CondExprDemo();
}
示例1-26：基于變量的條件
proctype VarCondDemo() {int flag = rand() % 2; /* 0或1 */if:: flag == 0 -> printf("flag=0\n");:: flag == 1 -> printf("flag=1\n");fi;
}init {run VarCondDemo();
}
示例1-27：枚舉類型條件
mtype { ON, OFF };proctype MtypeCondDemo() {mtype state = ON;if:: state == ON -> printf("設備開啟\n");:: state == OFF -> printf("設備關閉\n");fi;
}init {run MtypeCondDemo();
}
1.7 Repetitive statements（重復語句）
PROMELA支持do（類似while）和for（計數循環）兩種循環結構。
1.7.1 do循環（無限循環）
do循環重復執行分支，直到break或所有分支條件不滿足（do無退出條件時會無限循環）。
示例1-28：簡單do循環
proctype DoLoopDemo() {int count = 0;do:: count < 3 -> printf("計數: %d\n", count);count++;:: else -> break; /* 退出循環 */od;
}init {run DoLoopDemo(); /* 輸出0,1,2 */
}
示例1-29：多分支do循環
proctype MultiBranchDo() {int x = 0;do:: x < 2 -> printf("x=%d（分支1）\n", x);x++;:: x >= 2 -> printf("x=%d（分支2）\n", x);break;od;
}init {run MultiBranchDo(); /* 輸出x=0（分支1），x=1（分支1），x=2（分支2） */
}
示例1-30：無退出條件的do循環（死鎖）
proctype InfiniteDo() {do:: true -> /* 永遠滿足 */printf("循環中...\n");od; /* 無限循環，SPIN模擬時需手動終止 */
}init {run InfiniteDo();
}
1.7.2 Counting loops（計數循環）
for循環用于已知次數的迭代，語法為for (init; cond; update) { ... }。
示例1-31：基本for循環
proctype ForLoopDemo() {int sum = 0;for (int i=1; i<=5; i++) { /* i從1到5 */sum += i;}printf("1+2+3+4+5=%d\n", sum); /* 輸出15 */
}init {run ForLoopDemo();
}
示例1-32：嵌套for循環
proctype NestedForDemo() {for (int i=1; i<=2; i++) {for (int j=1; j<=3; j++) {printf("i=%d, j=%d\n", i, j);}}
}init {run NestedForDemo(); /* 輸出i=1,j=1; i=1,j=2; ... i=2,j=3 */
}
示例1-33：for循環與break
proctype ForBreakDemo() {for (int i=1; i<=5; i++) {if (i == 3) {break; /* 退出循環 */}printf("i=%d\n", i); /* 輸出i=1,2 */}
}init {run ForBreakDemo();
}
關鍵說明：
do循環更靈活（支持多分支），for循環適合固定次數的迭代。- 避免在
for循環中修改循環變量（可能導致不可預期的行為）。
1.8 Jump statements（跳轉語句）
PROMELA支持break（退出循環）和goto（跳轉到標簽），需謹慎使用以避免代碼混亂。
示例1-34：break退出循環
proctype BreakDemo() {int i = 0;do:: i < 5 -> i++;if (i == 3) {break; /* 退出do循環 */}printf("i=%d\n", i); /* 輸出i=1,2 */od;
}init {run BreakDemo();
}
示例1-35：goto跳轉到標簽
proctype GotoDemo() {int x = 0;start: /* 標簽 */x++;if:: x < 3 -> printf("x=%d\n", x); /* 輸出x=1,2 */goto start; /* 跳轉回start標簽 */:: else -> printf("結束\n");fi;
}init {run GotoDemo();
}
示例1-36：goto跨循環跳轉
proctype GotoCrossLoop() {int i = 0, j = 0;outer: /* 外層循環標簽 */for (i=1; i<=2; i++) {for (j=1; j<=3; j++) {if (j == 2) {goto outer; /* 跳轉到外層循環 */}printf("i=%d, j=%d\n", i, j); /* 輸出i=1,j=1 */}}
}init {run GotoCrossLoop();
}
關鍵說明：
break僅退出當前最內層循環，goto可跳轉到任意標簽（包括循環外）。- 過度使用
goto會降低代碼可讀性，建議優先使用break或重構循環邏輯。
總結
本教程圍繞PROMELA順序編程的核心知識點，結合JSPIN工具演示了從基礎程序結構到控制語句的完整流程。通過30+示例代碼，你已掌握：
- PROMELA的進程定義與
init入口。 - 隨機模擬與非確定性行為。
- 數據類型、操作符與表達式的使用。
- 選擇語句（
if/alt）和循環語句（do/for）的區別。 - 跳轉語句（
break/goto）的應用場景。
后續可結合SPIN的模型檢查功能（如spin -a生成驗證代碼），進一步驗證并發系統的正確性。
