使用TLA+ CLI时，报错如何显示第n层动作追踪名及符号参数名？

使用TLA+ CLI工具时，如何在添加状态过滤条件后，仍能在错误追踪中显示第n层动作的名称及符号参数？
执行命令：java -jar tla2tools.jar Test.tla

正常情况 #

当Spec定义为：

Spec == Init /\ [][Next]_<<AllStates>>

模型检查器的输出会正确显示动作名称：

State 1: <Initial predicate>
...
State 2: <BuyComputer line 15, col 5 to line 15, col 23 of module Test>
...
State 3: <BuyHouse line 17, col 3 to line 17, col 55 of module Test>
...

添加过滤条件后的问题 #

当为了减少不必要的状态访问，给Next动作添加成本过滤条件后：

Spec == Init /\ [][Next /\ ((cost' > 100) => UNCHANGED <<AllStates>>)]_<<AllStates>>

输出中的动作名称会被替换为通用的Action，丢失了原有的动作标识：

State 1: <Initial predicate>
...
State 2: <Action line 15, col 5 to line 15, col 23 of module Test>
...
State 3: <Action line 17, col 3 to line 17, col 55 of module Test>
...

期望输出 #

希望过滤状态的同时，仍能显示具体动作名称及参数：

State 1: <Initial predicate>
...
State 2: <BuyComputer(Me) line 15, col 5 to line 15, col 23 of module Test>
...
State 3: <BuyHouse(Neighbour) line 17, col 3 to line 17, col 55 of module Test>
...

其中动作定义为BuyComputer(who) == ...和BuyHouse(who) == ...。

需求背景 #

需要过滤掉cost > 100的无效状态以提升检查效率，同时保留动作名称便于调试错误。

1. 将过滤逻辑嵌入具体动作定义 #

不要直接修改Next的合取表达式，而是把成本检查逻辑放到每个具体动作内部，让模型检查器仍能识别独立的动作名称：

BuyComputer(who) == 
    IF cost + ComputerCost > 100 THEN
        UNCHANGED <<AllStates>>  // 成本超支时保持状态不变
    ELSE
        /\ cost' = cost + ComputerCost
        /\ ... 原有动作逻辑 ...

BuyHouse(who) == 
    IF cost + HouseCost > 100 THEN
        UNCHANGED <<AllStates>>
    ELSE
        /\ cost' = cost + HouseCost
        /\ ... 原有动作逻辑 ...

// 保持Next和Spec的原有结构
Next == \/ BuyComputer(Me)
         \/ BuyHouse(Neighbour)
Spec == Init /\ [][Next]_<<AllStates>>

2. 使用动作Guard条件过滤 #

另一种方式是给每个动作添加前置Guard，仅当成本符合要求时才允许动作执行：

BuyComputer(who) == 
    /\ cost + ComputerCost ≤ 100  // 前置Guard，过滤超支情况
    /\ cost' = cost + ComputerCost
    /\ ... 原有动作逻辑 ...

BuyHouse(who) == 
    /\ cost + HouseCost ≤ 100
    /\ cost' = cost + HouseCost
    /\ ... 原有动作逻辑 ...

Next == \/ BuyComputer(Me)
         \/ BuyHouse(Neighbour)
Spec == Init /\ [][Next]_<<AllStates>>

3. 确保工具版本支持参数化动作追踪 #

如果仍无法显示参数名称，确认使用的tla2tools.jar是较新版本（v1.5+以上），旧版本对带参数的动作追踪支持有限。

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