合金表达式未能被识别

Question

我是合金（规范语言）的初学者，需要根据案例研究做一些进一步的工作，可以找到here（代码在第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) } 

纠正一些语法后，我收到此错误信息：“这种表达未能被typechecked”，它凸显了let t' = T0/t.nextt'。我如何检查t'？

Answer 1

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

另一评论：您可以删除所有这些共同的符号，并使用隐式相结合，撰写

{ A B C } 

，而不是A && B && C。