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

Temporal properties were violated in the simple euclid_gcd algorithm.










                          


The state (num=4) should not be the last state. It should go ahead, and get pc = "Done", isn't it?

------------------------------- MODULE hello3 -------------------------------

EXTENDS Integers

CONSTANTS M, N

ASSUME /\ M \in Nat \ {0}
       /\ N \in Nat \ {0}

(*
--algorithm ComputeGCD
{   variable x = M, y = N;
    {   abc:while( x # y ) 
        { if (x < y) { y := y - x}
            else { x := x - y }}}}
*)
\* BEGIN TRANSLATION
VARIABLES x, y, pc

vars == << x, y, pc >>

Init == (* Global variables *)
        /\ x = M
        /\ y = N
        /\ pc = "abc"

abc == /\ pc = "abc"
       /\ IF x # y
             THEN /\ IF x < y
                        THEN /\ y' = y - x
                             /\ x' = x
                        ELSE /\ x' = x - y
                             /\ y' = y
                  /\ pc' = "abc"
             ELSE /\ pc' = "Done"
                  /\ UNCHANGED << x, y >>

Next == abc
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

=============================================================================