Thank you for the prompt reply,
Based on your suggestions I’ve tried the following formula
(hope I didn’t miss any parenthesis now!)
Integrity == \forall u1 \in U:
(u1.st="terminated")~>(\E u2 \in U : u2.st="activated"
/\ u2.sid#u1.sid)
The same messages (TLC cannot handle the temporal formula) arises again.
Based on constants the temporal formula should goes like
this
Integrity == \forall
u1 \in U: (u1.st="terminated"/\u1.id=CONSTANT1)~>(\E u2 \in U :
u2.st="activated" /\ u2.sid#CONSTANT1)
Which is accepted by the TLC but it adds the additional
burden of checking the property for every constant id value utilized in the
specification.
If you have any other ideas, please share. Thank you again !