Sets with mixed type elements

[Leroy van Engelen]

Hi,

It seems that TLC does not support sets of mixed 'types': evaluating `{1, "a"}`,  `{1, {}}`, `"a" \in {1}` result in errors like "Attempted to compare string "a" with non-string".

I thought sets would allow any mixed types of elements. Or is this a TLC optimization. I am trying to use to improve on the Json module to support arbitrary inputs, not just sequences.

Regards,

-Leroy van Engelen

[Stephan Merz]

TLA+ leaves the truth value of formulas such as 1 = "a" or 1 = {} unspecified, and therefore we cannot know if, say,

"a" \in {1, "b"}

holds or not. This explains the error message that TLC produces.

Stephan

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/1fb74ada-56d2-486e-8476-0c097236ed1b%40googlegroups.com.

[Shiyao MA]

Elements of different types cannot be compared (or to say, unspecified).

Therefore, you cannot compare integer 1 with string "a".

Since a set requires unique elements, hence each element should be comparable against with each other.

There is one exception that, an element of "type" model value can be compared against other elements regardless of their type. The value is always false.

[Alex Shirley]

Does that mean that it wouldn't be possible switch based on type?

For example:

doTheThing(x) ==

    IF x \in Nat

    THEN \* Do something

    ELSE IF x = "none"

    THEN \* Do something else

    ELSE \* Something else as well