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

Re: [tlaplus] TLC cannot handle the temporal formula

Hello Christos,

the temporal formulas that TLC can handle are described in section 14.2.4 of Specifying Systems.

In your examples I believe that TLC chokes because you quantify over the elements of a variable (the section mentioned above is not very clear on what kinds of quantification are allowed but seems to imply that any quantifiers that arise must be transformable to explicit conjunction and disjunction). Observe by the way that the first formula that you describe is not well-formed (there are more closing than opening parentheses, also, the bound variables u1 and u2 are used outside of the scope of the quantifier, and there is a u that is not bound anywhere).

I'd recommend that you quantify over constants. I'm assuming that the potential elements of U are all values in a constant set Entities (that you can define as a set of records with the relevant fields taken in the set of identifies and statuses); you can then write formulas such as

A e1 \in Entities : (e1 \in U /\ e1.st = "terminated") ~> (\E e2 \in Entities : e2 \in U /\ e2 # e1 /\ e2.st = "activated")

In order for this to work, the set Entities must be explicitly enumerable and small.

Hope this helps,

On Jul 23, 2013, at 9:23 AM, Christos Grompanopoulos <gro...@xxxxxxxxx> wrote:

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?