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

TLC cannot handle the temporal formula

Hello to everyone in this group!

During the development of a TLA+ specification the following problem was emerged.

The specification utilizes a single variable U that represents a set of entities u, while each entity is a record with fields:

The property that must be evaluated states there is no entity which transits from “terminated” to “requested” state.  

Integrity ==  (\E u1 \in U: u.st=”terminated”)~>(\E u2 \in U:u2.st=”activated”) ) /\ u1.id#u2.id)

However TLC states that it cannot handle this formula. The same with the following attempt

Integrity == \forall u1, u2 \in U :  (( u1.st=”terminated” ) ~> (u2.st=”activated”)) /\ ( u1.id # u2.id))

Any suggestions?