var i, j; location l0 with (i=1 j=10) ; location l1 ; location l2; location l3; location l4; transition t0 l0 -> l3 with i:=i+2 j:=j-1; transition t1 l3 -> l4 with i:=i+2 j:=j-1; transition t2 l4 -> l4 with Guard (i<=j) i := i+2 j := j-1 ; transition t2 l1->l2 with Guard (i>=j+1) ; end