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, Stephan On Jul 23, 2013, at 9:23 AM, Christos Grompanopoulos <gro...@xxxxxxxxx> wrote:
|