CODEWITHSUNDEEP
logicmodelingspecificationsfirst-order-logicalloy
gorn
gorn

Reputation: 8177

Alloy expression failed to be typechecked

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

After correcting some syntax, I get this error message: “This expression failed to be typechecked”, and it highlights t' in let t' = T0/t.next. How do I typecheck t'?

Upvotes: 1

Views: 628

Answers (1)

Daniel
Daniel

Reputation: 66

The error here is that next is a function in the module referred to by the alias T0, so the expression on the RHS of the let binding should be t.T0/next and not T0/t.next. But actually you don't need the T0 anyway, since Alloy can determine which module is being referred to. So just remove all references to T0 and it should compile fine.

Another comment: you can remove all those conjunction symbols and use implicit conjunction, writing 

{ A B C }

instead of A && B && C.

Upvotes: 5

Related Questions