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

Re: [tlaplus] Three questions

Hi Ron,

1. I don't know of a non-hackish way of doing what you want to achieve, but how many different record types do you have? Would it be an option to define the sets of fields as separate operators, e.g.

RecordFieldsA == {"foo", "bar"}
RecordFieldsB == {"foo", "bar", "baz"}

and work from there? (Alternatively, you could define a prototype record of each type and take its DOMAIN.)

2. TLC can check formulas of the form [][A]_v, which is at the basis of checking refinement. So yes, you can check the formula [][~B]_v in order to find out if action B is never taken.

3. No, there is no more concise way to write this. Set comprehensions must be written in one of the two syntactic forms

  { pattern \in S : predicate }    or    { _expression_ : pattern \in S }

so the form that you want is not syntactically correct.


On 28 Oct 2015, at 12:14, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:


1. "Subclassing"/composing records

Is there a way to represent record composition (or subclassing) -- e.g. to have a header reused by several message record "types" (i.e. sets of the form [field1 : ..., field2: ...]) -- that's efficient in TLC? I've tried:

    LOCAL Fields(type) == DOMAIN CHOOSE x \in type : TRUE

    Project(r, type) == [f \in Fields(type) |-> r[f]]

    IsInstance(r, types) == \A type \in types : Project(r, type) \in type

    \* Same as TLC's @@ operator

    Build(r1, r2) == [f \in DOMAIN r1 \cup DOMAIN r2 |-> IF f \in DOMAIN r2 THEN r2[f] ELSE r1[f]]

But aside from Build (TLC's @@), everything else requires an element in the set to get the domain (found by CHOOSE : TRUE), and performing CHOOSE requires enumerating the set, which is something I'd like to avoid.

2. Transition (action) invariants

TLC allows checking invariants in the form of state predicates, or liveness properties in the form of temporal formulas that may specify actions or subactions (e.g. <><A>_var). Can TLC check "action invariants", e.g.  \A x \in {1,2,3} : ~A(k)   ? My intention is to check whether the action (or subaction) A(x) for those particular values of x is ever taken. I don't mean checking if A(x) is ENABLED, but actually taken (i.e., the primed variables are taken into account)

3. Can the _expression_ { <<x, y>> \in { <<x, y>> : x \in 1..3, y \in 2..7 } : y <= x } be written more concisely? I've tried { <<x, y>>  : x \in 1..3, y \in 2..7 : y <= x }, but that doesn't work.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.