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?