【SPIN】高级时序规范（SPIN学习系列--6）

时序操作符[]（总是）和 <>（最终）可应用于任何LTL公式，因此 []<><>A 和 <>[]<>(A ∧ []B) 在语法上是正确的。本书不涉及LTL的演绎理论（如公理、推理规则及公式的结合律、交换律等定理），仅提及两个结论：

• 连续出现的同名时序操作符序列可简化为单个操作符。例如，[] []<><>A 等价于 []<>A。
• 交替出现的 [] 和 <> 序列可简化为 []<>或 <>[] 两种双操作符组合之一。例如，<>[]<>A 等价于 []<>A。

因此，任意一元时序操作符序列均可简化为一个或两个操作符的序列。
接下来两个小节将介绍双操作符序列在表达常见正确性规范中的应用，随后是关于二元时序操作符U（直到）的讨论，最后介绍在SPIN中较少使用的“下一个”（X）操作符。
含超过两三个操作符的时序逻辑公式难以理解。堪萨斯州立大学开发了一套模式（patterns）帮助编写时序逻辑正确性规范，这些模式按优先级、存在性等属性及“之前”“之间”等作用域分类，不仅适用于SPIN的线性时序逻辑，也适用于其他验证逻辑。项目网站地址见附录B。

锁存（Latching）

公式 <>[]A 表示锁存属性：A在计算初始时可能为假，但最终变为真并保持为真。

状态序列：s0 s1 s2 s3 s4 s5 s6 s7  
A的取值：¬A  ¬A  A  A  A  A  A  A  

在s0状态，<>[]A为真：尽管s0和s1中A为假，但s2及之后所有状态A均为真。
锁存属性很重要，因为“初始且始终为真”的属性并不常见：通常需执行某些操作使属性为真，且一旦为真便持续为真。锁存也可描述异常情况，例如多处理器系统中若处理器故障，其变量自动置零。对清单5.1中的程序，可断言 <>failsQ → <>[]¬wantQ（若执行进程Q的处理器故障，wantQ将锁存为假）。由此可推导出：即使Q故障，进程P也不会饥饿，因为第7行的条件wantQ将始终为假，可执行第10行的else分支。

无限次出现（Infinitely Often）

公式 []<>A 表示A无限次为真：A无需始终为真，但在计算的任意状态s，A在s或之后某状态为真。

状态序列：s0 s1 s2 s3 s4 s5 s6 s7  
A的取值：¬A  ¬A  ¬A  A  ¬A  ¬A  ¬A  ¬A  

A在s3、s9、s15…等状态为真，因此对任意状态si，A必在si, si+1,…中某状态为真。
对临界区问题的解，活性（liveness）不仅指进程能进入临界区，还指能重复进入。在PROMELA中可如下建模：设置表示进程P在临界区的变量后，立即重置以表示离开临界区：

active proctype P() {do:: /* 尝试进入临界区 */csp = true;    // 进入临界区csp = false;   // 离开临界区od
}

若算法无饥饿，则可用时序公式 []<>csp 验证程序。

5.9.3 优先级（Precedence）

一元操作符 [] 和 <> 无法表达“时间先后”类属性（如A必须在B之前为真）。此类优先级属性可通过二元操作符U（直到，SPIN中写作U）表示为 ¬B U A，含义为“B保持为假，直到A变为真”。形式化定义：
在计算τ的状态si，p U q为真当且仅当存在k ≥ i，使得sk中q为真，且对所有i ≤ j < k，sj中p为真。
若si中q已为真，则第二个条件自动满足。
例1：在以下计算的s0状态，¬B U A为真，因B在A为假时保持为假，直到s4中A为真时B也为真。

状态：s0 s1 s2 s3 s4 s5  
A,B取值：¬A,¬B  ¬A,¬B  ¬A,¬B  ¬A,¬B  A,B  ¬A,B  

例2：即使s4后B仍为假，¬B U A在s0状态仍为真，因只需保证A首次为真前B为假。

状态：s0 s1 s2 s3 s4 s5  
A,B取值：¬A,¬B  ¬A,¬B  A,¬B  ¬A,¬B  ¬A,¬B  ¬A,¬B  

U称为“强直到”操作符，因要求右侧子公式最终为真。事实上，<>q 可定义为 true U q（因true恒真，true U q等价于q最终为真）。
弱直到操作符W不要求右侧子公式最终为真，二者关系为：

p U q ≡ p W q ∧ <>q，p W q ≡ p U q ∨[]p  

注意：SPIN不支持弱直到操作符W。
高级内容：V操作符
SPIN中的V操作符定义为 pVq ≡ !( (!p) U (!q) )，与W不同（若等价则应为 !( (!q) U (!p && !q) )）。

5.9.4 超越（Overtaking）

以Peterson算法（清单5.4）为例，演示用U操作符描述“一次有界超越”（one-bounded overtaking）：若进程P尝试进入临界区，进程Q最多可在P之前进入临界区一次。
定义符号：

#define ptry P@try   // P在尝试进入临界区
#define qcs Q@cs     // Q在临界区
#define pcs P@cs     // P在临界区

“一次有界超越”的LTL公式为：

[] ( ptry -> ( !qcs U ( qcs U (!qcs U pcs) ) ) )  

该嵌套U公式表示：当P尝试进入临界区（ptry为真）时，计算必须按以下顺序出现区间：
(a) Q不在临界区（!qcs）；
(b) Q在临界区（qcs）；
© Q再次不在临界区（!qcs）；
(d) 最终P进入临界区（pcs）。
根据U操作符定义，区间可空，但公式正确性保证在pcs为真前，qcs为真的区间最多出现一次。
对清单5.4的程序验证此公式，可证明“一次有界超越”成立。

清单5.4 Peterson算法

1 bool wantP, wantQ;
2 byte last = 1;
3 
4 active proctype P() {
5   do
6   :: wantP = true;       // P希望进入临界区
7      last = 1;           // 设置最后请求为P
8      try: (wantQ == false) || (last == 2); // 尝试进入（Q不希望进入 或 最后请求为Q）
9      cs: wantP = false;  // 离开临界区
10  od
11 }
12 
13 active proctype Q() {
14   do
15   :: wantQ = true;       // Q希望进入临界区
16      last = 2;           // 设置最后请求为Q
17      try: (wantP == false) || (last == 1); // 尝试进入（P不希望进入 或 最后请求为P）
18      cs: wantQ = false;  // 离开临界区
19  od
20 }

注意：SPIN中U操作符为左结合，而标准LTL中U为右结合（更符合区间序列语义）。为避免歧义，需大量使用括号！
高级内容：用弱直到实现有界超越
通常“一次有界超越”应用弱直到W验证（因进程可能不尝试进入临界区，qcs可能始终为假）。SPIN无W，故用U替代，验证仍有效（清单5.4的算法未建模“进程永远停留在非临界区”的场景）。

下一个（Next）

时序逻辑包含一元操作符X（下一个，SPIN中写作X），X A在状态si为真当且仅当si+1中A为真。X的局限性在于：

1. 并发系统抽象特性：并发/分布式系统通常不关注具体时间点（如客户端何时收到服务，只需保证“最终”而非“下一个状态”）。实时系统的时间建模见11.3和11.4节案例研究。
2. 抗颤动不变性（Stutter Invariance）：不含X的时序公式具有抗颤动性，即删除连续重复状态不影响公式真值。SPIN的部分序约简（partial order reduction）优化要求规范具有抗颤动性，而LTL公式自动满足这一点（SPIN警告信息提示：never断言需抗颤动，由LTL生成的断言天然满足）。

代码与知识点解析

1. 锁存属性（<>[]A）

• 作用：确保某属性最终稳定为真。
• 场景：故障处理（如变量锁存为特定值）、资源初始化完成后保持可用状态。
• PROMELA关联：通过状态标签（如cs）和远程引用（如P@cs）标记稳定状态，结合LTL公式 <> 验证。

2. 无限次出现（[]<>A）

• 作用：保证活性，如进程无限次进入临界区。
• 代码实现：

  active proctype P() {do:: csp = true;  // 进入临界区csp = false; // 离开临界区（允许重复进入）od
  }
  

  • 用LTL公式 []<>csp 验证csp无限次为真。

3. 强直到操作符U

• 语法：p U q，表示“p持续为真，直到q为真且q最终为真”。
• 应用场景：
  • 优先级：A必须在B前发生（¬B U A）。
  • 有界超越：嵌套U公式描述事件序列（如Q最多超越P一次）。
• SPIN注意事项：
  • 左结合性，需显式括号避免歧义。
  • 用U替代W时，需确保右侧条件最终成立（如算法保证进程会尝试进入临界区）。

4. Peterson算法与超越验证

• 算法逻辑：通过标志变量（wantP/wantQ）和last标记实现互斥，允许Q最多在P前进入临界区一次。
• 关键公式：

  [] (ptry -> (!qcs U (qcs U (!qcs U pcs))) )  
  

  • 含义：当P尝试进入（ptry），Q最多进入临界区一次（qcs出现一次），最终P进入（pcs）。
• 验证意义：确保公平性，避免某进程无限次被另一进程超越。

5. 抗颤动性与X操作符

• 抗颤动性：SPIN优化依赖规范不敏感于连续重复状态，LTL天然满足，而含X的公式可能不满足。
• X的局限性：仅用于精确时间建模（如实时系统），一般并发验证优先使用[]/<>/U。

总结

高级时序规范通过组合[]/<>/U操作符，可精确描述锁存、无限活性、优先级、有界超越等复杂属性。在SPIN中需注意操作符结合性、括号使用及抗颤动性要求，合理利用远程引用和进程变量引用，结合LTL公式完成正确性验证。