-------------------------------- MODULE ex5 --------------------------------
EXTENDS TLC, Integers
VARIABLES y,z,pc
CONSTANTS x

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

astartloop == /\ pc="start" 
              /\ y'=2 /\ pc'="loop"
              /\ y' = z
              
aloophalt == /\ pc="loop" 
             /\ y < x 
             /\ z' = "true"
             /\ y = y'
             /\ pc'="halt"

alooprem == /\pc="loop"
            /\ y \geq x
            /\ z' = z
            /\ y' = y
            /\ pc'="rem"
            
aremhalt == /\ pc="rem"
            /\ x % y = 0
            /\ y' = y
            /\ z' = "false"
            /\ pc' = "halt"
            
aremloop == /\ pc="rem"
            /\ x % y # 0
            /\ y' = y+1
            /\ z' = z
            /\ pc' = "loop"

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

init == pc = "start" /\ z= 0 /\ y=0
next == astartloop \/ aloophalt \/ alooprem \/ aremhalt \/ aremloop
            
safety ==
            /\ pc="halt" /\ z = "true" => \A k : ( 2 \leq k /\ k < x => ( x % k # 0))
            /\ pc="halt" /\ z= "false" => ~(\A k : ( 2 \leq k /\ k < x =>(x % k # 0)))


=============================================================================
\* Modification History
\* Last modified Mon Oct 12 15:13:04 CEST 2015 by arthur
\* Created Mon Oct 12 14:14:06 CEST 2015 by arthur