[tlaplus] User defined symmetry in TLA+ Toolbox

["leroy.va...@xxxxxxxxx" <leroy.vanengelen@xxxxxxxxx>]

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

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/48a31f52-78bb-4b7a-8765-6acc352fcd86n%40googlegroups.com.