Nesting/Unnesting Sets

[Amir Hossein Sayyad Abdi]

Hi everyone,

I woud like to know is there a way to unnest a set in TLA+?

The reason I am asking is because I have a set, say {a, b, c} which its elements are constants, and when I perform a union on this set with another set that contains the same elements I will get: {a, b, c, {a, b, c}}. But I expect the result to be {a, b, c}.

Best Regards
AmirHossein

[Hillel Wayne]

The reason I am asking is because I have a set, say {a, b, c} which its elements are constants, and when I perform a union on this set with another set that contains the same elements I will get: {a, b, c, {a, b, c}}. But I expect the result to be {a, b, c}.

That shouldn't happen. If S = {a, b, c}, then S \union S = {a, b, c}. Are you accidentally writing S \union {S}?

If you have S = {{a}, {b}, {c}}, then UNION S = {a, b, c}.

H

Best Regards
AmirHossein

--
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/CAKxfy0sdTWMRETZEJkqUAVvVNspbC9VpRmXRtJJYa56-RkNNhA%40mail.gmail.com.

[Amir Hossein Sayyad Abdi]

Correct, thanks for your help.

AmirHossein

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/dcc0ac19-a4d8-73fd-46c3-80ab939bbf47%40gmail.com.

[Amir Hossein Sayyad Abdi]

Is there a way to unnest this set?

S = {{a, b, c}}

I mean for S to be as follows:

S = {a, b, c}

I have tried using SUBSET with cardinality equal to 1, but no luck so far.

Best Regards

AmirHossein

[Stephan Merz]

UNION {{a,b,c}} = {a,b,c}

Regards,

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAKxfy0syShF0JhtffZ9RVG4YttNSikaXPzR5GNyQog1i3-sxWQ%40mail.gmail.com.

[Amir Hossein Sayyad Abdi]

Thank you very much. Sorry I did not understand it earlier from Hillel's answer.

Best Regards,

AmirHossein

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C29335BC-48D8-456F-A1ED-41D841FD0D02%40gmail.com.