Re: [tlaplus] TLC cannot handle the temporal formula

Not sure I understand your reply. From what you told us before, U was a VARIABLE, and I suggested to restrict to quantification over sets E where E is a constant _expression_ (i.e., containing no state variable). Obviously, this will require TLC to enumerate all values contained in E, so in practice you have to ensure that E is sufficiently small.

On Jul 24, 2013, at 10:50 AM, Christos Grompanopoulos <gro...@xxxxxxxxx> wrote:

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 !