Re: [tlaplus] Checking whether something is a record or a set?

[Stephan Merz <stepha...@xxxxxxxxx>]

> On 12 Nov 2015, at 10:00, Jaak Ristioja <jaak.r...@xxxxxxxx> 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


> On 12.11.2015 10:41, Stephan Merz wrote:
>> 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
>> 
>> 
>>> On 12 Nov 2015, at 09:30, Jaak Ristioja <jaak.r...@xxxxxxxx> wrote:
>>> 
>>> 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
>>> 
>>> -- 
>>> 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.
>> 
> 
> -- 
> 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.