Project

General

Profile

« Previous | Next » 

Revision 105b3645

Added by Guillaume Davy over 9 years ago

Delete tests files that have no k

View differences:

tests/gen_contracts.py
12 12
re_node = re.compile('.*node.*')
13 13
re_ensures = re.compile('.*ensures.*')
14 14
re_k = re.compile('--![ ]*k[ ]*:([^;]*);')
15
re_frama_res = re.compile('Proved goals:[ ]*([0-9]*)[ ]*/[ ]*([0-9]*)')
15 16

  
16 17
def findInLines(lines, regex):
17 18
	res = []
......
59 60
	properties = findInLines(lines, re_property)
60 61
	k = findInLines(lines, re_k)
61 62
	if k:
62
		return (None, "ALREADY", None)
63
		return (None, "ALREADY", "KEEP")
63 64
	if not properties:
64 65
		return (None, "NOPR", None)
65 66
	if len(properties) > 1:
......
68 69
	f = open(top, 'w')
69 70
	f.write("".join(lines))
70 71
	f.close()
71
	p = subprocess.Popen(["timeout", "40", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
72
	p = subprocess.Popen(["timeout", "10", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
72 73
	(stdout, stderr) = p.communicate()
73 74
	try:
74 75
		root = ET.fromstring(stdout)
75 76
	except ET.ParseError:
76 77
		return (None, "TIMEOUT", None)
78
	answer = root.find(".//Answer")
79
	if answer is None:
80
		return (None, "NO_ANS", None)
81
	if answer.text != "valid":
82
		return (None, "INVALID", None)
77 83
	k = root.find(".//K")
78 84
	if k is None:
79
		return (None, "ERR", None)
85
		return (None, "NO_K", None)
80 86
	try:
81 87
		k = int(k.text)
82 88
	except ValueError:
83 89
		return (None, "NOTPROVED", None)
84 90
	lines.insert(properties[0][0], "--!k:{};\n".format(k))
85
	return (lines, "OK("+"k=" + str(k)+")", None)
91
	return (lines, "OK("+"k=" + str(k)+")", "KEEP")
86 92

  
87 93
def compileLustre(lines, temp):
88 94
	top = temp + "/top.lus"
......
93 99
	(stdout, stderr) = p.communicate()
94 100
	res = p.wait()
95 101
	if res != 0:
96
		return (None, "ERR_"+str(res), stdout+"\n-------\n"+stderr)
102
		return (None, "ERR_"+str(res), None)
97 103
	return (lines, "OK", None)
98 104

  
99

  
100

  
101 105
def framac(lines, temp):
102
	FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-rte", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10""", "-wp-script", temp+"/top.coq" "-wp-no-let"]
106
	FRAMAC=["frama-c", temp+"/top.c"]
103 107
	p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
104 108
	(stdout, stderr) = p.communicate()
105 109
	res = p.wait()
106 110
	if res != 0:
107
		return (None, "ERR_"+str(res), temp+"\n"+stdout+"\n-------\n"+stderr)
108
	return (lines, "OK", stdout)
111
		return (None, "PARSE_"+str(res), None)
112
	FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" """, "-wp-script", temp+"/top.coq", "-wp-no-let"]
113
	#"-wp-rte", 
114
	p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
115
	(stdout, stderr) = p.communicate()
116
	res = p.wait()
117
	if res != 0:
118
		return (None, "ERR_"+str(res), None)
119
	m = re_frama_res.search(stdout)
120
	if not m:
121
		return (None, "BAD_OUT", None)
122
	return (lines, str(m.group(1))+"/"+str(m.group(2)), None)
109 123

  
110 124

  
111
def parseFile(inp, out, todo):
125
def parseFile(inp, todo):
112 126
	lines = inp.readlines()
113 127
	
114 128
	temp = tempfile.mkdtemp(prefix="contracts_")
115 129
	res = ""
116
	dats = []
130
	data = None
131
	ok = False
117 132
	for f in todo:
118 133
		x = [[]]
119
		(newlines, r, data) = f(lines[:], temp)
120
		res += "{:10} ".format(r[:10])
134
		(newlines, r, cmd) = f(lines[:], temp)
135
		res += "{:8} ".format(r[:8])
121 136
		if newlines:
122 137
			lines = newlines
123
		if data:
124
			dats.append(data)
125
	out.write("".join(lines))
138
		if cmd == "STOP":
139
			break
140
		if cmd == "KEEP":
141
			ok = True
142
	if ok:
143
		res += "WRITE"
144
		data = "".join(lines)
126 145
	shutil.rmtree(temp)
127 146
	
128
	return (res, dats)
147
	return (res, data)
129 148

  
130
TODO=[modProperties, addEnsures, addK, compileLustre]
149
TODO=[modProperties, addEnsures, addK, compileLustre, framac]
131 150

  
132
LENGTH=50
151
LENGTH=40
133 152

  
134 153
target="./generated/"
135 154

  
136
#if os.path.exists(target):
137
#	shutil.rmtree(target)
155
if os.path.exists(target):
156
	shutil.rmtree(target)
138 157

  
139
orig = "/home/davyg/good"
158
orig = "tests_new"
140 159
for root, dirs, files in os.walk(orig):
141 160
	short = root[len(orig):]
142 161
	os.mkdir(target+"/"+short)
......
144 163
		if not x.endswith(".lus"):
145 164
			continue
146 165
		inp = open(root+"/"+x, "r")
147
		out = open(target+"/"+short+"/"+x, "w")
148
		(res, dats) = parseFile(inp, out, TODO)
166
		(res, data) = parseFile(inp, TODO)
149 167
		inp.close()
150
		out.close()
168
		if data:
169
			out = open(target+"/"+short+"/"+x, "w")
170
			out.write(data)
171
			out.close()
151 172
		print(("Process {0:"+str(LENGTH)+"} : {1}").format(("./"+short+"/"+x)[:LENGTH], res))
152
		if dats:
153
			print("\n/////////////////////\n".join(dats))
154 173
		sys.stdout.flush()
tests/large/ccp01.lus
1

  
2

  
3
--@ ensures OK;
4
node top(onOff: bool; 
5
      decelSet: bool; 
6
      accelResume: bool; 
7
      cancel: bool; 
8
      brakePedal: bool; 
9
      carGear: int ; 
10
      carSpeed: real; 
11
      validInputs: bool)
12
      returns (OK:bool);
13

  
14
var
15
   mode: int ; 
16
      cruiseThrottle: real; 
17
      desiredSpeed: real; 
18
      VRP1: bool; 
19
      VRP2: bool; 
20
      CP8a: bool; 
21
      VRP3: bool; 
22
      VRP4: bool; 
23
      SP4: bool; 
24
      SP5: bool; 
25
      SP6: bool; 
26
      SP7: bool; 
27
      SP3b: bool; 
28
      SP3c: bool; 
29
      SP3: bool; 
30
      SP3a: bool; 
31
      SP2: bool; 
32
      SP1: bool; 
33
      SP8: bool; 
34
      SP9: bool; 
35
      SP10: bool; 
36
      SP11: bool;
37
   zz0: bool; 
38
   zz1: bool; 
39
   zz2: real; 
40
   zz3: bool; 
41
   zz4: bool; 
42
   zz5: real; 
43
   zz6: int ; 
44
   zz7: int ; 
45
   zz8: int ; 
46
   zz9: int ; 
47
   zz10: int ; 
48
   zz11: int ; 
49
   zz12: int ; 
50
   zz13: int ; 
51
   zz14: int ; 
52
   zz15: bool; 
53
   zz16: int ; 
54
   zz17: int ; 
55
   zz18: int ; 
56
   zz19: bool; 
57
   zz20: int ; 
58
   zz21: int ; 
59
   zz22: int ; 
60
   zz23: bool; 
61
   zz24: bool; 
62
   zz25: int ; 
63
   zz26: bool; 
64
   zz27: bool; 
65
   zz28: int ; 
66
   zz29: int ; 
67
   zz30: bool; 
68
   zz31: bool; 
69
   zz32: int ; 
70
   zz33: bool; 
71
   zz34: int ; 
72
   zz35: int ; 
73
   zz36: bool; 
74
   zz37: bool; 
75
   zz38: int ; 
76
   zz39: bool; 
77
   zz40: int ; 
78
   zz41: int ; 
79
   zz42: bool; 
80
   zz43: bool; 
81
   zz44: int ; 
82
   zz45: int ; 
83
   zz46: int ; 
84
   zz47: bool; 
85
   zz48: bool; 
86
   zz49: int ; 
87
   zz50: int ; 
88
   zz51: int ; 
89
   zz52: bool; 
90
   zz53: int ; 
91
   zz54: int ; 
92
   zz55: int ; 
93
   zz56: bool; 
94
   zz58: int ; 
95
   zz59: int ; 
96
   zz60: int ; 
97
   zz61: int ; 
98
   zz62: int ; 
99
   zz63: int ; 
100
   zz64: bool; 
101
   zz65: bool; 
102
   zz66: int ; 
103
   zz67: int ; 
104
   zz68: int ; 
105
   zz69: int ; 
106
   zz70: int ; 
107
   zz71: int ; 
108
   zz72: bool; 
109
   zz73: bool; 
110
   zz74: int ; 
111
   zz75: int ; 
112
   zz76: int ; 
113
   zz77: int ; 
114
   zz78: int ; 
115
   zz79: int ; 
116
   zz80: int ; 
117
   zz81: int ; 
118
   zz82: bool; 
119
   zz83: int ; 
120
   zz84: int ; 
121
   zz85: int ; 
122
   zz86: int ; 
123
   zz87: bool; 
124
   zz88: bool; 
125
   zz89: int ; 
126
   zz90: bool; 
127
   zz91: int ; 
128
   zz92: int ; 
129
   zz93: bool; 
130
   zz94: bool; 
131
   zz95: int ; 
132
   zz96: bool; 
133
   zz97: int ; 
134
   zz98: int ; 
135
   zz99: bool; 
136
   zz100: bool; 
137
   zz101: int ; 
138
   zz102: int ; 
139
   zz103: int ; 
140
   zz104: bool; 
141
   zz105: bool; 
142
   zz106: int ; 
143
   zz107: bool; 
144
   zz108: int ; 
145
   zz109: int ; 
146
   zz110: int ; 
147
   zz111: int ; 
148
   zz112: bool; 
149
   zz113: int ; 
150
   zz114: int ; 
151
   zz115: int ; 
152
   zz116: bool; 
153
   zz117: bool; 
154
   zz118: int ; 
155
   zz119: int ; 
156
   zz120: int ; 
157
   zz121: int ; 
158
   zz122: int ; 
159
   zz123: int ; 
160
   zz124: int ; 
161
   zz125: int ; 
162
   zz126: int ; 
163
   zz127: int ; 
164
   zz128: bool; 
165
   zz129: int ; 
166
   zz130: int ; 
167
   zz131: int ; 
168
   zz132: int ; 
169
   zz133: bool; 
170
   zz134: int ; 
171
   zz135: int ; 
172
   zz136: int ; 
173
   zz137: int ; 
174
   zz138: bool; 
175
   zz139: bool; 
176
   zz140: int ; 
177
   zz141: bool; 
178
   zz142: int ; 
179
   zz143: int ; 
180
   zz144: bool; 
181
   zz145: bool; 
182
   zz146: int ; 
183
   zz147: int ; 
184
   zz148: int ; 
185
   zz149: int ; 
186
   zz150: int ; 
187
   zz151: bool; 
188
   zz152: bool; 
189
   zz153: int ; 
190
   zz154: int ; 
191
   zz155: bool; 
192
   zz156: int ; 
193
   zz157: int ; 
194
   zz158: bool; 
195
   zz159: int ; 
196
   zz160: int ; 
197
   zz161: int ; 
198
   zz162: bool; 
199
   zz163: bool; 
200
   zz164: bool; 
201
   zz165: bool; 
202
   zz166: int ; 
203
   zz167: int ; 
204
   zz168: int ; 
205
   zz169: int ; 
206
   zz170: int ; 
207
   zz171: bool; 
208
   zz172: int ; 
209
   zz173: int ; 
210
   zz174: int ; 
211
   zz175: int ; 
212
   zz176: int ; 
213
   zz177: bool; 
214
   zz178: bool; 
215
   zz179: bool; 
216
   zz180: bool; 
217
   zz181: bool; 
218
   zz182: bool; 
219
   zz183: bool; 
220
   zz184: bool; 
221
   zz185: bool; 
222
   zz186: bool; 
223
   zz187: bool; 
224
   zz188: bool; 
225
   zz189: bool; 
226
   zz190: real; 
227
   zz191: bool; 
228
   zz192: bool; 
229
   zz193: bool; 
230
   zz194: bool; 
231
   zz195: bool; 
232
   zz196: bool; 
233
   zz197: bool; 
234
   zz198: bool; 
235
   zz199: bool; 
236
   zz200: bool; 
237
   zz201: bool; 
238
   zz202: bool; 
239
   zz203: bool; 
240
   zz204: real; 
241
   zz205: real; 
242
   zz206: bool; 
243
   zz207: bool; 
244
   zz208: bool; 
245
   zz209: bool; 
246
   zz210: bool; 
247
   zz211: real; 
248
   zz212: bool; 
249
   zz213: bool; 
250
   zz214: bool; 
251
   zz215: bool; 
252
   zz216: bool; 
253
   zz217: bool; 
254
   zz218: real; 
255
   zz219: real; 
256
   zz220: real; 
257
   zz221: real; 
258
   zz222: real; 
259
   zz223: real; 
260
   zz224: real; 
261
   zz225: real; 
262
   zz226: real; 
263
   zz227: real; 
264
   zz228: real; 
265
   zz229: real; 
266
   zz230: real; 
267
   zz231: bool; 
268
   zz232: bool; 
269
   zz233: bool; 
270
   zz234: bool; 
271
   zz235: bool; 
272
   zz236: bool; 
273
   zz237: bool; 
274
   zz238: bool; 
275
   zz239: bool;
276

  
277
let 
278
   zz166 = 
279
      (if (0 >= zz168)
280
         then 0
281
         else zz168);
282

  
283
   zz168 = 
284
      (if accelResume
285
         then zz167
286
         else 0);
287

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

  
290
   zz172 = 
291
      (if (0 >= zz174)
292
         then 0
293
         else zz174);
294

  
295
   zz174 = 
296
      (if decelSet
297
         then zz173
298
         else 0);
299

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

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

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

  
306
   zz159 = 
307
      (if SP3c
308
         then 1
309
         else 0);
310

  
311
   (* Beginning transition segment: trans20
312
      <fired> is true if the following are true: 
313
         1. the previous transition guard was true, 
314
         2. the source node for the transition is active, 
315
         3. the condition for the transition to fire is true, and 
316
         4. no higher-priority transition has completed (not <complete>) *)
317
   zz93 = ((zz91 = 8) and 
318
      (((
319
      (if ((zz185 = true) = false)
320
         then 0
321
         else 1) <> 0) and 
322
      (
323
      (if ((zz186 = true) = false)
324
         then 0
325
         else 1) <> 0)) and 
326
      (not zz88)));
327

  
328
   (* Beginning transition segment: trans19
329
      <fired> is true if the following are true: 
330
         1. the previous transition guard was true, 
331
         2. the source node for the transition is active, 
332
         3. the condition for the transition to fire is true, and 
333
         4. no higher-priority transition has completed (not <complete>) *)
334
   zz99 = ((zz97 = 8) and 
335
      (((
336
      (if ((zz180 = true) = false)
337
         then 0
338
         else 1) <> 0) and 
339
      (
340
      (if ((zz186 = true) = false)
341
         then 0
342
         else 1) <> 0)) and 
343
      (not zz94)));
344

  
345
   (* Beginning transition segment: trans22
346
      <fired> is true if the following are true: 
347
         1. the previous transition guard was true, 
348
         2. the source node for the transition is active, 
349
         3. the condition for the transition to fire is true, and 
350
         4. no higher-priority transition has completed (not <complete>) *)
351
   zz104 = ((zz102 = 7) and 
352
      (((
353
      (if ((zz185 = true) = false)
354
         then 0
355
         else 1) <> 0) and 
356
      (
357
      (if ((zz186 = true) = false)
358
         then 0
359
         else 1) <> 0)) and 
360
      (not zz100)));
361

  
362
   (* Beginning transition segment: trans24
363
      <fired> is true if the following are true: 
364
         1. the previous transition guard was true, 
365
         2. the source node for the transition is active, 
366
         3. the condition for the transition to fire is true, and 
367
         4. no higher-priority transition has completed (not <complete>) *)
368
   zz24 = ((zz108 = 4) and 
369
      (
370
      (if ((zz185 = true) = false)
371
         then 0
372
         else 1) <> 0));
373

  
374
   (* Beginning transition segment: trans14
375
      <fired> is true if the following are true: 
376
         1. the previous transition guard was true, 
377
         2. the source node for the transition is active, 
378
         3. the condition for the transition to fire is true, and 
379
         4. no higher-priority transition has completed (not <complete>) *)
380
   zz30 = ((zz28 = 4) and 
381
      ((
382
      (if ((zz171 = true) = false)
383
         then 0
384
         else 1) <> 0) and 
385
      (not zz24)));
386

  
387
   (* Beginning transition segment: trans15
388
      <fired> is true if the following are true: 
389
         1. the previous transition guard was true, 
390
         2. the source node for the transition is active, 
391
         3. the condition for the transition to fire is true, and 
392
         4. no higher-priority transition has completed (not <complete>) *)
393
   zz36 = ((zz34 = 4) and 
394
      ((
395
      (if ((zz177 = true) = false)
396
         then 0
397
         else 1) <> 0) and 
398
      (not zz31)));
399

  
400
   (* Beginning transition segment: trans17
401
      <fired> is true if the following are true: 
402
         1. the previous transition guard was true, 
403
         2. the source node for the transition is active, 
404
         3. the condition for the transition to fire is true, and 
405
         4. no higher-priority transition has completed (not <complete>) *)
406
   zz42 = ((zz40 = 6) and 
407
      ((
408
      (if ((zz177 = false) = false)
409
         then 0
410
         else 1) <> 0) and 
411
      (not zz37)));
412

  
413
   (* Beginning transition segment: trans16
414
      <fired> is true if the following are true: 
415
         1. the previous transition guard was true, 
416
         2. the source node for the transition is active, 
417
         3. the condition for the transition to fire is true, and 
418
         4. no higher-priority transition has completed (not <complete>) *)
419
   zz47 = ((zz45 = 5) and 
420
      ((
421
      (if ((zz171 = false) = false)
422
         then 0
423
         else 1) <> 0) and 
424
      (not zz43)));
425

  
426
   OK = ((zz58 = 4) or 
427
      ((zz58 = 5) or 
428
      (zz58 = 6)));
429

  
430
   zz63 = 
431
      (if (not 
432
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
433
         ((zz101 >= 3) and 
434
         (zz101 <= 6)))
435
         then 
436
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
437
               3
438
         else zz101);
439

  
440
   (* Beginning transition segment: trans18
441
      <fired> is true if the following are true: 
442
         1. the previous transition guard was true, 
443
         2. the source node for the transition is active, 
444
         3. the condition for the transition to fire is true, and 
445
         4. no higher-priority transition has completed (not <complete>) *)
446
   zz64 = ((not 
447
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
448
      ((zz101 >= 3) and 
449
      (zz101 <= 6))) and 
450

  
451
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
452
      ((zz63 >= 3) and 
453
      (zz63 <= 6)));
454

  
455
   (* Beginning transition segment: trans12
456
      <fired> is true if the following are true: 
457
         1. the previous transition guard was true, 
458
         2. the source node for the transition is active, 
459
         3. the condition for the transition to fire is true, and 
460
         4. no higher-priority transition has completed (not <complete>) *)
461
   zz116 = ((not 
462
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
463
      ((zz146 >= 2) and 
464
      (zz146 <= 8))) and 
465

  
466
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
467
      ((zz115 >= 2) and 
468
      (zz115 <= 8)));
469

  
470
   zz120 = 
471
      (if (zz142 = 1)
472
         then 
473
               (* <Exit state> path: Off maps to field: __root and value: 0 *)
474
               0
475
         else zz142);
476

  
477
   zz137 = 
478
      (if 
479
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
480
         ((zz156 >= 2) and 
481
         (zz156 <= 8))
482
         then 
483
               (* <Exit state> path: On maps to field: __root and value: 0 *)
484
               0
485
         else zz136);
486

  
487
   SP3c = true;
488

  
489
   zz171 = (zz170 = 20);
490

  
491
   (* Condition actions for transition segment: trans22: NONE
492
      Transition action(s) for transition: trans22
493
      <complete> is true if either: 
494
         1. this transition has completed, or 
495
         2. a higher-priority transition has already completed 
496
       *)
497
   zz105 = (zz104 or 
498
      zz100);
499

  
500
   zz127 = 
501
      (if (zz156 = 4)
502
         then 
503
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
504
               3
505
         else zz156);
506

  
507
   zz204 = cruiseThrottle;
508

  
509
   zz165 = (mode = 6);
510

  
511
   SP7 = ((not zz165) or 
512
      zz208);
513

  
514
   zz136 = 
515
      (if 
516
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
517
         ((zz156 >= 2) and 
518
         (zz156 <= 8))
519
         then zz123
520
         else zz135);
521

  
522
   (* Exit action(s) for transition: On_Init -> On_Active *)
523
   zz106 = 
524
      (if zz104
525
         then zz60
526
         else zz102);
527

  
528
   zz173 = (zz175 + 1);
529

  
530
   zz81 = 
531
      (if (zz147 = 4)
532
         then 
533
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
534
               3
535
         else zz147);
536

  
537
   zz181 = (carGear = 3);
538

  
539
   zz79 = 
540
      (if (zz84 = 6)
541
         then 
542
               (* <Exit state> path: On.Active.Decrease maps to field: __root and value: 3 *)
543
               3
544
         else zz84);
545

  
546
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
547
   zz38 = 
548
      (if zz36
549
         then zz14
550
         else zz34);
551

  
552
   (* Exit action(s) for transition: On -> On_Init: NONE
553
      Transition action(s) for transition: On -> On_Init: NONE
554
      Entry action(s) for transition: On -> On_Init *)
555
   zz119 = 
556
      (if zz116
557
         then zz114
558
         else zz143);
559
   (* Transition segment: trans12 complete. *)
560

  
561
   zz78 = 
562
      (if (not (zz89 = 8))
563
         then 3
564
         else zz148);
565

  
566
   zz15 = 
567
      (if (zz34 = 4)
568
         then false
569
         else zz33);
570

  
571
   zz83 = 
572
      (if 
573
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
574
         ((zz147 >= 3) and 
575
         (zz147 <= 6))
576
         then zz81
577
         else zz147);
578

  
579
   zz54 = 
580
      (if (not (zz55 = 4))
581
         then 4
582
         else zz103);
583

  
584
   zz192 = (zz211 > desiredSpeed);
585

  
586
   zz16 = 
587
      (if (not (zz32 = 5))
588
         then 
589
               (* <Enter state> path: On.Active.Increase maps to field: __root and value: 5 *)
590
               5
591
         else zz32);
592

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

  
595
   SP3a = ((not (not zz163)) or 
596
      (not zz199));
597

  
598
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
599
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
600
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
601
   zz67 = 
602
      (if zz64
603
         then zz62
604
         else zz98);
605
   (* Transition segment: trans18 complete. *)
606

  
607
   (* Condition actions for transition segment: trans17: NONE
608
      Transition action(s) for transition: trans17
609
      <complete> is true if either: 
610
         1. this transition has completed, or 
611
         2. a higher-priority transition has already completed 
612
       *)
613
   zz43 = (zz42 or 
614
      zz37);
615

  
616
   zz76 = 
617
      (if (zz91 = 8)
618
         then 
619
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
620
               2
621
         else zz91);
622

  
623
   zz80 = 
624
      (if (zz83 = 5)
625
         then 
626
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
627
               3
628
         else zz83);
629

  
630
   zz198 = (zz197 or 
631
      zz196);
632

  
633
   zz193 = (desiredSpeed <> 0.0);
634

  
635
   SP1 = ((not (not zz186)) or 
636
      zz187);
637

  
638
   zz231 = (cruiseThrottle <= 100.0);
639

  
640
   zz123 = 
641
      (if (zz135 = 8)
642
         then 
643
               (* <Exit state> path: On.Inactive maps to field: __root and value: 2 *)
644
               2
645
         else zz135);
646

  
647
   zz19 = 
648
      (if (zz28 = 4)
649
         then false
650
         else zz27);
651

  
652
   (* Condition actions for transition segment: trans20: NONE
653
      Transition action(s) for transition: trans20
654
      <complete> is true if either: 
655
         1. this transition has completed, or 
656
         2. a higher-priority transition has already completed 
657
       *)
658
   zz94 = (zz93 or 
659
      zz88);
660

  
661
   cruiseThrottle = 
662
      (if zz201
663
         then zz226
664
         else 0.0);
665

  
666
   zz86 = 
667
      (if 
668
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
669
         ((zz147 >= 3) and 
670
         (zz147 <= 6))
671
         then 
672
               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)
673
               2
674
         else zz85);
675

  
676
   VRP1 = (zz232 and 
677
      zz231);
678

  
679
   zz131 = 
680
      (if 
681
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
682
         ((zz156 >= 3) and 
683
         (zz156 <= 6))
684
         then zz125
685
         else zz130);
686

  
687
   zz235 = (desiredSpeed < 0.0);
688

  
689
   SP9 = ((not zz214) or 
690
      zz215);
691

  
692
   zz138 = 
693
      (if 
694
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
695
         ((zz156 >= 2) and 
696
         (zz156 <= 8))
697
         then zz133
698
         else zz158);
699

  
700
   zz65 = ((zz66 = 4) or 
701
      ((zz66 = 5) or 
702
      (zz66 = 6)));
703

  
704
   zz194 = (desiredSpeed >= 15.0);
705

  
706
   zz197 = (mode = 1);
707

  
708
   VRP3 = (not zz237);
709

  
710
   zz6 = 
711
      (if (not (zz49 = 4))
712
         then 
713
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
714
               4
715
         else zz49);
716

  
717
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
718
   zz33 = 
719
      (if zz30
720
         then zz19
721
         else zz27);
722

  
723
   zz134 = 
724
      (if 
725
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
726
         ((zz156 >= 2) and 
727
         (zz156 <= 8))
728
         then zz132
729
         else zz156);
730

  
731
   zz61 = 
732
      (if (not (zz63 = 4))
733
         then 
734
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
735
               4
736
         else zz63);
737

  
738
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE
739
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
740
   zz34 = 
741
      (if zz30
742
         then zz16
743
         else zz32);
744
   (* Transition segment: trans14 complete. *)
745

  
746
   (* Exit action(s) for transition: On -> Off *)
747
   zz141 = 
748
      (if zz139
749
         then zz138
750
         else zz158);
751

  
752
   (* Beginning transition segment: trans13
753
      <fired> is true if the following are true: 
754
         1. the previous transition guard was true, 
755
         2. the source node for the transition is active, 
756
         3. the condition for the transition to fire is true, and 
757
         4. no higher-priority transition has completed (not <complete>) *)
758
   zz139 = (
759
      (* <In state> path: On maps to field: __root and value range: [2, 8] *)
760
      ((zz156 >= 2) and 
761
      (zz156 <= 8)) and 
762
      (not onOff));
763

  
764
   zz178 = accelResume;
765

  
766
   zz234 = (desiredSpeed >= 0.0);
767

  
768
   (* Transition action(s) for transition: On_Active_Decrease -> On_Active_Maintain: NONE
769
      Entry action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
770
   zz45 = 
771
      (if zz42
772
         then zz9
773
         else zz44);
774
   (* Transition segment: trans17 complete. *)
775

  
776
   zz121 = 
777
      (if (not (zz140 = 1))
778
         then 
779
               (* <Enter state> path: Off maps to field: __root and value: 1 *)
780
               1
781
         else zz140);
782

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

  
785
   (* Exit action(s) for transition: On -> On_Init: NONE
786
      Transition action(s) for transition: On -> On_Init: NONE
787
      Entry action(s) for transition: On -> On_Init *)
788
   zz118 = 
789
      (if zz116
790
         then zz113
791
         else zz115);
792
   (* Transition segment: trans12 complete. *)
793

  
794
   zz191 = (zz189 and 
795
      zz188);
796

  
797
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE
798
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
799
   zz41 = 
800
      (if zz36
801
         then zz13
802
         else zz35);
803
   (* Transition segment: trans15 complete. *)
804

  
805
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Increase: NONE
806
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Increase *)
807
   zz35 = 
808
      (if zz30
809
         then zz17
810
         else zz29);
811
   (* Transition segment: trans14 complete. *)
812

  
813
   zz208 = (zz211 >= desiredSpeed);
814

  
815
   zz200 = (zz223 = 0.0);
816

  
817
   zz154 = 
818
      (if (not (zz156 = 1))
819
         then 1
820
         else zz157);
821

  
822
   zz73 = ((zz74 = 4) or 
823
      ((zz74 = 5) or 
824
      (zz74 = 6)));
825

  
826
   (* Transition action(s) for transition: On -> Off: NONE
827
      Entry action(s) for transition: On -> Off *)
828
   zz142 = 
829
      (if zz139
830
         then zz121
831
         else zz140);
832
   (* Transition segment: trans13 complete. *)
833

  
834
   zz124 = 
835
      (if (zz134 = 7)
836
         then 
837
               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)
838
               2
839
         else zz134);
840

  
841
   VRP4 = ((zz238 or 
842
      zz195) or 
843
      zz239);
844

  
845
   (* Exit action(s) for transition: On_Active -> On_Active_Maintain: NONE
846
      Transition action(s) for transition: On_Active -> On_Active_Maintain: NONE
847
      Entry action(s) for transition: On_Active -> On_Active_Maintain *)
848
   zz75 = 
849
      (if zz72
850
         then zz70
851
         else zz92);
852
   (* Transition segment: trans18 complete. *)
853

  
854
   zz233 = (desiredSpeed <= 100.0);
855

  
856
   zz223 = 
857
      (if zz217
858
         then zz2
859
         else zz218);
860

  
861
   zz185 = ((not zz184) and 
862
      zz183);
863

  
864
   zz180 = ((not zz179) and 
865
      zz178);
866

  
867
   zz239 = (desiredSpeed = carSpeed);
868

  
869
   (* Transition action(s) for transition: Off -> On: NONE
870
      Entry action(s) for transition: Off -> On *)
871
   zz148 = 
872
      (if zz144
873
         then zz119
874
         else zz143);
875
   (* Transition segment: trans23 complete. *)
876

  
877
   zz115 = 
878
      (if (not 
879
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
880
         ((zz146 >= 2) and 
881
         (zz146 <= 8)))
882
         then 
883
               (* <Enter state> path: On maps to field: __root and value: 2 *)
884
               2
885
         else zz146);
886

  
887
   (* Transition action(s) for transition: On_Active_Maintain -> On_Active_Decrease: NONE
888
      Entry action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
889
   zz40 = 
890
      (if zz36
891
         then zz12
892
         else zz38);
893
   (* Transition segment: trans15 complete. *)
894

  
895
   (* Exit action(s) for transition: On -> Off *)
896
   zz140 = 
897
      (if zz139
898
         then zz137
899
         else zz156);
900

  
901
   (* Exit action(s) for transition: On_Active_Maintain -> On_Active_Decrease *)
902
   zz39 = 
903
      (if zz36
904
         then zz15
905
         else zz33);
906

  
907
   zz8 = 
908
      (if (zz45 = 5)
909
         then 
910
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
911
               3
912
         else zz45);
913

  
914
   zz122 = 
915
      (if (not (zz140 = 1))
916
         then 1
917
         else zz157);
918

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

  
921
   zz82 = 
922
      (if (zz147 = 4)
923
         then false
924
         else zz141);
925

  
926
   zz203 = (zz201 or 
927
      zz202);
928

  
929
   zz186 = (((((not cancel) and 
930
      (not brakePedal)) and 
931
      zz181) and 
932
      zz182) and 
933
      validInputs);
934

  
935
   zz183 = decelSet;
936

  
937
   zz155 = (true -> 
938
      (if (pre SP3c)
939
         then false
940
         else (pre zz155)));
941

  
942
   zz196 = (mode = 2);
943

  
944
   zz161 = zz160;
945

  
946
   zz9 = 
947
      (if (not (zz44 = 4))
948
         then 
949
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
950
               4
951
         else zz44);
952

  
953
   (* Transition action(s) for transition: On_Inactive -> On_Active *)
954
   zz96 = 
955
      (if zz93
956
         then true
957
         else zz90);
958

  
959
   zz52 = 
960
      (if ((not zz48) and 
961
         (zz50 = 4))
962
         then false
963
         else zz39);
964

  
965
   zz0 = zz217;
966

  
967
   zz2 = (
968
      (if (zz1 and 
969
         (not zz0))
970
         then 0.0
971
         else (zz222 + 0.05)) -> 
972
      (if (zz1 and 
973
         (not zz0))
974
         then 0.0
975
         else 
976
      (if zz0
977
         then (zz222 + 0.05)
978
         else (pre zz2))));
979

  
980
   zz1 = (true -> 
981
      (if (pre zz0)
982
         then false
983
         else (pre zz1)));
984

  
985
   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE
986
      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
987
   zz51 = 
988
      (if zz47
989
         then zz7
990
         else zz46);
991
   (* Transition segment: trans16 complete. *)
992

  
993
   zz162 = 
994
      (if SP3c
995
         then 
996
               (if zz155
997
                  then zz158
998
                  else zz151)
999
         else zz158);
1000

  
1001
   (* Condition actions for transition segment: trans19: NONE
1002
      Transition action(s) for transition: trans19
1003
      <complete> is true if either: 
1004
         1. this transition has completed, or 
1005
         2. a higher-priority transition has already completed 
1006
       *)
1007
   zz100 = (zz99 or 
1008
      zz94);
1009

  
1010
   zz53 = 
1011
      (if (not (zz55 = 4))
1012
         then 
1013
               (* <Enter state> path: On.Active.Maintain maps to field: __root and value: 4 *)
1014
               4
1015
         else zz55);
1016

  
1017
   zz188 = (desiredSpeed <> 100.0);
1018

  
1019
   SP10 = ((not zz191) or 
1020
      zz192);
1021

  
1022
   zz13 = 
1023
      (if (not (zz38 = 6))
1024
         then 5
1025
         else zz35);
1026

  
1027
   zz201 = ((zz163 or 
1028
      zz164) or 
1029
      zz165);
1030

  
1031
   zz14 = 
1032
      (if (zz34 = 4)
1033
         then 
1034
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1035
               3
1036
         else zz34);
1037

  
1038
   zz126 = 
1039
      (if (zz129 = 5)
1040
         then 
1041
               (* <Exit state> path: On.Active.Increase maps to field: __root and value: 3 *)
1042
               3
1043
         else zz129);
1044

  
1045
   (* Exit action(s) for outer loop transition: On_Active_Maintain *)
1046
   zz26 = 
1047
      (if zz24
1048
         then zz23
1049
         else zz107);
1050

  
1051
   (* Exit action(s) for transition: Off -> On *)
1052
   zz146 = 
1053
      (if zz144
1054
         then zz120
1055
         else zz142);
1056

  
1057
   zz199 = (
1058
      (if (zz162 = false)
1059
         then 0.0
1060
         else 1.0) = 1.0);
1061

  
1062
   zz227 = (desiredSpeed - carSpeed);
1063

  
1064
   zz150 = 
1065
      (if ((not zz145) and 
1066

  
1067
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1068
         ((zz147 >= 2) and 
1069
         (zz147 <= 8)))
1070
         then zz111
1071
         else zz148);
1072

  
1073
   zz177 = (zz176 = 20);
1074

  
1075
   (* Transition action(s) for outer loop transition: On_Active_Maintain *)
1076
   zz27 = 
1077
      (if zz24
1078
         then true
1079
         else zz26);
1080

  
1081
   (* Entry action(s) for transition: On_Inactive -> On_Active *)
1082
   zz97 = 
1083
      (if zz93
1084
         then zz74
1085
         else zz95);
1086
   (* Transition segment: trans20 complete. *)
1087

  
1088
   zz195 = (desiredSpeed = 0.0);
1089

  
1090
   zz71 = 
1091
      (if (not 
1092
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1093
         ((zz95 >= 3) and 
1094
         (zz95 <= 6)))
1095
         then 
1096
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
1097
               3
1098
         else zz95);
1099

  
1100
   zz62 = 
1101
      (if (not (zz63 = 4))
1102
         then 4
1103
         else zz98);
1104

  
1105
   zz229 = 
1106
      (if (zz228 < ( -10.0))
1107
         then ( -10.0)
1108
         else 
1109
      (if (zz228 > 10.0)
1110
         then 10.0
1111
         else zz228));
1112

  
1113
   (* Transition action(s) for transition: On_Inactive -> On_Active: NONE
1114
      Entry action(s) for transition: On_Inactive -> On_Active *)
1115
   zz103 = 
1116
      (if zz99
1117
         then zz67
1118
         else zz98);
1119
   (* Transition segment: trans19 complete. *)
1120

  
1121
   zz55 = 
1122
      (if (not 
1123
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1124
         ((zz106 >= 3) and 
1125
         (zz106 <= 6)))
1126
         then 
1127
               (* <Enter state> path: On.Active maps to field: __root and value: 3 *)
1128
               3
1129
         else zz106);
1130

  
1131
   (* Beginning transition segment: trans18
1132
      <fired> is true if the following are true: 
1133
         1. the previous transition guard was true, 
1134
         2. the source node for the transition is active, 
1135
         3. the condition for the transition to fire is true, and 
1136
         4. no higher-priority transition has completed (not <complete>) *)
1137
   zz56 = ((not 
1138
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1139
      ((zz106 >= 3) and 
1140
      (zz106 <= 6))) and 
1141

  
1142
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1143
      ((zz55 >= 3) and 
1144
      (zz55 <= 6)));
1145

  
1146
   (* Beginning transition segment: trans18
1147
      <fired> is true if the following are true: 
1148
         1. the previous transition guard was true, 
1149
         2. the source node for the transition is active, 
1150
         3. the condition for the transition to fire is true, and 
1151
         4. no higher-priority transition has completed (not <complete>) *)
1152
   zz72 = ((not 
1153
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1154
      ((zz95 >= 3) and 
1155
      (zz95 <= 6))) and 
1156

  
1157
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1158
      ((zz71 >= 3) and 
1159
      (zz71 <= 6)));
1160

  
1161
   (* Transition action(s) for transition: On_Active -> On_Inactive: NONE
1162
      Entry action(s) for transition: On_Active -> On_Inactive *)
1163
   zz91 = 
1164
      (if zz88
1165
         then zz77
1166
         else zz89);
1167
   (* Transition segment: trans21 complete. *)
1168

  
1169
   zz202 = (mode = 3);
1170

  
1171
   zz221 = 
1172
      (if zz162
1173
         then carSpeed
1174
         else zz223);
1175

  
1176
   SP2 = ((not (not zz201)) or 
1177
      zz187);
1178

  
1179
   (* Entry action(s) for transition: On_Init -> On_Active *)
1180
   zz108 = 
1181
      (if zz104
1182
         then zz58
1183
         else zz106);
1184
   (* Transition segment: trans22 complete. *)
1185

  
1186
   zz238 = (desiredSpeed = zz211);
1187

  
1188
   zz212 = (zz211 = desiredSpeed);
1189

  
1190
   (* Beginning transition segment: trans21
1191
      <fired> is true if the following are true: 
1192
         1. the previous transition guard was true, 
1193
         2. the source node for the transition is active, 
1194
         3. the condition for the transition to fire is true, and 
1195
         4. no higher-priority transition has completed (not <complete>) *)
1196
   zz88 = (
1197
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1198
      ((zz147 >= 3) and 
1199
      (zz147 <= 6)) and 
1200
      (not zz186));
1201

  
1202
   (* Condition actions for transition segment: trans16: NONE
1203
      Transition action(s) for transition: trans16
1204
      <complete> is true if either: 
1205
         1. this transition has completed, or 
1206
         2. a higher-priority transition has already completed 
1207
       *)
1208
   zz48 = (zz47 or 
1209
      zz43);
1210

  
1211
   SP4 = ((not zz203) or 
1212
      zz194);
1213

  
1214
   zz149 = 
1215
      (if ((not zz145) and 
1216

  
1217
         (* <In state> path: On maps to field: __root and value range: [2, 8] *)
1218
         ((zz147 >= 2) and 
1219
         (zz147 <= 8)))
1220
         then zz110
1221
         else zz147);
1222

  
1223
   zz132 = 
1224
      (if 
1225
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1226
         ((zz156 >= 3) and 
1227
         (zz156 <= 6))
1228
         then 
1229
               (* <Exit state> path: On.Active maps to field: __root and value: 2 *)
1230
               2
1231
         else zz131);
1232

  
1233
   zz112 = 
1234
      (if ((not zz105) and 
1235

  
1236
         (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1237
         ((zz108 >= 3) and 
1238
         (zz108 <= 6)))
1239
         then zz52
1240
         else zz107);
1241

  
1242
   (* Exit action(s) for transition: On_Active_Decrease -> On_Active_Maintain *)
1243
   zz44 = 
1244
      (if zz42
1245
         then zz11
1246
         else zz40);
1247

  
1248
   zz215 = (zz211 < desiredSpeed);
1249

  
1250
   zz236 = (desiredSpeed > 0.0);
1251

  
1252
   zz113 = 
1253
      (if (not (zz115 = 7))
1254
         then 
1255
               (* <Enter state> path: On.Init maps to field: __root and value: 7 *)
1256
               7
1257
         else zz115);
1258

  
1259
   (* Transition action(s) for transition: On_Active_Increase -> On_Active_Maintain: NONE
1260
      Entry action(s) for transition: On_Active_Increase -> On_Active_Maintain *)
1261
   zz50 = 
1262
      (if zz47
1263
         then zz6
1264
         else zz49);
1265
   (* Transition segment: trans16 complete. *)
1266

  
1267
   (* Exit action(s) for transition: On_Inactive -> On_Active *)
1268
   zz95 = 
1269
      (if zz93
1270
         then zz76
1271
         else zz91);
1272

  
1273
   zz3 = zz216;
1274

  
1275
   zz5 = (
1276
      (if (zz4 and 
1277
         (not zz3))
1278
         then 0.0
1279
         else (zz222 - 0.05)) -> 
1280
      (if (zz4 and 
1281
         (not zz3))
1282
         then 0.0
1283
         else 
1284
      (if zz3
1285
         then (zz222 - 0.05)
1286
         else (pre zz5))));
1287

  
1288
   zz4 = (true -> 
1289
      (if (pre zz3)
1290
         then false
1291
         else (pre zz4)));
1292

  
1293
   zz60 = 
1294
      (if (zz102 = 7)
1295
         then 
1296
               (* <Exit state> path: On.Init maps to field: __root and value: 2 *)
1297
               2
1298
         else zz102);
1299

  
1300
   (* Entry action(s) for transition: On_Init -> On_Active *)
1301
   zz109 = 
1302
      (if zz104
1303
         then zz59
1304
         else zz103);
1305
   (* Transition segment: trans22 complete. *)
1306

  
1307
   zz205 = (0.0 -> (pre zz204));
1308

  
1309
   zz209 = zz163;
1310

  
1311
   zz216 = zz164;
1312

  
1313
   zz217 = zz165;
1314

  
1315
   zz117 = (
1316
      (* <In state> path: On.Active maps to field: __root and value range: [3, 6] *)
1317
      ((zz118 >= 3) and 
1318
      (zz118 <= 6)) or 
1319
      ((zz118 = 7) or 
1320
      (zz118 = 8)));
1321

  
1322
   zz70 = 
1323
      (if (not (zz71 = 4))
1324
         then 4
1325
         else zz92);
1326

  
1327
   zz22 = 
1328
      (if (zz108 = 4)
1329
         then 
1330
               (* <Exit state> path: On.Active.Maintain maps to field: __root and value: 3 *)
1331
               3
1332
         else zz108);
1333

  
1334
   zz160 = 
1335
      (if SP3c
1336
         then 
1337
               (if zz155
1338
                  then zz153
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff