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

[tlaplus] User defined symmetry in TLA+ Toolbox


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?



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.