Checking whether something is a record or a set?

[Jaak Ristioja]

Hello!

Is it possible in TLA+ to check whether something is a record or set?
For example:

Invariant == isRecord(myRecord) /\ isSet(someVariable.mySet)


Best regards,
Jaak

[Stephan Merz]

Hello Jaak,

semantically, any value in TLA+ is a set, so isSet(x) would always return TRUE. (TLC optimizes its representation of values and will complain if you, say, use a number as a set as in the predicate "0 \in 2" – note that TLA+ leaves the semantics of this formula undefined.)

You can define the predicate

IsRecord(r) ==
/\ DOMAIN r \subseteq STRING
/\ r = [ fld \in DOMAIN r |-> r[fld] ]

but in practice one tends to be more interested in checking if a record is an element of a particular set of records.

Best,
Stephan

> --
> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Jaak Ristioja]

So, TLC also optimizes sets and record? Because one cannot take the
element of a record, e.g. \E e \in record: Print(e, TRUE) yields in
"java.lang.RuntimeException: TLC encountered a non-enumerable quantifier
bound [answer |-> 42]."

So I guess the question is really whether it is possible in TLC to check
whether something is a record or a set, e.g.:

IF isRecord(r) THEN (* handle record *) ELSE (* handle set *)


Jaak

[Stephan Merz]

> On 12 Nov 2015, at 10:00, Jaak Ristioja <jaak.r...@cyber.ee> wrote:
>
> So, TLC also optimizes sets and record?

That's correct. In fact, TLA+ does not specify how functions (and thus records) are represented as sets. That's different from standard Zermelo-Fraenkel set theory where functions are sets of ordered pairs (argument, result).

> Because one cannot take the
> element of a record, e.g. \E e \in record: Print(e, TRUE) yields in
> "java.lang.RuntimeException: TLC encountered a non-enumerable quantifier
> bound [answer |-> 42]."

What would you expect as a result? Your formula looks strange to me. If you want to print the entire record, you'd write Print(record, TRUE). If you want to print some record from a set of records, you might write \E e \in records : Print(e, TRUE). If you want to print some record field, you might write \E fld \in DOMAIN record : Print(record[fld], TRUE).

(But in fact, in both these cases, writing a CHOOSE expression would be clearer, although you have to handle the case of the empty set separately.)

> So I guess the question is really whether it is possible in TLC to check
> whether something is a record or a set, e.g.:
>
> IF isRecord(r) THEN (* handle record *) ELSE (* handle set *)

Again, you could use the IsRecord predicate that I defined in my previous message. To my knowledge, there is no built-in function, and I confess I've never missed it because I know the type of the objects that appear in the specification. I might want to write

IF r \in BusinessRecords THEN ... ELSE IF r \in PrivateRecords THEN ... ELSE ...

to handle different kinds of records that are stored in some set. Storing different types of values (such as numbers, functions or sets) in one data structure is legal in TLA+ but usually a bad idea because TLC will give you error messages such as the one above.

Stephan

[Jaak Ristioja]

On 12.11.2015 11:17, Stephan Merz wrote:
>> So I guess the question is really whether it is possible in TLC to check
>> whether something is a record or a set, e.g.:
>>
>> IF isRecord(r) THEN (* handle record *) ELSE (* handle set *)
>
> Again, you could use the IsRecord predicate that I defined in my previous message. To my knowledge, there is no built-in function, and I confess I've never missed it because I know the type of the objects that appear in the specification. I might want to write
>
> IF r \in BusinessRecords THEN ... ELSE IF r \in PrivateRecords THEN ... ELSE ...
>
> to handle different kinds of records that are stored in some set. Storing different types of values (such as numbers, functions or sets) in one data structure is legal in TLA+ but usually a bad idea because TLC will give you error messages such as the one above.

Which is why one cant actually use something like

IsRecord(r) ==
/\ DOMAIN r \subseteq STRING
/\ r = [ fld \in DOMAIN r |-> r[fld] ]

on sets, because TLC will err with "java.lang.RuntimeException:
Attempted to apply the operator DOMAIN to a non-function (a set of the
form {1, ..., eN} )".

So in short, it is not (yet?) possible to define an operator which
during TLC runs would return whether something is either a record or a set.


Best regards,
Jaak

[Y2i]

Just a thought:

If a Record is defined as a set of records (p. 28 in Specifying Systems), then

IsRecord(r) == r \in Record

should do the test.  I use this approach for my TypeInvariants.

Thank you,

Yuri

[Y2i]

Another thought:

To test if something is a set of records, I use

IsSet(s) == s \subseteq Record

The main idea is to define a Record as a set of records.

[Y2i]

I actually duplicated Stephan's original response:

> but in practice one tends to be more interested in checking if a record is an element of a particular set of records.

I'll read full threads more carefully next time.

Yuri