----------------------------- MODULE squareroot -----------------------------


EXTENDS Integers, TLC
CONSTANTS x
VARIABLES pc, y1, y2, y3, z

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

al0l1 == pc="l0" /\ y1'=0 /\ y2' = 1 /\ y3' = 1 /\ z'=z /\pc'="l2"

al1l2 == pc="l1" /\ y2 \leq x /\ pc' = "l2" /\ UNCHANGED <<y1, y2, y3, z>>

al1l4 == pc="l1" /\ y2 > x /\ pc'="l4" /\ UNCHANGED <<y1, y2, y3, z>>

al2l3 == pc="l2" /\ y1' = y1+1 /\ y2' = y2+y3+2 /\ pc'="l3" /\ z'=z

al3l2 == pc="l3" /\ y2 \leq x /\ pc'="l2" /\UNCHANGED <<y1, y2, y3, z>>

al3l4 == pc="l3" /\ y2 > x /\ pc'="l4" /\ UNCHANGED <<y1, y2, y3, z>>

al4l5 == pc="l4" /\ z' = y1 /\ pc' = "l5" /\ UNCHANGED <<y1, y2, y3>>

Init == y1 =1 /\ y2=0 /\ y3=0 /\ z=0 /\ pc="l0"

Next == al0l1 \/ al1l2 \/ al1l4 \/ al2l3 \/ al3l2 \/ al3l4 \/ al4l5



=============================================================================
\* Modification History
\* Last modified Mon Oct 12 15:45:00 CEST 2015 by arthur
\* Created Mon Oct 12 15:33:31 CEST 2015 by arthur