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

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

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.