Re: [tlaplus] Verification of Temporal Property

[Martin <martin...@xxxxxxxxxxxxxx>]

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.