合金表达式类型检查失败

Question

我是Alloy(规范语言)的初学者，需要根据案例研究做一些进一步的工作，可以在这里找到(代码在第5页)。相关代码:

open util/ordering[Time] as T0
pred Eavesdropping() {   
  some pro:Process | some m:Protected_Msg |  
  some t: (Time - T0/last) - T0/prev[T0/last] |   let t' = T0/t.next |
  let t'' = T0/t'.next |   !HasReadAccess[pro,m] && (m->t in pro.knows)
  &&   (m.contents->t not in pro.knows) &&   (m.contents->t'' in
  pro.knows) && IsUnique(m.contents) }

在纠正了一些语法之后，我得到了这个错误消息:" this expression failed to be typecchecked "，并且在let t' = T0/t.next中突出显示了t'。如何对t'进行类型检查

Answer 1

这里的错误是next是别名T0引用的模块中的函数，因此let绑定的RHS上的表达式应该是t.T0/next而不是T0/t.next。但实际上你不需要T0，因为Alloy可以确定哪个模块被引用。所以只要删除所有对T0的引用，它应该可以正常编译。

另一个注释:你可以删除所有的连接符号，使用隐式连接，写

{ A B C }

代替A && B && C