Hello,
Martin pointed you to the right document but I think you both failed to read the full explanation of the operator and its implementation in TLC.
Fundamentally, TLA+ has no notion of random choice. However, you can model nondeterminism – i.e., choice that is not governed by a probability distribution to constrain its behavior over time. The operator RandomElement was added to TLC in view of statistical explorations of state spaces but this is not implemented. I think that it is useful for simulation, but not for model checking.
Indeed, you indeed want to write
Next == IF (x+y#10) THEN /\ x' \in Domain /\ y' \in Domain ELSE /\ UNCHANGED <<x,y>>
with Domain defined as 1 .. 10, modeling nondeterministic 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 counterexample 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.
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/currenttools.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/currenttools.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/currenttools.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.
