# Re: [tlaplus] Verification of Temporal Property

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.

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:
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> 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
>
>
>