Project

General

Profile

Revision fa9e78e5

View differences:

regression_tests/CMakeLists.txt
4 4

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

  
8
file(COPY ${PROJECT_SOURCE_DIR}/modules/read_value.c  DESTINATION  ${CMAKE_BINARY_DIR}/modules)
9
add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/modules/read_value 
10
					COMMAND ${CMAKE_C_COMPILER} -o  read_value read_value.c
11
					WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/modules 
12
					COMMENT "compiling read_value")
13
add_custom_target (read_value ALL
14
	DEPENDS ${CMAKE_BINARY_DIR}/modules/read_value)
7
include(./modules/Zustre_compile.cmake)
15 8
	
16 9
add_subdirectory(lustre_files)
17 10

  
regression_tests/lustre_files/success/CMakeLists.txt
2 2

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

  
2
include(FindUnixCommands)
3 3

  
4 4

  
5 5

  
......
22 22
  list(APPEND GLOBAL_LUSTRE_FILES ${LFILE})
23 23
  get_filename_component(L ${LFILE} NAME_WE)
24 24
  set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
25

  
26
  file(COPY ${LFILE} "${subdir}/input_values" "${subdir}/outputs_values" DESTINATION  ${LUSTRE_OUTPUT_DIR})
25
  file(COPY ${LFILE} "${subdir}/input_values" "${subdir}/outputs_values"   DESTINATION  ${LUSTRE_OUTPUT_DIR})
27 26
ENDFOREACH()
28 27

  
29 28
#first combination :no option
30 29
set(LUSTRE_OPTIONS_OPT "")
31
set(GENERATION_RESULTS "")
32
set(REPORT_PATH  "${CMAKE_CURRENT_BINARY_DIR}/report")
33
file(WRITE ${REPORT_PATH}  "")
34 30
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
35 31
	get_filename_component(L ${lus_file} NAME_WE)
36 32
	set(LUSTRE_NODE_OPT  "${L}")
37
	set(LUSTRE_OPTIONS_OPT  "" )
38 33
	
39 34
	# First command generate C files from Lustre file
40 35
	Lustre_Compile(LUS_FILE ${lus_file}
41 36
					NODE ${LUSTRE_NODE_OPT}
42 37
					OPTS ${LUSTRE_OPTIONS_OPT})
38
					
39
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
40
	add_test(NAME Simulink_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
41
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
42
			#REQUIRED_FILES ${lus_file}
43
	)
43 44

  
44
	if(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0" )
45
		message("****************${LUSTRE_GENERATED_FILES_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}: Failed********")
46
	else(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0")
47
		#second command : generate C binary from C files generated before		
48
		#third step : compare binary outputs with the reference.
49
		add_custom_command(
50
			OUTPUT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report
51
			DEPENDS ${LUSTRE_GENERATED_FILES_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
52
			COMMAND make 
53
			ARGS  -f ${L}.makefile
54
			COMMAND ./${L}_${LUSTRE_NODE_OPT} 
55
			ARGS < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs
56
			COMMAND diff
57
			ARGS -s ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values > report
58
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
59
			COMMENT " make -f ${L}.makefile \n ./${L}_${LUSTRE_NODE_OPT}  < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs \n diff -s ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values > report"
45
	 #********************* make -f ${L}.makefile ***************************
46
	 add_test(NAME Simulink_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
47
			COMMAND  make -f ${L}.makefile
48
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
49
	)
50
	SET_TESTS_PROPERTIES ( Simulink_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
51
	 PROPERTIES DEPENDS Simulink_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
52
				REQUIRED_FILES ${L}.makefile
53
				)
54
	 
55
	 #************** execute C binary **********************************
56
	
57
	if (BASH)
58
		add_test(
59
			NAME Simulink_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} 
60
			COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
61
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
60 62
		)
61
		add_test(NAME Stateflow_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}
62
				WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
63
				COMMAND diff -s  ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values)
64
		set_tests_properties(Stateflow_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}
65
				PROPERTIES PASS_REGULAR_EXPRESSION "are identical")
66
				
67
				
68
		set(GENERATION_RESULTS ${GENERATION_RESULTS} ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report)
69
		
70
		if(EXISTS ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report )
71
			file(READ ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report REPORT)
72
			file(APPEND ${REPORT_PATH}.in  "${REPORT}")
73
			# Copy the temporary file to the final location
74
			configure_file(${REPORT_PATH}.in ${REPORT_PATH} COPYONLY)
75
		endif()
76
	endif(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0")
63
		SET_TESTS_PROPERTIES ( Simulink_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
64
			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
65
				DEPENDS Simulink_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
66
	else()
67
		message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
68
	endif()
77 69

  
70
	 #************** execute C binary **********************************
71
	 add_test(NAME Simulink_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
72
			COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values 
73
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
74
	)
75
	SET_TESTS_PROPERTIES ( Simulink_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
76
	 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
77
				DEPENDS Simulink_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
78
				
79
	
78 80
ENDFOREACH()
79 81

  
80 82

  
81
add_custom_target (Simulink_GENERATE_FILES ALL
82
	DEPENDS ${GENERATION_RESULTS})
regression_tests/lustre_files/success/Stateflow/CMakeLists.txt
1 1
cmake_minimum_required(VERSION 2.8.4)
2

  
2
include(FindUnixCommands)
3 3

  
4 4

  
5 5

  
......
22 22
  list(APPEND GLOBAL_LUSTRE_FILES ${LFILE})
23 23
  get_filename_component(L ${LFILE} NAME_WE)
24 24
  set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
25
  file(COPY ${LFILE} "${subdir}/input_values" "${subdir}/outputs_values" "${subdir}/${L}.smt2"  DESTINATION  ${LUSTRE_OUTPUT_DIR})
25
  file(COPY ${LFILE} "${subdir}/input_values" "${subdir}/outputs_values"   DESTINATION  ${LUSTRE_OUTPUT_DIR})
26 26
ENDFOREACH()
27 27

  
28 28
#first combination :no option
29 29
set(LUSTRE_OPTIONS_OPT "")
30
set(GENERATION_RESULTS "")
31
set(REPORT_PATH  "${CMAKE_CURRENT_BINARY_DIR}/report")
32
file(WRITE ${REPORT_PATH}  "")
30

  
33 31
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
34 32
	get_filename_component(L ${lus_file} NAME_WE)
35 33
	set(LUSTRE_NODE_OPT  "${L}")
......
38 36
	Lustre_Compile(LUS_FILE ${lus_file}
39 37
					NODE ${LUSTRE_NODE_OPT}
40 38
					OPTS ${LUSTRE_OPTIONS_OPT})
41

  
42
	if(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0" )
43
		message("****************${LUSTRE_GENERATED_FILES_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}: Failed********")
44
	else(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0")
45
		#second command : generate C binary from C files generated before		
46
		#third step : compare binary outputs with the reference.
47
		add_custom_command(
48
			OUTPUT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report
49
			DEPENDS ${LUSTRE_GENERATED_FILES_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
50
			COMMAND make 
51
			ARGS  -f ${L}.makefile
52
			COMMAND ./${L}_${LUSTRE_NODE_OPT} 
53
			ARGS < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs
54
			COMMAND diff
55
			ARGS -s ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values > report
56
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
57
			COMMENT " make -f ${L}.makefile \n ./${L}_${LUSTRE_NODE_OPT}  < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs \n diff -s ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values > report"
58
		)
59
		add_test(NAME Stateflow_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}
60
				WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
61
				COMMAND diff -s  ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values)
62
		set_tests_properties(Stateflow_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}
63
				PROPERTIES PASS_REGULAR_EXPRESSION "are identical")
64
				
65
				
66
		set(GENERATION_RESULTS ${GENERATION_RESULTS} ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report)
67
		
68
		if(EXISTS ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report )
69
			file(READ ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report REPORT)
70
			file(APPEND ${REPORT_PATH}.in  "${REPORT}")
71
			# Copy the temporary file to the final location
72
			configure_file(${REPORT_PATH}.in ${REPORT_PATH} COPYONLY)
73
		endif()
74
	endif(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0")
75

  
76
ENDFOREACH()
77

  
78

  
79
add_custom_target (Stateflow_GENERATE_FILES ALL
80
	DEPENDS ${GENERATION_RESULTS})
81

  
82

  
83

  
84

  
85

  
86

  
87

  
88

  
89

  
90

  
91
#second combination :-horn
92
set(LUSTRE_OPTIONS_OPT "-horn")
93
#string(REPLACE "-" "" LUS_OPTS_CUT ${LUSTRE_OPTIONS_OPT})
94
#string(REPLACE " " "_" LUS_OPTS_CUT ${LUS_OPTS_CUT})
95
set(LUSTRE_NODE_OPT  "")
96
set(GENERATION_RESULTS "")
97
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
98
	get_filename_component(L ${lus_file} NAME_WE)
39
					
40
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
41
	add_test(NAME Stateflow_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
42
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
43
			#REQUIRED_FILES ${lus_file}
44
	)
45

  
46
	 #********************* make -f ${L}.makefile ***************************
47
	 add_test(NAME Stateflow_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
48
			COMMAND  make -f ${L}.makefile
49
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
50
	)
51
	SET_TESTS_PROPERTIES ( Stateflow_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
52
	 PROPERTIES DEPENDS Stateflow_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
53
				REQUIRED_FILES ${L}.makefile
54
				)
55
	 
56
	 #************** execute C binary **********************************
99 57
	
100
	# First command generate C files from Lustre file
101
	Lustre_Compile(LUS_FILE ${lus_file}
102
					NODE ${LUSTRE_NODE_OPT}
103
					OPTS ${LUSTRE_OPTIONS_OPT})
104

  
105
	if(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0" )
106
		message("****************${LUSTRE_GENERATED_FILES_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}: Failed********")
107
	else(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0")
108
		#second command : generate C binary from C files generated before		
109
		#third step : compare binary outputs with the reference.
110
		add_custom_command(
111
			OUTPUT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report
112
			DEPENDS ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/${L}.smt2
113
			COMMAND diff
114
			ARGS -s ${L}.smt2 ../${L}.smt2 > report
115
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
116
			COMMENT "diff -s ${L}.smt2 ../${L}.smt2 > report"
58
	if (BASH)
59
		add_test(
60
			NAME Stateflow_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} 
61
			COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ../input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
62
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
117 63
		)
118
		add_test(NAME Stateflow_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}
119
				WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}
120
				COMMAND diff -s   ${L}.smt2 ../${L}.smt2 )
121
		set_tests_properties(Stateflow_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}
122
				PROPERTIES PASS_REGULAR_EXPRESSION "are identical")
64
		SET_TESTS_PROPERTIES ( Stateflow_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
65
			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
66
				DEPENDS Stateflow_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
67
	else()
68
		message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
69
	endif()
70

  
71
	 #************** execute C binary **********************************
72
	 add_test(NAME Stateflow_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
73
			COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ../outputs_values 
74
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
75
	)
76
	SET_TESTS_PROPERTIES ( Stateflow_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
77
	 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
78
				DEPENDS Stateflow_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
123 79
				
124
				
125
		set(GENERATION_RESULTS ${GENERATION_RESULTS} ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report)
126
		
127
		if(EXISTS ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report )
128
			file(READ ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}}/report REPORT)
129
			file(APPEND ${REPORT_PATH}.in  "${REPORT}")
130
			# Copy the temporary file to the final location
131
			configure_file(${REPORT_PATH}.in ${REPORT_PATH} COPYONLY)
132
		endif()
133
	endif(NOT ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUSTRE_OPTIONS_OPT}_RESULT} STREQUAL "0")
134

  
80
	
135 81
ENDFOREACH()
136 82

  
137 83

  
138
add_custom_target (Stateflow_GENERATE_FILES_horn ALL
139
	DEPENDS ${GENERATION_RESULTS})
regression_tests/lustre_files/success/kind_fmcad08/large/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

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

  
3

  
4

  
5
if(ZUSTRE_COMPILER)
6
  message(STATUS "Found zustre: ${ZUSTRE_COMPILER} ")
7
else(ZUSTRE_COMPILER)
8
  message(FATAL_ERROR "zustre not found")
9
endif(ZUSTRE_COMPILER)
10

  
11
#take all lustre files
12
  set(GLOBAL_LUSTRE_FILES "")
13
  LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
14
  list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
15
  FOREACH(lfile ${LFILES})
16
	  get_filename_component(L ${lfile} NAME_WE)
17
	  set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
18
	  file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
19
  ENDFOREACH()
20

  
21

  
22
#first combination :no option
23
set(ZUSTRE_OPTIONS_OPT "--timeout" "60" "--xml" )
24

  
25
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
26
	get_filename_component(L ${lus_file} NAME_WE)
27
	set(ZUSTRE_NODE_OPT  "top")
28

  
29
	Lustre_Compile(LUS_FILE ${lus_file}
30
					NODE ""
31
					OPTS "-horn")
32
					
33
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
34
	add_test(NAME Kind_fmcad08_large_BROKEN_COMPIL_LUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
35
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
36
	)
37

  
38
	Zustre_Compile(LUS_FILE ${lus_file}
39
					NODE ${ZUSTRE_NODE_OPT}
40
					OPTS ${ZUSTRE_OPTIONS_OPT})
41
	set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
42
	
43
	
44
	add_test(NAME Kind_fmcad08_large_BROKEN_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
45
			COMMAND  ${ZUSTRE_COMPILER} ${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}} 
46
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}
47
	)
48
	SET_TESTS_PROPERTIES (  Kind_fmcad08_large_BROKEN_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
49
			PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
50
					DEPENDS Kind_fmcad08_large_BROKEN_COMPIL_LUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
51
				
52

  
53
ENDFOREACH()
54

  
55

  
regression_tests/lustre_files/success/kind_fmcad08/large/src/BROKEN/steam_boiler_no_arr1.h
1
/* C code generated by lustrec
2
   Version number 1.3-458
3
   Code is C99 compliant
4
   Using (double) floating-point numbers */
5
   
6
#ifndef _STEAM_BOILER_NO_ARR1
7
#define _STEAM_BOILER_NO_ARR1
8

  
9
/* Imports standard library */
10
#include "/usr/local/include/lustrec/arrow.h"
11

  
12

  
13
/* Import dependencies */
14

  
15
/* Types definitions */
16

  
17
/* Global constant (declarations, definitions are in C file) */
18

  
19
/* Structs declarations */
20
struct top_mem;
21
struct Verification_mem;
22
struct BoilerController_mem;
23
struct FEDGE2_mem;
24
struct FEDGE1_mem;
25
struct Valve_mem;
26
struct SteamDefect_mem;
27
struct PumpsStatus_mem;
28
struct PumpsOutput_mem;
29
struct PumpsDecision_mem;
30
struct PumpDefect_mem;
31
struct Operator_mem;
32
struct LevelDefect_mem;
33
struct Dynamics_mem;
34
struct ControlMode_mem;
35
struct REDGE_mem;
36
struct operate_pumps_mem;
37

  
38
/* Nodes declarations */
39
extern void top_reset (struct top_mem *self);
40

  
41
extern void top_init (struct top_mem *self);
42

  
43
extern void top_clear (struct top_mem *self);
44

  
45
extern void top_step (_Bool stop, _Bool steam_boiler_waiting,
46
                      _Bool physical_units_ready, int level, int steam,
47
                      int pump_state_0, int pump_state_1, int pump_state_2,
48
                      int pump_state_3, _Bool pump_control_state_0,
49
                      _Bool pump_control_state_1, _Bool pump_control_state_2,
50
                      _Bool pump_control_state_3, _Bool pump_repaired_0,
51
                      _Bool pump_repaired_1, _Bool pump_repaired_2,
52
                      _Bool pump_repaired_3, _Bool pump_control_repaired_0,
53
                      _Bool pump_control_repaired_1,
54
                      _Bool pump_control_repaired_2,
55
                      _Bool pump_control_repaired_3, _Bool level_repaired,
56
                      _Bool steam_repaired,
57
                      _Bool pump_failure_acknowledgement_0,
58
                      _Bool pump_failure_acknowledgement_1,
59
                      _Bool pump_failure_acknowledgement_2,
60
                      _Bool pump_failure_acknowledgement_3,
61
                      _Bool pump_control_failure_acknowledgement_0,
62
                      _Bool pump_control_failure_acknowledgement_1,
63
                      _Bool pump_control_failure_acknowledgement_2,
64
                      _Bool pump_control_failure_acknowledgement_3,
65
                      _Bool level_failure_acknowledgement,
66
                      _Bool steam_failure_acknowledgement, 
67
                      _Bool (*OK),
68
                      struct top_mem *self);
69

  
70
extern void NOT_step (_Bool a_0, _Bool a_1, _Bool a_2, _Bool a_3, 
71
                      _Bool (*NOT_0), _Bool (*NOT_1), _Bool (*NOT_2),
72
                      _Bool (*NOT_3)
73
                      );
74

  
75
extern void Verification_reset (struct Verification_mem *self);
76

  
77
extern void Verification_init (struct Verification_mem *self);
78

  
79
extern void Verification_clear (struct Verification_mem *self);
80

  
81
extern void Verification_step (_Bool S1, _Bool S2, 
82
                               _Bool (*property_ok),
83
                               struct Verification_mem *self);
84

  
85
extern void BoilerController_reset (struct BoilerController_mem *self);
86

  
87
extern void BoilerController_init (struct BoilerController_mem *self);
88

  
89
extern void BoilerController_clear (struct BoilerController_mem *self);
90

  
91
extern void BoilerController_step (_Bool stop, _Bool steam_boiler_waiting,
92
                                   _Bool physical_units_ready, int level,
93
                                   int steam, int pump_state_0,
94
                                   int pump_state_1, int pump_state_2,
95
                                   int pump_state_3,
96
                                   _Bool pump_control_state_0,
97
                                   _Bool pump_control_state_1,
98
                                   _Bool pump_control_state_2,
99
                                   _Bool pump_control_state_3,
100
                                   _Bool pump_repaired_0,
101
                                   _Bool pump_repaired_1,
102
                                   _Bool pump_repaired_2,
103
                                   _Bool pump_repaired_3,
104
                                   _Bool pump_control_repaired_0,
105
                                   _Bool pump_control_repaired_1,
106
                                   _Bool pump_control_repaired_2,
107
                                   _Bool pump_control_repaired_3,
108
                                   _Bool level_repaired,
109
                                   _Bool steam_repaired,
110
                                   _Bool pump_failure_acknowledgement_0,
111
                                   _Bool pump_failure_acknowledgement_1,
112
                                   _Bool pump_failure_acknowledgement_2,
113
                                   _Bool pump_failure_acknowledgement_3,
114
                                   _Bool pump_control_failure_acknowledgement_0,
115
                                   _Bool pump_control_failure_acknowledgement_1,
116
                                   _Bool pump_control_failure_acknowledgement_2,
117
                                   _Bool pump_control_failure_acknowledgement_3,
118
                                   _Bool level_failure_acknowledgement,
119
                                   _Bool steam_failure_acknowledgement, 
120
                                   _Bool (*program_ready), int (*mode),
121
                                   _Bool (*valve), _Bool (*open_pump_0),
122
                                   _Bool (*open_pump_1),
123
                                   _Bool (*open_pump_2),
124
                                   _Bool (*open_pump_3),
125
                                   _Bool (*close_pump_0),
126
                                   _Bool (*close_pump_1),
127
                                   _Bool (*close_pump_2),
128
                                   _Bool (*close_pump_3),
129
                                   _Bool (*pump_failure_detection_0),
130
                                   _Bool (*pump_failure_detection_1),
131
                                   _Bool (*pump_failure_detection_2),
132
                                   _Bool (*pump_failure_detection_3),
133
                                   _Bool (*pump_control_failure_detection_0),
134
                                   _Bool (*pump_control_failure_detection_1),
135
                                   _Bool (*pump_control_failure_detection_2),
136
                                   _Bool (*pump_control_failure_detection_3),
137
                                   _Bool (*level_failure_detection),
138
                                   _Bool (*steam_outcome_failure_detection),
139
                                   _Bool (*pump_repaired_acknowledgement_0),
140
                                   _Bool (*pump_repaired_acknowledgement_1),
141
                                   _Bool (*pump_repaired_acknowledgement_2),
142
                                   _Bool (*pump_repaired_acknowledgement_3),
143
                                   _Bool (*pump_control_repaired_acknowledgement_0),
144
                                   _Bool (*pump_control_repaired_acknowledgement_1),
145
                                   _Bool (*pump_control_repaired_acknowledgement_2),
146
                                   _Bool (*pump_control_repaired_acknowledgement_3),
147
                                   _Bool (*level_repaired_acknowledgement),
148
                                   _Bool (*steam_outcome_repaired_acknowledgement),
149
                                   struct BoilerController_mem *self);
150

  
151
extern void FEDGE2_reset (struct FEDGE2_mem *self);
152

  
153
extern void FEDGE2_init (struct FEDGE2_mem *self);
154

  
155
extern void FEDGE2_clear (struct FEDGE2_mem *self);
156

  
157
extern void FEDGE2_step (_Bool S, 
158
                         _Bool (*FEDGE2),
159
                         struct FEDGE2_mem *self);
160

  
161
extern void FEDGE1_reset (struct FEDGE1_mem *self);
162

  
163
extern void FEDGE1_init (struct FEDGE1_mem *self);
164

  
165
extern void FEDGE1_clear (struct FEDGE1_mem *self);
166

  
167
extern void FEDGE1_step (_Bool S, 
168
                         _Bool (*FEDGE1),
169
                         struct FEDGE1_mem *self);
170

  
171
extern void Valve_reset (struct Valve_mem *self);
172

  
173
extern void Valve_init (struct Valve_mem *self);
174

  
175
extern void Valve_clear (struct Valve_mem *self);
176

  
177
extern void Valve_step (int op_mode, int q, 
178
                        _Bool (*valve), int (*valve_state),
179
                        struct Valve_mem *self);
180

  
181
extern void SteamOutput_step (int op_mode, int steam_defect,
182
                              _Bool steam_repaired, 
183
                              _Bool (*steam_outcome_failure_detection),
184
                              _Bool (*steam_outcome_repaired_acknowledgement)
185
                              );
186

  
187
extern void SteamDefect_reset (struct SteamDefect_mem *self);
188

  
189
extern void SteamDefect_init (struct SteamDefect_mem *self);
190

  
191
extern void SteamDefect_clear (struct SteamDefect_mem *self);
192

  
193
extern void SteamDefect_step (_Bool steam_failure_acknowledgement,
194
                              _Bool steam_repaired, int steam, 
195
                              int (*SteamDefect),
196
                              struct SteamDefect_mem *self);
197

  
198
extern void PumpsStatus_reset (struct PumpsStatus_mem *self);
199

  
200
extern void PumpsStatus_init (struct PumpsStatus_mem *self);
201

  
202
extern void PumpsStatus_clear (struct PumpsStatus_mem *self);
203

  
204
extern void PumpsStatus_step (int n_pumps, int pump_defect_0,
205
                              int pump_defect_1, int pump_defect_2,
206
                              int pump_defect_3, _Bool flow_0, _Bool flow_1,
207
                              _Bool flow_2, _Bool flow_3, 
208
                              int (*pump_status_0), int (*pump_status_1),
209
                              int (*pump_status_2), int (*pump_status_3),
210
                              struct PumpsStatus_mem *self);
211

  
212
extern void PumpsOutput_reset (struct PumpsOutput_mem *self);
213

  
214
extern void PumpsOutput_init (struct PumpsOutput_mem *self);
215

  
216
extern void PumpsOutput_clear (struct PumpsOutput_mem *self);
217

  
218
extern void PumpsOutput_step (int op_mode, int pump_status_0,
219
                              int pump_status_1, int pump_status_2,
220
                              int pump_status_3, int pump_defect_0,
221
                              int pump_defect_1, int pump_defect_2,
222
                              int pump_defect_3, int pump_control_defect_0,
223
                              int pump_control_defect_1,
224
                              int pump_control_defect_2,
225
                              int pump_control_defect_3,
226
                              _Bool pump_repaired_0, _Bool pump_repaired_1,
227
                              _Bool pump_repaired_2, _Bool pump_repaired_3,
228
                              _Bool pump_control_repaired_0,
229
                              _Bool pump_control_repaired_1,
230
                              _Bool pump_control_repaired_2,
231
                              _Bool pump_control_repaired_3, 
232
                              _Bool (*open_pump_0), _Bool (*open_pump_1),
233
                              _Bool (*open_pump_2), _Bool (*open_pump_3),
234
                              _Bool (*close_pump_0), _Bool (*close_pump_1),
235
                              _Bool (*close_pump_2), _Bool (*close_pump_3),
236
                              _Bool (*pump_failure_detection_0),
237
                              _Bool (*pump_failure_detection_1),
238
                              _Bool (*pump_failure_detection_2),
239
                              _Bool (*pump_failure_detection_3),
240
                              _Bool (*pump_repaired_acknowledgement_0),
241
                              _Bool (*pump_repaired_acknowledgement_1),
242
                              _Bool (*pump_repaired_acknowledgement_2),
243
                              _Bool (*pump_repaired_acknowledgement_3),
244
                              _Bool (*pump_control_failure_detection_0),
245
                              _Bool (*pump_control_failure_detection_1),
246
                              _Bool (*pump_control_failure_detection_2),
247
                              _Bool (*pump_control_failure_detection_3),
248
                              _Bool (*pump_control_repaired_acknowledgement_0),
249
                              _Bool (*pump_control_repaired_acknowledgement_1),
250
                              _Bool (*pump_control_repaired_acknowledgement_2),
251
                              _Bool (*pump_control_repaired_acknowledgement_3),
252
                              struct PumpsOutput_mem *self);
253

  
254
extern void PumpsDecision_reset (struct PumpsDecision_mem *self);
255

  
256
extern void PumpsDecision_init (struct PumpsDecision_mem *self);
257

  
258
extern void PumpsDecision_clear (struct PumpsDecision_mem *self);
259

  
260
extern void PumpsDecision_step (int q, int v, 
261
                                int (*n_pumps),
262
                                struct PumpsDecision_mem *self);
263

  
264
extern void PumpDefect_reset (struct PumpDefect_mem *self);
265

  
266
extern void PumpDefect_init (struct PumpDefect_mem *self);
267

  
268
extern void PumpDefect_clear (struct PumpDefect_mem *self);
269

  
270
extern void PumpDefect_step (_Bool pump_failure_acknowledgement,
271
                             _Bool pump_repaired,
272
                             _Bool pump_control_failure_acknowledgement,
273
                             _Bool pump_control_repaired, int pump_status,
274
                             int pump_state, _Bool pump_control_state, 
275
                             int (*PumpDefect), int (*PumpControlDefect),
276
                             _Bool (*Flow),
277
                             struct PumpDefect_mem *self);
278

  
279
extern void Operator_reset (struct Operator_mem *self);
280

  
281
extern void Operator_init (struct Operator_mem *self);
282

  
283
extern void Operator_clear (struct Operator_mem *self);
284

  
285
extern void Operator_step (_Bool stop, 
286
                           _Bool (*stop_request),
287
                           struct Operator_mem *self);
288

  
289
extern void LevelOutput_step (int op_mode, int level_defect,
290
                              _Bool level_repaired, 
291
                              _Bool (*level_outcome_failure_detection),
292
                              _Bool (*level_outcome_repaired_acknowledgement)
293
                              );
294

  
295
extern void LevelDefect_reset (struct LevelDefect_mem *self);
296

  
297
extern void LevelDefect_init (struct LevelDefect_mem *self);
298

  
299
extern void LevelDefect_clear (struct LevelDefect_mem *self);
300

  
301
extern void LevelDefect_step (_Bool level_failure_acknowledgement,
302
                              _Bool level_repaired, int level, 
303
                              int (*LevelDefect),
304
                              struct LevelDefect_mem *self);
305

  
306
extern void Dynamics_reset (struct Dynamics_mem *self);
307

  
308
extern void Dynamics_init (struct Dynamics_mem *self);
309

  
310
extern void Dynamics_clear (struct Dynamics_mem *self);
311

  
312
extern void Dynamics_step (int valve_state, int level, int steam,
313
                           int level_defect, int steam_defect, _Bool flow_0,
314
                           _Bool flow_1, _Bool flow_2, _Bool flow_3, 
315
                           int (*q), int (*v), int (*p_0), int (*p_1),
316
                           int (*p_2), int (*p_3),
317
                           struct Dynamics_mem *self);
318

  
319
extern void ControlOutput_step (int op_mode, int level, _Bool valve, 
320
                                _Bool (*program_ready), int (*mode)
321
                                );
322

  
323
extern void ControlMode_reset (struct ControlMode_mem *self);
324

  
325
extern void ControlMode_init (struct ControlMode_mem *self);
326

  
327
extern void ControlMode_clear (struct ControlMode_mem *self);
328

  
329
extern void ControlMode_step (_Bool steam_boiler_waiting,
330
                              _Bool physical_units_ready, _Bool stop_request,
331
                              int steam, int level_defect, int steam_defect,
332
                              int pump_defect_0, int pump_defect_1,
333
                              int pump_defect_2, int pump_defect_3,
334
                              int pump_control_defect_0,
335
                              int pump_control_defect_1,
336
                              int pump_control_defect_2,
337
                              int pump_control_defect_3, int q,
338
                              int pump_state_0, int pump_state_1,
339
                              int pump_state_2, int pump_state_3, 
340
                              int (*op_mode),
341
                              struct ControlMode_mem *self);
342

  
343
extern void REDGE_reset (struct REDGE_mem *self);
344

  
345
extern void REDGE_init (struct REDGE_mem *self);
346

  
347
extern void REDGE_clear (struct REDGE_mem *self);
348

  
349
extern void REDGE_step (_Bool S, 
350
                        _Bool (*REDGE),
351
                        struct REDGE_mem *self);
352

  
353
extern void steam_failure_detect_step (int steam, 
354
                                       _Bool (*steam_failure_detect)
355
                                       );
356

  
357
extern void operate_pumps_reset (struct operate_pumps_mem *self);
358

  
359
extern void operate_pumps_init (struct operate_pumps_mem *self);
360

  
361
extern void operate_pumps_clear (struct operate_pumps_mem *self);
362

  
363
extern void operate_pumps_step (int n, int n_pumps_to_open,
364
                                int pump_status_0, int pump_status_1,
365
                                int pump_status_2, int pump_status_3,
366
                                int pump_defect_0, int pump_defect_1,
367
                                int pump_defect_2, int pump_defect_3,
368
                                _Bool flow_0, _Bool flow_1, _Bool flow_2,
369
                                _Bool flow_3, 
370
                                int (*operate_pumps_0),
371
                                int (*operate_pumps_1),
372
                                int (*operate_pumps_2),
373
                                int (*operate_pumps_3),
374
                                struct operate_pumps_mem *self);
375

  
376
extern void pump_failure_detect_step (int pump_status, int pump_state,
377
                                      _Bool pump_control_state, 
378
                                      _Bool (*pump_failure_detect),
379
                                      _Bool (*pump_control_failure_detect),
380
                                      _Bool (*flow)
381
                                      );
382

  
383
extern void level_failure_detect_step (int level, 
384
                                       _Bool (*level_failure_detect)
385
                                       );
386

  
387
extern void Defect_step (int statein, _Bool fail_cond, _Bool ack_chan,
388
                         _Bool repair_chan, 
389
                         int (*stateout)
390
                         );
391

  
392
extern void sum_step (int a_0, int a_1, int a_2, int a_3, 
393
                      int (*sum)
394
                      );
395

  
396
extern void initialization_complete_step (int op_mode, int level,
397
                                          _Bool valve, 
398
                                          _Bool (*initialization_complete)
399
                                          );
400

  
401
extern void failure_step (int level_defect, int steam_defect,
402
                          int pump_defect_0, int pump_defect_1,
403
                          int pump_defect_2, int pump_defect_3,
404
                          int pump_control_defect_0,
405
                          int pump_control_defect_1,
406
                          int pump_control_defect_2,
407
                          int pump_control_defect_3, 
408
                          _Bool (*failure)
409
                          );
410

  
411
extern void critical_failure_step (int op_mode, int steam, int level_defect,
412
                                   int steam_defect, int pump_defect_0,
413
                                   int pump_defect_1, int pump_defect_2,
414
                                   int pump_defect_3, int q,
415
                                   int pump_state_0, int pump_state_1,
416
                                   int pump_state_2, int pump_state_3, 
417
                                   _Bool (*critical_failure)
418
                                   );
419

  
420
extern void pump_control_failure_step (int pump_defect, 
421
                                       _Bool (*pump_failure)
422
                                       );
423

  
424
extern void OR_step (_Bool a_0, _Bool a_1, _Bool a_2, _Bool a_3, 
425
                     _Bool (*OR)
426
                     );
427

  
428
extern void transmission_failure_step (int pump_state_0, int pump_state_1,
429
                                       int pump_state_2, int pump_state_3, 
430
                                       _Bool (*transmission_failure)
431
                                       );
432

  
433
extern void steam_failure_startup_step (int steam, 
434
                                        _Bool (*steam_failure_startup)
435
                                        );
436

  
437
extern void steam_failure_step (int steam_defect, 
438
                                _Bool (*steam_failure)
439
                                );
440

  
441
extern void pump_failure_step (int pump_defect, 
442
                               _Bool (*pump_failure)
443
                               );
444

  
445
extern void level_failure_step (int level_defect, 
446
                                _Bool (*level_failure)
447
                                );
448

  
449
extern void dangerous_level_step (int q, 
450
                                  _Bool (*dangerous_level)
451
                                  );
452

  
453
extern void AND_step (_Bool a_0, _Bool a_1, _Bool a_2, _Bool a_3, 
454
                      _Bool (*AND)
455
                      );
456

  
457

  
458
#endif
459

  
regression_tests/lustre_files/success/kind_fmcad08/large/src/BROKEN/steam_boiler_no_arr1.lus
1
-- STEAM BOILER example
2
-- from The Steam Boiler Problem in Lustre
3
-- by Thierry Cattel and Gregory Duval
4

  
5

  
6

  
7

  
8
node REDGE(S:bool) returns(REDGE:bool); 
9
let 
10
  REDGE= S -> S and not(pre(S)); 
11
tel
12

  
13
 
14

  
15
node sum(a_0,a_1,a_2,a_3:int) returns(sum:int); 
16
let 
17
  sum = a_0 + a_1 + a_2 + a_3; 
18
tel
19

  
20
node AND(a_0,a_1,a_2,a_3:bool) returns(AND:bool); 
21
let 
22
  AND = a_0 and a_1 and a_2 and a_3;
23
tel
24

  
25
node OR(a_0,a_1,a_2,a_3:bool) returns(OR:bool); 
26
let 
27
  OR = a_0 or a_1 or a_2 or a_3;
28
tel
29
 
30

  
31
node NOT(a_0,a_1,a_2,a_3:bool) returns(NOT_0,NOT_1,NOT_2,NOT_3:bool); 
32
let 
33
  NOT_0 = not a_0;
34
  NOT_1 = not a_1;
35
  NOT_2 = not a_2;
36
  NOT_3 = not a_3;
37
tel
38

  
39
 
40

  
41
node FEDGE1(S:bool) returns(FEDGE1:bool); 
42
let 
43
  FEDGE1= not(S) -> not(S) and pre(S); 
44
tel
45

  
46
 
47

  
48
node FEDGE2(S:bool) returns(FEDGE2:bool); 
49
let 
50
  FEDGE2= REDGE(not(S)); 
51
tel
52

  
53
 
54

  
55
node Verification(S1,S2:bool) returns(property_ok:bool); 
56
var property1,property2:bool; 
57
let 
58
  property1=FEDGE1(S1)=FEDGE2(S1); 
59

  
60
--assert(S2=not(S1)); 
61
  property2= FEDGE1(S1)=REDGE(S2); 
62

  
63
  property_ok=
64
if S2=not(S1) then
65
property1 and property2
66
 else true
67
; 
68
tel
69

  
70
 
71
node Operator(stop:bool) returns (stop_request:bool); 
72
var nb_stops:int; 
73
let 
74
  nb_stops = (if stop then 1 else 0) -> 
75
    if stop then pre(nb_stops)+1 else 0; 
76
  stop_request = (nb_stops>=3); 
77
tel
78

  
79
 
80

  
81
node Defect(statein:int; fail_cond,ack_chan,repair_chan:bool) 
82
  returns(stateout:int); 
83
let 
84
  stateout = if (statein=0) then 
85
    if fail_cond then 1 else 0 
86
    else 
87
      if (statein=1) then 
88
        if ack_chan then 2 else 1 
89
      else --statein=2 
90
        if repair_chan then 0 else 2; 
91
tel
92

  
93
 
94
node level_failure_detect(level:int) returns(level_failure_detect:bool); 
95
let 
96
  level_failure_detect = ((level < 0) or (level > 1000)); 
97
tel
98

  
99
node steam_failure_detect(steam:int) returns(steam_failure_detect:bool); 
100
let 
101
  steam_failure_detect = ((steam < 0) or (steam > 25)); 
102
tel
103

  
104
node LevelDefect(level_failure_acknowledgement,level_repaired:bool; 
105
  level:int) 
106
  returns( LevelDefect:int); 
107
let 
108
  LevelDefect = 0 -> 
109
    Defect(pre(LevelDefect), level_failure_detect(level), level_failure_acknowledgement, level_repaired); 
110
tel
111

  
112

  
113
node SteamDefect(steam_failure_acknowledgement,steam_repaired:bool; 
114
  steam:int) 
115
  returns( SteamDefect:int); 
116
let 
117
  SteamDefect = 0 -> 
118
    Defect(pre(SteamDefect), steam_failure_detect(steam), steam_failure_acknowledgement, steam_repaired); 
119
tel
120

  
121
 
122
node pump_failure_detect(pump_status,pump_state:int; 
123
  pump_control_state:bool) 
124
  returns(pump_failure_detect,pump_control_failure_detect,flow:bool); 
125
let 
126
  pump_failure_detect = ((pump_status=0) and pump_state=1) 
127
    or (((pump_status=1) or (pump_status=2))and pump_state=0); 
128
  pump_control_failure_detect = (((pump_status=0) or 
129
    (pump_status=2)) and pump_state=0 and pump_control_state) 
130
    or ((pump_status=1) and pump_state=1 and not(pump_control_state)) 
131
    or ((pump_status=2) and pump_state=1 and pump_control_state); 
132
  flow = ((pump_status=0) and pump_state=1 and pump_control_state) 
133
    or ((pump_status=1) and pump_state=0 and pump_control_state) 
134
    or ((pump_status=1) and pump_state=1); 
135
tel
136

  
137

  
138
 
139

  
140
node PumpDefect( 
141
  pump_failure_acknowledgement,pump_repaired, 
142
  pump_control_failure_acknowledgement,pump_control_repaired:bool; 
143
  pump_status,pump_state:int; 
144
  pump_control_state:bool) 
145
  returns(PumpDefect,PumpControlDefect:int;Flow:bool); 
146
var 
147
  pump_failure_d, pump_control_failure_d:bool; 
148
let 
149
  (pump_failure_d, pump_control_failure_d, Flow) = pump_failure_detect(pump_status, pump_state, pump_control_state); 
150
  PumpDefect = 0 -> 
151
    Defect(pre(PumpDefect), pump_failure_d, pump_failure_acknowledgement, pump_repaired); 
152
  PumpControlDefect = 0 -> 
153
    Defect(pre(PumpControlDefect), pump_control_failure_d, pump_control_failure_acknowledgement, pump_control_repaired); 
154
tel
155

  
156

  
157
node level_failure(level_defect:int) returns(level_failure:bool); 
158
let 
159
  level_failure = (level_defect<>0); 
160
tel
161
 
162
node steam_failure(steam_defect:int) returns(steam_failure:bool); 
163
let 
164
  steam_failure = (steam_defect<>0); 
165
tel
166

  
167
node pump_failure(pump_defect:int) returns(pump_failure:bool); 
168
let 
169
  pump_failure = (pump_defect<>0); 
170
tel
171

  
172
node pump_control_failure(pump_defect:int) returns(pump_failure:bool); 
173
let 
174
  pump_failure = (pump_defect<>0); 
175
tel
176
 
177

  
178
node Dynamics(valve_state,level,steam,level_defect,steam_defect:int; 
179
  flow_0,flow_1,flow_2,flow_3:bool) 
180
  returns (q,v:int; p_0,p_1,p_2,p_3:int); 
181
let 
182
  q = level-> 
183
    if level_failure(level_defect) then 
184
      pre(q) - steam*5 + sum(p_0,p_1,p_2,p_3)*5 - (if valve_state=1 then 10*5 else 0) 
185
    else 
186
      level; 
187
  v = steam-> 
188
    if steam_failure(steam_defect) then 
189
      (pre(q) -q) div 5 + sum(p_0,p_1,p_2,p_3)*5 
190
    else 
191
      steam; 
192
  p_0 = 0-> 
193
    if (not(flow_0)) then 
194
      0 
195
    else 
196
      15; 
197
  p_1 = 0-> 
198
    if (not(flow_1)) then 
199
      0 
200
    else 
201
      15; 
202
  p_2 = 0-> 
203
    if (not(flow_2)) then 
204
      0 
205
    else 
206
      15; 
207
  p_3 = 0-> 
208
    if (not(flow_3)) then 
209
      0 
210
    else 
211
      15; 
212
      
213
tel
214

  
215
 
216

  
217
node PumpsDecision(q,v:int) returns (n_pumps:int); 
218
let 
219
  n_pumps = if q>600 then 
220
      (v div 15) 
221
    else 
222
      if q<400 then 
223
        (v div 15) +1 
224
      else 
225
        pre(n_pumps) ; 
226
tel
227

  
228
 
229

  
230
node operate_pumps( n, n_pumps_to_open:int; 
231
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
232
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
233
  flow_0,flow_1,flow_2,flow_3:bool) 
234
  returns(operate_pumps_0,operate_pumps_1,operate_pumps_2,operate_pumps_3:int); 
235
let 
236
  operate_pumps_0 =  
237
      if ((n_pumps_to_open>0) and 
238
        not(flow_0) and 
239
        not(pump_failure(pump_defect_0)) and 
240
        (pump_status_0=0)) then 
241
        2 
242
      else 
243
        if ((n_pumps_to_open<0) and 
244
          flow_0 and 
245
          not(pump_failure(pump_defect_0)) and 
246
          (pump_status_0=1)) then 
247
          0 
248
        else 
249
          if (pump_status_0=2) then 
250
            1 
251
          else 
252
            if (pre(pump_defect_0)=2 and 
253
              pump_defect_0=0) then 
254
              if pump_status_0=1 then 
255
                0 
256
              else --necessarily 0 
257
                1 
258
            else 
259
              pump_status_0; 
260

  
261
  operate_pumps_1 =  
262
      if ((n_pumps_to_open>0) and 
263
        not(flow_1) and 
264
        not(pump_failure(pump_defect_1)) and 
265
        (pump_status_1=0)) then 
266
        2 
267
      else 
268
        if ((n_pumps_to_open<0) and 
269
          flow_1 and 
270
          not(pump_failure(pump_defect_1)) and 
271
          (pump_status_1=1)) then 
272
          0 
273
        else 
274
          if (pump_status_1=2) then 
275
            1 
276
          else 
277
            if (pre(pump_defect_1)=2 and 
278
              pump_defect_1=0) then 
279
              if pump_status_1=1 then 
280
                0 
281
              else --necessarily 0 
282
                1 
283
            else 
284
              pump_status_1; 
285

  
286
  operate_pumps_2 =  
287
      if ((n_pumps_to_open>0) and 
288
        not(flow_2) and 
289
        not(pump_failure(pump_defect_2)) and 
290
        (pump_status_2=0)) then 
291
        2 
292
      else 
293
        if ((n_pumps_to_open<0) and 
294
          flow_2 and 
295
          not(pump_failure(pump_defect_2)) and 
296
          (pump_status_2=1)) then 
297
          0 
298
        else 
299
          if (pump_status_2=2) then 
300
            1 
301
          else 
302
            if (pre(pump_defect_2)=2 and 
303
              pump_defect_2=0) then 
304
              if pump_status_2=1 then 
305
                0 
306
              else --necessarily 0 
307
                1 
308
            else 
309
              pump_status_2; 
310

  
311
  operate_pumps_3 =  
312
      if ((n_pumps_to_open>0) and 
313
        not(flow_3) and 
314
        not(pump_failure(pump_defect_3)) and 
315
        (pump_status_3=0)) then 
316
        2 
317
      else 
318
        if ((n_pumps_to_open<0) and 
319
          flow_3 and 
320
          not(pump_failure(pump_defect_3)) and 
321
          (pump_status_3=1)) then 
322
          0 
323
        else 
324
          if (pump_status_3=2) then 
325
            1 
326
          else 
327
            if (pre(pump_defect_3)=2 and 
328
              pump_defect_3=0) then 
329
              if pump_status_3=1 then 
330
                0 
331
              else --necessarily 0 
332
                1 
333
            else 
334
              pump_status_3; 
335

  
336
tel
337

  
338

  
339
node PumpsStatus( 
340
  n_pumps:int; 
341
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
342
  flow_0,flow_1,flow_2,flow_3:bool) 
343
  returns(pump_status_0,pump_status_1,pump_status_2,pump_status_3:int); 
344
var 
345
  n_pumps_flow,n_pumps_to_open:int; 
346
  t0,t1,t2,t3:int;
347
let 
348
  n_pumps_flow = (if flow_0 then 1 else 0) + (if flow_1 then 1 else 0) + 
349
    (if flow_2 then 1 else 0) + (if flow_3 then 1 else 0); 
350
  n_pumps_to_open = n_pumps-n_pumps_flow; 
351
  
352
  pump_status_0 = 0 ->t0;
353
  pump_status_1 = 0 ->t1;
354
  pump_status_2 = 0 ->t2;
355
  pump_status_3 = 0 ->t3;
356
  
357
  (t0,t1,t2,t3) =
358
    operate_pumps(4, n_pumps_to_open, 
359
      pre(pump_status_0),pre(pump_status_1),pre(pump_status_2),pre(pump_status_3), 
360
      pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, 
361
      flow_0,flow_1,flow_2,flow_3); 
362
tel
363

  
364
node transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
365
  returns(transmission_failure:bool); 
366
let 
367
  transmission_failure = pump_state_0=3 or pump_state_1=3 or pump_state_2=3 or pump_state_3=3; 
368
tel
369

  
370
node steam_failure_startup(steam:int) returns(steam_failure_startup:bool); 
371
let 
372
  steam_failure_startup=(steam<>0); 
373
tel
374

  
375
node dangerous_level(q:int) returns(dangerous_level:bool); 
376
let 
377
  dangerous_level = (q <= 150) or (q >= 850); 
378
tel
379

  
380
 
381

  
382
node critical_failure( 
383
  op_mode,steam,level_defect,steam_defect:int; 
384
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 
385
  q:int; 
386
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
387
  returns(critical_failure:bool); 
388
let 
389
  critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
390
    (op_mode=1 and steam_failure_startup(steam)) or 
391
    (op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 
392
    (op_mode=3 and dangerous_level(q)) or 
393
    (op_mode=4 and dangerous_level(q)) or 
394
    (op_mode=5 and (dangerous_level(q) or steam_failure(steam_defect) or AND(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)))); 
395
tel
396

  
397

  
398
node failure( 
399
  level_defect,steam_defect:int; 
400
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int) 
401
  returns(failure:bool); 
402
let 
403
  failure = level_failure(level_defect) or 
404
    steam_failure(steam_defect) or 
405
    OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or 
406
    OR(pump_control_failure(pump_control_defect_0),pump_control_failure(pump_control_defect_1),pump_control_failure(pump_control_defect_2),pump_control_failure(pump_control_defect_3)); 
407
tel
408

  
409
 
410

  
411
node ControlMode( 
412
  steam_boiler_waiting,physical_units_ready,stop_request:bool; 
413
  steam,level_defect,steam_defect:int; 
414
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 
415
  q:int; 
416
  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 
417
  returns(op_mode :int); 
418
let 
419
  op_mode= 1-> 
420
    if (critical_failure(pre(op_mode), 
421
      steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 
422
      stop_request or pre(op_mode)=6) then 
423
      6 
424
    else 
425
      if (pre(op_mode)=1) then 
426
        if steam_boiler_waiting then 2 else 1 
427
      else 
428
        if (pre(op_mode)=2 and not physical_units_ready) then 
429
          2 
430
        else 
431
          if level_failure(level_defect) then 
432
            5 
433
          else 
434
            if failure(level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3) then 
435
              4 
436
            else 
437
              3; 
438
tel
439

  
440
 
441

  
442
 
443

  
444
 
445
 
446

  
447
 
448

  
449
node Valve(op_mode:int;q:int) returns (valve:bool;valve_state:int); 
450
let 
451
  valve_state=0-> 
452
    if (op_mode=2) then 
453
      if (q>600) then 
454
        1 
455
      else 
456
        if (q<=600) then 0 else pre(valve_state) 
457
    else 
458
      pre(valve_state); 
459
  valve =false-> 
460
    (valve_state<>pre(valve_state)); 
461
tel
462

  
463
 
464
node initialization_complete(op_mode,level:int;valve:bool) 
465
  returns(initialization_complete:bool); 
466
let 
467
  initialization_complete =(op_mode=2) and 
468
    ((400<=level) and (level<=600))and 
469
    not(valve); 
470
tel
471

  
472

  
473
node ControlOutput(op_mode,level:int;valve:bool) 
474
  returns(program_ready:bool;mode:int); 
475
let 
476
  program_ready=initialization_complete(op_mode,level,valve); 
477
  mode =op_mode; 
478
tel
479

  
480
 
481

  
482
 
483

  
484
node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool) 
485
  returns (steam_outcome_failure_detection, 
486
steam_outcome_repaired_acknowledgement : bool); 
487
let 
488
  steam_outcome_failure_detection= 
489
    not ((op_mode=6) or (op_mode=1)) and 
490
    (steam_defect=1); 
491
  steam_outcome_repaired_acknowledgement = 
492
    not ((op_mode=6) or (op_mode=1)) and 
493
    steam_repaired; 
494
tel
495

  
496
node LevelOutput(op_mode,level_defect:int; level_repaired:bool) 
497
  returns (level_outcome_failure_detection, 
498
level_outcome_repaired_acknowledgement : bool); 
499
let 
500
  level_outcome_failure_detection= 
501
    not ((op_mode=6) or (op_mode=1)) and 
502
    (level_defect=1); 
503
  level_outcome_repaired_acknowledgement = 
504
    not ((op_mode=6) or (op_mode=1)) and 
505
    level_repaired; 
506
tel
507

  
508
 
509

  
510
node PumpsOutput(op_mode:int; 
511
  pump_status_0,pump_status_1,pump_status_2,pump_status_3,
512
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,
513
  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 
514
  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,
515
  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3:bool) 
516
  
517
  returns (open_pump_0,open_pump_1,open_pump_2,open_pump_3,
518
  close_pump_0,close_pump_1,close_pump_2,close_pump_3,
519
  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3, 
520
  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,
521
  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3, 
522
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool); 
523
let 
524
  open_pump_0 = 
525
     op_mode<>6 and op_mode<>1 and pump_status_0=2;
526
  open_pump_1 = 
527
     op_mode<>6 and op_mode<>1 and pump_status_1=2;
528
  open_pump_2 = 
529
     op_mode<>6 and op_mode<>1 and pump_status_2=2;
530
  open_pump_3 = 
531
     op_mode<>6 and op_mode<>1 and pump_status_3=2; 
532
    
533
  close_pump_0 = 
534
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_0)<>0 and pump_defect_0=0 and pre(pump_defect_0)=0;
535
  close_pump_1 = 
536
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_1)<>0 and pump_defect_0=0 and pre(pump_defect_1)=0;
537
  close_pump_2 = 
538
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_2)<>0 and pump_defect_0=0 and pre(pump_defect_2)=0;
539
  close_pump_3 = 
540
     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_3)<>0 and pump_defect_0=0 and pre(pump_defect_3)=0;
541
    
542
  pump_failure_detection_0 = 
543
    op_mode<>6 and op_mode<>1 and pump_defect_0=1;
544
  pump_failure_detection_1 = 
545
     op_mode<>6 and op_mode<>1 and pump_defect_1=1;
546
  pump_failure_detection_2 = 
547
     op_mode<>6 and op_mode<>1 and pump_defect_2=1;
548
  pump_failure_detection_3 = 
549
     op_mode<>6 and op_mode<>1 and pump_defect_3=1;
550
    
551
  pump_repaired_acknowledgement_0 = 
552
    op_mode<>6 and op_mode<>1 and pump_repaired_0;
553
  pump_repaired_acknowledgement_1 = 
554
     op_mode<>6 and op_mode<>1 and pump_repaired_1;
555
  pump_repaired_acknowledgement_2 = 
556
     op_mode<>6 and op_mode<>1 and pump_repaired_2;
557
  pump_repaired_acknowledgement_3 = 
558
     op_mode<>6 and op_mode<>1 and pump_repaired_3;
559
    
560
  pump_control_failure_detection_0 = 
561
    op_mode<>6 and op_mode<>1 and pump_control_defect_0=1;
562
  pump_control_failure_detection_1 = 
563
    op_mode<>6 and op_mode<>1 and pump_control_defect_1=1;
564
  pump_control_failure_detection_2 = 
565
    op_mode<>6 and op_mode<>1 and pump_control_defect_2=1;
566
  pump_control_failure_detection_3 = 
567
    op_mode<>6 and op_mode<>1 and pump_control_defect_3=1;
568
    
569
  pump_control_repaired_acknowledgement_0 = 
570
    op_mode<>6 and op_mode<>1 and pump_control_repaired_0;
571
  pump_control_repaired_acknowledgement_1 = 
572
    op_mode<>6 and op_mode<>1 and pump_control_repaired_1;
573
  pump_control_repaired_acknowledgement_2 = 
574
    op_mode<>6 and op_mode<>1 and pump_control_repaired_2;
575
  pump_control_repaired_acknowledgement_3 = 
576
    op_mode<>6 and op_mode<>1 and pump_control_repaired_3;
577
tel
578

  
579
 
580

  
581
node BoilerController( 
582
  stop, 
583
  steam_boiler_waiting, 
584
  physical_units_ready : bool; 
585
  level : int; 
586
  steam : int; 
587
  pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int; 
588
  pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool; 
589
  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool; 
590
  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool; 
591
  level_repaired : bool; 
592
  steam_repaired : bool; 
593
  pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool; 
594
  pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool; 
595
  level_failure_acknowledgement : bool; 
596
  steam_failure_acknowledgement : bool) 
597
  
598
  returns(
599
  program_ready : bool; 
600
  mode : int; 
601
  valve : bool; 
602
  open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool; 
603
  close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool; 
604
  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool; 
605
  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool; 
606
  level_failure_detection : bool; 
607
  steam_outcome_failure_detection : bool; 
608
  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool; 
609
  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool; 
610
  level_repaired_acknowledgement : bool; 
611
  steam_outcome_repaired_acknowledgement: bool); 
612
var 
613
  stop_request : bool; 
614
  op_mode : int; 
615
  q : int; 
616
  v : int; 
617
  p_0,p_1,p_2,p_3 : int; 
618
  valve_state : int; 
619
  n_pumps : int; 
620
  pump_status_0,pump_status_1,pump_status_2,pump_status_3 : int; 
621
  level_defect : int; 
622
  steam_defect : int; 
623
  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3 : int; 
624
  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3 : int; 
625
  flow_0,flow_1,flow_2,flow_3 : bool; 
626
  t00,t01,t10,t20,t30,t11,t21,t31:int;
627
  t02,t12,t22,t32,u4,u6:bool;
628
  t4,t5,t6,t7,t8,t9,u0,u1,u2,u3,u5,u7:int;
629
  a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24:bool;
630
  b0,b1,b2,b3:bool;
631
let 
632
  stop_request = Operator(stop); 
633

  
634
  level_defect = 0-> 
635
    LevelDefect(level_failure_acknowledgement, level_repaired, level); 
636

  
637
  steam_defect = 0-> 
638
    SteamDefect(steam_failure_acknowledgement, steam_repaired, steam); 
639

  
640
  pump_defect_0 = 0 -> t00;
641
  pump_control_defect_0 = 0 -> t01;
642
  flow_0 = false -> t02;
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff