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

*From*: Martin <martin...@xxxxxxxxxxxxxx>*Date*: Tue, 30 Jan 2018 13:14:45 +0100*References*: <9caabae9-7fb5-460e-9f31-769f58705a01@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.5.2

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...@xxxxxxxxxxxxxxxx > <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx > <mailto:tla...@xxxxxxxxxxxxxxxx>. > 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:*Stephen

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

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