Re: [tlaplus] Verification of Temporal Property

Next == IF (x+y#10) THEN
/\ x' \in Domain
/\ y' \in Domain
ELSE
/\ UNCHANGED <<x,y>>

with Domain defined as 1 .. 10, modeling non-deterministic choice of x and y. However, this specification will fail to satisfy the liveness property <>(x + y = 10), even when you include your fairness condition in the definition of Spec [1]. A counter-example would be a behavior where x equals 1 at each state and y oscillates between 1 and 2.

You can ensure the liveness property by imposing the fairness property

WF_vars(Next /\ (x+y)'=10)

but that's somewhat trivializing the problem. I do not think I really understand what you are trying to model.

Regards,

Stephan

[1] From what you write, it looks like Spec does not include the fairness condition, which explains the stuttering behavior that you observe.

On 31 Jan 2018, at 06:42, Stephen <stephen...@xxxxxxxxx> wrote:

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

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

and got a trace as:

Step 1: x=2 y=6
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.
"

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...@googlegroups.com
> <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.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...@googlegroups.com
> <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.