-------------------------------- MODULE ex3 --------------------------------

EXTENDS Naturals

CONSTANTS x0
VARIABLES  x,pc

---------------------------------------------------------------------

al0l1 ==
    /\ pc="l0"
    /\ pc'="l1"
    /\ 0<x
    /\ x'=x
  
al0l3 ==
    /\ pc="l0"
    /\ pc'="l3"
    /\ x=0
    /\ x'=x
      
al1l2 ==
    /\ pc="l1"
    /\ pc'="l2"
    /\ x'=x-1
    

al2l1 ==
    /\ pc="l2"
    /\ pc'="l1"
    /\ 0<x
    /\ x'=x
    
 al2l3 ==
    /\ pc="l2"
    /\ pc'="l3"
    /\ 0=x
    /\ x'=x
       
next == al0l1 \/ al0l3 \/ al1l2  \/ al2l1 \/ al2l3

init == pc="l0" /\ x=x0

i ==
    /\ pc="l0" =>  x=x0
    /\ pc="l1" => 0<x /\ x \leq x0 
    /\ pc="l2" => 0 \leq x /\ x \leq x0
    /\ pc="l3" => x=0
    
safe ==      pc="l3" => x=0
    
  
    


=============================================================================
\* Modification History
\* Last modified Wed Sep 09 18:08:35 CEST 2015 by mery
\* Created Wed Sep 09 18:07:50 CEST 2015 by mery