【SPIN】PROMELA语言编程入门基础语法（SPIN学习系列--1）

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工具）：

1. 打开JSPIN，新建文件并输入上述代码，保存为hello.pml。
2. 点击Verify → Parse检查语法（无错误则显示Parsing completed）。
3. 点击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生成验证代码），进一步验证并发系统的正确性。