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

*From*: Hengfeng Wei <hengx...@xxxxxxxxx>*Date*: Sun, 25 Nov 2018 18:52:20 -0800 (PST)

Dear all,

is a predicate testing whether a function f is injective.

**My problem is: ****Is it correct to use "Symmetry set" as follows (only safety properties are checked)? **

**If not, is it possible to rewrite the definition of Priority (or make it a model value) to enable the symmetry set technique?**

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.

`CONSTANT Client`

I need to give a unique priority to each client, written as

`Priority == CHOOSE f \in [Client -> 1 .. Cardinality(Client)] : Injective(f)`

where,

`Injective(f)`

Now, I use "set of model values" for Client.

`Client <- [ model value ] {c1, c2, c3}`

`Client <- [ model value ] <symmetrical> {c1, c2, c3}`

(Because the only requirement of priority is uniqueness, I do wish the symmetry set technique can help reduce state spaces.)

Best regards,

hengxin

**Follow-Ups**:**Re: Is it correct to use symmetry set in this spec?***From:*Leslie Lamport

- Prev by Date:
**Re: Sequence of sets -> Set** - Next by Date:
**Re: Is it correct to use symmetry set in this spec?** - Previous by thread:
**Re: Sequence of sets -> Set** - Next by thread:
**Re: Is it correct to use symmetry set in this spec?** - Index(es):