Project

General

Profile

Revision eb639349

View differences:

regression_tests/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

  
3
project (lustrec-tests)
4

  
5
set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
6
include(./modules/FindLustre.cmake)
7

  
8
add_subdirectory(lustre_files)
9

  
10

  
regression_tests/lustre_files/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

  
3
add_subdirectory(success)
regression_tests/lustre_files/success/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

  
3
add_subdirectory(Stateflow)
regression_tests/lustre_files/success/Stateflow/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

  
3
#helpfull functions and macros
4
MACRO(SUBDIRLIST result curdir)
5
  FILE(GLOB children RELATIVE ${curdir} ${curdir}/*)
6
  SET(dirlist "")
7
  FOREACH(child ${children})
8
    IF(IS_DIRECTORY ${curdir}/${child})
9
      LIST(APPEND dirlist ${child})
10
    ENDIF()
11
  ENDFOREACH()
12
  SET(${result} ${dirlist})
13
ENDMACRO()
14

  
15
MACRO(LUSTREFILES result dir)
16
  FILE(GLOB children ${dir} ${dir}/*.lus)
17
  SET(lustreFileslist "")
18
  FOREACH(child ${children})
19
    IF(EXISTS ${child} AND NOT IS_DIRECTORY ${child})
20
      LIST(APPEND lustreFileslist ${child})
21
    ENDIF()
22
  ENDFOREACH()
23
  SET(${result} ${lustreFileslist})
24
ENDMACRO()
25

  
26
find_package(Lustre)
27

  
28
if(LUSTRE_COMPILER)
29
  message(STATUS "Found lustrec: ${LUSTRE_COMPILER} ")
30
else(LUSTRE_COMPILER)
31
  message(FATAL_ERROR "lustrec not found")
32
endif(LUSTRE_COMPILER)
33

  
34
#proceed all subdirectories
35
SUBDIRLIST(SUBDIRS ${CMAKE_CURRENT_SOURCE_DIR})
36

  
37
#take all lustre files
38
set(GLOBAL_LUSTRE_FILES "")
39
FOREACH(subdir ${SUBDIRS})
40
  LUSTREFILES(LFILE ${subdir} )
41
  list(APPEND GLOBAL_LUSTRE_FILES ${LFILE})
42
  #message("directory ${subdir} is proceeded with file ${LFILE}")
43
ENDFOREACH()
44

  
45
#first combination :no option
46
set(LUSTRE_OPTIONS_OPT "")
47
set(GENERATION_RESULTS "")
48
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
49
	get_filename_component(L ${lus_file} NAME_WE)
50
	set(LUSTRE_NODE_OPT  "${L}")
51
	Lustre_Compile(LUS_FILE ${lus_file}
52
					NODE ${LUSTRE_NODE_OPT}
53
					OPTS ${LUSTRE_OPTIONS_OPT})
54
	set(GENERATION_RESULTS ${GENERATION_RESULTS} ${LUSTRE_GENERATED_FILES_${lus_file}})
55
	#message("GENERATION_RESULTS : ${GENERATION_RESULTS}")
56
ENDFOREACH()
57
add_custom_target (GENERATE_FILES ALL
58
	DEPENDS ${GENERATION_RESULTS})
regression_tests/lustre_files/success/Stateflow/src_Arrays1/Arrays1.lus
1
-- This file has been generated by cocoSim
2

  
3

  
4
-- System nodes
5

  
6

  
7

  
8

  
9

  
10

  
11

  
12

  
13
-- Entry action for state :Arrays1_B
14
node Arrays1_B_en(idArrays1_Arrays1_1:int;
15
	x_2_1:int;
16
	isInner:bool)
17

  
18
returns (idArrays1_Arrays1:int;
19
	x_2:int);
20

  
21

  
22
var 	idArrays1_Arrays1_2:int;
23
	x_2_2:int;
24

  
25

  
26
let
27

  
28

  
29

  
30
	-- set state as active 
31
	idArrays1_Arrays1_2 
32
	= 512;
33
	
34

  
35
	x_2_2 
36
	= if (not isInner) then  x_2_1  + 1
37
	 else x_2_1;
38
	
39

  
40
	(idArrays1_Arrays1, x_2) 
41
	= (idArrays1_Arrays1_2, x_2_2);
42
	
43

  
44
tel
45

  
46

  
47

  
48

  
49

  
50
-- Exit action for state :Arrays1_B
51
node Arrays1_B_ex(idArrays1_Arrays1_1:int;
52
	isInner:bool)
53

  
54
returns (idArrays1_Arrays1:int);
55

  
56

  
57
var 	idArrays1_Arrays1_2:int;
58

  
59

  
60
let
61

  
62

  
63

  
64
	-- set state as inactive 
65
	idArrays1_Arrays1_2
66
	 = if (not isInner) then 0 else idArrays1_Arrays1_1;
67

  
68

  
69
	(idArrays1_Arrays1) 
70
	= (idArrays1_Arrays1_1);
71
	
72

  
73
tel
74

  
75

  
76

  
77

  
78

  
79

  
80
-- Entry action for state :Arrays1_A
81
node Arrays1_A_en(idArrays1_Arrays1_1:int;
82
	x_1_1:int;
83
	isInner:bool)
84

  
85
returns (idArrays1_Arrays1:int;
86
	x_1:int);
87

  
88

  
89
var 	idArrays1_Arrays1_2:int;
90
	x_1_2:int;
91

  
92

  
93
let
94

  
95

  
96

  
97
	-- set state as active 
98
	idArrays1_Arrays1_2 
99
	= 511;
100
	
101

  
102
	x_1_2 
103
	= if (not isInner) then  x_1_1  + 1
104
	 else x_1_1;
105
	
106

  
107
	(idArrays1_Arrays1, x_1) 
108
	= (idArrays1_Arrays1_2, x_1_2);
109
	
110

  
111
tel
112

  
113

  
114

  
115

  
116

  
117
-- Exit action for state :Arrays1_A
118
node Arrays1_A_ex(idArrays1_Arrays1_1:int;
119
	isInner:bool)
120

  
121
returns (idArrays1_Arrays1:int);
122

  
123

  
124
var 	idArrays1_Arrays1_2:int;
125

  
126

  
127
let
128

  
129

  
130

  
131
	-- set state as inactive 
132
	idArrays1_Arrays1_2
133
	 = if (not isInner) then 0 else idArrays1_Arrays1_1;
134

  
135

  
136
	(idArrays1_Arrays1) 
137
	= (idArrays1_Arrays1_1);
138
	
139

  
140
tel
141

  
142

  
143

  
144

  
145

  
146

  
147
-- Entry action for state :Arrays1_C
148
node Arrays1_C_en(idArrays1_Arrays1_1:int;
149
	x_3_1:int;
150
	isInner:bool)
151

  
152
returns (idArrays1_Arrays1:int;
153
	x_3:int);
154

  
155

  
156
var 	idArrays1_Arrays1_2:int;
157
	x_3_2:int;
158

  
159

  
160
let
161

  
162

  
163

  
164
	-- set state as active 
165
	idArrays1_Arrays1_2 
166
	= 513;
167
	
168

  
169
	x_3_2 
170
	= if (not isInner) then  x_3_1  + 1
171
	 else x_3_1;
172
	
173

  
174
	(idArrays1_Arrays1, x_3) 
175
	= (idArrays1_Arrays1_2, x_3_2);
176
	
177

  
178
tel
179

  
180

  
181

  
182

  
183

  
184
-- Exit action for state :Arrays1_C
185
node Arrays1_C_ex(idArrays1_Arrays1_1:int;
186
	isInner:bool)
187

  
188
returns (idArrays1_Arrays1:int);
189

  
190

  
191
var 	idArrays1_Arrays1_2:int;
192

  
193

  
194
let
195

  
196

  
197

  
198
	-- set state as inactive 
199
	idArrays1_Arrays1_2
200
	 = if (not isInner) then 0 else idArrays1_Arrays1_1;
201

  
202

  
203
	(idArrays1_Arrays1) 
204
	= (idArrays1_Arrays1_1);
205
	
206

  
207
tel
208

  
209

  
210
--***************************************************State :Arrays1_Arrays1 Automaton***************************************************
211

  
212
node Arrays1_Arrays1_node(idArrays1_Arrays1_1:int;
213
	x_1_1:int;
214
	E:bool;
215
	x_2_1:int;
216
	x_3_1:int)
217

  
218
returns (idArrays1_Arrays1:int;
219
	x_1:int;
220
	x_2:int;
221
	x_3:int);
222

  
223

  
224
let
225

  
226
	 automaton arrays1_arrays1
227

  
228
	state POINTArrays1_Arrays1:
229
	unless (idArrays1_Arrays1_1=0) restart POINT__TO__ARRAYS1_A_1
230

  
231

  
232

  
233
	unless (idArrays1_Arrays1_1=511) and E restart ARRAYS1_A__TO__ARRAYS1_B_1
234

  
235

  
236

  
237
	unless (idArrays1_Arrays1_1=512) and E restart ARRAYS1_B__TO__ARRAYS1_C_1
238

  
239

  
240

  
241
	unless (idArrays1_Arrays1_1=513) and E restart ARRAYS1_C__TO__ARRAYS1_A_1
242

  
243

  
244

  
245
	unless (idArrays1_Arrays1_1=511) restart ARRAYS1_A_IDL
246

  
247
	unless (idArrays1_Arrays1_1=512) restart ARRAYS1_B_IDL
248

  
249
	unless (idArrays1_Arrays1_1=513) restart ARRAYS1_C_IDL
250

  
251
	let
252

  
253
		(idArrays1_Arrays1, x_1, x_2, x_3) 
254
	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);
255
	
256

  
257
	tel
258

  
259

  
260

  
261
	state POINT__TO__ARRAYS1_A_1:
262

  
263
	 var 	idArrays1_Arrays1_2:int;
264
	x_1_2:int;
265
	let
266

  
267
		-- transition trace :
268
	--POINT__To__Arrays1_A_1
269
		(idArrays1_Arrays1_2, x_1_2) 
270
	= Arrays1_A_en(idArrays1_Arrays1_1, x_1_1, false);
271
		
272

  
273
	(idArrays1_Arrays1, x_1) 
274
	=  (idArrays1_Arrays1_2, x_1_2);
275

  
276
	--add unused variables
277
	(x_2, x_3) 
278
	= (x_2_1, x_3_1);
279
	
280

  
281
	tel
282

  
283
	until true restart POINTArrays1_Arrays1
284

  
285

  
286

  
287
	state ARRAYS1_A__TO__ARRAYS1_B_1:
288

  
289
	 var 	idArrays1_Arrays1_2, idArrays1_Arrays1_3:int;
290
	x_2_2:int;
291
	let
292

  
293
		-- transition trace :
294
	--Arrays1_A__To__Arrays1_B_1
295
		(idArrays1_Arrays1_2) 
296
	= Arrays1_A_ex(idArrays1_Arrays1_1, false);
297
		
298

  
299
		(idArrays1_Arrays1_3, x_2_2) 
300
	= Arrays1_B_en(idArrays1_Arrays1_2, x_2_1, false);
301
		
302

  
303
	(idArrays1_Arrays1, x_1, x_2) 
304
	=  (idArrays1_Arrays1_3, x_1_1, x_2_2);
305

  
306
	--add unused variables
307
	(x_3) 
308
	= (x_3_1);
309
	
310

  
311
	tel
312

  
313
	until true restart POINTArrays1_Arrays1
314

  
315

  
316

  
317
	state ARRAYS1_B__TO__ARRAYS1_C_1:
318

  
319
	 var 	idArrays1_Arrays1_2, idArrays1_Arrays1_3:int;
320
	x_3_2:int;
321
	let
322

  
323
		-- transition trace :
324
	--Arrays1_B__To__Arrays1_C_1
325
		(idArrays1_Arrays1_2) 
326
	= Arrays1_B_ex(idArrays1_Arrays1_1, false);
327
		
328

  
329
		(idArrays1_Arrays1_3, x_3_2) 
330
	= Arrays1_C_en(idArrays1_Arrays1_2, x_3_1, false);
331
		
332

  
333
	(idArrays1_Arrays1, x_1, x_2, x_3) 
334
	=  (idArrays1_Arrays1_3, x_1_1, x_2_1, x_3_2);
335

  
336

  
337
	tel
338

  
339
	until true restart POINTArrays1_Arrays1
340

  
341

  
342

  
343
	state ARRAYS1_C__TO__ARRAYS1_A_1:
344

  
345
	 var 	idArrays1_Arrays1_2, idArrays1_Arrays1_3:int;
346
	x_1_2:int;
347
	let
348

  
349
		-- transition trace :
350
	--Arrays1_C__To__Arrays1_A_1
351
		(idArrays1_Arrays1_2) 
352
	= Arrays1_C_ex(idArrays1_Arrays1_1, false);
353
		
354

  
355
		(idArrays1_Arrays1_3, x_1_2) 
356
	= Arrays1_A_en(idArrays1_Arrays1_2, x_1_1, false);
357
		
358

  
359
	(idArrays1_Arrays1, x_1, x_2, x_3) 
360
	=  (idArrays1_Arrays1_3, x_1_2, x_2_1, x_3_1);
361

  
362

  
363
	tel
364

  
365
	until true restart POINTArrays1_Arrays1
366

  
367

  
368

  
369
	state ARRAYS1_A_IDL:
370

  
371
	 	let
372

  
373
		
374

  
375
	(idArrays1_Arrays1, x_1, x_2, x_3) 
376
	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);
377
	
378

  
379
	tel
380

  
381
	until true restart POINTArrays1_Arrays1
382

  
383

  
384

  
385
	state ARRAYS1_B_IDL:
386

  
387
	 	let
388

  
389
		
390

  
391
	(idArrays1_Arrays1, x_1, x_2, x_3) 
392
	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);
393
	
394

  
395
	tel
396

  
397
	until true restart POINTArrays1_Arrays1
398

  
399

  
400

  
401
	state ARRAYS1_C_IDL:
402

  
403
	 	let
404

  
405
		
406

  
407
	(idArrays1_Arrays1, x_1, x_2, x_3) 
408
	= (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);
409
	
410

  
411
	tel
412

  
413
	until true restart POINTArrays1_Arrays1
414

  
415

  
416

  
417
tel
418

  
419

  
420
--***************************************************State :Arrays1_Arrays1 Automaton***************************************************
421

  
422
node Arrays1_Arrays1(E:bool)
423

  
424
returns (x_1:int;
425
	x_2:int;
426
	x_3:int);
427

  
428

  
429
var x_1_1: int;
430

  
431
	x_2_1: int;
432

  
433
	x_3_1: int;
434

  
435
	idArrays1_Arrays1, idArrays1_Arrays1_1: int;
436

  
437
	let
438

  
439
	x_1_1 = 1 -> pre x_1;
440

  
441
	x_2_1 = 1 -> pre x_2;
442

  
443
	x_3_1 = 1 -> pre x_3;
444

  
445
	idArrays1_Arrays1_1 = 0 -> pre idArrays1_Arrays1;
446

  
447
	
448

  
449

  
450

  
451
	(idArrays1_Arrays1, x_1, x_2, x_3)
452
	 = 
453

  
454
	 if E then Arrays1_Arrays1_node(idArrays1_Arrays1_1, x_1_1, E, x_2_1, x_3_1)
455

  
456
	 else (idArrays1_Arrays1_1, x_1_1, x_2_1, x_3_1);
457

  
458
	
459

  
460

  
461
--unused outputs
462
	
463

  
464
tel
465

  
466

  
467

  
468
node Arrays1 (E_1_1 : real)
469
returns (x1_1_1 : int;
470
	x2_2_1 : int;
471
	x3_3_1 : int); 
472
var
473
	Arrays1_1_1 : int; Arrays1_1_2 : int; Arrays1_1_3 : int;
474
	Demux_1_1 : int; Demux_2_1 : int; Demux_3_1 : int;
475
	i_virtual_local : real;
476
	Arrays1E_1_1_event: bool;
477
let 
478
	Arrays1E_1_1_event = false -> (pre(E_1_1) <= 0.0 and E_1_1 > 0.0);
479
	(Arrays1_1_1, Arrays1_1_2, Arrays1_1_3) =  Arrays1_Arrays1(Arrays1E_1_1_event);
480
	Demux_1_1 = Arrays1_1_1 ;
481
	Demux_2_1 = Arrays1_1_2 ;
482
	Demux_3_1 = Arrays1_1_3 ;
483
	x1_1_1 = Demux_1_1;
484
	x2_2_1 = Demux_2_1;
485
	x3_3_1 = Demux_3_1;
486
	i_virtual_local= 0.0 -> 1.0;
487
tel
488

  
regression_tests/lustre_files/success/Stateflow/src_Arrays1/Arrays1.lustrec.lus
1
type arrays1_arrays1__type = enum {POINTArrays1_Arrays1, POINT__TO__ARRAYS1_A_1, ARRAYS1_A__TO__ARRAYS1_B_1, ARRAYS1_B__TO__ARRAYS1_C_1, ARRAYS1_C__TO__ARRAYS1_A_1, ARRAYS1_A_IDL, ARRAYS1_B_IDL, ARRAYS1_C_IDL };
2
 
3
node Arrays1_A_ex (idArrays1_Arrays1_1: int; isInner: bool;) returns (idArrays1_Arrays1: int);
4
var __Arrays1_A_ex_1: bool;
5
    idArrays1_Arrays1_2: int;
6
let
7
    
8
    idArrays1_Arrays1_2 = (if __Arrays1_A_ex_1 then 0 else idArrays1_Arrays1_1);
9
    __Arrays1_A_ex_1 = (not (isInner));
10
    idArrays1_Arrays1 = idArrays1_Arrays1_1;
11
     
12
tel
13
 
14
node Arrays1_B_en (idArrays1_Arrays1_1: int; x_2_1: int; isInner: bool;) returns (idArrays1_Arrays1: int; x_2: int;);
15
var __Arrays1_B_en_1: bool;
16
    idArrays1_Arrays1_2: int;
17
    x_2_2: int;
18
let
19
    
20
    idArrays1_Arrays1_2 = 37;
21
    x_2_2 = (if __Arrays1_B_en_1 then (x_2_1 + 1) else x_2_1);
22
    __Arrays1_B_en_1 = (not (isInner));
23
    idArrays1_Arrays1, x_2 = (idArrays1_Arrays1_2,x_2_2);
24
     
25
tel
26
 
27
node Arrays1_B_ex (idArrays1_Arrays1_1: int; isInner: bool;) returns (idArrays1_Arrays1: int;);
28
var __Arrays1_B_ex_1: bool;
29
    idArrays1_Arrays1_2: int;
30
let
31
    
32
    idArrays1_Arrays1_2 = (if __Arrays1_B_ex_1 then 0 else idArrays1_Arrays1_1);
33
    __Arrays1_B_ex_1 = (not (isInner));
34
    idArrays1_Arrays1 = idArrays1_Arrays1_1;
35
     
36
tel
37
 
38
node Arrays1_C_en (idArrays1_Arrays1_1: int; x_3_1: int; isInner: bool;) returns (idArrays1_Arrays1: int; x_3: int;);
39
var __Arrays1_C_en_1: bool;
40
    idArrays1_Arrays1_2: int;
41
    x_3_2: int;
42
let
43
    
44
    idArrays1_Arrays1_2 = 38;
45
    x_3_2 = (if __Arrays1_C_en_1 then (x_3_1 + 1) else x_3_1);
46
    __Arrays1_C_en_1 = (not (isInner));
47
    idArrays1_Arrays1, x_3 = (idArrays1_Arrays1_2,x_3_2);
48
     
49
tel
50
 
51
node Arrays1_A_en (idArrays1_Arrays1_1: int; x_1_1: int; isInner: bool;) returns (idArrays1_Arrays1: int; x_1: int;);
52
var __Arrays1_A_en_1: bool;
53
    idArrays1_Arrays1_2: int;
54
    x_1_2: int;
55
let
56
    
57
    idArrays1_Arrays1_2 = 36;
58
    x_1_2 = (if __Arrays1_A_en_1 then (x_1_1 + 1) else x_1_1);
59
    __Arrays1_A_en_1 = (not (isInner));
60
    idArrays1_Arrays1, x_1 = (idArrays1_Arrays1_2,x_1_2);
61
     
62
tel
63
 
64
node Arrays1_C_ex (idArrays1_Arrays1_1: int; isInner: bool;) returns (idArrays1_Arrays1: int;);
65
var __Arrays1_C_ex_1: bool;
66
    idArrays1_Arrays1_2: int;
67
let
68
    
69
    idArrays1_Arrays1_2 = (if __Arrays1_C_ex_1 then 0 else idArrays1_Arrays1_1);
70
    __Arrays1_C_ex_1 = (not (isInner));
71
    idArrays1_Arrays1 = idArrays1_Arrays1_1;
72
     
73
tel
74
 
75
node arrays1_arrays1__ARRAYS1_A_IDL_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;);
76
var idArrays1_Arrays1: int;
77
    x_1: int;
78
    x_2: int;
79
    x_3: int;
80
let
81
    
82
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,ARRAYS1_A_IDL));
83
    idArrays1_Arrays1_out = idArrays1_Arrays1;
84
    x_1_out = x_1;
85
    x_2_out = x_2;
86
    x_3_out = x_3;
87
    idArrays1_Arrays1, x_1, x_2, x_3 = (idArrays1_Arrays1_1,x_1_1,x_2_1,x_3_1);
88
     
89
tel
90
 
91
node arrays1_arrays1__ARRAYS1_A_IDL_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;);
92
let
93
    
94
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
95
     
96
tel
97
 
98
node arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;);
99
var idArrays1_Arrays1: int;
100
    x_1: int;
101
    x_2: int;
102
    x_3: int;
103
    x_2_2: int;
104
    idArrays1_Arrays1_3: int;
105
    idArrays1_Arrays1_2: int;
106
let
107
    
108
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,ARRAYS1_A__TO__ARRAYS1_B_1));
109
    idArrays1_Arrays1_out = idArrays1_Arrays1;
110
    x_1_out = x_1;
111
    x_2_out = x_2;
112
    x_3_out = x_3;
113
    idArrays1_Arrays1_2 = Arrays1_A_ex (idArrays1_Arrays1_1,false);
114
    idArrays1_Arrays1_3, x_2_2 = Arrays1_B_en (idArrays1_Arrays1_2,x_2_1,false);
115
    idArrays1_Arrays1, x_1, x_2 = (idArrays1_Arrays1_3,x_1_1,x_2_2);
116
    x_3 = x_3_1;
117
     
118
tel
119
 
120
node arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
121
let
122
    
123
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
124
     
125
tel
126
 
127
node arrays1_arrays1__ARRAYS1_B_IDL_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;)
128
var idArrays1_Arrays1: int;
129
    x_1: int;
130
    x_2: int;
131
    x_3: int;
132
let
133
    
134
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,ARRAYS1_B_IDL));
135
    idArrays1_Arrays1_out = idArrays1_Arrays1;
136
    x_1_out = x_1;
137
    x_2_out = x_2;
138
    x_3_out = x_3;
139
    idArrays1_Arrays1, x_1, x_2, x_3 = (idArrays1_Arrays1_1,x_1_1,x_2_1,x_3_1);
140
     
141
tel
142
 
143
node arrays1_arrays1__ARRAYS1_B_IDL_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
144
let
145
    
146
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
147
     
148
tel
149
 
150
node arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;)
151
var idArrays1_Arrays1: int;
152
    x_1: int;
153
    x_2: int;
154
    x_3: int;
155
    x_3_2: int;
156
    idArrays1_Arrays1_3: int;
157
    idArrays1_Arrays1_2: int;
158
let
159
    
160
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,ARRAYS1_B__TO__ARRAYS1_C_1));
161
    idArrays1_Arrays1_out = idArrays1_Arrays1;
162
    x_1_out = x_1;
163
    x_2_out = x_2;
164
    x_3_out = x_3;
165
    idArrays1_Arrays1_2 = Arrays1_B_ex (idArrays1_Arrays1_1,false);
166
    idArrays1_Arrays1_3, x_3_2 = Arrays1_C_en (idArrays1_Arrays1_2,x_3_1,false);
167
    idArrays1_Arrays1, x_1, x_2, x_3 = (idArrays1_Arrays1_3,x_1_1,x_2_1,x_3_2);
168
     
169
tel
170
 
171
node arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
172
let
173
    
174
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
175
     
176
tel
177
 
178
node arrays1_arrays1__ARRAYS1_C_IDL_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;)
179
var idArrays1_Arrays1: int;
180
    x_1: int;
181
    x_2: int;
182
    x_3: int;
183
let
184
    
185
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,ARRAYS1_C_IDL));
186
    idArrays1_Arrays1_out = idArrays1_Arrays1;
187
    x_1_out = x_1;
188
    x_2_out = x_2;
189
    x_3_out = x_3;
190
    idArrays1_Arrays1, x_1, x_2, x_3 = (idArrays1_Arrays1_1,x_1_1,x_2_1,x_3_1);
191
     
192
tel
193
 
194
node arrays1_arrays1__ARRAYS1_C_IDL_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
195
let
196
    
197
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
198
     
199
tel
200
 
201
node arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;)
202
var idArrays1_Arrays1: int;
203
    x_1: int;
204
    x_2: int;
205
    x_3: int;
206
    x_1_2: int;
207
    idArrays1_Arrays1_3: int;
208
    idArrays1_Arrays1_2: int;
209
let
210
    
211
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,ARRAYS1_C__TO__ARRAYS1_A_1));
212
    idArrays1_Arrays1_out = idArrays1_Arrays1;
213
    x_1_out = x_1;
214
    x_2_out = x_2;
215
    x_3_out = x_3;
216
    idArrays1_Arrays1_2 = Arrays1_C_ex (idArrays1_Arrays1_1,false);
217
    idArrays1_Arrays1_3, x_1_2 = Arrays1_A_en (idArrays1_Arrays1_2,x_1_1,false);
218
    idArrays1_Arrays1, x_1, x_2, x_3 = (idArrays1_Arrays1_3,x_1_2,x_2_1,x_3_1);
219
     
220
tel
221
 
222
node arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
223
let
224
    
225
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
226
     
227
tel
228
 
229
node arrays1_arrays1__POINTArrays1_Arrays1_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;)
230
var idArrays1_Arrays1: int;
231
    x_1: int;
232
    x_2: int;
233
    x_3: int;
234
let
235
    
236
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (false,POINTArrays1_Arrays1);
237
    idArrays1_Arrays1_out = idArrays1_Arrays1;
238
    x_1_out = x_1;
239
    x_2_out = x_2;
240
    x_3_out = x_3;
241
    idArrays1_Arrays1, x_1, x_2, x_3 = (idArrays1_Arrays1_1,x_1_1,x_2_1,x_3_1);
242
     
243
tel
244
 
245
node arrays1_arrays1__POINTArrays1_Arrays1_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_1: int; E: bool;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
246
var __arrays1_arrays1__POINTArrays1_Arrays1_unless_7: bool;
247
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_6: bool;
248
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_5: bool;
249
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_4: bool;
250
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_3: bool;
251
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_2: bool;
252
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_1: bool;
253
let
254
    
255
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_1 then (true,POINT__TO__ARRAYS1_A_1) else (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_2 then (true,ARRAYS1_A__TO__ARRAYS1_B_1) else (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_3 then (true,ARRAYS1_B__TO__ARRAYS1_C_1) else (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_4 then (true,ARRAYS1_C__TO__ARRAYS1_A_1) else (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_5 then (true,ARRAYS1_A_IDL) else (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_6 then (true,ARRAYS1_B_IDL) else (if __arrays1_arrays1__POINTArrays1_Arrays1_unless_7 then (true,ARRAYS1_C_IDL) else (arrays1_arrays1__restart_in,arrays1_arrays1__state_in))))))));
256
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_7 = (idArrays1_Arrays1_1 = 38);
257
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_6 = (idArrays1_Arrays1_1 = 37);
258
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_5 = (idArrays1_Arrays1_1 = 36);
259
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_4 = ((idArrays1_Arrays1_1 = 38) and E);
260
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_3 = ((idArrays1_Arrays1_1 = 37) and E);
261
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_2 = ((idArrays1_Arrays1_1 = 36) and E);
262
    __arrays1_arrays1__POINTArrays1_Arrays1_unless_1 = (idArrays1_Arrays1_1 = 0);
263
     
264
tel
265
 
266
node arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until (idArrays1_Arrays1_1: int; x_1_1: int; x_2_1: int; x_3_1: int;) returns (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type; idArrays1_Arrays1_out: int; x_1_out: int; x_2_out: int; x_3_out: int;)
267
var idArrays1_Arrays1: int;
268
    x_1: int;
269
    x_2: int;
270
    x_3: int;
271
    x_1_2: int;
272
    idArrays1_Arrays1_2: int;
273
let
274
    
275
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = (if true then (true,POINTArrays1_Arrays1) else (false,POINT__TO__ARRAYS1_A_1));
276
    idArrays1_Arrays1_out = idArrays1_Arrays1;
277
    x_1_out = x_1;
278
    x_2_out = x_2;
279
    x_3_out = x_3;
280
    idArrays1_Arrays1_2, x_1_2 = Arrays1_A_en (idArrays1_Arrays1_1,x_1_1,false);
281
    idArrays1_Arrays1, x_1 = (idArrays1_Arrays1_2,x_1_2);
282
    x_2, x_3 = (x_2_1,x_3_1);
283
     
284
tel
285
 
286
node arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless (arrays1_arrays1__restart_in: bool; arrays1_arrays1__state_in: arrays1_arrays1__type;) returns (arrays1_arrays1__restart_act: bool; arrays1_arrays1__state_act: arrays1_arrays1__type;)
287
let
288
    
289
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = (arrays1_arrays1__restart_in,arrays1_arrays1__state_in);
290
     
291
tel
292
 
293
node Arrays1_Arrays1_node (idArrays1_Arrays1_1: int; x_1_1: int; E: bool; x_2_1: int; x_3_1: int;) returns (idArrays1_Arrays1: int; x_1: int; x_2: int; x_3: int;)
294
var __Arrays1_Arrays1_node_65: bool;
295
    __Arrays1_Arrays1_node_66: arrays1_arrays1__type;
296
    __Arrays1_Arrays1_node_59: bool; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_act)
297
    __Arrays1_Arrays1_node_60: arrays1_arrays1__type; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_act)
298
    __Arrays1_Arrays1_node_61: int; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_act)
299
    __Arrays1_Arrays1_node_62: int; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_act)
300
    __Arrays1_Arrays1_node_63: int; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_act)
301
    __Arrays1_Arrays1_node_64: int; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_act)
302
    __Arrays1_Arrays1_node_53: bool; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
303
    __Arrays1_Arrays1_node_54: arrays1_arrays1__type; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
304
    __Arrays1_Arrays1_node_55: int; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
305
    __Arrays1_Arrays1_node_56: int; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
306
    __Arrays1_Arrays1_node_57: int; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
307
    __Arrays1_Arrays1_node_58: int; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
308
    __Arrays1_Arrays1_node_47: bool; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)
309
    __Arrays1_Arrays1_node_48: arrays1_arrays1__type; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)
310
    __Arrays1_Arrays1_node_49: int; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)
311
    __Arrays1_Arrays1_node_50: int; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)
312
    __Arrays1_Arrays1_node_51: int; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)
313
    __Arrays1_Arrays1_node_52: int; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)
314
    __Arrays1_Arrays1_node_41: bool; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)
315
    __Arrays1_Arrays1_node_42: arrays1_arrays1__type; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)
316
    __Arrays1_Arrays1_node_43: int; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)
317
    __Arrays1_Arrays1_node_44: int; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)
318
    __Arrays1_Arrays1_node_45: int; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)
319
    __Arrays1_Arrays1_node_46: int; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)
320
    __Arrays1_Arrays1_node_35: bool; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
321
    __Arrays1_Arrays1_node_36: arrays1_arrays1__type; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
322
    __Arrays1_Arrays1_node_37: int; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
323
    __Arrays1_Arrays1_node_38: int; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
324
    __Arrays1_Arrays1_node_39: int; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
325
    __Arrays1_Arrays1_node_40: int; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)
326
    __Arrays1_Arrays1_node_29: bool; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_act)
327
    __Arrays1_Arrays1_node_30: arrays1_arrays1__type; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_act)
328
    __Arrays1_Arrays1_node_31: int; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_act)
329
    __Arrays1_Arrays1_node_32: int; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_act)
330
    __Arrays1_Arrays1_node_33: int; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_act)
331
    __Arrays1_Arrays1_node_34: int; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_act)
332
    __Arrays1_Arrays1_node_23: bool; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_act)
333
    __Arrays1_Arrays1_node_24: arrays1_arrays1__type; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_act)
334
    __Arrays1_Arrays1_node_25: int; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_act)
335
    __Arrays1_Arrays1_node_26: int; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_act)
336
    __Arrays1_Arrays1_node_27: int; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_act)
337
    __Arrays1_Arrays1_node_28: int; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_act)
338
    __Arrays1_Arrays1_node_17: bool; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_act)
339
    __Arrays1_Arrays1_node_18: arrays1_arrays1__type; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_act)
340
    __Arrays1_Arrays1_node_19: int; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_act)
341
    __Arrays1_Arrays1_node_20: int; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_act)
342
    __Arrays1_Arrays1_node_21: int; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_act)
343
    __Arrays1_Arrays1_node_22: int; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_act)
344
    __Arrays1_Arrays1_node_15: bool; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_in)
345
    __Arrays1_Arrays1_node_16: arrays1_arrays1__type; --  when POINTArrays1_Arrays1(arrays1_arrays1__state_in)
346
    __Arrays1_Arrays1_node_13: bool; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_in)
347
    __Arrays1_Arrays1_node_14: arrays1_arrays1__type; --  when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_in)
348
    __Arrays1_Arrays1_node_11: bool; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_in)
349
    __Arrays1_Arrays1_node_12: arrays1_arrays1__type; --  when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_in)
350
    __Arrays1_Arrays1_node_9: bool; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_in)
351
    __Arrays1_Arrays1_node_10: arrays1_arrays1__type; --  when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_in)
352
    __Arrays1_Arrays1_node_7: bool; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_in)
353
    __Arrays1_Arrays1_node_8: arrays1_arrays1__type; --  when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_in)
354
    __Arrays1_Arrays1_node_5: bool; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_in)
355
    __Arrays1_Arrays1_node_6: arrays1_arrays1__type; --  when ARRAYS1_A_IDL(arrays1_arrays1__state_in)
356
    __Arrays1_Arrays1_node_3: bool; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_in)
357
    __Arrays1_Arrays1_node_4: arrays1_arrays1__type; --  when ARRAYS1_B_IDL(arrays1_arrays1__state_in)
358
    __Arrays1_Arrays1_node_1: bool; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_in)
359
    __Arrays1_Arrays1_node_2: arrays1_arrays1__type; --  when ARRAYS1_C_IDL(arrays1_arrays1__state_in)
360
    arrays1_arrays1__next_restart_in: bool;
361
    arrays1_arrays1__restart_in: bool;
362
    arrays1_arrays1__restart_act: bool;
363
    arrays1_arrays1__next_state_in: arrays1_arrays1__type;
364
    arrays1_arrays1__state_in: arrays1_arrays1__type clock;
365
    arrays1_arrays1__state_act: arrays1_arrays1__type clock;
366
let
367
    
368
    arrays1_arrays1__restart_in, arrays1_arrays1__state_in = ((false,POINTArrays1_Arrays1) -> (__Arrays1_Arrays1_node_65,__Arrays1_Arrays1_node_66));
369
    arrays1_arrays1__next_restart_in, arrays1_arrays1__next_state_in, idArrays1_Arrays1, x_1, x_2, x_3 = merge arrays1_arrays1__state_act (POINTArrays1_Arrays1 -> (__Arrays1_Arrays1_node_59,__Arrays1_Arrays1_node_60,__Arrays1_Arrays1_node_61,__Arrays1_Arrays1_node_62,__Arrays1_Arrays1_node_63,__Arrays1_Arrays1_node_64)) (POINT__TO__ARRAYS1_A_1 -> (__Arrays1_Arrays1_node_53,__Arrays1_Arrays1_node_54,__Arrays1_Arrays1_node_55,__Arrays1_Arrays1_node_56,__Arrays1_Arrays1_node_57,__Arrays1_Arrays1_node_58)) (ARRAYS1_A__TO__ARRAYS1_B_1 -> (__Arrays1_Arrays1_node_47,__Arrays1_Arrays1_node_48,__Arrays1_Arrays1_node_49,__Arrays1_Arrays1_node_50,__Arrays1_Arrays1_node_51,__Arrays1_Arrays1_node_52)) (ARRAYS1_B__TO__ARRAYS1_C_1 -> (__Arrays1_Arrays1_node_41,__Arrays1_Arrays1_node_42,__Arrays1_Arrays1_node_43,__Arrays1_Arrays1_node_44,__Arrays1_Arrays1_node_45,__Arrays1_Arrays1_node_46)) (ARRAYS1_C__TO__ARRAYS1_A_1 -> (__Arrays1_Arrays1_node_35,__Arrays1_Arrays1_node_36,__Arrays1_Arrays1_node_37,__Arrays1_Arrays1_node_38,__Arrays1_Arrays1_node_39,__Arrays1_Arrays1_node_40)) (ARRAYS1_A_IDL -> (__Arrays1_Arrays1_node_29,__Arrays1_Arrays1_node_30,__Arrays1_Arrays1_node_31,__Arrays1_Arrays1_node_32,__Arrays1_Arrays1_node_33,__Arrays1_Arrays1_node_34)) (ARRAYS1_B_IDL -> (__Arrays1_Arrays1_node_23,__Arrays1_Arrays1_node_24,__Arrays1_Arrays1_node_25,__Arrays1_Arrays1_node_26,__Arrays1_Arrays1_node_27,__Arrays1_Arrays1_node_28)) (ARRAYS1_C_IDL -> (__Arrays1_Arrays1_node_17,__Arrays1_Arrays1_node_18,__Arrays1_Arrays1_node_19,__Arrays1_Arrays1_node_20,__Arrays1_Arrays1_node_21,__Arrays1_Arrays1_node_22));
370
    __Arrays1_Arrays1_node_59, __Arrays1_Arrays1_node_60, __Arrays1_Arrays1_node_61, __Arrays1_Arrays1_node_62, __Arrays1_Arrays1_node_63, __Arrays1_Arrays1_node_64 = arrays1_arrays1__POINTArrays1_Arrays1_handler_until (idArrays1_Arrays1_1 when POINTArrays1_Arrays1(arrays1_arrays1__state_act),x_1_1 when POINTArrays1_Arrays1(arrays1_arrays1__state_act),x_2_1 when POINTArrays1_Arrays1(arrays1_arrays1__state_act),x_3_1 when POINTArrays1_Arrays1(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
371
    __Arrays1_Arrays1_node_53, __Arrays1_Arrays1_node_54, __Arrays1_Arrays1_node_55, __Arrays1_Arrays1_node_56, __Arrays1_Arrays1_node_57, __Arrays1_Arrays1_node_58 = arrays1_arrays1__POINT__TO__ARRAYS1_A_1_handler_until (idArrays1_Arrays1_1 when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act),x_1_1 when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act),x_2_1 when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act),x_3_1 when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
372
    __Arrays1_Arrays1_node_47, __Arrays1_Arrays1_node_48, __Arrays1_Arrays1_node_49, __Arrays1_Arrays1_node_50, __Arrays1_Arrays1_node_51, __Arrays1_Arrays1_node_52 = arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until (idArrays1_Arrays1_1 when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act),x_1_1 when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act),x_2_1 when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act),x_3_1 when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
373
    __Arrays1_Arrays1_node_41, __Arrays1_Arrays1_node_42, __Arrays1_Arrays1_node_43, __Arrays1_Arrays1_node_44, __Arrays1_Arrays1_node_45, __Arrays1_Arrays1_node_46 = arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until (idArrays1_Arrays1_1 when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act),x_1_1 when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act),x_2_1 when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act),x_3_1 when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
374
    __Arrays1_Arrays1_node_35, __Arrays1_Arrays1_node_36, __Arrays1_Arrays1_node_37, __Arrays1_Arrays1_node_38, __Arrays1_Arrays1_node_39, __Arrays1_Arrays1_node_40 = arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until (idArrays1_Arrays1_1 when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act),x_1_1 when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act),x_2_1 when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act),x_3_1 when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
375
    __Arrays1_Arrays1_node_29, __Arrays1_Arrays1_node_30, __Arrays1_Arrays1_node_31, __Arrays1_Arrays1_node_32, __Arrays1_Arrays1_node_33, __Arrays1_Arrays1_node_34 = arrays1_arrays1__ARRAYS1_A_IDL_handler_until (idArrays1_Arrays1_1 when ARRAYS1_A_IDL(arrays1_arrays1__state_act),x_1_1 when ARRAYS1_A_IDL(arrays1_arrays1__state_act),x_2_1 when ARRAYS1_A_IDL(arrays1_arrays1__state_act),x_3_1 when ARRAYS1_A_IDL(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
376
    __Arrays1_Arrays1_node_23, __Arrays1_Arrays1_node_24, __Arrays1_Arrays1_node_25, __Arrays1_Arrays1_node_26, __Arrays1_Arrays1_node_27, __Arrays1_Arrays1_node_28 = arrays1_arrays1__ARRAYS1_B_IDL_handler_until (idArrays1_Arrays1_1 when ARRAYS1_B_IDL(arrays1_arrays1__state_act),x_1_1 when ARRAYS1_B_IDL(arrays1_arrays1__state_act),x_2_1 when ARRAYS1_B_IDL(arrays1_arrays1__state_act),x_3_1 when ARRAYS1_B_IDL(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
377
    __Arrays1_Arrays1_node_17, __Arrays1_Arrays1_node_18, __Arrays1_Arrays1_node_19, __Arrays1_Arrays1_node_20, __Arrays1_Arrays1_node_21, __Arrays1_Arrays1_node_22 = arrays1_arrays1__ARRAYS1_C_IDL_handler_until (idArrays1_Arrays1_1 when ARRAYS1_C_IDL(arrays1_arrays1__state_act),x_1_1 when ARRAYS1_C_IDL(arrays1_arrays1__state_act),x_2_1 when ARRAYS1_C_IDL(arrays1_arrays1__state_act),x_3_1 when ARRAYS1_C_IDL(arrays1_arrays1__state_act)) every (arrays1_arrays1__restart_act);
378
    arrays1_arrays1__restart_act, arrays1_arrays1__state_act = merge arrays1_arrays1__state_in (POINTArrays1_Arrays1 -> (__Arrays1_Arrays1_node_15,__Arrays1_Arrays1_node_16)) (POINT__TO__ARRAYS1_A_1 -> (__Arrays1_Arrays1_node_13,__Arrays1_Arrays1_node_14)) (ARRAYS1_A__TO__ARRAYS1_B_1 -> (__Arrays1_Arrays1_node_11,__Arrays1_Arrays1_node_12)) (ARRAYS1_B__TO__ARRAYS1_C_1 -> (__Arrays1_Arrays1_node_9,__Arrays1_Arrays1_node_10)) (ARRAYS1_C__TO__ARRAYS1_A_1 -> (__Arrays1_Arrays1_node_7,__Arrays1_Arrays1_node_8)) (ARRAYS1_A_IDL -> (__Arrays1_Arrays1_node_5,__Arrays1_Arrays1_node_6)) (ARRAYS1_B_IDL -> (__Arrays1_Arrays1_node_3,__Arrays1_Arrays1_node_4)) (ARRAYS1_C_IDL -> (__Arrays1_Arrays1_node_1,__Arrays1_Arrays1_node_2));
379
    __Arrays1_Arrays1_node_15, __Arrays1_Arrays1_node_16 = arrays1_arrays1__POINTArrays1_Arrays1_unless (arrays1_arrays1__restart_in when POINTArrays1_Arrays1(arrays1_arrays1__state_in),arrays1_arrays1__state_in when POINTArrays1_Arrays1(arrays1_arrays1__state_in),idArrays1_Arrays1_1 when POINTArrays1_Arrays1(arrays1_arrays1__state_in),E when POINTArrays1_Arrays1(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
380
    __Arrays1_Arrays1_node_13, __Arrays1_Arrays1_node_14 = arrays1_arrays1__POINT__TO__ARRAYS1_A_1_unless (arrays1_arrays1__restart_in when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_in),arrays1_arrays1__state_in when POINT__TO__ARRAYS1_A_1(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
381
    __Arrays1_Arrays1_node_11, __Arrays1_Arrays1_node_12 = arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless (arrays1_arrays1__restart_in when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_in),arrays1_arrays1__state_in when ARRAYS1_A__TO__ARRAYS1_B_1(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
382
    __Arrays1_Arrays1_node_9, __Arrays1_Arrays1_node_10 = arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless (arrays1_arrays1__restart_in when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_in),arrays1_arrays1__state_in when ARRAYS1_B__TO__ARRAYS1_C_1(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
383
    __Arrays1_Arrays1_node_7, __Arrays1_Arrays1_node_8 = arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless (arrays1_arrays1__restart_in when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_in),arrays1_arrays1__state_in when ARRAYS1_C__TO__ARRAYS1_A_1(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
384
    __Arrays1_Arrays1_node_5, __Arrays1_Arrays1_node_6 = arrays1_arrays1__ARRAYS1_A_IDL_unless (arrays1_arrays1__restart_in when ARRAYS1_A_IDL(arrays1_arrays1__state_in),arrays1_arrays1__state_in when ARRAYS1_A_IDL(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
385
    __Arrays1_Arrays1_node_3, __Arrays1_Arrays1_node_4 = arrays1_arrays1__ARRAYS1_B_IDL_unless (arrays1_arrays1__restart_in when ARRAYS1_B_IDL(arrays1_arrays1__state_in),arrays1_arrays1__state_in when ARRAYS1_B_IDL(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
386
    __Arrays1_Arrays1_node_1, __Arrays1_Arrays1_node_2 = arrays1_arrays1__ARRAYS1_C_IDL_unless (arrays1_arrays1__restart_in when ARRAYS1_C_IDL(arrays1_arrays1__state_in),arrays1_arrays1__state_in when ARRAYS1_C_IDL(arrays1_arrays1__state_in)) every (arrays1_arrays1__restart_in);
387
    __Arrays1_Arrays1_node_65, __Arrays1_Arrays1_node_66 = pre (arrays1_arrays1__next_restart_in,arrays1_arrays1__next_state_in);
388
     
389
tel
390
 
391
node Arrays1_Arrays1 (E: bool;) returns (x_1: int; x_2: int; x_3: int;)
392
var __Arrays1_Arrays1_8: int;
393
    __Arrays1_Arrays1_7: int;
394
    __Arrays1_Arrays1_6: int;
395
    __Arrays1_Arrays1_5: int;
396
    __Arrays1_Arrays1_1: int;
397
    __Arrays1_Arrays1_2: int;
398
    __Arrays1_Arrays1_3: int;
399
    __Arrays1_Arrays1_4: int;
400
    x_1_1: int;
401
    x_2_1: int;
402
    x_3_1: int;
403
    idArrays1_Arrays1: int;
404
    idArrays1_Arrays1_1: int;
405
let
406
    
407
    x_1_1 = (1 -> __Arrays1_Arrays1_8);
408
    x_2_1 = (1 -> __Arrays1_Arrays1_7);
409
    x_3_1 = (1 -> __Arrays1_Arrays1_6);
410
    idArrays1_Arrays1_1 = (0 -> __Arrays1_Arrays1_5);
411
    idArrays1_Arrays1, x_1, x_2, x_3 = (if E then (__Arrays1_Arrays1_1,__Arrays1_Arrays1_2,__Arrays1_Arrays1_3,__Arrays1_Arrays1_4) else (idArrays1_Arrays1_1,x_1_1,x_2_1,x_3_1));
412
    __Arrays1_Arrays1_1, __Arrays1_Arrays1_2, __Arrays1_Arrays1_3, __Arrays1_Arrays1_4 = Arrays1_Arrays1_node (idArrays1_Arrays1_1,x_1_1,E,x_2_1,x_3_1);
413
    __Arrays1_Arrays1_8 = pre x_1;
414
    __Arrays1_Arrays1_7 = pre x_2;
415
    __Arrays1_Arrays1_6 = pre x_3;
416
    __Arrays1_Arrays1_5 = pre idArrays1_Arrays1;
417
     
418
tel
419
 
420
node Arrays1 (E_1_1: real;) returns (x1_1_1: int; x2_2_1: int; x3_3_1: int;)
421
var __Arrays1_1: real;
422
    Arrays1_1_1: int;
423
    Arrays1_1_2: int;
424
    Arrays1_1_3: int;
425
    Demux_1_1: int;
426
    Demux_2_1: int;
427
    Demux_3_1: int;
428
    E_1_1_event: bool;
429
let
430
    
431
    E_1_1_event = (false -> ((__Arrays1_1 <= 0.) and (E_1_1 > 0.)));
432
    Arrays1_1_1, Arrays1_1_2, Arrays1_1_3 = Arrays1_Arrays1 (E_1_1_event);
433
    Demux_1_1 = Arrays1_1_1;
434
    Demux_2_1 = Arrays1_1_2;
435
    Demux_3_1 = Arrays1_1_3;
436
    x1_1_1 = Demux_1_1;
437
    x2_2_1 = Demux_2_1;
438
    x3_3_1 = Demux_3_1;
439
    __Arrays1_1 = pre E_1_1;
440
     
441
tel
regression_tests/lustre_files/success/Stateflow/src_Arrays1/Arrays1.smt2
1
(declare-datatypes () ((arrays1_arrays1__type POINTArrays1_Arrays1 POINT__TO__ARRAYS1_A_1 ARRAYS1_A__TO__ARRAYS1_B_1 ARRAYS1_B__TO__ARRAYS1_C_1 ARRAYS1_C__TO__ARRAYS1_A_1 ARRAYS1_A_IDL ARRAYS1_B_IDL ARRAYS1_C_IDL)));
2

  
3
; Arrays1_A_ex
4
(declare-var Arrays1_A_ex.idArrays1_Arrays1_1 Int)
5
(declare-var Arrays1_A_ex.isInner Bool)
6
(declare-var Arrays1_A_ex.idArrays1_Arrays1 Int)
7
(declare-var Arrays1_A_ex.idArrays1_Arrays1_2 Int)
8
(declare-rel Arrays1_A_ex (Int Bool Int))
9
(rule (=> 
10
  (and (and (or (not (= (not Arrays1_A_ex.isInner) true))
11
               (= Arrays1_A_ex.idArrays1_Arrays1_2 0))
12
            (or (not (= (not Arrays1_A_ex.isInner) false))
13
               (= Arrays1_A_ex.idArrays1_Arrays1_2 Arrays1_A_ex.idArrays1_Arrays1_1))
14
       )
15
       (= Arrays1_A_ex.idArrays1_Arrays1 Arrays1_A_ex.idArrays1_Arrays1_1)
16
       )
17
  (Arrays1_A_ex Arrays1_A_ex.idArrays1_Arrays1_1 Arrays1_A_ex.isInner Arrays1_A_ex.idArrays1_Arrays1)
18
))
19

  
20
; Arrays1_B_en
21
(declare-var Arrays1_B_en.idArrays1_Arrays1_1 Int)
22
(declare-var Arrays1_B_en.x_2_1 Int)
23
(declare-var Arrays1_B_en.isInner Bool)
24
(declare-var Arrays1_B_en.idArrays1_Arrays1 Int)
25
(declare-var Arrays1_B_en.x_2 Int)
26
(declare-var Arrays1_B_en.x_2_2 Int)
27
(declare-rel Arrays1_B_en (Int Int Bool Int Int))
28
(rule (=> 
29
  (and (and (or (not (= (not Arrays1_B_en.isInner) true))
30
               (= Arrays1_B_en.x_2_2 (+ Arrays1_B_en.x_2_1 1)))
31
            (or (not (= (not Arrays1_B_en.isInner) false))
32
               (= Arrays1_B_en.x_2_2 Arrays1_B_en.x_2_1))
33
       )
34
       (= Arrays1_B_en.x_2 Arrays1_B_en.x_2_2)
35
       (= Arrays1_B_en.idArrays1_Arrays1 512)
36
       )
37
  (Arrays1_B_en Arrays1_B_en.idArrays1_Arrays1_1 Arrays1_B_en.x_2_1 Arrays1_B_en.isInner Arrays1_B_en.idArrays1_Arrays1 Arrays1_B_en.x_2)
38
))
39

  
40
; Arrays1_B_ex
41
(declare-var Arrays1_B_ex.idArrays1_Arrays1_1 Int)
42
(declare-var Arrays1_B_ex.isInner Bool)
43
(declare-var Arrays1_B_ex.idArrays1_Arrays1 Int)
44
(declare-var Arrays1_B_ex.idArrays1_Arrays1_2 Int)
45
(declare-rel Arrays1_B_ex (Int Bool Int))
46
(rule (=> 
47
  (and (and (or (not (= (not Arrays1_B_ex.isInner) true))
48
               (= Arrays1_B_ex.idArrays1_Arrays1_2 0))
49
            (or (not (= (not Arrays1_B_ex.isInner) false))
50
               (= Arrays1_B_ex.idArrays1_Arrays1_2 Arrays1_B_ex.idArrays1_Arrays1_1))
51
       )
52
       (= Arrays1_B_ex.idArrays1_Arrays1 Arrays1_B_ex.idArrays1_Arrays1_1)
53
       )
54
  (Arrays1_B_ex Arrays1_B_ex.idArrays1_Arrays1_1 Arrays1_B_ex.isInner Arrays1_B_ex.idArrays1_Arrays1)
55
))
56

  
57
; Arrays1_C_en
58
(declare-var Arrays1_C_en.idArrays1_Arrays1_1 Int)
59
(declare-var Arrays1_C_en.x_3_1 Int)
60
(declare-var Arrays1_C_en.isInner Bool)
61
(declare-var Arrays1_C_en.idArrays1_Arrays1 Int)
62
(declare-var Arrays1_C_en.x_3 Int)
63
(declare-var Arrays1_C_en.x_3_2 Int)
64
(declare-rel Arrays1_C_en (Int Int Bool Int Int))
65
(rule (=> 
66
  (and (and (or (not (= (not Arrays1_C_en.isInner) true))
67
               (= Arrays1_C_en.x_3_2 (+ Arrays1_C_en.x_3_1 1)))
68
            (or (not (= (not Arrays1_C_en.isInner) false))
69
               (= Arrays1_C_en.x_3_2 Arrays1_C_en.x_3_1))
70
       )
71
       (= Arrays1_C_en.x_3 Arrays1_C_en.x_3_2)
72
       (= Arrays1_C_en.idArrays1_Arrays1 513)
73
       )
74
  (Arrays1_C_en Arrays1_C_en.idArrays1_Arrays1_1 Arrays1_C_en.x_3_1 Arrays1_C_en.isInner Arrays1_C_en.idArrays1_Arrays1 Arrays1_C_en.x_3)
75
))
76

  
77
; Arrays1_A_en
78
(declare-var Arrays1_A_en.idArrays1_Arrays1_1 Int)
79
(declare-var Arrays1_A_en.x_1_1 Int)
80
(declare-var Arrays1_A_en.isInner Bool)
81
(declare-var Arrays1_A_en.idArrays1_Arrays1 Int)
82
(declare-var Arrays1_A_en.x_1 Int)
83
(declare-var Arrays1_A_en.x_1_2 Int)
84
(declare-rel Arrays1_A_en (Int Int Bool Int Int))
85
(rule (=> 
86
  (and (and (or (not (= (not Arrays1_A_en.isInner) true))
87
               (= Arrays1_A_en.x_1_2 (+ Arrays1_A_en.x_1_1 1)))
88
            (or (not (= (not Arrays1_A_en.isInner) false))
89
               (= Arrays1_A_en.x_1_2 Arrays1_A_en.x_1_1))
90
       )
91
       (= Arrays1_A_en.x_1 Arrays1_A_en.x_1_2)
92
       (= Arrays1_A_en.idArrays1_Arrays1 511)
93
       )
94
  (Arrays1_A_en Arrays1_A_en.idArrays1_Arrays1_1 Arrays1_A_en.x_1_1 Arrays1_A_en.isInner Arrays1_A_en.idArrays1_Arrays1 Arrays1_A_en.x_1)
95
))
96

  
97
; Arrays1_C_ex
98
(declare-var Arrays1_C_ex.idArrays1_Arrays1_1 Int)
99
(declare-var Arrays1_C_ex.isInner Bool)
100
(declare-var Arrays1_C_ex.idArrays1_Arrays1 Int)
101
(declare-var Arrays1_C_ex.idArrays1_Arrays1_2 Int)
102
(declare-rel Arrays1_C_ex (Int Bool Int))
103
(rule (=> 
104
  (and (and (or (not (= (not Arrays1_C_ex.isInner) true))
105
               (= Arrays1_C_ex.idArrays1_Arrays1_2 0))
106
            (or (not (= (not Arrays1_C_ex.isInner) false))
107
               (= Arrays1_C_ex.idArrays1_Arrays1_2 Arrays1_C_ex.idArrays1_Arrays1_1))
108
       )
109
       (= Arrays1_C_ex.idArrays1_Arrays1 Arrays1_C_ex.idArrays1_Arrays1_1)
110
       )
111
  (Arrays1_C_ex Arrays1_C_ex.idArrays1_Arrays1_1 Arrays1_C_ex.isInner Arrays1_C_ex.idArrays1_Arrays1)
112
))
113

  
114
; arrays1_arrays1__ARRAYS1_A_IDL_handler_until
115
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1 Int)
116
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1 Int)
117
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1 Int)
118
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1 Int)
119
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in Bool)
120
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
121
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out Int)
122
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out Int)
123
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out Int)
124
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out Int)
125
(declare-rel arrays1_arrays1__ARRAYS1_A_IDL_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
126
(rule (=> 
127
  (and (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1)
128
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1)
129
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1)
130
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1)
131
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
132
       (= arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in true)
133
       )
134
  (arrays1_arrays1__ARRAYS1_A_IDL_handler_until arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A_IDL_handler_until.x_3_out)
135
))
136

  
137
; arrays1_arrays1__ARRAYS1_A_IDL_unless
138
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in Bool)
139
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
140
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act Bool)
141
(declare-var arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
142
(declare-rel arrays1_arrays1__ARRAYS1_A_IDL_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
143
(rule (=> 
144
  (and (= arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_in)
145
       (= arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in)
146
       )
147
  (arrays1_arrays1__ARRAYS1_A_IDL_unless arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A_IDL_unless.arrays1_arrays1__state_act)
148
))
149

  
150
; arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until
151
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1 Int)
152
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1 Int)
153
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1 Int)
154
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1 Int)
155
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in Bool)
156
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
157
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out Int)
158
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out Int)
159
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out Int)
160
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out Int)
161
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2 Int)
162
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3 Int)
163
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2 Int)
164
(declare-rel arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
165
(rule (=> 
166
  (and (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1)
167
       (Arrays1_A_ex arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1
168
                     false
169
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2)
170
       (Arrays1_B_en arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_2
171
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1
172
                     false
173
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3
174
                     arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2)
175
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_2)
176
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1)
177
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_3)
178
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
179
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in true)
180
       )
181
  (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_handler_until.x_3_out)
182
))
183

  
184
; arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless
185
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in Bool)
186
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
187
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act Bool)
188
(declare-var arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
189
(declare-rel arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
190
(rule (=> 
191
  (and (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_in)
192
       (= arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in)
193
       )
194
  (arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_A__TO__ARRAYS1_B_1_unless.arrays1_arrays1__state_act)
195
))
196

  
197
; arrays1_arrays1__ARRAYS1_B_IDL_handler_until
198
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1 Int)
199
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1 Int)
200
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1 Int)
201
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1 Int)
202
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in Bool)
203
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
204
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out Int)
205
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out Int)
206
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out Int)
207
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out Int)
208
(declare-rel arrays1_arrays1__ARRAYS1_B_IDL_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
209
(rule (=> 
210
  (and (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1)
211
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1)
212
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1)
213
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1)
214
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
215
       (= arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in true)
216
       )
217
  (arrays1_arrays1__ARRAYS1_B_IDL_handler_until arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B_IDL_handler_until.x_3_out)
218
))
219

  
220
; arrays1_arrays1__ARRAYS1_B_IDL_unless
221
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in Bool)
222
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
223
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act Bool)
224
(declare-var arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
225
(declare-rel arrays1_arrays1__ARRAYS1_B_IDL_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
226
(rule (=> 
227
  (and (= arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_in)
228
       (= arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in)
229
       )
230
  (arrays1_arrays1__ARRAYS1_B_IDL_unless arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B_IDL_unless.arrays1_arrays1__state_act)
231
))
232

  
233
; arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until
234
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1 Int)
235
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1 Int)
236
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1 Int)
237
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1 Int)
238
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in Bool)
239
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
240
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out Int)
241
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out Int)
242
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out Int)
243
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out Int)
244
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2 Int)
245
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3 Int)
246
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2 Int)
247
(declare-rel arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
248
(rule (=> 
249
  (and (Arrays1_B_ex arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1
250
                     false
251
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2)
252
       (Arrays1_C_en arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_2
253
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1
254
                     false
255
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3
256
                     arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2)
257
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_2)
258
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1)
259
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1)
260
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_3)
261
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
262
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in true)
263
       )
264
  (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_handler_until.x_3_out)
265
))
266

  
267
; arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless
268
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in Bool)
269
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
270
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act Bool)
271
(declare-var arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
272
(declare-rel arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
273
(rule (=> 
274
  (and (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_in)
275
       (= arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in)
276
       )
277
  (arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_B__TO__ARRAYS1_C_1_unless.arrays1_arrays1__state_act)
278
))
279

  
280
; arrays1_arrays1__ARRAYS1_C_IDL_handler_until
281
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1 Int)
282
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1 Int)
283
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1 Int)
284
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1 Int)
285
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in Bool)
286
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
287
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out Int)
288
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out Int)
289
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out Int)
290
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out Int)
291
(declare-rel arrays1_arrays1__ARRAYS1_C_IDL_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
292
(rule (=> 
293
  (and (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1)
294
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1)
295
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1)
296
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1)
297
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
298
       (= arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in true)
299
       )
300
  (arrays1_arrays1__ARRAYS1_C_IDL_handler_until arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C_IDL_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C_IDL_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C_IDL_handler_until.x_3_out)
301
))
302

  
303
; arrays1_arrays1__ARRAYS1_C_IDL_unless
304
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in Bool)
305
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
306
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act Bool)
307
(declare-var arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
308
(declare-rel arrays1_arrays1__ARRAYS1_C_IDL_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
309
(rule (=> 
310
  (and (= arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_in)
311
       (= arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in)
312
       )
313
  (arrays1_arrays1__ARRAYS1_C_IDL_unless arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C_IDL_unless.arrays1_arrays1__state_act)
314
))
315

  
316
; arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until
317
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 Int)
318
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1 Int)
319
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1 Int)
320
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1 Int)
321
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in Bool)
322
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
323
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out Int)
324
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out Int)
325
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out Int)
326
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out Int)
327
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2 Int)
328
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3 Int)
329
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2 Int)
330
(declare-rel arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
331
(rule (=> 
332
  (and (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1)
333
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1)
334
       (Arrays1_C_ex arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1
335
                     false
336
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2)
337
       (Arrays1_A_en arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_2
338
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1
339
                     false
340
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3
341
                     arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2)
342
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_2)
343
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_3)
344
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
345
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in true)
346
       )
347
  (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_1 arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_1_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_2_out arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_handler_until.x_3_out)
348
))
349

  
350
; arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless
351
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in Bool)
352
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
353
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act Bool)
354
(declare-var arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
355
(declare-rel arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless (Bool arrays1_arrays1__type Bool arrays1_arrays1__type))
356
(rule (=> 
357
  (and (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in)
358
       (= arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in)
359
       )
360
  (arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_in arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__restart_act arrays1_arrays1__ARRAYS1_C__TO__ARRAYS1_A_1_unless.arrays1_arrays1__state_act)
361
))
362

  
363
; arrays1_arrays1__POINTArrays1_Arrays1_handler_until
364
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1 Int)
365
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1 Int)
366
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1 Int)
367
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1 Int)
368
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in Bool)
369
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__type)
370
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out Int)
371
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out Int)
372
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out Int)
373
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out Int)
374
(declare-rel arrays1_arrays1__POINTArrays1_Arrays1_handler_until (Int Int Int Int Bool arrays1_arrays1__type Int Int Int Int))
375
(rule (=> 
376
  (and (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1)
377
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1)
378
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1)
379
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1)
380
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in POINTArrays1_Arrays1)
381
       (= arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in false)
382
       )
383
  (arrays1_arrays1__POINTArrays1_Arrays1_handler_until arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_1 arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__restart_in arrays1_arrays1__POINTArrays1_Arrays1_handler_until.arrays1_arrays1__state_in arrays1_arrays1__POINTArrays1_Arrays1_handler_until.idArrays1_Arrays1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_1_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_2_out arrays1_arrays1__POINTArrays1_Arrays1_handler_until.x_3_out)
384
))
385

  
386
; arrays1_arrays1__POINTArrays1_Arrays1_unless
387
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in Bool)
388
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_in arrays1_arrays1__type)
389
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 Int)
390
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.E Bool)
391
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act Bool)
392
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act arrays1_arrays1__type)
393
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 Bool)
394
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 Bool)
395
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 Bool)
396
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 Bool)
397
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 Bool)
398
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 Bool)
399
(declare-var arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 Bool)
400
(declare-rel arrays1_arrays1__POINTArrays1_Arrays1_unless (Bool arrays1_arrays1__type Int Bool Bool arrays1_arrays1__type))
401
(rule (=> 
402
  (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 513))
403
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 512))
404
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 511))
405
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 513) arrays1_arrays1__POINTArrays1_Arrays1_unless.E))
406
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 512) arrays1_arrays1__POINTArrays1_Arrays1_unless.E))
407
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 511) arrays1_arrays1__POINTArrays1_Arrays1_unless.E))
408
       (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 (= arrays1_arrays1__POINTArrays1_Arrays1_unless.idArrays1_Arrays1_1 0))
409
       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 false))
410
               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 false))
411
                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 false))
412
                               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 false))
413
                                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 false))
414
                                               (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 false))
415
                                                       (and (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 false))
416
                                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_in)
417
                                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_in)
418
                                                                    ))
419
                                                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_7 true))
420
                                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_C_IDL)
421
                                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
422
                                                                    ))
423
                                                       ))
424
                                                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_6 true))
425
                                                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_B_IDL)
426
                                                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
427
                                                            ))
428
                                               ))
429
                                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_5 true))
430
                                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_A_IDL)
431
                                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
432
                                                    ))
433
                                       ))
434
                                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_4 true))
435
                                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_C__TO__ARRAYS1_A_1)
436
                                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
437
                                            ))
438
                               ))
439
                            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_3 true))
440
                               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_B__TO__ARRAYS1_C_1)
441
                                    (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
442
                                    ))
443
                       ))
444
                    (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_2 true))
445
                       (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act ARRAYS1_A__TO__ARRAYS1_B_1)
446
                            (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__restart_act true)
447
                            ))
448
               ))
449
            (or (not (= arrays1_arrays1__POINTArrays1_Arrays1_unless.__arrays1_arrays1__POINTArrays1_Arrays1_unless_1 true))
450
               (and (= arrays1_arrays1__POINTArrays1_Arrays1_unless.arrays1_arrays1__state_act POINT__TO__ARRAYS1_A_1)
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff