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

*From*: Hengfeng Wei <hengx...@xxxxxxxxx>*Date*: Tue, 4 Dec 2018 19:39:29 -0800 (PST)*References*: <acdf7c0a-c74a-4074-86e8-f24e924761e8@googlegroups.com> <6b11bc76-9675-4fd5-a1e5-2532787b2f42@googlegroups.com>

Great thanks.

On Tuesday, November 27, 2018 at 9:05:52 AM UTC+8, Leslie Lamport wrote:

I understand your point now.

(Sorry for the late reply.)

Best regards,

hengxin

On Tuesday, November 27, 2018 at 9:05:52 AM UTC+8, Leslie Lamport wrote:

With your definition of priority, declareCONSTANT Nand write the following PlusCal spec--algorithm Foo {

variable x \in Client ;

{ x := 1 div (N - Priority[x])

}

}Create a model with Client instantiated by a set of 3 model values

and run the spec three times with N = 1, 2, and 3. TLC should

report an error all three times. Now make those model values a

symmetry set. For what values of N does TLC now find an error?Leslie

On Sunday, November 25, 2018 at 6:52:20 PM UTC-8, Hengfeng Wei wrote: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.

CONSTANT ClientI need to give a unique priority to each client, written as

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

Injective(f)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

**References**:**Is it correct to use symmetry set in this spec?***From:*Hengfeng Wei

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

- Prev by Date:
**What to do with distributed computing?** - Next by Date:
**Trying to figure out how theorems work with this basic example** - Previous by thread:
**Re: Is it correct to use symmetry set in this spec?** - Next by thread:
**Safe, regular or atomic registers** - Index(es):