------------------------------ MODULE serie4_2 ------------------------------
EXTENDS Naturals
VARIABLES pc, m, i
CONSTANTS n
ASSUME n # 0 /\ n \in Nat

=============================================================================
\* Modification History
\* Last modified Mon Nov 16 17:51:29 CET 2015 by garnier34u
\* Created Mon Nov 16 09:38:12 CET 2015 by garnier34u

f == [ i \in 0..n-1 |->
                    IF i=0 THEN 3
                    ELSE IF i=1 THEN 6
                    ELSE IF i=2 THEN 2*i
                    ELSE IF i=3 then 9
                    ELSE 5] 

(* Define actions from the text of annoted algo *)

al0l1 == 
    /\ pc = "l0"
    /\ m' = f[0]
    /\ pc' = "l1"
    
al1l2 ==
    /\ pc="l1"
    /\ i' = 1
    /\ m'=m
    /\ pc'="l2"
    
al2l3 == 
    /\ pc="l2"
    /\ i < n
    /\ i' = i
    /\ m'=m
    /\ pc'="l3"
    
al3l4 ==
    /\ pc="l3"
    /\ pc'="l4"
    /\ f[i] > m
    /\ i' = i
    /\ m' = m
    
al4l5 ==
    /\ pc="l4"
    /\ pc'="l5"
    /\ m'=f[i]
    /\ i'=i

al3l6 ==
    /\ pc="l3"
    /\ pc'="l6"
    /\ f[i] \leq m
    /\ i'=i
    /\ m'=m
    
al5l6 ==
    /\ pc="l5"
    /\ pc'="l6"
    /\ TRUE
    /\ i'=i
    /\ m'=m
    
al6l7 ==
    /\ pc="l6"
    /\ pc'="l7"
    /\ TRUE
    /\ i' = i+1
    /\ m'=m
    
al2l8 ==
    /\ pc="l2"
    /\ pc'="l8"
   (* /\ i \geq n*)
    /\ i \geq n
    /\ i' = i
    /\ m' = m

(*al7l8 ==
    /\ pc="l7"
    /\ pc'="l8"
    /\ i=n
    /\ i' = i
    /\ m'=m*)
    
al7l2 ==
    /\pc="l7"
    /\pc'="l2"
    /\i'=i
    /\m'=m

(* Define the computation relation *)
(* next == *)

next == 
    \/al0l1
    \/al1l2
    \/al2l3
    \/al3l4
    \/al4l5
    \/al3l6
    \/al5l6
    \/al6l7
    \/al2l8
    \/al7l2
    

(*Define the initial conditions *)
(*init == *)

init == /\ i=0
    /\ pc="l0"
    /\ m = f[0]

(* Define the invariant from the annotation *)
(* i == *)

(*DeadLock, QcorrectionPartielle, invariant, Qoverflowfree*)

QcorrecPartielle == pc="l8" => (\A j: j \in 0..n-1 => m\geq f[j] /\ f[k]=m)