var t,x,y,z;

initial linit;

linit -> para :
      guard x=0 and y=0 and z=0 assign { t := 0; };
linit -> paray :
      guard x=0 and y=0 and z=0 assign { t := 0; };
linit -> parax :
      guard x=0 and y=0 and z=0 assign { t := 0; };
linit -> paraxy :
      guard x=0 and y=0 and z=0 assign { t := 0; };
linit -> paraxyy :
      guard x=0 and y=0 and z=0 assign { t := 0; };

para -> para :
      guard true assign { t:=t+1; x:=x+y; y:=y+z; z:=z+1; }
      /* load("diag"); set_display('xml)$
	 m:matrix([1,0,0,0,1],[0,1,1,0,0],[0,0,1,1,0],[0,0,0,1,1],[0,0,0,0,1]); j:jordan(m); mj:dispJordan(j); pinv:ModeMatrix(m,j);p:invert(pinv);pinv.mj.p;  set_display('none)$ float(rectform(pinv)); float(rectform(j)); float(rectform(p));
      */
      jordan
 matrix([0.0,0.0,1.0,0.0,1.0],[1.0,0.0,0.0,0.0,0.0],
	       [0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0])
 [[1.0,4.0,1.0]]
 matrix([0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0],[0.0,0.0,0.0,0.0,1.0],
	       [1.0,0.0,0.0,-1.0,0.0])
     ;
para -> parae :
      guard true assign {};

paray -> paray :
      guard y<=7 assign { t:=t+1; x:=x+y; y:=y+z; z:=z+1; }
      jordan
 matrix([0.0,0.0,1.0,0.0,1.0],[1.0,0.0,0.0,0.0,0.0],
	       [0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0])
 [[1.0,4.0,1.0]]
 matrix([0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0],[0.0,0.0,0.0,0.0,1.0],
	       [1.0,0.0,0.0,-1.0,0.0])
     ;
paray -> paraye :
      guard y>=8 assign {};

parax -> parax :
      guard x<=30 assign { t:=t+1; x:=x+y; y:=y+z; z:=z+1; }
      jordan
 matrix([0.0,0.0,1.0,0.0,1.0],[1.0,0.0,0.0,0.0,0.0],
	       [0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0])
 [[1.0,4.0,1.0]]
 matrix([0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0],[0.0,0.0,0.0,0.0,1.0],
	       [1.0,0.0,0.0,-1.0,0.0])
     ;
parax -> paraxe :
      guard x>=31 assign {};

paraxy -> paraxy :
      guard x+y<=30 assign { t:=t+1; x:=x+y; y:=y+z; z:=z+1; }
      jordan
 matrix([0.0,0.0,1.0,0.0,1.0],[1.0,0.0,0.0,0.0,0.0],
	       [0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0])
 [[1.0,4.0,1.0]]
 matrix([0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0],[0.0,0.0,0.0,0.0,1.0],
	       [1.0,0.0,0.0,-1.0,0.0])
     ;
paraxy -> paraxye :
      guard x+y>=31 assign {};

paraxyy -> paraxyy :
      guard x-2y<=30 assign { t:=t+1; x:=x+y; y:=y+z; z:=z+1; }
      jordan
 matrix([0.0,0.0,1.0,0.0,1.0],[1.0,0.0,0.0,0.0,0.0],
	       [0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0])
 [[1.0,4.0,1.0]]
 matrix([0.0,1.0,0.0,0.0,0.0],[0.0,0.0,1.0,0.0,0.0],
	       [0.0,0.0,0.0,1.0,0.0],[0.0,0.0,0.0,0.0,1.0],
	       [1.0,0.0,0.0,-1.0,0.0])
     ;
paraxyy -> paraxyye :
      guard x-2y>=31 assign {};