CristalCaveGem » LustreC

#open "dummy_lib"

const MatrixAddition_Constant_Value = [ [ 2, 3, 4 ], [ 5, 6, 7 ] ] ;

const MatrixAddition_Constant1_Value = [ [ 8, 9, 10 ], [ 11, 12, 13 ] ] ;

const MatrixAddition_Constant2_Value = [ [ 2, 3, 4 ] ] ;

const MatrixAddition_Constant4_Value = [ [ 5 ], [ 6 ], [ 7 ] ] ;

const MatrixAddition_Constant5_Value = [ [ 11 ], [ 12 ], [ 13 ] ] ;

node MatrixAddition (

	In1_Out1_11 : int)

returns (

	Out1_In1_93 : int^2^3 ;

	Out3_In1_105 : int^3^1 ;

	Out2_In1_117 : int^1^3) ;

var

	Sum_Out1_61 : int^2^3 ;

	Sum1_Out1_71 : int^1^3 ;

	Sum2_Out1_81 : int^3^1 ;

	Sum_In1_59 : int^2^3 ;

	Sum_In2_60 : int^2^3 ;

	Sum1_In1_69 : int^1^3 ;

	Sum1_In2_70 : int^1^3 ;

	Sum2_In1_79 : int^3^1 ;

	Sum2_In2_80 : int^3^1 ;

let

	Sum_Out1_61 = Sum_In1_59 + Sum_In2_60 ;

	Sum1_Out1_71 = Sum1_In1_69 + Sum1_In2_70 ;

	Sum2_Out1_81 = Sum2_In1_79 + Sum2_In2_80 ;

	Sum1_In1_69 = MatrixAddition_Constant2_Value ;

	Sum2_In1_79 = MatrixAddition_Constant4_Value ;

	Sum2_In2_80 = MatrixAddition_Constant5_Value ;

	Out1_In1_93 = Sum_Out1_61 ;

	Sum_In1_59 = MatrixAddition_Constant_Value ;

	Sum_In2_60 = MatrixAddition_Constant1_Value ;

	Out2_In1_117 = Sum1_Out1_71 ;

	Out3_In1_105 = Sum2_Out1_81 ;

	Sum1_In2_70 = In1_Out1_11 ;

	--! MAIN : true ;

tel

#open "dummy_lib"

const MatrixAndArrays_Constant_Value = [ [ 2.2, 3.3, 4.4, 2.2, 4.4, 3.3 ] ] ;

const MatrixAndArrays_Gain_Gain = [ [ 2.1, 1.0, 3.0, 4.2 ] ] ;

const MatrixAndArrays_UnitDelay_InitialValue = [ [ 1.1, 2.2, 1.0, 1.0 ] ] ;

node MatrixAndArrays (

	In1_Out1_11 : real^2^3)

returns (

	Out1_In1_57 : real^2^2) ;

var

	Gain_Out1_28 : real^2^2 ;

	Product_Out1_40 : real^2^2 ;

	UnitDelay_Out1_45 : real^2^2 ;

	Gain_In1_27 : real^2^2 ;

	Product_In1_38 : real^2^3 ;

	Product_In2_39 : real^3^2 ;

	UnitDelay_In1_44 : real^2^2 ;

let

	Gain_Out1_28 = _MatMul_real (2, 2, 2, MatrixAndArrays_Gain_Gain, Gain_In1_27) ;

	Product_Out1_40 = _MatMul_real (2, 3, Product_In1_38, Product_In2_39) ;

	UnitDelay_Out1_45 = MatrixAndArrays_UnitDelay_InitialValue -> pre UnitDelay_In1_44 ;

	Product_In1_38 = In1_Out1_11 ;

	Product_In2_39 = MatrixAndArrays_Constant_Value ;

	Gain_In1_27 = Product_Out1_40 ;

	UnitDelay_In1_44 = Gain_Out1_28 ;

	Out1_In1_57 = UnitDelay_Out1_45 ;

	--! MAIN : true ;

tel

#open "dummy_lib"

const RelOpMatrix_Constant_Value = 1.1 ;

node RelOpMatrix (

	In1_Out1_11 : real^2)

returns (

	Out1_In1_37 : bool^2) ;

var

	RelationalOperator_Out1_25 : bool^2 ;

	RelationalOperator_In1_23 : real^2 ;

	RelationalOperator_In2_24 : real^2 ;

let

	RelationalOperator_Out1_25 = _Vect_Leqt_real (2, RelationalOperator_In1_23, RelationalOperator_In2_24) ;

	RelationalOperator_In1_23 = In1_Out1_11 ;

RelationalOperator_In2_24 = [ RelOpMatrix_Constant_Value, RelOpMatrix_Constant_Value ] ;

	Out1_In1_37 = RelationalOperator_Out1_25 ;

	--! MAIN : true ;

tel

#open "dummy_lib"

node access(tab : int^3^4) returns (o:int)

var tab2,x;

let

  tab2 = [ 1, 2 ];

  x = 1^2^3[1];

  o = (tab[0][1]^2+test(pre o)+ tab2)[1];

tel

node add_vect_3 (in1,in2 : int^2) returns (out : int^2)

var t:int;

let

 t = in1[0];

out = [in1[0]+in2[0],in1[1]+in2[1]];

tel

node min_vect_2 (in : int^2) returns (out: int)

let

	out = if (in[0] < in[1]) then in[0] else in[1];

tel

node mumuse (in1 : int^2^2; mult : int) returns (out : int^4)

var

	tmp : int^2^2;

	tmp2 : int^2;

let

	tmp = [ [ in1[0][0]*mult , in1[0][1] ] , [ in1[1][0]*mult , in1[1][1] ] ];

	tmp2 = add_vect_3 ( tmp[0] , [ mult,mult ] );

	out = [ tmp[0][0] , min_vect_2 (tmp2) , tmp[0][1] , tmp2[1] ];

tel

node test(x:int) returns (t:int^2);

function _MatMul_real (

	const n, m, p : int ;

	in1 : real^n^m ;

	in2 : real^m^p)

returns (

	out : real^n^p) ;

function _Vect_Leqt_real (

	const n : int ;

	in : real^n ;

	in2 : real^n)

returns (

	out : bool^n) ;

node imp1(const m:int; a:int^(3*m)) returns (c:int^m);

node imp2(const n:int; a:int^n) returns (d:int^n);

#open "dummy_lib"

type choice = enum { one, two };

type entier = int;

const PI = 3;

const tab = [1.,2.,3.,4.];

const M1 = [ [ 2.1 ], [ 1.0 ], [ 3.0 ], [ 4.2 ] ] ;

const M2 = [ [ 1.1, 2.2, 1.0, 1.0 ] ] ;

node mult(

     in1 : real^4^1)

returns (

     out : real^1^1)

var l,p;

let

  l = [ tab, [3.,4.,5.,6.] ];

  p = l + [tab,tab+[3.,4.,5.,6.]];

  out = _MatMul_real (1,4,1,[ [ 2.1 ], [ 1.0 ], [ 3.0 ], [ 4.2 ] ], in1);

tel

node base(const p:int; x:int^(PI*p)) returns (y:int^p)

var z:int^(PI*p);

let

  z = imp2(PI*p, x);

  y = imp1(p, z);

tel

#open "dummy_lib"

const PI = 3;

node base(const p:int; x:int^(PI*p)) returns (y:int^p)

var z:int^(PI*p)^2;

    t;

let

  t = imp2(PI*p, x);

  z = [t, t];

  y = imp1(p, (pre z)[1]);

tel

#open "dummy_lib"

const PI = 3;

node base(const p:int; x:int^(PI*p)) returns (y:int^p)

var z:int^(PI*p);

let

  z = imp2(PI*p, x);

  y = imp1(p, z);

tel

node top(a:int) returns (y:int)

var x;

let

  x = [a,1,2,3,4,5,6,7,8,9,10,11,12,13,14];

  y = base (5, x)[0];

tel

node test (x:bool; d:bool) returns (a:int;b:int)

var e,f : bool;

let

  a = 1 when d;

  b = if x = d then 1 else 0;

  e = true fby e;

  f = if x then d else e;

tel

type choice = enum { one, two };

type entier = int;

const PI = 3;

const choix = one;

node toto (x:int) returns (a:int;y:int)

var c : choice;b1, b2:entier;

let

  a = PI fby (a+1);

  c = if a=x then one else two ;

  b1 = 1 when one(c);

  b2 = 2 when two(c);

  y = merge c (one -> b1) (two -> b2);

tel

node test (x:bool) returns (y:int)

var a:int; b:int;

let

   (a,b) = toto(if x then 0 else 1);

   y = a ;

tel

node f(x :int ) returns (cpt , y :int )

let

  y = x + 1;

  cpt = (0 fby cpt) + 1;

tel

node g(x :int ; c : bool ) returns (out :int )

var t, cpt , y, last_y :int;

let

  (cpt , y) = f(t);

  t = merge c (true -> x) (false -> last_y when false(c));

  last_y = 0 fby y;

  out = y when false(c);

tel

(*

node main (x:int) returns (out :int; c:bool)

var toto:int;

let

  toto = 1 ;

  c = toto = 0 (*true fby false fby c*);

  out = g(x,toto=0);

tel

*)

--@ ensures OK;

node top(onOff: bool; 

      decelSet: bool; 

      accelResume: bool; 

      cancel: bool; 

      brakePedal: bool; 

      carGear: int ; 

      carSpeed: real; 

      validInputs: bool)

      returns (OK:bool);

var

   mode: int ; 

      cruiseThrottle: real; 

      desiredSpeed: real; 

      VRP1: bool; 

      VRP2: bool; 

      CP8a: bool; 

      VRP3: bool; 

      VRP4: bool; 

      SP4: bool; 

      SP5: bool; 

      SP6: bool; 

      SP7: bool; 

      SP3b: bool; 

      SP3c: bool; 

      SP3: bool; 

      SP3a: bool; 

      SP2: bool; 

      SP1: bool; 

      SP8: bool; 

      SP9: bool; 

      SP10: bool; 

      SP11: bool;

   zz0: bool; 

   zz1: bool; 

   zz2: real; 

   zz3: bool; 

   zz4: bool; 

   zz5: real; 

   zz6: int ; 

   zz7: int ; 

   zz8: int ; 

   zz9: int ; 

   zz10: int ; 

   zz11: int ; 

   zz12: int ; 

   zz13: int ; 

   zz14: int ; 

   zz15: bool; 

   zz16: int ; 

   zz17: int ; 

   zz18: int ; 

   zz19: bool; 

   zz20: int ; 

   zz21: int ; 

   zz22: int ; 

   zz23: bool; 

   zz24: bool; 

   zz25: int ; 

   zz26: bool; 

   zz27: bool; 

   zz28: int ; 

   zz29: int ; 

   zz30: bool; 

   zz31: bool; 

   zz32: int ; 

   zz33: bool; 

   zz34: int ; 

   zz35: int ; 

   zz36: bool; 

   zz37: bool; 

   zz38: int ; 

   zz39: bool; 

   zz40: int ; 

   zz41: int ; 

   zz42: bool; 

   zz43: bool; 

   zz44: int ; 

   zz45: int ; 

   zz46: int ; 

   zz47: bool; 

   zz48: bool; 

   zz49: int ; 

   zz50: int ; 

   zz51: int ; 

   zz52: bool; 

   zz53: int ; 

   zz54: int ; 

   zz55: int ; 

   zz56: bool; 

   zz58: int ; 

   zz59: int ; 

   zz60: int ; 

   zz61: int ; 

   zz62: int ; 

   zz63: int ; 

   zz64: bool; 

   zz65: bool; 

   zz66: int ; 

   zz67: int ; 

   zz68: int ; 

   zz69: int ; 

   zz70: int ; 

   zz71: int ; 

   zz72: bool; 

   zz73: bool; 

   zz74: int ; 

   zz75: int ; 

   zz76: int ; 

   zz77: int ; 

   zz78: int ; 

   zz79: int ; 

   zz80: int ; 

   zz81: int ; 

   zz82: bool; 

   zz83: int ; 

   zz84: int ; 

   zz85: int ; 

   zz86: int ; 

   zz87: bool; 

   zz88: bool; 

   zz89: int ; 

   zz90: bool; 

   zz91: int ; 

   zz92: int ; 

   zz93: bool; 

   zz94: bool; 

   zz95: int ; 

   zz96: bool; 

   zz97: int ; 

   zz98: int ; 

   zz99: bool; 

   zz100: bool; 

   zz101: int ; 

   zz102: int ; 

   zz103: int ; 

   zz104: bool; 

   zz105: bool; 

   zz106: int ; 

   zz107: bool; 

   zz108: int ; 

   zz109: int ; 

   zz110: int ; 

   zz111: int ; 

   zz112: bool; 

   zz113: int ; 

   zz114: int ; 

   zz115: int ; 

   zz116: bool; 

   zz117: bool; 

   zz118: int ; 

   zz119: int ; 

   zz120: int ; 

   zz121: int ; 

   zz122: int ; 

   zz123: int ; 

   zz124: int ; 

   zz125: int ; 

   zz126: int ; 

   zz127: int ; 

   zz128: bool; 

   zz129: int ; 

   zz130: int ; 

   zz131: int ; 

   zz132: int ; 

   zz133: bool; 

   zz134: int ; 

   zz135: int ; 

   zz136: int ; 

   zz137: int ; 

   zz138: bool; 

   zz139: bool; 

   zz140: int ; 

   zz141: bool; 

   zz142: int ; 

   zz143: int ; 

   zz144: bool; 

   zz145: bool; 

   zz146: int ; 

   zz147: int ; 

   zz148: int ; 

   zz149: int ; 

   zz150: int ; 

   zz151: bool; 

   zz152: bool; 

   zz153: int ; 

   zz154: int ; 

   zz155: bool; 

   zz156: int ; 

   zz157: int ; 

   zz158: bool; 

   zz159: int ; 

   zz160: int ; 

   zz161: int ; 

   zz162: bool; 

   zz163: bool; 

   zz164: bool; 

   zz165: bool; 

   zz166: int ; 

   zz167: int ; 

   zz168: int ; 

   zz169: int ; 

   zz170: int ; 

   zz171: bool; 

   zz172: int ; 

   zz173: int ; 

   zz174: int ; 

   zz175: int ; 

   zz176: int ; 

   zz177: bool; 

   zz178: bool; 

   zz179: bool; 

   zz180: bool; 

   zz181: bool; 

   zz182: bool; 

   zz183: bool; 

   zz184: bool; 

   zz185: bool; 

   zz186: bool; 

   zz187: bool; 

   zz188: bool; 

   zz189: bool; 

   zz190: real; 

   zz191: bool; 

   zz192: bool; 

   zz193: bool; 

   zz194: bool; 

   zz195: bool; 

   zz196: bool; 

   zz197: bool; 

   zz198: bool; 

   zz199: bool; 

   zz200: bool; 

   zz201: bool; 

   zz202: bool; 

   zz203: bool; 

   zz204: real; 

   zz205: real; 

   zz206: bool; 

   zz207: bool; 

   zz208: bool; 

   zz209: bool; 

   zz210: bool; 

   zz211: real; 

   zz212: bool; 

   zz213: bool; 

   zz214: bool; 

   zz215: bool; 

   zz216: bool; 

   zz217: bool; 

   zz218: real; 

   zz219: real; 

   zz220: real; 

   zz221: real; 

   zz222: real; 

   zz223: real; 

   zz224: real; 

   zz225: real; 

   zz226: real; 

   zz227: real; 

   zz228: real; 

   zz229: real; 

   zz230: real; 

   zz231: bool; 

   zz232: bool; 

   zz233: bool; 

   zz234: bool; 

   zz235: bool; 

   zz236: bool; 

   zz237: bool; 

   zz238: bool; 

   zz239: bool;

let 

   zz166 = 

      (if (0 >= zz168)

         then 0

         else zz168);

   zz168 = 

      (if accelResume

         then zz167

         else 0);

   zz169 = (0 -> (pre zz170));

   zz172 = 

      (if (0 >= zz174)

         then 0

         else zz174);

   zz174 = 

      (if decelSet

         then zz173

         else 0);

   zz175 = (0 -> (pre zz176));

   zz156 = (0 -> (pre zz161));

   zz157 = (0 -> (pre mode));

   zz159 = 

      (if SP3c

         then 1

         else 0);

   (* Beginning transition segment: trans20

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz93 = ((zz91 = 8) and 

      (((

      (if ((zz185 = true) = false)

         then 0

         else 1) <> 0) and 

      (

      (if ((zz186 = true) = false)

         then 0

         else 1) <> 0)) and 

      (not zz88)));

   (* Beginning transition segment: trans19

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz99 = ((zz97 = 8) and 

      (((

      (if ((zz180 = true) = false)

         then 0

         else 1) <> 0) and 

      (

      (if ((zz186 = true) = false)

         then 0

         else 1) <> 0)) and 

      (not zz94)));

   (* Beginning transition segment: trans22

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz104 = ((zz102 = 7) and 

      (((

      (if ((zz185 = true) = false)

         then 0

         else 1) <> 0) and 

      (

      (if ((zz186 = true) = false)

         then 0

         else 1) <> 0)) and 

      (not zz100)));

   (* Beginning transition segment: trans24

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz24 = ((zz108 = 4) and 

      (

      (if ((zz185 = true) = false)

         then 0

         else 1) <> 0));

   (* Beginning transition segment: trans14

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz30 = ((zz28 = 4) and 

      ((

      (if ((zz171 = true) = false)

         then 0

         else 1) <> 0) and 

      (not zz24)));

   (* Beginning transition segment: trans15

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz36 = ((zz34 = 4) and 

      ((

      (if ((zz177 = true) = false)

         then 0

         else 1) <> 0) and 

      (not zz31)));

   (* Beginning transition segment: trans17

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz42 = ((zz40 = 6) and 

      ((

      (if ((zz177 = false) = false)

         then 0

         else 1) <> 0) and 

      (not zz37)));

   (* Beginning transition segment: trans16

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz47 = ((zz45 = 5) and 

      ((

      (if ((zz171 = false) = false)

         then 0

         else 1) <> 0) and 

      (not zz43)));

   OK = ((zz58 = 4) or 

      ((zz58 = 5) or 

      (zz58 = 6)));

   zz63 = 

      (if (not 

         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

         ((zz101 >= 3) and 

         (zz101 <= 6)))

         then 

               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)

               3

         else zz101);

   (* Beginning transition segment: trans18

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz64 = ((not 

      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

      ((zz101 >= 3) and 

      (zz101 <= 6))) and 

      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

      ((zz63 >= 3) and 

      (zz63 <= 6)));

   (* Beginning transition segment: trans12

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz116 = ((not 

      (* <In state> path: On maps to field: __root and value range: [2, 8] *)

      ((zz146 >= 2) and 

      (zz146 <= 8))) and 

      (* <In state> path: On maps to field: __root and value range: [2, 8] *)

      ((zz115 >= 2) and 

      (zz115 <= 8)));

   zz120 = 

      (if (zz142 = 1)

         then 

               (* <Exit state> path: Off maps to field: __root and value: 0 *)

               0

         else zz142);

   zz137 = 

      (if 

         (* <In state> path: On maps to field: __root and value range: [2, 8] *)

         ((zz156 >= 2) and 

         (zz156 <= 8))

         then 

               (* <Exit state> path: On maps to field: __root and value: 0 *)

               0

         else zz136);

   SP3c = true;

   zz171 = (zz170 = 20);

   (* Condition actions for transition segment: trans22: NONE

      Transition action(s) for transition: trans22

      <complete> is true if either: 

         1. this transition has completed, or 

         2. a higher-priority transition has already completed 

       *)

   zz105 = (zz104 or 

      zz100);

   zz127 = 

      (if (zz156 = 4)

         then 

               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)

               3

         else zz156);

   zz204 = cruiseThrottle;

   zz165 = (mode = 6);

   SP7 = ((not zz165) or 

      zz208);

   zz136 = 

      (if 

         (* <In state> path: On maps to field: __root and value range: [2, 8] *)

         ((zz156 >= 2) and 

         (zz156 <= 8))

         then zz123

         else zz135);

   (* Exit action(s) for transition: On_Init -> On_Active *)

   zz106 = 

      (if zz104

         then zz60

         else zz102);

   zz173 = (zz175 + 1);

   zz81 = 

      (if (zz147 = 4)

         then 

               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)

               3

         else zz147);

   zz181 = (carGear = 3);

   zz79 = 

      (if (zz84 = 6)

         then 

               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)

               3

         else zz84);

   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)

   zz38 = 

      (if zz36

         then zz14

         else zz34);

   (* Exit action(s) for transition: On -> On_Init: NONE

      Transition action(s) for transition: On -> On_Init: NONE

      Entry action(s) for transition: On -> On_Init *)

   zz119 = 

      (if zz116

         then zz114

         else zz143);

   (* Transition segment: trans12 complete. *)

   zz78 = 

      (if (not (zz89 = 8))

         then 3

         else zz148);

   zz15 = 

      (if (zz34 = 4)

         then false

         else zz33);

   zz83 = 

      (if 

         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

         ((zz147 >= 3) and 

         (zz147 <= 6))

         then zz81

         else zz147);

   zz54 = 

      (if (not (zz55 = 4))

         then 4

         else zz103);

   zz192 = (zz211 > desiredSpeed);

   zz16 = 

      (if (not (zz32 = 5))

         then 

               (* <Enter state> path: On.Active.Increase maps to field: __root and value: 5 *)

               5

         else zz32);

   zz158 = (false -> (pre zz162));

   SP3a = ((not (not zz163)) or 

      (not zz199));

   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE

      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE

      Entry action(s) for transition: On_Active -> On_Active_Maintain *)

   zz67 = 

      (if zz64

         then zz62

         else zz98);

   (* Transition segment: trans18 complete. *)

   (* Condition actions for transition segment: trans17: NONE

      Transition action(s) for transition: trans17

      <complete> is true if either: 

         1. this transition has completed, or 

         2. a higher-priority transition has already completed 

       *)

   zz43 = (zz42 or 

      zz37);

   zz76 = 

      (if (zz91 = 8)

         then 

               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)

               2

         else zz91);

   zz80 = 

      (if (zz83 = 5)

         then 

               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)

               3

         else zz83);

   zz198 = (zz197 or 

      zz196);

   zz193 = (desiredSpeed <> 0.0);

   SP1 = ((not (not zz186)) or 

      zz187);

   zz231 = (cruiseThrottle <= 100.0);

   zz123 = 

      (if (zz135 = 8)

         then 

               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)

               2

         else zz135);

   zz19 = 

      (if (zz28 = 4)

         then false

         else zz27);

   (* Condition actions for transition segment: trans20: NONE

      Transition action(s) for transition: trans20

      <complete> is true if either: 

         1. this transition has completed, or 

         2. a higher-priority transition has already completed 

       *)

   zz94 = (zz93 or 

      zz88);

   cruiseThrottle = 

      (if zz201

         then zz226

         else 0.0);

   zz86 = 

      (if 

         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

         ((zz147 >= 3) and 

         (zz147 <= 6))

         then 

               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)

               2

         else zz85);

   VRP1 = (zz232 and 

      zz231);

   zz131 = 

      (if 

         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

         ((zz156 >= 3) and 

         (zz156 <= 6))

         then zz125

         else zz130);

   zz235 = (desiredSpeed < 0.0);

   SP9 = ((not zz214) or 

      zz215);

   zz138 = 

      (if 

         (* <In state> path: On maps to field: __root and value range: [2, 8] *)

         ((zz156 >= 2) and 

         (zz156 <= 8))

         then zz133

         else zz158);

   zz65 = ((zz66 = 4) or 

      ((zz66 = 5) or 

      (zz66 = 6)));

   zz194 = (desiredSpeed >= 15.0);

   zz197 = (mode = 1);

   VRP3 = (not zz237);

   zz6 = 

      (if (not (zz49 = 4))

         then 

               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)

               4

         else zz49);

   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Increase *)

   zz33 = 

      (if zz30

         then zz19

         else zz27);

   zz134 = 

      (if 

         (* <In state> path: On maps to field: __root and value range: [2, 8] *)

         ((zz156 >= 2) and 

         (zz156 <= 8))

         then zz132

         else zz156);

   zz61 = 

      (if (not (zz63 = 4))

         then 

               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)

               4

         else zz63);

   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE

      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)

   zz34 = 

      (if zz30

         then zz16

         else zz32);

   (* Transition segment: trans14 complete. *)

   (* Exit action(s) for transition: On -> Off *)

   zz141 = 

      (if zz139

         then zz138

         else zz158);

   (* Beginning transition segment: trans13

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz139 = (

      (* <In state> path: On maps to field: __root and value range: [2, 8] *)

      ((zz156 >= 2) and 

      (zz156 <= 8)) and 

      (not onOff));

   zz178 = accelResume;

   zz234 = (desiredSpeed >= 0.0);

   (* Transition action(s) for transition: On_Active_Decrease -> On_Active_Maintain: NONE

      Entry action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)

   zz45 = 

      (if zz42

         then zz9

         else zz44);

   (* Transition segment: trans17 complete. *)

   zz121 = 

      (if (not (zz140 = 1))

         then 

               (* <Enter state> path: Off maps to field: __root and value: 1 *)

               1

         else zz140);

   zz184 = (true -> (pre zz183));

   (* Exit action(s) for transition: On -> On_Init: NONE

      Transition action(s) for transition: On -> On_Init: NONE

      Entry action(s) for transition: On -> On_Init *)

   zz118 = 

      (if zz116

         then zz113

         else zz115);

   (* Transition segment: trans12 complete. *)

   zz191 = (zz189 and 

      zz188);

   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE

      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)

   zz41 = 

      (if zz36

         then zz13

         else zz35);

   (* Transition segment: trans15 complete. *)

   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE

      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)

   zz35 = 

      (if zz30

         then zz17

         else zz29);

   (* Transition segment: trans14 complete. *)

   zz208 = (zz211 >= desiredSpeed);

   zz200 = (zz223 = 0.0);

   zz154 = 

      (if (not (zz156 = 1))

         then 1

         else zz157);

   zz73 = ((zz74 = 4) or 

      ((zz74 = 5) or 

      (zz74 = 6)));

   (* Transition action(s) for transition: On -> Off: NONE

      Entry action(s) for transition: On -> Off *)

   zz142 = 

      (if zz139

         then zz121

         else zz140);

   (* Transition segment: trans13 complete. *)

   zz124 = 

      (if (zz134 = 7)

         then 

               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)

               2

         else zz134);

   VRP4 = ((zz238 or 

      zz195) or 

      zz239);

   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE

      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE

      Entry action(s) for transition: On_Active -> On_Active_Maintain *)

   zz75 = 

      (if zz72

         then zz70

         else zz92);

   (* Transition segment: trans18 complete. *)

   zz233 = (desiredSpeed <= 100.0);

   zz223 = 

      (if zz217

         then zz2

         else zz218);

   zz185 = ((not zz184) and 

      zz183);

   zz180 = ((not zz179) and 

      zz178);

   zz239 = (desiredSpeed = carSpeed);

   (* Transition action(s) for transition: Off -> On: NONE

      Entry action(s) for transition: Off -> On *)

   zz148 = 

      (if zz144

         then zz119

         else zz143);

   (* Transition segment: trans23 complete. *)

   zz115 = 

      (if (not 

         (* <In state> path: On maps to field: __root and value range: [2, 8] *)

         ((zz146 >= 2) and 

         (zz146 <= 8)))

         then 

               (* <Enter state> path: On maps to field: __root and value: 2 *)

               2

         else zz146);

   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE

      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)

   zz40 = 

      (if zz36

         then zz12

         else zz38);

   (* Transition segment: trans15 complete. *)

   (* Exit action(s) for transition: On -> Off *)

   zz140 = 

      (if zz139

         then zz137

         else zz156);

   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)

   zz39 = 

      (if zz36

         then zz15

         else zz33);

   zz8 = 

      (if (zz45 = 5)

         then 

               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)

               3

         else zz45);

   zz122 = 

      (if (not (zz140 = 1))

         then 1

         else zz157);

   zz179 = (true -> (pre zz178));

   zz82 = 

      (if (zz147 = 4)

         then false

         else zz141);

   zz203 = (zz201 or 

      zz202);

   zz186 = (((((not cancel) and 

      (not brakePedal)) and 

      zz181) and 

      zz182) and 

      validInputs);

   zz183 = decelSet;

   zz155 = (true -> 

      (if (pre SP3c)

         then false

         else (pre zz155)));

   zz196 = (mode = 2);

   zz161 = zz160;

   zz9 = 

      (if (not (zz44 = 4))

         then 

               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)

               4

         else zz44);

   (* Transition action(s) for transition: On_Inactive -> On_Active *)

   zz96 = 

      (if zz93

         then true

         else zz90);

   zz52 = 

      (if ((not zz48) and 

         (zz50 = 4))

         then false

         else zz39);

   zz0 = zz217;

   zz2 = (

      (if (zz1 and 

         (not zz0))

         then 0.0

         else (zz222 + 0.05)) -> 

      (if (zz1 and 

         (not zz0))

         then 0.0

         else 

      (if zz0

         then (zz222 + 0.05)

         else (pre zz2))));

   zz1 = (true -> 

      (if (pre zz0)

         then false

         else (pre zz1)));

   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE

      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)

   zz51 = 

      (if zz47

         then zz7

         else zz46);

   (* Transition segment: trans16 complete. *)

   zz162 = 

      (if SP3c

         then 

               (if zz155

                  then zz158

                  else zz151)

         else zz158);

   (* Condition actions for transition segment: trans19: NONE

      Transition action(s) for transition: trans19

      <complete> is true if either: 

         1. this transition has completed, or 

         2. a higher-priority transition has already completed 

       *)

   zz100 = (zz99 or 

      zz94);

   zz53 = 

      (if (not (zz55 = 4))

         then 

               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)

               4

         else zz55);

   zz188 = (desiredSpeed <> 100.0);

   SP10 = ((not zz191) or 

      zz192);

   zz13 = 

      (if (not (zz38 = 6))

         then 5

         else zz35);

   zz201 = ((zz163 or 

      zz164) or 

      zz165);

   zz14 = 

      (if (zz34 = 4)

         then 

               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)

               3

         else zz34);

   zz126 = 

      (if (zz129 = 5)

         then 

               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)

               3

         else zz129);

   (* Exit action(s) for outer loop transition: On_Active_Maintain *)

   zz26 = 

      (if zz24

         then zz23

         else zz107);

   (* Exit action(s) for transition: Off -> On *)

   zz146 = 

      (if zz144

         then zz120

         else zz142);

   zz199 = (

      (if (zz162 = false)

         then 0.0

         else 1.0) = 1.0);

   zz227 = (desiredSpeed - carSpeed);

   zz150 = 

      (if ((not zz145) and 

         (* <In state> path: On maps to field: __root and value range: [2, 8] *)

         ((zz147 >= 2) and 

         (zz147 <= 8)))

         then zz111

         else zz148);

   zz177 = (zz176 = 20);

   (* Transition action(s) for outer loop transition: On_Active_Maintain *)

   zz27 = 

      (if zz24

         then true

         else zz26);

   (* Entry action(s) for transition: On_Inactive -> On_Active *)

   zz97 = 

      (if zz93

         then zz74

         else zz95);

   (* Transition segment: trans20 complete. *)

   zz195 = (desiredSpeed = 0.0);

   zz71 = 

      (if (not 

         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

         ((zz95 >= 3) and 

         (zz95 <= 6)))

         then 

               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)

               3

         else zz95);

   zz62 = 

      (if (not (zz63 = 4))

         then 4

         else zz98);

   zz229 = 

      (if (zz228 < ( -10.0))

         then ( -10.0)

         else 

      (if (zz228 > 10.0)

         then 10.0

         else zz228));

   (* Transition action(s) for transition: On_Inactive -> On_Active: NONE

      Entry action(s) for transition: On_Inactive -> On_Active *)

   zz103 = 

      (if zz99

         then zz67

         else zz98);

   (* Transition segment: trans19 complete. *)

   zz55 = 

      (if (not 

         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

         ((zz106 >= 3) and 

         (zz106 <= 6)))

         then 

               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)

               3

         else zz106);

   (* Beginning transition segment: trans18

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz56 = ((not 

      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

      ((zz106 >= 3) and 

      (zz106 <= 6))) and 

      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

      ((zz55 >= 3) and 

      (zz55 <= 6)));

   (* Beginning transition segment: trans18

      <fired> is true if the following are true: 

         1. the previous transition guard was true, 

         2. the source node for the transition is active, 

         3. the condition for the transition to fire is true, and 

         4. no higher-priority transition has completed (not <complete>) *)

   zz72 = ((not 

      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)

      ((zz95 >= 3) and 

      (zz95 <= 6))) and