var i,j,k,l,m; location l0 with (i=0 j=100 k=1000 l=10000 m=100000); location l1; location l2; location l3; location l4; location l5; location l6; transition t0 l0 -> l1; transition t1 l1 -> l1 with Guard (i <= 999) i := i+1; transition t2 l1 -> l2 with Guard (i >= 1000); transition t3 l2 -> l2 with Guard (j <= 999) j := j+k; transition t4 l2 -> l3 with Guard (j >= 1000); transition t5 l3 -> l3 with Guard (k >= 101) k := k-j; transition t6 l3 -> l4 with Guard (k <= 100); transition t7 l4 -> l4 with Guard (l >= 1001) l := l+k; transition t8 l4 -> l5 with Guard (l <= 1000); transition t9 l5 -> l5 with Guard (m >= 2) m := m-l; transition t10 l5 -> l6 with Guard (m <= 1); end