User defined symmetry in TLA+ Toolbox

[leroy.va...@gmail.com]

Hi,

I have a specification where there are sets of model values `ObjectIds` and `EntityIds`. These represent objects of a specific entity; i.e. there is a mapping from object id to entity id to model the entity of the object.

Say I have `ObjectIds == {o1, o2, o3}` and `EntityIds == {e1, e2}` then the object to entity mapping`(o1 :> e1) @@ (o2 :> e2) @@ (o3 :> e2)` means that there are 3 objects, 1 with entity type `e1` and 2 with entity type `e2`. In my model, this means that `o2` and `o3` are symmetrical.

I normally run TLC from the command line. To reduce the state space I have defined a `SYMMETRY` definition in the configuration: `{(o1 :> o1 @@ o2 :> o2 @@ o3 :> o3), (o1 :> o1 @@ o2 :> o3 @@ o3 :> o2)}` which works: states that are equal when swapping all occurrences of `o2` and `o3` are only visited once.

Now I'd like to run this specification in the TLA+ Toolbox. However, as far as I know, the only place I can define symmetry is on the whole `ObjectIds` set. Is there a way to customize the `SYMMETRY` definition when running from the Toolbox?

Regards,

-Leroy