[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] The effect of symmetry sets on TLC performance

   I think this model is semantically symmetrical in both sets

If you are convinced that the model of the spec is symmetrical, then
you should be able to prove that it satisfies the definition of

Thank you for making me realize that symmetry with respect to a set S
can be broken by CHOOSE expressions involving S other than ones of the
form  CHOOSE x \in S : ...   -- for example a CHOOSE _expression_ like

    Map == CHOOSE f \in [S -> T] : ...

As I did mention, symmetry can also be broken by instantiating a
constant like Map with an _expression_ that explicitly mentions
individual elements of S.