Temporal properties were violated in the simple euclid_gcd algorithm.

[Jianjun Zheng <code...@xxxxxxxxx>]

                          

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

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