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.

[Stephan Merz]

I agree with Hillel on the answer to the first question.

I also agree on his second answer. Just to expand: in TLA+, strings are sequences of characters, so "Hello" is semantically identical to a value that could be represented as <<'H', 'e', 'l', 'l', 'o'>> if we had a notation for characters [1]. This means that a string cannot be distinguished from a tuple. However, you can check if S \subseteq STRING or S \subseteq Seq(Int), for example.

Stephan

[1] Traditionally, TLC has handled strings natively without being fully faithful to the TLA+ semantics.

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8swTCzim7hYvbD9WfVNU_iMcp%3D8Lo7UC-82f3BDdgt%2B1Qg%40mail.gmail.com.