[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLC cannot handle the temporal formula

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 !