-------------------------------- MODULE ex1 --------------------------------
EXTENDS Naturals
VARIABLES  v,pc
---------------------------------------------------------------------
(* Define actions from the text of annotated algorithm *)
al0l1 ==
    /\ pc="l0"
    /\ pc'="l1"
    /\ v'=v+4
---------------------------------------------------------------------    
(*  Define  the computation relation *)
next == al0l1
(* Define the initial conditions *)
init == pc="l0" /\ v=3
---------------------------------------------------------------------    
(* Define the invariant from the annotation *)    
i == 
    /\ pc="l0" => v=3
    /\ pc="l1" => v=7
(* Define the safety property to check namely the partial correctness *)    

safe == pc="l1" => v=7

=============================================================================
\* Modification History
\* Last modified Wed Sep 09 17:08:32 CEST 2015 by mery
\* Created Wed Sep 09 17:02:47 CEST 2015 by mery