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 !