Question

I’m a beginner in Alloy (specification language) and need to do some further work based on a case study, which can be found here (code is on page 5). Relevant code:

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) }

在纠正一些辛塔克斯之后,我收到了这一错误信息:“这一表述没有被打上打字”,它突出了<代码>t in let t = T0/t.next。如何打字?

Answer 1

这里的错误是,下一个功能是T0提及的模块中的一种功能,因此,关于特许使用地的表述应为t.T0/next,而不是T0/t.next。但是,实际上,你不需要<代码>T0,因为Alloy可以确定哪些模块正在被提及。因此,仅删除所有提及<代码>T0之处,并应当汇编罚款。

另一种意见:你可以删除所有这些关联符号,使用暗中结合,撰写

{ A B C }

而不是<代码> A && B && C。

友情链接