【SPIN】PROMELA数据与程序结构详解（SPIN学习系列--7）
PROMELA是专为系统建模设计的语言，而非实现可执行程序。其模型通常较小，便于通过状态空间搜索验证正确性。尽管模型可能仅含少量变量和语句，但行为复杂，需SPIN进行模型检查。因此，PROMELA未提供函数、类等大型程序结构，而是通过数组、类型定义、宏和内联声明实现数据和代码组织。
1 数组（Arrays）
PROMELA的数组与C语言类似，是同类型数据的有序序列，通过索引（从0开始）访问元素，越界会在仿真和验证时报错。
核心知识点：
- 一维数组：PROMELA仅支持一维数组，二维数组需通过类型定义模拟。
- 初始化方式：
- 直接赋值：
int a[5] = {0, 10, 20, 30, 40};（需逐个元素赋值）。 - 循环初始化：
for (j, 0, 4) a[j] = j * 10; // 顺序赋值 rof (j); - 非确定性初始化：
for (j, 0, 4) if :: a[j] = j * 10 :: a[j] = j + 5 fi; // 随机选择赋值 rof (j); - 全局初始化：
int a[5] = 10;（所有元素初始化为10）。
- 直接赋值：
- 内存注意：
bit或bool类型数组实际存储为byte，大数组可通过位运算压缩内存。
代码示例：
#include "for.h" // 引入循环宏
active proctype P() {int a[5]; // 声明长度为5的整型数组a[0] = 0; a[1] = 10; a[2] = 20; a[3] = 30; a[4] = 40; // 逐个赋值int sum = 0; // 累加器for (i, 0, 4) // 循环变量i从0到4（for宏展开为循环结构）sum = sum + a[i]; // 累加数组元素rof (i); // for循环结束（宏展开包含i++）printf("The sum of the numbers = %d\n", sum); // 输出结果
}
2 类型定义（Type Definitions）
通过typedef定义复合类型，主要用于消息结构定义，也可模拟多维数组。
核心知识点：
- 消息结构定义：
typedef MESSAGE { // 定义消息类型mtype message; // 消息类型byte source; // 源地址byte destination; // 目标地址bool urgent; // 紧急标志 } - 模拟二维数组：
typedef VECTOR { // 定义一维数组类型int vector[10]; // 每个元素是长度为10的数组 } VECTOR matrix[5]; // 二维数组：5行，每行是VECTOR类型 matrix[3].vector[6] = matrix[4].vector[7]; // 访问元素（行3列6 = 行4列7） - 稀疏数组实现：
- 用结构体存储非零元素的行、列、值，节省内存。
- 嵌套循环遍历行列，输出矩阵（非零元素按字典序存储）。
代码示例：
typedef ENTRY { // 稀疏数组元素类型byte row; // 行号byte col; // 列号int value; // 值
}
ENTRY a[N]; // 长度为N的ENTRY数组（存储非零元素）// 初始化非零元素（逐个字段赋值）
a[0].row = 0; a[0].col = 1; a[0].value = -5;
a[1].row = 0; a[1].col = 3; a[1].value = 8;// 打印矩阵（嵌套循环遍历行列）
for (r, 0, N-1) // 行循环for (c, 0, N-1) { // 列循环if (i == N) // 所有非零元素已输出，补0printf("0 ");else if (r == a[i].row && c == a[i].col) { // 匹配行列，输出值printf("%d ", a[i].value);i++; // 移动到下一个非零元素} else // 不匹配，补0printf("0 ");}
3 预处理器（The Preprocessor）
SPIN基于C语言实现，预处理器负责文件包含、宏定义和条件编译，处理纯文本替换，不解析语言语法。
核心知识点：
- 文件包含：
#include "for.h"引入循环宏定义文件。 - 符号定义：
- 常量定义：
#define N 4（编译时替换为4，不占内存）。 - 表达式定义：
#define mutex (critical <= 1)（用于正确性验证）。
- 常量定义：
- 条件编译：
- 通过
#ifdef根据宏定义选择代码分支：#ifdef VerOnecurrentPriority = (p1 > p2 -> p1 : p2); // 版本1逻辑 #elif defined(VerTwo)currentPriority = PMAX; // 版本2逻辑 #elsecurrentPriority = PMIN; // 默认逻辑 #endif - 命令行定义宏：
spin -DVerTwo pri.pml（无需修改代码）。
- 通过
- 宏定义：
- 带参数宏（如循环宏）：
#define for(I,low,high) \ // 反斜杠表示换行续接byte I; I = low; do \ // 声明变量I，初始化:: (I > high) -> break \ // 终止条件:: else -> // 循环体开始 #define rof(I) ; I++; od // 循环体结束，I自增 - 注意参数副作用：避免传递
j+1等表达式作为参数，会导致语法错误。
- 带参数宏（如循环宏）：
4 内联声明（Inline）
通过inline为语句序列命名，实现代码重用，类似C语言的宏，但语法更友好。
核心知识点：
- 基本用法：
inline write(ar) { // 定义内联函数，参数ar为数组名d_step { // d_step表示确定执行的步骤for (k, 0, N-1) // 循环打印数组元素printf("%d ", ar[k]);printf("\n");} } // 使用内联：write(a); // 编译时替换为内联体，ar替换为a - 参数传递：纯文本替换，无类型检查，需确保参数合法。
- 作用域问题：内联体内声明的变量（如
k）会与调用处变量冲突，需避免重复声明。 - 与宏的区别：无需反斜杠续接，错误提示指向内联定义行，而非调用行。
代码示例：
inline initEntry(I, R, C, V) { // 初始化稀疏数组元素的内联a[I].row = R; // 设置行号a[I].col = C; // 设置列号a[I].value = V; // 设置值
}
// 使用内联初始化
initEntry(0, 0, 1, -5); // 等价于a[0].row=0; a[0].col=1; a[0].value=-5;
总结
PROMELA通过数组实现数据结构化，类型定义扩展复合数据类型，预处理器和内联声明提升代码可读性和可维护性。尽管缺乏高级程序结构，这些特性足以建模复杂并发系统。需注意数组越界、类型定义的内存占用、宏和内联的文本替换副作用，确保模型的正确性和验证效率。
for.h 作为 PROMELA 的头文件，通常用于定义 循环宏（Loop Macros），简化计数循环的编写。以下是其可能的内容及解析：
附：for.h 典型实现
// for.h：定义计数循环的宏（类似 C 语言的 for 循环）
#define for(var, start, end) \ // 宏名 for，参数：循环变量var、起始值start、结束值endbyte var; \ // 声明字节类型的循环变量（PROMELA中常用byte表示整数索引）var = (start); \ // 初始化变量为起始值do \ // 进入do-od循环结构:: (var > (end)) -> break // 终止条件：若var超过end，跳出循环:: else -> // 否则执行循环体
#define rof(var) \ // 宏名 rof（for 倒写），结束循环; var++ \ // 循环变量自增od // do-od循环结束