var x,y;

initial linit;

linit -> l0 :
      guard 1<=x and x<=3 and 0<=y and y<=2 assign {};
linit -> l1 :
      guard 1<=x and x<=3 and 0<=y and y<=2 assign {};
linit -> l2 :
      guard 1<=x and x<=3 and 0<=y and y<=2 assign {};
linit -> l3 :
      guard 1<=x and x<=3 and 0<=y and y<=2 assign {};
l0 -> l0 :
      guard true assign { x:=1.5*x; y:=y+1; }
      jordan
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
      [[1.5,1],[1.0,2]]
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
;
l0 -> l0e :
      guard true assign {}
;
l1 -> l1 :
      guard y<=3 assign { x:=1.5*x; y:=y+1; }
      jordan
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
      [[1.5,1],[1.0,2]]
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
;
l1 -> l1e :
      guard y>=3 assign {}
;
l2 -> l2 :
      guard x+3*y<=100 assign { x:=1.5*x; y:=y+1; }
      jordan
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
      [[1.5,1],[1.0,2]]
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
;
l2 -> l2e :
      guard x+3*y>=100 assign {}
;
l3 -> l3 :
      guard x<=100 assign { x:=1.5*x; y:=y+1; }
      jordan
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
      [[1.5,1],[1.0,2]]
      matrix([1.0,0.0,0.0],[0.0,1.0,0.0],[0.0,0.0,1.0])
;
l3 -> l3e :
      guard x>=100 assign {}
;