Dear all,
I am writing a spec of a distributed algorithm which involves n clients.
In TLA+, I use the constant Client to denote a set of clients.
I need to give a unique priority to each client, written as
Priority == CHOOSE f \in [Client -> 1 .. Cardinality(Client)] : Injective(f)
where,
is a predicate testing whether a function f is injective.
Now, I use "set of model values" for Client.
Client <- [ model value ] {c1, c2, c3}
My problem is:
Is it correct to use "Symmetry set" as follows (only safety properties are checked)?
Client <- [ model value ] <symmetrical> {c1, c2, c3}
If not, is it possible to rewrite the definition of Priority (or make it a model value) to enable the symmetry set technique?
(Because the only requirement of priority is uniqueness, I do wish the symmetry set technique can help reduce state spaces.)
Best regards,
hengxin