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配置） | -2³¹ ~ 2³¹-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生成验证代码），进一步验证并发系统的正确性。
