----------------------------- MODULE tri -----------------------------

EXTENDS Naturals, TLC
CONSTANT N

(*
--algorithm Tri {
    variables c = 0, d = 0, t = 0,
    array = [k \in 0..N-1 |->
                IF k=0 THEN 3                        
                ELSE IF k=1 THEN 15
                ELSE IF k=2 THEN 2
                ELSE IF k=3 THEN 5 
                ELSE 10
            ];
    {
        c := 0;
        \* Pour chaque éléments du tableau
        while (c <= N - 1) {
            \* On récupère l'élément actuel
            d := c;
            
            \* On décale les éléments
            while ((d > 0) /\ (array[d] < array[d-1])) {
                t := array[d];
                array[d] := array[d-1];
                array[d-1] := t;
                d := d - 1;
            };
            c := c + 1;
        };
        c := 0;
        print <<"Affichage du tableau : ">>;
        while (c <= N - 1) {
            print <<c, array[c]>>;
            c := c + 1;
        };
    }
}

*)
\* BEGIN TRANSLATION
VARIABLES c, d, t, array, pc

vars == << c, d, t, array, pc >>

Init == (* Global variables *)
        /\ c = 0
        /\ d = 0
        /\ t = 0
        /\ array = [k \in 0..N-1 |->
                       IF k=0 THEN 3
                       ELSE IF k=1 THEN 15
                       ELSE IF k=2 THEN 2
                       ELSE IF k=3 THEN 5
                       ELSE 10
                   ]
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ c' = 0
         /\ pc' = "Lbl_2"
         /\ UNCHANGED << d, t, array >>

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF c <= N - 1
               THEN /\ d' = c
                    /\ pc' = "Lbl_3"
                    /\ c' = c
               ELSE /\ c' = 0
                    /\ PrintT(<<"Affichage du tableau : ">>)
                    /\ pc' = "Lbl_5"
                    /\ d' = d
         /\ UNCHANGED << t, array >>

Lbl_3 == /\ pc = "Lbl_3"
         /\ IF (d > 0) /\ (array[d] < array[d-1])
               THEN /\ t' = array[d]
                    /\ array' = [array EXCEPT ![d] = array[d-1]]
                    /\ pc' = "Lbl_4"
                    /\ c' = c
               ELSE /\ c' = c + 1
                    /\ pc' = "Lbl_2"
                    /\ UNCHANGED << t, array >>
         /\ d' = d

Lbl_4 == /\ pc = "Lbl_4"
         /\ array' = [array EXCEPT ![d-1] = t]
         /\ d' = d - 1
         /\ pc' = "Lbl_3"
         /\ UNCHANGED << c, t >>

Lbl_5 == /\ pc = "Lbl_5"
         /\ IF c <= N - 1
               THEN /\ PrintT(<<c, array[c]>>)
                    /\ c' = c + 1
                    /\ pc' = "Lbl_5"
               ELSE /\ pc' = "Done"
                    /\ c' = c
         /\ UNCHANGED << d, t, array >>

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

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

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

\* END TRANSLATION
  
Qpc == (pc = "Done") => (\A k: k \in 0..N-1 /\ array[k] < array[k+1])  
        /\ PrintT(<<"Le tableau est bien trie">>)   
        
Qpc2 == (pc = "Done") => array[0] = 2 
        /\ array[1] = 3 
        /\ array[2] = 5 
        /\ array[3] = 10
        /\ array[4] = 15
        /\ PrintT(<<"Le tableau est bien trie">>)
    

=============================================================================
\* Modification History
\* Last modified Fri May 27 15:08:20 CEST 2016 by arthur
\* Last modified Tue May 24 16:02:12 CEST 2016 by Julien
\* Created Tue May 24 15:09:10 CEST 2016 by Julien