Performance when using tuples

[Mathew Kuthur James]

Hi,

I understand that TLA+ supports non-flat tuples, so {a} and {<<a>>} and {<<<<a>>>>} are considered distinct. My question is - if all sets of the form {a,b,c...} are replaced by sets of the form {<<a>>,<<b>>,<<c>>...}, are there performance implications for model-checking? 

Also, is there any way to dynamically check whether a set consists of strings or tuples, and have a different behaviour in each case?
Something like:

F(S) == G(S) if S is a set of strings, H(S) if S is a set of tuples

[Hillel Wayne]

I believe the answers to both questions is no. If there are performance implications for model checking, they are probably not significant, and there is no way built-in way to tell the types of values. You could sort of hack something together with `ToString`: if `SubSeq(ToString(val), 1, 2)` is "<<", then it is probably a sequence.

H

--
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...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/1c58eefc-6f78-4828-a257-240da5946f66n%40googlegroups.com.