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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Sun, 22 Nov 2015 06:22:35 -0800 (PST)*References*: <ba346fe3-48a2-47ca-8185-d330f5566cfd@googlegroups.com> <11ae948d-cf1b-4518-bb1a-c1a7ac3b4e3d@googlegroups.com>

RE "subclassing" records, I have found a way to do it which doesn't cause TLC to enumerate any sets. The approach has some downsides, but it's nice enough to be useful, so I'm posting it here:

The downside is that it requires abandoning the [f1 : s1, f2 : s2] syntax, and that handling sequences requires another definition.

On Wednesday, October 28, 2015 at 1:33:30 PM UTC+2, Ron Pressler wrote:

Is(r, types) ==

\A type \in types :

/\ DOMAIN type \subseteq DOMAIN r

/\ \A f \in DOMAIN type: r[f] \in type[f]

(other variations are possible, such as taking a set of "types" rather than one)

And then:

HeaderT == [from |-> STRING

id |-> Nat]

DataT == {HeaderT,

[data |-> A]}

TypeOK == Is(data, DataT)

Ron

On Wednesday, October 28, 2015 at 1:33:30 PM UTC+2, Ron Pressler wrote:

Thanks, Stephan!2. Right... So simple... <facepalm>1 + 3: Sure, I was just wondering if there perhaps was a better way I missed. Future improvements, perhaps?Ron

On Wednesday, October 28, 2015 at 1:14:32 PM UTC+2, Ron Pressler wrote:Hi.1. "Subclassing"/composing recordsIs 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.

Ron

**References**:**Three questions***From:*Ron Pressler

**Re: Three questions***From:*Ron Pressler

- Prev by Date:
**Re: The implementation of records and functions in TLC** - Next by Date:
**Assuming a contiguous subset of Nat** - Previous by thread:
**Re: Three questions** - Next by thread:
**a question about WF** - Index(es):