How to specify Semmetry sets in config file in visual studio code

[tamarind code]

I am using vscode with the TLA+ extension but I am having trouble adding symmetry sets in the config file. 

If I try

CONSTANTS

RM = {r1, r2}

\* Mark RM and Acceptor as symmetry sets to reduce state space

SYMMETRY Permutations(RM)

I keep getting the following error

The exception was a tlc2.tool.ConfigFileException
: TLC found an error in the configuration file at line 10
It was expecting a keyword, but did not find it.

I found this solution but that only works if I need to mark only one set as a symmetry set. 

What is the way to mark two or more sets as symmetry sets please?

[Stephan Merz]

You want to define an operator in your TLA+ module such as

Symmetry == Permutations(RM)

then put

SYMMETRY Symmetry

in your config file. See Specifying Systems, section 14.7.1 for the grammar of config files.

Hope this helps,

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 visit https://groups.google.com/d/msgid/tlaplus/ea1381fa-bc74-458c-93d8-55ce483945aen%40googlegroups.com.

[tamari...@gmail.com]

Thanks Stephen for the prompt response, very kind of you.
The approach you suggested does work but allows onely one set to be marked as a symmetrc set.
The section in the book you mentioned above does say only on SYMMETRY statement is allowed.
But us there a way to use that single symmetry statement to mark multiple sets as symmetry sets?
I have tried listing them separated by comma but doesn't seem to work.
Just wanted to confirm if it is possible?

Thanks so much again for your help

Sumuhan

[Stephan Merz]

If you have two symmetry sets X and Y, you can define

Symmetry == Permutations(X) \union Permutations(Y)

I recommend you have a look at section 14.3.4 of Specifying Systems, where this is explained in detail.

Stephan

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4f773d7b-4b40-47d6-bf9e-08b7b7c8035fn%40googlegroups.com.

[Markus Kuppe]

Also see https://github.com/tlaplus/vscode-tlaplus/discussions/271#discussioncomment-13719128

[tamari...@gmail.com]

Thanks so much Stephan 😃 That really makes sense!

I actually saw something like "Symmetry == Permutations(X) \union Permutations(Y)" somewhere but then I was thinking mistakenly that if we have 

X { 1,2,3} and Y = { "a","b"} then I was thinking TLC will treat the entire Union as a symmetry set and that might break the spec as it might think it is OK to replace 1 with "a"

But now I think that won't be a problem as long as the spec prevents such substitution. For example if we have a counter with 

Init == x = 1

Next == x' = x +1

Then x can never be "a" anyway so using such a union for symmetry shouldn't break the rest of the spec

Thank you so much for your the guidance

[tamari...@gmail.com]

And thanks Markus, That was very useful. It confirms the same answer. Thank you for pointing that out.