Re: Is it correct to use symmetry set in this spec?

[Hengfeng Wei <hengx...@xxxxxxxxx>]

Great thanks.

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, declare

  CONSTANT N

and 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 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)

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