------------------------------ MODULE serie6_7 ------------------------------
EXTENDS Naturals, Integers, TLC, Reals

CONSTANT n

=============================================================================
\* Modification History
\* Last modified Mon Nov 23 15:25:25 CET 2015 by garnier34u
\* Created Mon Nov 23 15:14:37 CET 2015 by garnier34u



(*
--algorithm tribulle 
{
    variables t,i,j,d=TRUE;
    {
        i:=0;
        while(i < n /\ d)
        {
            d := FALSE;
            j:=1;
            while(j < (n-i))
            {
                if(t[j-1] > t[j])
                {
                    temp := t[j-1];
                    t[j-1] := t[j];
                    t[j] := temp;
                    d := TRUE;
                };
                j:=j+1;
            };
            i:=i+1;
     
    }
}
}
*)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES t, i, j, d, pc

vars == << t, i, j, d, pc >>

Init == (* Global variables *)
        /\ t = defaultInitValue
        /\ i = defaultInitValue
        /\ j = defaultInitValue
        /\ d = TRUE
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ i' = 0
         /\ pc' = "Lbl_2"
         /\ UNCHANGED << t, j, d >>

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF i < n /\ d
               THEN /\ d' = FALSE
                    /\ j' = 1
                    /\ pc' = "Lbl_3"
               ELSE /\ pc' = "Done"
                    /\ UNCHANGED << j, d >>
         /\ UNCHANGED << t, i >>

Lbl_3 == /\ pc = "Lbl_3"
         /\ IF j < (n-i)
               THEN /\ IF t[j-1] > t[j]
                          THEN /\ temp' = t[j-1]
                               /\ t' = [t EXCEPT ![j-1] = t[j]]
                               /\ pc' = "Lbl_4"
                          ELSE /\ pc' = "Lbl_5"
                               /\ t' = t
                    /\ i' = i
               ELSE /\ i' = i+1
                    /\ pc' = "Lbl_2"
                    /\ t' = t
         /\ UNCHANGED << j, d >>

Lbl_5 == /\ pc = "Lbl_5"
         /\ j' = j+1
         /\ pc' = "Lbl_3"
         /\ UNCHANGED << t, i, d >>

Lbl_4 == /\ pc = "Lbl_4"
         /\ t' = [t EXCEPT ![j] = temp]
         /\ d' = TRUE
         /\ pc' = "Lbl_5"
         /\ UNCHANGED << i, j >>

Next == Lbl_1 \/ Lbl_2 \/ Lbl_3 \/ Lbl_5 \/ Lbl_4
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

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

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

\* END TRANSLATION


Safe1 == pc#"Done"
Safe2 == \A e \in 0..n-1: t[e] \leq t[e+1]