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