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

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

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

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.
>