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

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

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