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

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 <tamarindcode@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+unsubscribe@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/88EDE34A-1235-456A-A69B-DD0B453FE6D1%40gmail.com.