# TLC cannot handle the temporal formula

• From: Christos Grompanopoulos <gro...@xxxxxxxxx>
• Date: Tue, 23 Jul 2013 00:23:57 -0700 (PDT)

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:

• id - identity unique for each entity
• st the accomplishment status.

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?