How to type EXCEPT construction

[timimin]

Hi, I'm trying to enhance performance of invariant safety checking in my project with apalache. Gradually I'm supplying my specs with type annotations. As far as i understand we must add type annotations to most of standard functions we use (i.e. from Sequences spec). I faced a strange type errors while checking a spec with EXCEPT construction.

Say we have :

call (id, exprs) ==
   /\ Sessions' = 
             [
			 Sessions EXCEPT 
			 ![id].SessionM = exprs 
             ] 

where id is of type U, Sessions is of type SESSIONS and ![id].SessionM, exprs are of type Seq(POLICY)

The type checker says:

[RuntimeFS.tla:174:32-174:39]: Need annotation. Found 2 matching operator signatures ((Str, a1333) => (Str -> a1333)) or ((Str, a1333) => [SessionM: a1333]) for arguments Str and a3388 E@12:26:09.934
[RuntimeFS.tla:174:28-174:29]: Need annotation. Found 2 matching operator signatures ((a1334, a1335) => (a1334 -> a1335)) or ((Int, a1334) => Seq(a1334)) for arguments a3386 and a3389 E@12:26:09.960
[RuntimeFS.tla:169:1-175:14]: Error when computing the type of call E@12:26:09.987

So what annotation i need to add to fix it?

[konnov]

Hi @timimin,

These messages can be hard to understand. Basically, what the type checker is complaining about is that it does not know, whether Sessions[id] is a function of strings to something, that is, (Str -> a1333), or it is a record that has SessionM as a field. Most likely, the type checker does not see the annotation of Sessions. That happens sometimes, because the type checker gets the annotations as comments from the SANY parser.

How do you annotate Sessions?

[timimin]

Ooo...
Session[id] is a record. Annotations for Sessions and its components are in the extended module and look like the following...

\* @typeAlias: SESM  = Seq(POLICY); 
\* @typeAlias: PCLAB = Seq(POLICY); 
\* @typeAlias: RET   = Seq(POLICY); 
\* @typeAlias: SREGS = <<[pc: <<Str, Str>>, fp: Int]>>; 
\* @typeAlias: SESSIONS = U -> [SessionM: SESM, PCLabel: PCLAB, Ret: RET, StateRegs: SREGS];

\* @type: SESSIONS;
		  Sessions,  (******************************************************)
                     (* Sessions environment.  Maps user sessions to       *)
                     (* respective buffers.                                *)
                     (******************************************************)

Seems that it handles Sessions annotations right.
If i rewrite the operator definition to

call (id, exprs) ==

   /\   Sessions' = 
                  [u \in U |-> CASE u = id -> 
                                        [SessionM |-> exprs, PCLabel |-> Sessions[u].PCLabel,
					 Ret |-> Sessions[u].Ret, StateRegs |-> Sessions[u].StateRegs]
				    [] OTHER    -> 
				        [SessionM |-> Sessions[u].SessionM, PCLabel |-> Sessions[u].PCLabel,
					 Ret |-> Sessions[u].Ret, StateRegs |-> Sessions[u].StateRegs]
			      ]

it does not complain...

[timimin]

)
Now if i switch back to

call (id, exprs) ==
   /\ Sessions' = 
             [
			 Sessions EXCEPT 
			 ![id].SessionM = exprs 
             ] 

it works... May be i had to recompile the extended module.

Thanks.