[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Checking whether something is a record or a set?
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
/\ 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.
> On 12 Nov 2015, at 09:30, Jaak Ristioja <jaak.r...@xxxxxxxx> wrote:
> Is it possible in TLA+ to check whether something is a record or set?
> For example:
> Invariant == isRecord(myRecord) /\ isSet(someVariable.mySet)
> Best regards,
> 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.