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

*From*: Stephen <stephen...@xxxxxxxxx>*Date*: Tue, 30 Jan 2018 21:42:19 -0800 (PST)*References*: <9caabae9-7fb5-460e-9f31-769f58705a01@googlegroups.com> <5aca2aff-2c08-aa66-d77b-55b0bc8a78be@gmail.com>

Hi, Matin, thanks for your excellent explanation and kindly help. However, I am still confused.

在 2018年1月30日星期二 UTC+8下午8:14:50，Martin写道：

在 2018年1月30日星期二 UTC+8下午8:14:50，Martin写道：

"The fallacy is that CHOOSE picks some element x of S fulfilling the criterion (in this case just TRUE), but it will always return the same unknown representative. This is nice because equality behaves like we expect, i.e. RandomElement(S) = RandomElement(S) -- but his is not what you would expect of a random number generator in a programming language. "

What does "it will always return the same unknown representative" mean? Do you mean that RandomElement returns always a same but uncertain value (i.e., in the execution, the value of RandomElement returns will be used without changed anymore)? For example, I make changing as:

/\ x' = CHOOSE a \in 1..10: TRUE

/\ y' = CHOOSE a \in 1..10: TRUE

and got a trace as:

State 1: x=1,y=1

State 2: stuttering

This means that the CHOOSE operator returns a fixed value every time. That is, CHOOSE will choose 1 for every time without covering other values(i.e., it choose a value from the first value of 1..10), so it stutters as x=1,y=1. Do I get a right understanding?

While I change the value assignment of x y as:

/\ x' = RandomElement(1..10)

/\ y' = RandomElement(1..10)

/\ y' = RandomElement(1..10)

and got a trace as:

Step 1: x=2 y=6

Step 2: stuttering

Step 2: stuttering

Does it means that RandomElement selects a value of x that satisfies x \in 1..10 while the evaluation _expression_ always TRUE? However, as the define "RandomElement(S) == CHOOSE x \in S : TRUE" in https://lamport.azurewebsites.net/tla/current-tools.pdf, I think the returning value should be the same while just take RandomElement(S) as substitution of CHOOSE x \in S : TRUE. Is there any tricky I lost?

As the trace shows, can I understand that RandomElement(1..10) chooses 1 for x' at the first step, and then it always choose 1 for x' for the following infinitely steps and the same as y'? So, there is stuttering steps.

"

Next == IF (x+y#sum) THEN

/\ x' \in Domain

/\ y' \in Domain

ELSE

/\ UNCHANGED <<x,y>>

We get a similar trace:

Step 1: x=1 y=1

Step 2: stuttering

The problem here is that even when reassigning x and y, they could be

reassigned the same values over and over again. A number generator would

have some assumption of an equal distribution of values, but the random

function modeled here does not.

/\ x' \in Domain

/\ y' \in Domain

ELSE

/\ UNCHANGED <<x,y>>

We get a similar trace:

Step 1: x=1 y=1

Step 2: stuttering

The problem here is that even when reassigning x and y, they could be

reassigned the same values over and over again. A number generator would

have some assumption of an equal distribution of values, but the random

function modeled here does not.

"

At the first step, there are 10*10 possible combination of x and y as x=1,y=1;x=1,y=2;x=1,y=3,...? Then, at the next step there is possibility that x=1 and y=1, the same as following steps. This means stuttering steps and the property of <>(x+y=10) is violated?

when I change as

Next == IF (x+y#sum) THEN /\ PrintT(<<"0: ",x,y>>)

/\ x' \in 1..10

/\ y' \in 1..10

/\ PrintT(<<"1: ",x',y'>>)

ELSE /\ PrintT(<<RandomElement(1..10) , RandomElement(1..10)>>)

/\ UNCHANGED <<x,y>>

Liveness == WF_vars(Next)

Property1 == WF_vars(Next) => <>(x+y=10)

the trace as follows:

The first state : x=1 y=1, and there is a second step. How does it happen? Just because Property1 == WF_vars(Next) => <>(x+y=10) makes the execution of stuttering steps is allowed? Why State 2 can back to State 1? If this kind of backing allowed, do it means the execution can loop for ever and can not proceed to a new state?

I think I am not understanding TLA+ very well. I appreciate your help!

regards,

Yong

在 2018年1月30日星期二 UTC+8下午8:14:50，Martin写道：

Hi Stephen,

Perhaps let me summarize how I interpret your specification: you start

with two variables and want to update them with a random number as long

as they don't add up to some constant sum.

What you would like to show is that in any state, eventually x+y = 10

will become true (I guess this should be sum).

I see the following trace:

Step 1: x=2 y=6

Step 2: stuttering

So the first step stays unchanged over time. What's happening is a

little obscured by your use of RandomElement. If you look at its

definition (see e.g.

https://lamport.azurewebsites.net/tla/current-tools.pdf ), it is:

RandomElement(S) == CHOOSE x \in S : TRUE

The fallacy is that CHOOSE picks some element x of S fulfilling the

criterion (in this case just TRUE), but it will always return the same

unknown representative. This is nice because equality behaves like we

expect, i.e. RandomElement(S) = RandomElement(S) -- but his is not what

you would expect of a random number generator in a programming language.

We can think of assigning a random number as nondeterministic

assignment. Instead of writing x' = RandomElement({1..0}) you just write

x' \in 1..10 . TLC will then cover all possibilities for x.

But even when we update the Next state relation to

Next == IF (x+y#sum) THEN

/\ x' \in Domain

/\ y' \in Domain

ELSE

/\ UNCHANGED <<x,y>>

We get a similar trace:

Step 1: x=1 y=1

Step 2: stuttering

The problem here is that even when reassigning x and y, they could be

reassigned the same values over and over again. A number generator would

have some assumption of an equal distribution of values, but the random

function modeled here does not.

Even if you assume a random distribution, after a finite number of

steps, the chance of getting the the same number all over is very small

(1/10^n). The chance of getting the same state infinitely many times is

indeed zero (because lim n -> inf : 1/10 ^ n = 0), but even if you

exclude this case by assuming the property WF_vars(Next) => Property1,

you get a new counterexample, which is to switch between two states:

State 1: x=1 y=1

State 2: x=10 y=1

The main trouble we have here is that we are trying to reason on a

probabilistic process by discrete means. TLC will find traces that

exhibit the (un-)desired behavior, but it can't take the probalistic

reasoning from us. In some cases, we can axiomatize this behavior, but

in the case of randomized functions, I don't have any experience.

Disclaimer: Please feeel free to add any corrections / more information,

I still don't consider myself an expert in model checking :-)

cheers, Martin

On 01/30/2018 11:44 AM, Stephen wrote:

> Hi,

>

> I am learning TLA+ now, and I want to write a testing spec to exercise

> as below:

>

> -------------------------------- MODULE Sum ------------------------------ --

> EXTENDS Naturals, TLC

>

> CONSTANT sum

>

> VARIABLE x,y

>

> vars == <<x,y>>

>

> Init == /\ x \in 1..10

> /\ y \in 1..10

>

> Next == IF (x+y#sum) THEN /\ x' = RandomElement(1..10)

> /\ y' = RandomElement(1..10)

> /\ PrintT(<<x,y>>)

> ELSE /\ PrintT(<<x,y>>)

> /\ UNCHANGED <<x,y>>

>

> Liveness == WF_vars(Next)

>

> Property1 == <>(x+y=10)

>

> Spec == Init /\ [][Next]_<<vars>>

>

> ============================================================ =================

> \* Modification History

> \* Last modified Tue Jan 30 18:25:46 CST 2018 by stephen

> \* Created Tue Jan 30 17:53:14 CST 2018 by stephen

>

>

> The purpose of this spec is make summation of two variables equal 10,

> and keeping the values unchanged when the summation is 10. The

> following picture is the Model Checking Results:

> <https://lh3.googleusercontent.com/- >9r94o4sxGJE/WnBKXlOYcLI/ AAAAAAAAAzM/ dn56vspjeso7GASbXWF3Dt6a_ H9WmYVNQCLcBGAs/s1600/IMG_ 20180130_183240.jpg

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

> 1. why Temporal properties were violated at State(num=1) rather than

> other states?

> 2. Can I use Property1 == <>(x+y=10) to verify that x+y eventually

> equlas to 10? or at some time x+y equals to 10? or what is the right

> temporal property to verify this?

> 3. Can anybody point out as much as possible errors in this spec and

> tell me the reason?

>

>

> I appreciate,

>

> Yong

>

>

>

> <https://lh3.googleusercontent.com/- >9r94o4sxGJE/WnBKXlOYcLI/ AAAAAAAAAzM/ dn56vspjeso7GASbXWF3Dt6a_ H9WmYVNQCLcBGAs/s1600/IMG_ 20180130_183240.jpg

> <https://lh3.googleusercontent.com/- >9r94o4sxGJE/WnBKXlOYcLI/ AAAAAAAAAzM/ dn56vspjeso7GASbXWF3Dt6a_ H9WmYVNQCLcBGAs/s1600/IMG_ 20180130_183240.jpg

>

> --

> 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+u...@googlegroups.com

> <mailto:tlaplus+u...@googlegroups.com >.

> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx

> <mailto:tla...@googlegroups.com >.

> Visit this group at https://groups.google.com/group/tlaplus .

> For more options, visit https://groups.google.com/d/optout .

在 2018年1月30日星期二 UTC+8下午8:14:50，Martin写道：

Hi Stephen,

Perhaps let me summarize how I interpret your specification: you start

with two variables and want to update them with a random number as long

as they don't add up to some constant sum.

What you would like to show is that in any state, eventually x+y = 10

will become true (I guess this should be sum).

I see the following trace:

Step 1: x=2 y=6

Step 2: stuttering

So the first step stays unchanged over time. What's happening is a

little obscured by your use of RandomElement. If you look at its

definition (see e.g.

https://lamport.azurewebsites.net/tla/current-tools.pdf ), it is:

RandomElement(S) == CHOOSE x \in S : TRUE

The fallacy is that CHOOSE picks some element x of S fulfilling the

criterion (in this case just TRUE), but it will always return the same

unknown representative. This is nice because equality behaves like we

expect, i.e. RandomElement(S) = RandomElement(S) -- but his is not what

you would expect of a random number generator in a programming language.

We can think of assigning a random number as nondeterministic

assignment. Instead of writing x' = RandomElement({1..0}) you just write

x' \in 1..10 . TLC will then cover all possibilities for x.

But even when we update the Next state relation to

Next == IF (x+y#sum) THEN

/\ x' \in Domain

/\ y' \in Domain

ELSE

/\ UNCHANGED <<x,y>>

We get a similar trace:

Step 1: x=1 y=1

Step 2: stuttering

The problem here is that even when reassigning x and y, they could be

reassigned the same values over and over again. A number generator would

have some assumption of an equal distribution of values, but the random

function modeled here does not.

Even if you assume a random distribution, after a finite number of

steps, the chance of getting the the same number all over is very small

(1/10^n). The chance of getting the same state infinitely many times is

indeed zero (because lim n -> inf : 1/10 ^ n = 0), but even if you

exclude this case by assuming the property WF_vars(Next) => Property1,

you get a new counterexample, which is to switch between two states:

State 1: x=1 y=1

State 2: x=10 y=1

The main trouble we have here is that we are trying to reason on a

probabilistic process by discrete means. TLC will find traces that

exhibit the (un-)desired behavior, but it can't take the probalistic

reasoning from us. In some cases, we can axiomatize this behavior, but

in the case of randomized functions, I don't have any experience.

Disclaimer: Please feeel free to add any corrections / more information,

I still don't consider myself an expert in model checking :-)

cheers, Martin

On 01/30/2018 11:44 AM, Stephen wrote:

> Hi,

>

> I am learning TLA+ now, and I want to write a testing spec to exercise

> as below:

>

> -------------------------------- MODULE Sum ------------------------------ --

> EXTENDS Naturals, TLC

>

> CONSTANT sum

>

> VARIABLE x,y

>

> vars == <<x,y>>

>

> Init == /\ x \in 1..10

> /\ y \in 1..10

>

> Next == IF (x+y#sum) THEN /\ x' = RandomElement(1..10)

> /\ y' = RandomElement(1..10)

> /\ PrintT(<<x,y>>)

> ELSE /\ PrintT(<<x,y>>)

> /\ UNCHANGED <<x,y>>

>

> Liveness == WF_vars(Next)

>

> Property1 == <>(x+y=10)

>

> Spec == Init /\ [][Next]_<<vars>>

>

> ============================================================ =================

> \* Modification History

> \* Last modified Tue Jan 30 18:25:46 CST 2018 by stephen

> \* Created Tue Jan 30 17:53:14 CST 2018 by stephen

>

>

> The purpose of this spec is make summation of two variables equal 10,

> and keeping the values unchanged when the summation is 10. The

> following picture is the Model Checking Results:

> <https://lh3.AAAAAAAAAzM/ dn56vspjeso7GASbXWF3Dt6a_ H9WmYVNQCLcBGAs/s1600/IMG_ 20180130_183240.jpg

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

>

> 1. why Temporal properties were violated at State(num=1) rather than

> other states?

> 2. Can I use Property1 == <>(x+y=10) to verify that x+y eventually

> equlas to 10? or at some time x+y equals to 10? or what is the right

> temporal property to verify this?

> 3. Can anybody point out as much as possible errors in this spec and

> tell me the reason?

>

>

> I appreciate,

>

> Yong

>

>

>

> <https://lh3.AAAAAAAAAzM/ dn56vspjeso7GASbXWF3Dt6a_ H9WmYVNQCLcBGAs/s1600/IMG_ 20180130_183240.jpg

> <https://lh3.AAAAAAAAAzM/ dn56vspjeso7GASbXWF3Dt6a_ H9WmYVNQCLcBGAs/s1600/IMG_ 20180130_183240.jpg

>

> --

> 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+u...@googlegroups.com

> <mailto:tlaplus+u...@googlegroups.com >.

> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx

> <mailto:tla...@googlegroups.com >.

> Visit this group at https://groups.google.com/group/tlaplus .

> For more options, visit https://groups.google.com/d/optout .

**Follow-Ups**:**Re: [tlaplus] Verification of Temporal Property***From:*Stephan Merz

**References**:**Verification of Temporal Property***From:*Stephen

**Re: [tlaplus] Verification of Temporal Property***From:*Martin

- Prev by Date:
**Re: [tlaplus] Verification of Temporal Property** - Next by Date:
**Re: [tlaplus] Verification of Temporal Property** - Previous by thread:
**Re: [tlaplus] Verification of Temporal Property** - Next by thread:
**Re: [tlaplus] Verification of Temporal Property** - Index(es):