------------------------------ MODULE serie4_1 ------------------------------

EXTENDS Naturals
VARIABLES x, pc
CONSTANTS x0, min, max
ASSUME x0 \in Nat /\ min \geq x0 /\ x0 \leq max

=============================================================================
\* Modification History
\* Last modified Mon Nov 16 16:32:31 CET 2015 by garnier34u
\* Created Mon Nov 16 08:42:28 CET 2015 by garnier34u

al0l1 ==
    /\ pc="l0"
    /\ 0 < x
    /\ pc'="l1"
    /\ x'=x
    
al0l3 ==
    /\ pc="l0"
    /\ ~(0<x)
    /\ pc' = "l3"
    /\ x'=x
    
al1l2 ==
    /\ pc="l1"
    /\ TRUE
    /\ pc' = "l2"
    /\ x'=x-1
    
al2l1 ==
    /\ pc = "l2"
    /\ 0 < x
    /\ pc'="l1"
    /\ x'=x
    
al2l3 ==
    /\ pc="l2"
    /\ ~(0<x)
    /\ pc' = "l3"
    /\ x'=x
    
next == al0l1 \/ al0l3 \/ al1l2 \/ al2l1 \/ al2l3
init == pc="l0" /\ x=x0

(* invariant *)
i == 
    /\  pc = "l0" => x=x0
    /\ pc="l1" => 0<x /\ x \leq x0
    /\ pc="l2" => 0 \leq x /\ x < x0
    /\ pc="l3" => x=0
    
---------------------

(* define safety *) 
Q1 == x \geq 0 (* ok *)
Q2 ==x \leq -6 (*ko*)
Qpost == pc="l3" => x=0 (* correction partielle : ok *)
Qoverflowfree == min \leq x /\ x \leq max