如何在TLA+和TLC中正确实现模块的批量实例化？

问题背景 #

在TLA+中需要多次实例化同一模块（如多节点通信网络场景），但传统手动实例化的写法每次修改节点数量都要手动调整组合模块的Init和Next动作，无法实现通用化。

基础模块示例：single #

单个节点的核心逻辑，封装状态变量v及其初始状态和转移规则：

---- MODULE single ----
VARIABLE v

Init == v = 0

Next == v = 0 /\ v' = 1

Spec == Init /\ [][Next]_v
====

手动实例化的可行版本：concurrent_a #

手动实例化两次single模块，可正常运行，但新增节点时需修改Init和Next：

---- MODULE concurrent_a ----
VARIABLES
    a, b

A == INSTANCE single WITH v <- a
B == INSTANCE single WITH v <- b

Init == A!Init /\ B!Init
 
Next == [A!Next]_a /\ [B!Next]_b 

Spec == Init /\ [][Next]_<<a, b>>
====

尝试通用化的错误版本：concurrent_err #

试图用量化表达式动态实例化模块，但TLC报错：

---- MODULE concurrent_err ----
VARIABLES
    a, b, c, d

vars == <<a, b, c, d>> \* For usage in the next-state relation
Vars == {a, b, c, d} \* For quantification

N(v) == INSTANCE single

Init == \A v \in Vars: N(v)!Init
 
Next == \A v \in Vars: [N(v)!Next]_v 

Spec == Init /\ [][Next]_Vars
====

TLC报错信息 #

[...]
Computing initial states...
Error: In evaluation, the identifier a is either undefined or not an operator.
line 6, col 10 to line 6, col 10 of module concurrent
Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 10, column 9 to line 10, column 32 in concurrent
1. Line 10, column 18 to line 10, column 21 in concurrent
2. Line 6, column 9 to line 6, column 20 in concurrent
3. Line 6, column 10 to line 6, column 10 in concurrent


0 states generated, 0 distinct states found, 0 states left on queue.

错误原因 #

TLA+的INSTANCE是静态语义，只能在编译阶段绑定变量，无法在量化表达式中动态传递变量标识符。你试图将变量标识符（如a）作为值传入INSTANCE绑定，但TLA+中变量标识符和变量值是完全独立的概念，TLC无法在运行时解析这种动态生成的实例绑定。

通用化解决方案 #

正确的做法是用数组变量统一管理所有节点状态，通过静态索引实例化模块，完全避免手动修改Init和Next动作。

1. 优化基础模块（可选，增强灵活性） #

为single模块添加可选的nodeId常量，用于区分不同节点：

---- MODULE single ----
CONSTANT nodeId  \* 可选，用于日志或节点区分
VARIABLE v

Init == v = 0

Next == v = 0 /\ v' = 1

Spec == Init /\ [][Next]_v
====

2. 通用化组合模块：concurrent_general #

通过常量NumNodes指定节点数量，数组nodes存储所有节点状态，无需修改模块代码即可调整节点数：

---- MODULE concurrent_general ----
CONSTANT NumNodes  \* 节点数量，在模型配置中修改即可
VARIABLE nodes  \* 数组，nodes[i]表示第i个节点的状态（索引范围1..NumNodes）

\* 为每个节点索引静态实例化single模块
Node(i) == INSTANCE single WITH v <- nodes[i], nodeId <- i

\* 初始状态：所有节点满足single模块的初始条件
Init == \A i \in 1..NumNodes: Node(i)!Init

\* 下一步状态：任意一个节点执行其状态转移，或允许无动作（stuttering）
Next == \E i \in 1..NumNodes: [Node(i)!Next]_nodes
          \/ [][TRUE]_nodes  \* 可选：允许系统无动作的stuttering步骤

\* 整体规格
Spec == Init /\ [][Next]_nodes
====

核心优势 #

• 完全通用：只需在模型配置中修改NumNodes常量的值，即可调整节点数量，无需修改模块代码
• 符合TLA+语义：通过索引静态绑定数组元素，规避了动态实例化的语义限制
• 可扩展性强：数组方式天然支持任意数量的节点，无需手动添加变量

备选方案（宏定义，兼容性用） #

如果需要保留多个独立变量的写法（不推荐），可使用TLA+ Toolbox的预处理器宏简化重复代码，但仍需手动添加变量：

---- MODULE concurrent_macro ----
CONSTANT NumNodes
VARIABLES a, b, c, d  \* 需手动添加变量以支持更多节点

\* 预处理器宏生成Init和Next
DEFINE InitMacro == /\ a=0 /\ b=0 /\ c=0 /\ d=0
DEFINE NextMacro == [][(a=0/\a'=1) \/ (b=0/\b'=1) \/ (c=0/\c'=1) \/ (d=0/\d'=1)]_<<a,b,c,d>>

Spec == InitMacro /\ NextMacro
====

内容的提问来源于stack exchange，提问作者naumb