Re: [tlaplus] How to specify Semmetry sets in config file in visual studio code

["tamari...@xxxxxxxxx" <tamarindcode@xxxxxxxxx>]

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

On Wednesday, 9 July 2025 at 16:53:16 UTC+1 Stephan Merz wrote:

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

On 9 Jul 2025, at 17:36, tamarind code <tamari...@xxxxxxxxx> wrote:

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?

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

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4f773d7b-4b40-47d6-bf9e-08b7b7c8035fn%40googlegroups.com.