XJupiterImplCJupiter: Symmetry Sets in Models

[hengxin]

Questions to Resolve:

1. Is it OK to use "Symmetry Sets" in models of AJupiter, XJupiter, and CJupiter?

   • Priority == CHOOSE f \in [Client -> 1 .. ClientNum] : Injective(f) has used CHOOSE

   My Question @ tlaplus-googlegroup:

   • Is it correct to use symmetry set in this spec?

   References:

   • When to/not to use symmetry sets? @ tlaplus-googlegroup By Stephan Merz
   • Broken symmetry due to CHOOSE f \in [S -> T] @ tlaplus-googlegroup By Ron Pressler

2. XJupiterImplCJupiter without symmetry sets generates much more states and takes mucccccccch more time.
   References:

   • The effect of symmetry sets on TLC performance @ tlaplus-googlegroup By Ron Pressler

3. Symmetry set for combined "Client" and "Priority"?