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,
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.