在第 n 级显示迹线名称

Question

问题

使用 CLI 时，如何让它在发生错误时显示第 n 级操作跟踪名称（和符号参数名称）？

命令：

java -jar tla2tools.jar Test.tla

正常

例如，与：

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

显示：

状态1：
...
状态 2：<BuyComputer 第 15 行，第 5 列到第 15 行，模块测试的第 23 列>
...
状态 3：<BuyHouse 第 17 行，第 3 列到第 17 行，模块测试的第 55 列>
...

有条件

and with（如果总成本大于 100，则不访问状态）：

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

显示：

状态1：
...
状态 2：<Action 第 15 行，第 5 列到第 15 行，模块测试的第 23 列>
...
状态 3：<Action 第 17 行，第 3 列到第 17 行，模块测试的第 55 列>
...

Action

应该是

BuyComputer

和

BuyHouse

。

有条件需要

状态1：
...
状态 2：<BuyComputer(Me) 第 15 行，第 5 列到第 15 行，模块测试的第 23 列>
...
状态 3：<BuyHouse(Neighbour) 第 17 行，第 3 栏到第 17 行，模块测试的第 55 栏>
...

具有定义为

BuyComputer(who) == ...

和

BuyHouse(who) == ...

的功能。

为什么

我正在尝试减少我知道不会导致错误的已访问状态的数量。 在这种情况下，它是

cost > 100

的时候。我还想要动作名称而不是“未命名动作”以便于调试。

Answer 1

抱歉在评论中误导了你——我后来才意识到，你想要跟踪中的动作名称。据我所知，只有当 Next 是运算符定义的析取时，这才有效。我刚刚做了一个小玩具示例：

EXTENDS Naturals, TLAPS

VARIABLES x, y

Init == x = 0 /\ y = 0
AddOne(v, w) == v' = v + 1 /\ w' = w + 1
AddTwo(v, w) == v' = v + 2 /\ w' = w + 1
Next == AddOne(y,x) \/ AddTwo(y,x)

Spec == Init /\ [][Next]_<<x,y>> /\ WF_x(Next)

INV == x \in 2 .. 5 => y < 6

我假设

Next

的公平性较弱，以避免无限的口吃痕迹。我还明确地为不变量添加了定义

INV

，这样更容易进入模型检查属性。变量

y

可能会增加一到两个，而

x

只是跟踪所采取的步数。

与其修改 Next，不如将条件放入不变量中进行检查。显然，

y < 6

总是在六步之后失效。但是由于不变量被

x \in 2 .. 5

保护，它必须在该步数中无效。由于 Next 没有被更改，因此跟踪中的操作按预期发生：

Invariant INV is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ x = 0
/\ y = 0
2: <AddTwo line 10, col 24 to line 10, col 34 of module Distance2>
/\ x = 1
/\ y = 2
3: <AddTwo line 10, col 24 to line 10, col 34 of module Distance2>
/\ x = 2
/\ y = 4
4: <AddTwo line 10, col 24 to line 10, col 34 of module Distance2>
/\ x = 3
/\ y = 6

这就是你想解决的问题吗？在我看来，将条件放入不变量中也更好，因为规范是未修改的。否则，不清楚修改是否会导致特定的安全属性违规。

编辑：由于我们要减少状态，所以我们需要更改Next。我引入了一个谓词

Limit(P,N)

，它将

Next

的应用限制在

x < N

.

的情况下

Limit(P, N) == (x < N) /\ P
Spec2 == Init /\ [][Limit(Next, 4)]_<<x,y>> /\ WF_x(Next)

模型检查

Spec

发现跟踪访问 22 个状态（16 个不同），模型检查

Spec2

访问 18 个状态（13 个不同）。我希望那些是 x 为 4 或更大的状态。

Edit2：如果你想要跟踪中的名称，你需要添加可以在跟踪中命名的定义。例如：

LAddOne(v,w) == Limit(AddOne(v,w),4) 
LAddTwo(v,w) == Limit(AddTwo(v,w),4)
LNothing == x >= 5 /\ UNCHANGED <<x,y>>

Next3 == LAddOne(y,x) \/ LAddTwo(y,x) \/ LNothing
Spec3 == Init /\ [][Next3]_<<x,y>> /\ WF_x(Next)

Spec 和 Spec2 中还有一个错误，我们只有

[][Next]_x

而不是

[][Next]_<<x,y>>

在某些情况下导致非自愿死锁。我修好了。