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
