Project

General

Profile

Revision 02d89bbb

View differences:

regression_tests/CMakeLists.txt
7 7
set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/modules)
8 8
include(./modules/Lustre_compile.cmake)
9 9
include(./modules/Zustre_compile.cmake)
10

  
10
include(./modules/helpfull_functions.cmake)
11 11

  
12 12
if(LUSTRE_COMPILER)
13 13
  message(STATUS "Found zustre: ${LUSTRE_COMPILER} ")
regression_tests/lustre_files/success/CMakeLists.txt
4 4
add_subdirectory(Simulink)
5 5
add_subdirectory(kind_fmcad08)
6 6
add_subdirectory(adrien)
7
add_subdirectory(automata)
regression_tests/lustre_files/success/adrien/CMakeLists.txt
112 112
			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
113 113
				DEPENDS adrien_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
114 114
	else()
115
		message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
115
		message(FATAL_ERROR "Unknown shell command ${BASH} -c for ${CMAKE_HOST_SYSTEM_NAME}")
116 116
	endif()
117 117

  
118 118
	 #************** execute C binary **********************************
regression_tests/lustre_files/success/automata/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2

  
3
add_subdirectory(with_properties)
4
add_subdirectory(without_properties)
5
add_custom_target(automata COMMAND ${CMAKE_CTEST_COMMAND} -R automata)
regression_tests/lustre_files/success/automata/CMakeLists.txt~
1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
3

  
4

  
5

  
6

  
7

  
8
#take all lustre files
9
set(GLOBAL_LUSTRE_FILES "")
10
LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
11
list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
12
FOREACH(lfile ${LFILES})
13
	get_filename_component(L ${lfile} NAME_WE)
14
	set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
15
	file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
16
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
17
		file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
18
	else()
19
		message("generate ${L}.lusi \n")
20
		Lustre_Compile(LUS_FILE ${lfile}
21
				NODE ""
22
				OPTS "-lusi")				
23
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
24
		execute_process(RESULT_VARIABLE res 
25
					COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
26
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
27
		if(${res} STREQUAL "0")
28
			file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
29
		else()
30
			message("${L}.lusi Error")
31
		endif()
32
	endif()
33
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_input_values)
34
		file(COPY  ${L}_input_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
35
	elseif(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
36
		message("generate input_values \n")
37
		execute_process(RESULT_VARIABLE res 
38
					COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ Generate_inputs_lusi ${L} ${L}.lusi 
39
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
40
		if(${res} STREQUAL "0")
41
			file(COPY  ${L}_input_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
42
		else()
43
			message("${L}_input_values Error")
44
		endif()
45
	endif()
46
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_output_values)
47
		file(COPY  ${L}_output_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
48
	elseif(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}_input_values)
49
		message("generate output_values for reference \n")
50
		set(LUSTRE_NODE_OPT  "${L}")
51
		
52
		Lustre_Compile(LUS_FILE ${lfile}
53
						NODE ${LUSTRE_NODE_OPT}
54
						OPTS ""
55
						DIR ${CMAKE_CURRENT_SOURCE_DIR})
56
						
57
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
58
		
59
		execute_process(
60
					COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
61
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})			
62
		execute_process(
63
					COMMAND  make -f ${L}.makefile
64
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})	
65
		execute_process(RESULT_VARIABLE res 
66
					COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ${L}_input_values > ${L}_output_values"
67
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})	
68
		file(REMOVE ${L}_${LUSTRE_NODE_OPT} io_frontend.o ${L}.c ${L}.h ${L}.lusic ${L}.makefile ${L}.o ${L}_alloc.h ${L}_main.c ${L}_main.o )
69
		if(${res} STREQUAL "0")
70
			file(COPY  ${L}_output_values DESTINATION  ${LUSTRE_OUTPUT_DIR})
71
		else()
72
			message("${L} output_values Error")
73
		endif()
74
	endif()
75
ENDFOREACH()
76

  
77
#first combination :no option
78
set(LUSTRE_OPTIONS_OPT "")
79
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
80
	get_filename_component(L ${lus_file} NAME_WE)
81
	set(LUSTRE_NODE_OPT  "${L}")
82
	
83
	# First command generate C files from Lustre file
84
	Lustre_Compile(LUS_FILE ${lus_file}
85
					NODE ${LUSTRE_NODE_OPT}
86
					OPTS ${LUSTRE_OPTIONS_OPT})
87
					
88
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
89
	add_test(NAME automata_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
90
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
91
	)
92

  
93
	 #********************* make -f ${L}.makefile ***************************
94
	 add_test(NAME automata_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
95
			COMMAND  make -f ${L}.makefile
96
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
97
	)
98
	SET_TESTS_PROPERTIES ( automata_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
99
	 PROPERTIES DEPENDS automata_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
100
				REQUIRED_FILES ${L}.makefile
101
				)
102
	 
103
	 #************** execute C binary **********************************
104
	
105
	if (BASH)
106
		add_test(
107
			NAME automata_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} 
108
			COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < ../${L}_input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
109
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
110
		)
111
		SET_TESTS_PROPERTIES ( automata_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
112
			PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
113
				DEPENDS automata_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
114
	else()
115
		message(FATAL_ERROR "Unknown shell command ${BASH} -c for ${CMAKE_HOST_SYSTEM_NAME}")
116
	endif()
117

  
118
	 #************** execute C binary **********************************
119
	 add_test(NAME automata_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
120
			COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ../${L}_output_values 
121
			WORKING_DIRECTORY ${LUSTRE_OUTPUT_DIR_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}}
122
	)
123
	SET_TESTS_PROPERTIES ( automata_DIFF_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
124
	 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
125
				DEPENDS automata_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
126
ENDFOREACH()
127

  
128
add_custom_target(automata COMMAND ${CMAKE_CTEST_COMMAND} -R automata)
129

  
regression_tests/lustre_files/success/automata/with_properties/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
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

  
12

  
13

  
14
#first combination :no option
15
set(ZUSTRE_OPTIONS_OPT "--timeout" "60" "--xml" )
16
#take all lustre files
17
set(GLOBAL_LUSTRE_FILES "")
18
LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
19
list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
20
FOREACH(lfile ${LFILES})
21
	get_filename_component(L ${lfile} NAME_WE)
22
	set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
23
	file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
24
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
25
	file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
26
	else()
27
	message("generate ${L}.lusi \n")
28
	Lustre_Compile(LUS_FILE ${lfile}
29
			NODE ""
30
			OPTS "-lusi")				
31
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
32
	execute_process(RESULT_VARIABLE res 
33
				COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
34
				WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
35
	if(${res} STREQUAL "0")
36
		file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
37
	else()
38
		message("${L}.lusi Error")
39
	endif()
40
	endif()
41
  
42
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml)
43
		file(COPY ${L}.xml   DESTINATION  ${LUSTRE_OUTPUT_DIR})
44
		file(READ ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${L}_zustre_output)		
45
	else()
46
		message("generate ${L}.xml for reference\n")
47
		Zustre_Compile(LUS_FILE ${lfile}
48
					NODE "top"
49
					OPTS ${ZUSTRE_OPTIONS_OPT})
50
		set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
51
		execute_process(RESULT_VARIABLE res 
52
					OUTPUT_VARIABLE ${L}_zustre_output
53
					COMMAND  ${ZUSTRE_COMPILER} ${ZUSTRE_ARGS_${L}_top_${ZUS_OPTS_CUT}} 
54
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
55
		
56
		file(WRITE ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${${L}_zustre_output})
57
		file(COPY ${L}.xml   DESTINATION  ${LUSTRE_OUTPUT_DIR})
58
		message("${${L}_zustre_output}")
59
	endif()
60
    if( ${${L}_zustre_output} MATCHES "<Answer>CEX</Answer>")
61
		#message("${L}.xml is CEX")
62
		set(ZUSTRE_ANSWER_${L} "CEX")
63
	elseif( ${${L}_zustre_output} MATCHES "<Answer>SAFE</Answer>")
64
		#message("${L}.xml is SAFE")
65
		set(ZUSTRE_ANSWER_${L} "SAFE")
66
	elseif( ${${L}_zustre_output} MATCHES "<Answer>TIMEOUT</Answer>")
67
		#message("${L}.xml is TIMEOUT")
68
		set(ZUSTRE_ANSWER_${L} "TIMEOUT")
69
	else()
70
		#message("${L}.xml is Error")
71
		set(ZUSTRE_ANSWER_${L} "ERROR")
72
	endif()
73
ENDFOREACH()
74

  
75

  
76

  
77

  
78
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
79
	get_filename_component(L ${lus_file} NAME_WE)
80
	set(ZUSTRE_NODE_OPT  "top")
81

  
82
	Lustre_Compile(LUS_FILE ${lus_file}
83
					NODE ""
84
					OPTS "-horn")
85
					
86
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
87
	add_test(NAME automata_with_properties_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT}
88
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
89
	)
90

  
91
	Zustre_Compile(LUS_FILE ${lus_file}
92
					NODE ${ZUSTRE_NODE_OPT}
93
					OPTS ${ZUSTRE_OPTIONS_OPT})
94
	set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
95
	set(ZUSTRE_OUTPUT_DIR ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}})
96
	
97
	set(ZUSTRE_ARGS_TEMP "${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}" "> ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml")
98
    JOIN("${ZUSTRE_ARGS_TEMP}" " " ZUSTRE_ARGS)
99
    
100
	add_test(NAME automata_with_properties_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
101
			COMMAND bash -c "${ZUSTRE_COMPILER} ${ZUSTRE_ARGS}"
102
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
103
	)
104
	SET_TESTS_PROPERTIES (  automata_with_properties_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
105
			PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
106
					DEPENDS automata_with_properties_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT})
107
			
108
			
109
	add_test(NAME automata_with_properties_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
110
			COMMAND bash -c "tail -n +8 ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml > ${L}_tailed1.xml"
111
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
112
			#DEPENDS automata_with_properties_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
113
	)
114
	SET_TESTS_PROPERTIES ( automata_with_properties_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
115
	 PROPERTIES REQUIRED_FILES  ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
116
				DEPENDS automata_with_properties_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
117
	
118
	add_test(NAME automata_with_properties_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
119
			COMMAND bash -c "tail -n +8 ${L}.xml > ${L}_tailed2.xml"
120
			WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${L}/
121
	)
122
	SET_TESTS_PROPERTIES ( automata_with_properties_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
123
	 PROPERTIES REQUIRED_FILES  ${L}.xml
124
				DEPENDS automata_with_properties_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
125
				
126
				
127
	add_test(NAME automata_with_properties_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
128
			COMMAND ${CMAKE_COMMAND} -E compare_files  ${L}_tailed1.xml  ../${L}_tailed2.xml
129
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
130
	)
131
	SET_TESTS_PROPERTIES ( automata_with_properties_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
132
	 PROPERTIES REQUIRED_FILES  ${L}_tailed1.xml
133
				DEPENDS automata_with_properties_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})	
134

  
135
	
136
	if(EXISTS ${CMAKE_BINARY_DIR}/modules/XPathParser_lusi.class AND ${ZUSTRE_ANSWER_${L}} STREQUAL "CEX" AND EXISTS ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi)
137
	    #message("add tests for comaring Zustre and lustrec in memory")
138
		add_test(NAME automata_with_properties_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
139
			COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ XPathParser_lusi ${ZUSTRE_NODE_OPT} ../${L}.lusi ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
140
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
141
		)
142
		SET_TESTS_PROPERTIES ( automata_with_properties_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
143
		 PROPERTIES REQUIRED_FILES  ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi 
144
					DEPENDS automata_with_properties_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT} )	
145
		
146
		set(LUSTRE_NODE_OPT "top")
147
		# First command generate C files from Lustre file
148
		Lustre_Compile(LUS_FILE ${lus_file}
149
						NODE ${LUSTRE_NODE_OPT}
150
						OPTS ""
151
						DIR ${ZUSTRE_OUTPUT_DIR})
152
						
153
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
154
		add_test(NAME automata_with_properties_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
155
				COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
156
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
157
		)
158

  
159
		 #********************* make -f ${L}.makefile ***************************
160
		 add_test(NAME automata_with_properties_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
161
				COMMAND  make -f ${L}.makefile
162
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
163
		)
164
		SET_TESTS_PROPERTIES ( automata_with_properties_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
165
		 PROPERTIES DEPENDS automata_with_properties_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
166
					REQUIRED_FILES ${L}.makefile
167
					)
168
		 
169
		 #************** execute C binary **********************************
170
		
171
		if (BASH)
172
			add_test(
173
				NAME automata_with_properties_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} 
174
				COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
175
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
176
			)
177
			SET_TESTS_PROPERTIES ( automata_with_properties_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
178
				PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
179
					DEPENDS automata_with_properties_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
180
		else()
181
			message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
182
		endif()
183

  
184
		 #************** execute C binary **********************************
185
		 add_test(NAME automata_with_properties_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
186
				COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ZUSTRE_output_values
187
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
188
		)
189
		SET_TESTS_PROPERTIES ( automata_with_properties_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
190
		 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
191
					DEPENDS automata_with_properties_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
192
					
193
					
194

  
195
	endif()
196
	
197
ENDFOREACH()
198
add_custom_target(automata_with_properties COMMAND ${CMAKE_CTEST_COMMAND} -R automata_with_properties)
regression_tests/lustre_files/success/automata/with_properties/CMakeLists.txt~
1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
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

  
12

  
13

  
14
#first combination :no option
15
set(ZUSTRE_OPTIONS_OPT "--timeout" "60" "--xml" )
16
#take all lustre files
17
set(GLOBAL_LUSTRE_FILES "")
18
LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
19
list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
20
FOREACH(lfile ${LFILES})
21
	get_filename_component(L ${lfile} NAME_WE)
22
	set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
23
	file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
24
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
25
	file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
26
	else()
27
	message("generate ${L}.lusi \n")
28
	Lustre_Compile(LUS_FILE ${lfile}
29
			NODE ""
30
			OPTS "-lusi")				
31
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
32
	execute_process(RESULT_VARIABLE res 
33
				COMMAND ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
34
				WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
35
	if(${res} STREQUAL "0")
36
		file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
37
	else()
38
		message("${L}.lusi Error")
39
	endif()
40
	endif()
41
  
42
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml)
43
		file(COPY ${L}.xml   DESTINATION  ${LUSTRE_OUTPUT_DIR})
44
		file(READ ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${L}_zustre_output)		
45
	else()
46
		message("generate ${L}.xml for reference\n")
47
		Zustre_Compile(LUS_FILE ${lfile}
48
					NODE "top"
49
					OPTS ${ZUSTRE_OPTIONS_OPT})
50
		set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
51
		execute_process(RESULT_VARIABLE res 
52
					OUTPUT_VARIABLE ${L}_zustre_output
53
					COMMAND  ${ZUSTRE_COMPILER} ${ZUSTRE_ARGS_${L}_top_${ZUS_OPTS_CUT}} 
54
					WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR})
55
		
56
		file(WRITE ${CMAKE_CURRENT_SOURCE_DIR}/${L}.xml ${${L}_zustre_output})
57
		file(COPY ${L}.xml   DESTINATION  ${LUSTRE_OUTPUT_DIR})
58
		message("${${L}_zustre_output}")
59
	endif()
60
    if( ${${L}_zustre_output} MATCHES "<Answer>CEX</Answer>")
61
		#message("${L}.xml is CEX")
62
		set(ZUSTRE_ANSWER_${L} "CEX")
63
	elseif( ${${L}_zustre_output} MATCHES "<Answer>SAFE</Answer>")
64
		#message("${L}.xml is SAFE")
65
		set(ZUSTRE_ANSWER_${L} "SAFE")
66
	elseif( ${${L}_zustre_output} MATCHES "<Answer>TIMEOUT</Answer>")
67
		#message("${L}.xml is TIMEOUT")
68
		set(ZUSTRE_ANSWER_${L} "TIMEOUT")
69
	else()
70
		#message("${L}.xml is Error")
71
		set(ZUSTRE_ANSWER_${L} "ERROR")
72
	endif()
73
ENDFOREACH()
74

  
75

  
76

  
77

  
78
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
79
	get_filename_component(L ${lus_file} NAME_WE)
80
	set(ZUSTRE_NODE_OPT  "top")
81

  
82
	Lustre_Compile(LUS_FILE ${lus_file}
83
					NODE ""
84
					OPTS "-horn")
85
					
86
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
87
	add_test(NAME Kind_fmcad08_misc_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT}
88
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
89
	)
90

  
91
	Zustre_Compile(LUS_FILE ${lus_file}
92
					NODE ${ZUSTRE_NODE_OPT}
93
					OPTS ${ZUSTRE_OPTIONS_OPT})
94
	set(ZUS_OPTS_CUT ${ZUSTRE_OPTS_POSTFIX_${L}})
95
	set(ZUSTRE_OUTPUT_DIR ${ZUSTRE_OUTPUT_DIR_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}})
96
	
97
	set(ZUSTRE_ARGS_TEMP "${ZUSTRE_ARGS_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}}" "> ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml")
98
    JOIN("${ZUSTRE_ARGS_TEMP}" " " ZUSTRE_ARGS)
99
    
100
	add_test(NAME Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
101
			COMMAND bash -c "${ZUSTRE_COMPILER} ${ZUSTRE_ARGS}"
102
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
103
	)
104
	SET_TESTS_PROPERTIES (  Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
105
			PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
106
					DEPENDS Kind_fmcad08_misc_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT})
107
			
108
			
109
	add_test(NAME Kind_fmcad08_misc_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
110
			COMMAND bash -c "tail -n +8 ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml > ${L}_tailed1.xml"
111
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
112
			#DEPENDS Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
113
	)
114
	SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
115
	 PROPERTIES REQUIRED_FILES  ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
116
				DEPENDS Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
117
	
118
	add_test(NAME Kind_fmcad08_misc_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
119
			COMMAND bash -c "tail -n +8 ${L}.xml > ${L}_tailed2.xml"
120
			WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${L}/
121
	)
122
	SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
123
	 PROPERTIES REQUIRED_FILES  ${L}.xml
124
				DEPENDS Kind_fmcad08_misc_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
125
				
126
				
127
	add_test(NAME Kind_fmcad08_misc_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
128
			COMMAND ${CMAKE_COMMAND} -E compare_files  ${L}_tailed1.xml  ../${L}_tailed2.xml
129
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
130
	)
131
	SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_DIFF_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
132
	 PROPERTIES REQUIRED_FILES  ${L}_tailed1.xml
133
				DEPENDS Kind_fmcad08_misc_TAIL2_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})	
134

  
135
	
136
	if(EXISTS ${CMAKE_BINARY_DIR}/modules/XPathParser_lusi.class AND ${ZUSTRE_ANSWER_${L}} STREQUAL "CEX" AND EXISTS ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi)
137
	    #message("add tests for comaring Zustre and lustrec in memory")
138
		add_test(NAME Kind_fmcad08_misc_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
139
			COMMAND ${JAVA_RUNTIME} -cp ${CMAKE_BINARY_DIR}/modules/ XPathParser_lusi ${ZUSTRE_NODE_OPT} ../${L}.lusi ${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}.xml
140
			WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
141
		)
142
		SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_XPathParser_lusi_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
143
		 PROPERTIES REQUIRED_FILES  ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi 
144
					DEPENDS Kind_fmcad08_misc_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT} )	
145
		
146
		set(LUSTRE_NODE_OPT "top")
147
		# First command generate C files from Lustre file
148
		Lustre_Compile(LUS_FILE ${lus_file}
149
						NODE ${LUSTRE_NODE_OPT}
150
						OPTS ""
151
						DIR ${ZUSTRE_OUTPUT_DIR})
152
						
153
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
154
		add_test(NAME Kind_fmcad08_misc_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
155
				COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
156
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
157
		)
158

  
159
		 #********************* make -f ${L}.makefile ***************************
160
		 add_test(NAME Kind_fmcad08_misc_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
161
				COMMAND  make -f ${L}.makefile
162
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
163
		)
164
		SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
165
		 PROPERTIES DEPENDS Kind_fmcad08_misc_COMPIL_LUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
166
					REQUIRED_FILES ${L}.makefile
167
					)
168
		 
169
		 #************** execute C binary **********************************
170
		
171
		if (BASH)
172
			add_test(
173
				NAME Kind_fmcad08_misc_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} 
174
				COMMAND ${BASH} -c "./${L}_${LUSTRE_NODE_OPT} < input_values > ${L}_${LUSTRE_NODE_OPT}_outputs"
175
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
176
			)
177
			SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
178
				PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}
179
					DEPENDS Kind_fmcad08_misc_MAKE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT})
180
		else()
181
			message(FATAL_ERROR "Unknown shell command for ${CMAKE_HOST_SYSTEM_NAME}")
182
		endif()
183

  
184
		 #************** execute C binary **********************************
185
		 add_test(NAME Kind_fmcad08_misc_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
186
				COMMAND ${CMAKE_COMMAND} -E compare_files ${L}_${LUSTRE_NODE_OPT}_outputs ZUSTRE_output_values
187
				WORKING_DIRECTORY ${ZUSTRE_OUTPUT_DIR}
188
		)
189
		SET_TESTS_PROPERTIES ( Kind_fmcad08_misc_COMPARE_OUTPUTS_OF_LUSTREC_ZUSTRE_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}
190
		 PROPERTIES REQUIRED_FILES ${L}_${LUSTRE_NODE_OPT}_outputs
191
					DEPENDS Kind_fmcad08_misc_BIN_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT} )
192
					
193
					
194

  
195
	endif()
196
	
197
ENDFOREACH()
198
add_custom_target(Kind_fmcad08_misc COMMAND ${CMAKE_CTEST_COMMAND} -R Kind_fmcad08_misc)
regression_tests/lustre_files/success/automata/with_properties/aut1.lus
1

  
2
node top (x :int) returns (y:bool) 
3
var l:int;
4
let
5
 automaton parity
6
 state Even :
7
 unless (x mod 2 = 1) restart Odd
8
 let
9
   l = x -> pre (l/2);
10
 tel
11
 state Odd  :
12
 unless (x mod 2 = 0) restart Even
13
 let
14
  l = x -> pre (3*l + 1);
15
 tel
16
 y = (l = 1);
17
tel
regression_tests/lustre_files/success/automata/with_properties/aut1.lusi
1
(* Generated Lustre Interface file from aut1.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:29 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type parity__type = enum {Even, Odd }; 
6

  
7
node parity__Even_handler_until (parity__restart_act: bool; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
8

  
9
function parity__Even_unless (parity__restart_in: bool; x: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
10

  
11
node parity__Odd_handler_until (parity__restart_act: bool; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
12

  
13
function parity__Odd_unless (parity__restart_in: bool; x: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
14

  
15
node top (x: int) returns (y: bool);
16

  
regression_tests/lustre_files/success/automata/with_properties/aut1.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-21 13:58</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.09</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="parity__Even_unless">
11
            <Stream name="parity__Even_unless.parity__restart_act" type="unk">
12
                <Value instant="0">1</Value>
13
           </Stream>
14
            <Stream name="parity__Even_unless.parity__state_act" type="unk">
15
                <Value instant="0">Even</Value>
16
           </Stream>
17
            <Stream name="parity__Even_unless.parity__restart_in" type="unk">
18
                <Value instant="0">1</Value>
19
           </Stream>
20
            <Stream name="parity__Even_unless.x" type="unk">
21
                <Value instant="0">0</Value>
22
           </Stream>
23
         </Node>
24
 <Node name ="top">
25
            <Stream name="top.__top_13_x" type="unk">
26
                <Value instant="0">Even</Value>
27
           </Stream>
28
            <Stream name="top.__top_13_x" type="unk">
29
                <Value instant="0">Even</Value>
30
           </Stream>
31
            <Stream name="top.__top_12_x" type="unk">
32
                <Value instant="0">1</Value>
33
           </Stream>
34
            <Stream name="top.ni_1.parity__Odd_handler_until.__parity__Odd_handler_until_2_c" type="unk">
35
                <Value instant="0">5</Value>
36
           </Stream>
37
            <Stream name="top.ni_0.parity__Even_handler_until.__parity__Even_handler_until_2_x" type="unk">
38
                <Value instant="0">0</Value>
39
           </Stream>
40
            <Stream name="top.ni_1.parity__Odd_handler_until.__parity__Odd_handler_until_2_x" type="unk">
41
                <Value instant="0">0</Value>
42
           </Stream>
43
            <Stream name="top.__top_12_c" type="unk">
44
                <Value instant="0">1</Value>
45
           </Stream>
46
            <Stream name="y" type="bool">
47
                <Value instant="0">1</Value>
48
           </Stream>
49
            <Stream name="x" type="int">
50
                <Value instant="0">0</Value>
51
           </Stream>
52
            <Stream name="top.__top_13_c" type="unk">
53
                <Value instant="0">Even</Value>
54
           </Stream>
55
         </Node>
56
 <Node name ="parity__Even_handler_until">
57
            <Stream name="parity__Even_handler_until.l_out" type="unk">
58
                <Value instant="0">0</Value>
59
           </Stream>
60
            <Stream name="parity__Even_handler_until.parity__restart_in" type="unk">
61
                <Value instant="0">1</Value>
62
           </Stream>
63
            <Stream name="parity__Even_handler_until.__parity__Even_handler_until_2_x" type="unk">
64
                <Value instant="0">0</Value>
65
           </Stream>
66
            <Stream name="parity__Even_handler_until.parity__state_in" type="unk">
67
                <Value instant="0">Even</Value>
68
           </Stream>
69
            <Stream name="parity__Even_handler_until.x" type="unk">
70
                <Value instant="0">0</Value>
71
           </Stream>
72
            <Stream name="parity__Even_handler_until.__parity__Even_handler_until_2_c" type="unk">
73
                <Value instant="0">6</Value>
74
           </Stream>
75
            <Stream name="parity__Even_handler_until.parity__restart_act" type="unk">
76
                <Value instant="0">1</Value>
77
           </Stream>
78
         </Node>
79

  
80
      </Counterexample>
81
     </Property>
82
   </Results>
83

  
regression_tests/lustre_files/success/automata/with_properties/aut2.lus
1
  type parity__type = enum {Even, Odd };
2
  
3
  
4
  function parity__Odd_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type)
5
var __parity__Odd_unless_1: bool;
6
let
7
    
8
    parity__restart_act, parity__state_act = (if __parity__Odd_unless_1 then (true,Even) else (parity__restart_in,parity__state_in));
9
    __parity__Odd_unless_1 = ((l mod 2) = 0);
10
     
11
tel
12
 
13
node parity__Odd_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int)
14
var __parity__Odd_handler_until_2: int;
15
    __parity__Odd_handler_until_1: bool;
16
    l: int;
17
let
18
    
19
    parity__restart_in, parity__state_in = (parity__restart_act,parity__state_act);
20
    l_out = l;
21
    l = (if __parity__Odd_handler_until_1 then x else __parity__Odd_handler_until_2);
22
    __parity__Odd_handler_until_2 = pre ((3 * l) + 1);
23
    __parity__Odd_handler_until_1 = (true -> false);
24
     
25
tel
26
 
27
function parity__Even_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type)
28
var __parity__Even_unless_1: bool;
29
let
30
    
31
    parity__restart_act, parity__state_act = (if __parity__Even_unless_1 then (true,Odd) else (parity__restart_in,parity__state_in));
32
    __parity__Even_unless_1 = ((l mod 2) = 1);
33
     
34
tel
35
 
36
node parity__Even_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int)
37
var __parity__Even_handler_until_2: int;
38
    __parity__Even_handler_until_1: bool;
39
    l: int;
40
let
41
    
42
    parity__restart_in, parity__state_in = (parity__restart_act,parity__state_act);
43
    l_out = l;
44
    l = (if __parity__Even_handler_until_1 then x else __parity__Even_handler_until_2);
45
    __parity__Even_handler_until_2 = pre (l / 2);
46
    __parity__Even_handler_until_1 = (true -> false);
47
     
48
tel
49

  
50
node top (x: int) returns (y: bool)
51
var __test1_12: bool;
52
    __test1_13: parity__type;
53
    __test1_11: bool;
54
    __test1_8: bool;
55
    __test1_9: parity__type;
56
    __test1_10: int;
57
    __test1_5: bool;
58
    __test1_6: parity__type;
59
    __test1_7: int;
60
    __test1_3: bool;
61
    __test1_4: parity__type;
62
    __test1_1: bool;
63
    __test1_2: parity__type;
64
    parity__next_restart_in: bool;
65
    parity__restart_in: bool;
66
    parity__restart_act: bool;
67
    parity__next_state_in: parity__type;
68
    parity__state_in: parity__type clock;
69
    parity__state_act: parity__type clock;
70
    l: int;
71
let
72
    
73
    parity__restart_in, parity__state_in = (if __test1_11 then (false,Even) else (__test1_12,__test1_13));
74
    __test1_12, __test1_13 = pre (parity__next_restart_in,parity__next_state_in);
75
    __test1_11 = (true -> false);
76

  
77
    parity__next_restart_in, parity__next_state_in, l = merge parity__state_act (Even -> (__test1_8,__test1_9,__test1_10))
78
                                                                                (Odd -> (__test1_5,__test1_6,__test1_7));
79
    __test1_8, __test1_9, __test1_10 = parity__Even_handler_until (parity__restart_act when Even(parity__state_act),
80
                                                                   parity__state_act when Even(parity__state_act),
81
                                                                   x when Even(parity__state_act))
82
                                       every (parity__restart_act);
83
    __test1_5, __test1_6, __test1_7 = parity__Odd_handler_until (parity__restart_act when Odd(parity__state_act),
84
                                                                 parity__state_act when Odd(parity__state_act),
85
                                                                 x when Odd(parity__state_act))
86
                                      every (parity__restart_act);
87

  
88

  
89
    parity__restart_act, parity__state_act = merge parity__state_in (Even -> (__test1_3,__test1_4))
90
                                                                    (Odd -> (__test1_1,__test1_2));
91
    __test1_3, __test1_4 = parity__Even_unless (parity__restart_in when Even(parity__state_in),
92
                                                parity__state_in when Even(parity__state_in),
93
                                                l when Even(parity__state_in))
94
                           every (parity__restart_in);
95
    __test1_1, __test1_2 = parity__Odd_unless (parity__restart_in when Odd(parity__state_in),
96
                                               parity__state_in when Odd(parity__state_in),
97
                                               l when Odd(parity__state_in))
98
                           every (parity__restart_in);
99

  
100
    y = (l = 1);
101
     
102
tel
regression_tests/lustre_files/success/automata/with_properties/aut2.lusi
1
(* Generated Lustre Interface file from aut2.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:30 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type parity__type = enum {Even, Odd }; 
6

  
7
node parity__Even_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
8

  
9
function parity__Even_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
10

  
11
node parity__Odd_handler_until (parity__restart_act: bool; parity__state_act: parity__type; x: int) returns (parity__restart_in: bool; parity__state_in: parity__type; l_out: int);
12

  
13
function parity__Odd_unless (parity__restart_in: bool; parity__state_in: parity__type; l: int) returns (parity__restart_act: bool; parity__state_act: parity__type);
14

  
15
node top (x: int) returns (y: bool);
16

  
regression_tests/lustre_files/success/automata/with_properties/counters.lus
1
-- a simple boolean ant int counter
2

  
3
node greycounter (x:bool) returns (out:bool);
4
var a,b:bool;
5
let
6
  a = false -> not pre(b);
7
  b = false -> pre(a);
8
  out = a and b;
9
tel
10

  
11
node intloopcounter (x:bool) returns (out:bool);
12
var time: int;
13
let
14
  time = 0 -> if pre(time) = 3 then 0
15
            else pre time + 1;
16
  out = (time = 2);
17
tel
18

  
19
node auto (x:bool) returns -- (out:bool);
20
 (_state: int);
21
let
22
  automaton four_states
23
  state One : 
24
  let 
25
 --   out = false;
26
    _state = 1;
27
  tel until true restart Two
28
  state Two : 
29
  let 
30
 --   out = false;
31
    _state = 2;
32
  tel until true restart Three
33
  state Three : 
34
  let 
35
--    out = true;
36
   _state = 3;
37
  tel until true restart Four
38
  state Four :
39
  let 
40
 --   out = false;
41
    _state = 4;
42
  tel until true restart One
43
tel
44

  
45

  
46

  
47
--@ ensures OK;
48
node top (x:bool) returns (OK:bool);
49
var a,b,d:bool;
50
    s:int;
51
    OK1,OK2,OK3: bool;
52
    
53
let
54
  b = greycounter(x);
55
  d = intloopcounter(x);
56
  s = auto(x);
57
  a = s= 3;
58
  OK1 = b = d;
59
  OK2 = b = a;
60
  OK3 = a = d;
61
  OK = OK3;
62
  --%PROPERTY OK;
63
tel
regression_tests/lustre_files/success/automata/with_properties/counters.lusi
1
(* Generated Lustre Interface file from counters.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:31 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type four_states__type = enum {One, Two, Three, Four }; 
6

  
7
function four_states__Four_handler_until (four_states__restart_act: bool) returns (four_states__restart_in: bool; four_states__state_in: four_states__type; _state_out: int);
8

  
9
function four_states__Four_unless (four_states__restart_in: bool) returns (four_states__restart_act: bool; four_states__state_act: four_states__type);
10

  
11
function four_states__One_handler_until (four_states__restart_act: bool) returns (four_states__restart_in: bool; four_states__state_in: four_states__type; _state_out: int);
12

  
13
function four_states__One_unless (four_states__restart_in: bool) returns (four_states__restart_act: bool; four_states__state_act: four_states__type);
14

  
15
function four_states__Three_handler_until (four_states__restart_act: bool) returns (four_states__restart_in: bool; four_states__state_in: four_states__type; _state_out: int);
16

  
17
function four_states__Three_unless (four_states__restart_in: bool) returns (four_states__restart_act: bool; four_states__state_act: four_states__type);
18

  
19
function four_states__Two_handler_until (four_states__restart_act: bool) returns (four_states__restart_in: bool; four_states__state_in: four_states__type; _state_out: int);
20

  
21
function four_states__Two_unless (four_states__restart_in: bool) returns (four_states__restart_act: bool; four_states__state_act: four_states__type);
22

  
23
node auto (x: bool) returns (_state: int);
24

  
25
node greycounter (x: bool) returns (out: bool);
26

  
27
node intloopcounter (x: bool) returns (out: bool);
28

  
29
node top (x: bool) returns (OK: bool);
30

  
regression_tests/lustre_files/success/automata/with_properties/counters.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-21 13:58</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.62</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/automata/with_properties/heater.lus
1

  
2
const low = 5;
3

  
4
const high = 5;
5

  
6
const delay_on = 200;
7

  
8
const delay_off = 500;
9

  
10
node edge(c : bool) returns (edge_c : bool)
11
let
12
  edge_c = false -> c && not (pre c);
13
tel
14

  
15
node count(d : int; t : bool) returns (ok : bool)
16
var cpt:int;
17
let
18
  ok = (cpt = 0);
19
  cpt = 0 -> (if t then pre cpt + 1 else pre cpt) mod d;
20
tel
21

  
22
(* controling the heat *)
23
(* returns [true] when [expected_temp] does not agree with [actual_temp] *)
24
node heat(expected_temp, actual_temp : int) returns (ok : bool)
25
let
26
  automaton heat_control
27
    state Stop :
28
          unless (actual_temp <= expected_temp - low) resume Start
29
          let
30
            ok = false; 
31
          tel
32
    state Start :
33
          unless (actual_temp >= expected_temp + high) resume Stop
34
          let
35
            ok = true;
36
          tel
37
tel
38

  
39
(* a cyclic two mode automaton with an internal timer *)
40
(* [open_light = true] and [open_gas = true] for [delay_on millisecond] *)
41
(* then [open_light = false] and [open_gas = false] for *)
42
(* [delay_off millisecond] *)
43
node command(millisecond : bool) returns (open_light, open_gas : bool)
44
let
45
  automaton command_control
46
    state Open :
47
          let
48
            open_light = true;
49
            open_gas = true;
50
          tel
51
          until count(delay_on, millisecond) restart Silent
52
    state Silent :
53
          let
54
            open_light = false;
55
            open_gas = false;
56
          tel
57
          until count(delay_off, millisecond) restart Open
58
tel
59

  
60
(* the main command which control the opening of the light and gas *)
61
node light(millisecond : bool; on_heat, on_light : bool) returns (open_light, open_gas, nok : bool)
62
let
63
  automaton light_control
64
    state Light_off :
65
          let
66
            nok = false;
67
            open_light = false;
68
            open_gas = false;
69
          tel
70
          until on_heat restart Try
71
    state Light_on :
72
          let
73
            nok = false;
74
            open_light = false;
75
            open_gas = true;
76
          tel
77
          until not on_heat restart Light_off
78
    state Try :
79
          let
80
            nok = false;
81
            (open_light, open_gas) = command(millisecond);
82
          tel
83
          until on_light restart Light_on
84
          until count(3, edge(not open_light)) restart Failure
85
    state Failure :
86
          let
87
            nok = true; 
88
            open_light = false;
89
            open_gas = false;
90
          tel
91
tel
92

  
93
(* the main function *)
94
node top(millisecond : bool; reset : bool; expected_temp, actual_temp : int; on_light : bool) returns ( ok : bool)
95
var on_heat, nok , open_light, open_gas: bool;
96
let
97
  on_heat = heat(expected_temp,actual_temp) every reset;
98
  (open_light, open_gas, nok) = light(millisecond, on_heat, on_light) every reset;
99
  ok = not nok;
100
tel
regression_tests/lustre_files/success/automata/with_properties/heater.lusi
1
(* Generated Lustre Interface file from heater.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:29 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
const low = 5;
6

  
7
const high = 5;
8

  
9
const delay_on = 200;
10

  
11
const delay_off = 500;
12

  
13
type heat_control__type = enum {Stop, Start }; 
14

  
15
type command_control__type = enum {Open, Silent }; 
16

  
17
type light_control__type = enum {Light_off, Light_on, Try, Failure }; 
18

  
19
node count (d: int; t: bool) returns (ok: bool);
20

  
21
node command_control__Open_handler_until (command_control__restart_act: bool; millisecond: bool) returns (command_control__restart_in: bool; command_control__state_in: command_control__type; open_gas_out: bool; open_light_out: bool);
22

  
23
function command_control__Open_unless (command_control__restart_in: bool) returns (command_control__restart_act: bool; command_control__state_act: command_control__type);
24

  
25
node command_control__Silent_handler_until (command_control__restart_act: bool; millisecond: bool) returns (command_control__restart_in: bool; command_control__state_in: command_control__type; open_gas_out: bool; open_light_out: bool);
26

  
27
function command_control__Silent_unless (command_control__restart_in: bool) returns (command_control__restart_act: bool; command_control__state_act: command_control__type);
28

  
29
node command (millisecond: bool) returns (open_light: bool; open_gas: bool);
30

  
31
node edge (c: bool) returns (edge_c: bool);
32

  
33
function heat_control__Start_handler_until (heat_control__restart_act: bool) returns (heat_control__restart_in: bool; heat_control__state_in: heat_control__type; ok_out: bool);
34

  
35
function heat_control__Start_unless (heat_control__restart_in: bool; expected_temp: int; actual_temp: int) returns (heat_control__restart_act: bool; heat_control__state_act: heat_control__type);
36

  
37
function heat_control__Stop_handler_until (heat_control__restart_act: bool) returns (heat_control__restart_in: bool; heat_control__state_in: heat_control__type; ok_out: bool);
38

  
39
function heat_control__Stop_unless (heat_control__restart_in: bool; expected_temp: int; actual_temp: int) returns (heat_control__restart_act: bool; heat_control__state_act: heat_control__type);
40

  
41
function light_control__Failure_handler_until (light_control__restart_act: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
42

  
43
function light_control__Failure_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
44

  
45
function light_control__Light_off_handler_until (light_control__restart_act: bool; on_heat: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
46

  
47
function light_control__Light_off_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
48

  
49
function light_control__Light_on_handler_until (light_control__restart_act: bool; on_heat: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
50

  
51
function light_control__Light_on_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
52

  
53
node light_control__Try_handler_until (light_control__restart_act: bool; millisecond: bool; on_light: bool) returns (light_control__restart_in: bool; light_control__state_in: light_control__type; nok_out: bool; open_gas_out: bool; open_light_out: bool);
54

  
55
function light_control__Try_unless (light_control__restart_in: bool) returns (light_control__restart_act: bool; light_control__state_act: light_control__type);
56

  
57
node heat (expected_temp: int; actual_temp: int) returns (ok: bool);
58

  
59
node light (millisecond: bool; on_heat: bool; on_light: bool) returns (open_light: bool; open_gas: bool; nok: bool);
60

  
61
node top (millisecond: bool; reset: bool; expected_temp: int; actual_temp: int; on_light: bool) returns (ok: bool);
62

  
regression_tests/lustre_files/success/automata/with_properties/heater.xml
1
(error "line 100 column 19: unknown constant command_control__Open_handler_until.delay_on")
2
(error "line 182 column 19: unknown constant command_control__Silent_handler_until.delay_off")
3
(error "line 480 column 155: unknown constant heat_control__Start_unless.high")
4
(error "line 519 column 151: unknown constant heat_control__Stop_unless.low")
regression_tests/lustre_files/success/automata/with_properties/heater4.lus
1
(*@ ensures open_light; *)
2
node top(millisecond : bool) returns (open_light : bool)
3
let
4
  automaton command_control
5
    state Open :
6
          let
7
            open_light = true;
8
          tel
9
          
10
    state Silent :
11
          let
12
            open_light = false;
13
          tel
14
          
15
tel
regression_tests/lustre_files/success/automata/with_properties/heater4.lusi
1
(* Generated Lustre Interface file from heater4.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:30 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type command_control__type = enum {Open, Silent }; 
6

  
7
function command_control__Open_handler_until (command_control__restart_act: bool) returns (command_control__restart_in: bool; command_control__state_in: command_control__type; open_light_out: bool);
8

  
9
function command_control__Open_unless (command_control__restart_in: bool) returns (command_control__restart_act: bool; command_control__state_act: command_control__type);
10

  
11
function command_control__Silent_handler_until (command_control__restart_act: bool) returns (command_control__restart_in: bool; command_control__state_in: command_control__type; open_light_out: bool);
12

  
13
function command_control__Silent_unless (command_control__restart_in: bool) returns (command_control__restart_act: bool; command_control__state_act: command_control__type);
14

  
15
node top (millisecond: bool) returns (open_light: bool);
16

  
regression_tests/lustre_files/success/automata/with_properties/heater4.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-21 13:58</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.05</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/automata/with_properties/test_counter2.lus
1
node top (x:bool) returns (ok: bool);
2
var bit: bool;
3
    coin: bool;
4
let
5
  automaton mini_states
6
  state Even : 
7
  let 
8
    bit = true;
9
  tel until true restart Odd
10
  state Odd : 
11
  let 
12
    bit = false;
13
  tel until true restart Even
14

  
15
  coin = true -> not pre coin;
16
  ok = bit = coin;
17
tel
18

  
regression_tests/lustre_files/success/automata/with_properties/test_counter2.lusi
1
(* Generated Lustre Interface file from test_counter2.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:31 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type mini_states__type = enum {Even, Odd }; 
6

  
7
function mini_states__Even_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
8

  
9
function mini_states__Even_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
10

  
11
function mini_states__Odd_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
12

  
13
function mini_states__Odd_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
14

  
15
node top (x: bool) returns (ok: bool);
16

  
regression_tests/lustre_files/success/automata/with_properties/test_counter2.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-21 13:58</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.10</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/automata/with_properties/test_nok.lus
1
node top (x:bool) returns (ok: bool);
2
var bit: bool;
3
    coin: bool;
4
let
5
  automaton mini_states
6
  state Even : 
7
  let 
8
    bit = true;
9
  tel until true restart Odd
10
  state Odd : 
11
  let 
12
    bit = false;
13
  tel until true restart Even
14

  
15
  coin = true -> not pre coin;
16
  ok = bit = not coin;
17
tel
18

  
regression_tests/lustre_files/success/automata/with_properties/test_nok.lusi
1
(* Generated Lustre Interface file from test_nok.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:27 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type mini_states__type = enum {Even, Odd }; 
6

  
7
function mini_states__Even_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
8

  
9
function mini_states__Even_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
10

  
11
function mini_states__Odd_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
12

  
13
function mini_states__Odd_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
14

  
15
node top (x: bool) returns (ok: bool);
16

  
regression_tests/lustre_files/success/automata/with_properties/test_nok.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-21 13:58</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.12</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="top">
11
            <Stream name="top.x" type="unk">
12
                <Value instant="0">1</Value>
13
           </Stream>
14
            <Stream name="top.__top_14_c" type="unk">
15
                <Value instant="0">Even</Value>
16
           </Stream>
17
            <Stream name="top.__top_2_x" type="unk">
18
                <Value instant="0">1</Value>
19
           </Stream>
20
            <Stream name="top.__top_13_x" type="unk">
21
                <Value instant="0">1</Value>
22
           </Stream>
23
            <Stream name="top.__top_14_x" type="unk">
24
                <Value instant="0">Odd</Value>
25
           </Stream>
26
            <Stream name="top.__top_2_c" type="unk">
27
                <Value instant="0">1</Value>
28
           </Stream>
29
            <Stream name="top.ok" type="unk">
30
                <Value instant="0">1</Value>
31
           </Stream>
32
            <Stream name="top.__top_13_c" type="unk">
33
                <Value instant="0">1</Value>
34
           </Stream>
35
         </Node>
36
 <Node name ="mini_states__Even_unless">
37
            <Stream name="mini_states__Even_unless.mini_states__restart_act" type="unk">
38
                <Value instant="0">1</Value>
39
           </Stream>
40
            <Stream name="mini_states__Even_unless.mini_states__state_act" type="unk">
41
                <Value instant="0">Even</Value>
42
           </Stream>
43
            <Stream name="mini_states__restart_in" type="bool">
44
                <Value instant="0">1</Value>
45
           </Stream>
46
         </Node>
47
 <Node name ="mini_states__Even_handler_until">
48
            <Stream name="mini_states__Even_handler_until.mini_states__restart_in" type="unk">
49
                <Value instant="0">1</Value>
50
           </Stream>
51
            <Stream name="mini_states__Even_handler_until.bit_out" type="unk">
52
                <Value instant="0">1</Value>
53
           </Stream>
54
            <Stream name="mini_states__Even_handler_until.mini_states__restart_act" type="unk">
55
                <Value instant="0">1</Value>
56
           </Stream>
57
            <Stream name="mini_states__Even_handler_until.mini_states__state_in" type="unk">
58
                <Value instant="0">Odd</Value>
59
           </Stream>
60
         </Node>
61

  
62
      </Counterexample>
63
     </Property>
64
   </Results>
65

  
regression_tests/lustre_files/success/automata/with_properties/test_ok.lus
1
node top (x:bool) returns (ok: bool);
2
var bit: bool;
3
    coin: bool;
4
let
5
  automaton mini_states
6
  state Even : 
7
  let 
8
    bit = true;
9
  tel until true restart Odd
10
  state Odd : 
11
  let 
12
    bit = false;
13
  tel until true restart Even
14

  
15
  coin = true -> not pre coin;
16
  ok = bit = coin;
17
tel
18

  
regression_tests/lustre_files/success/automata/with_properties/test_ok.lusi
1
(* Generated Lustre Interface file from test_ok.lus *)
2
(* by Lustre-C compiler version 1.3-458, 2016/10/21, 12:58:30 *)
3
(* Feel free to mask some of the definitions by removing them from this file. *)
4

  
5
type mini_states__type = enum {Even, Odd }; 
6

  
7
function mini_states__Even_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
8

  
9
function mini_states__Even_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
10

  
11
function mini_states__Odd_handler_until (mini_states__restart_act: bool) returns (mini_states__restart_in: bool; mini_states__state_in: mini_states__type; bit_out: bool);
12

  
13
function mini_states__Odd_unless (mini_states__restart_in: bool) returns (mini_states__restart_act: bool; mini_states__state_act: mini_states__type);
14

  
15
node top (x: bool) returns (ok: bool);
16

  
regression_tests/lustre_files/success/automata/with_properties/test_ok.xml
1
<?xml version="1.0"?>
2
   <Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
3
     <Property name="top">
4
      <Date>2016-11-21 13:58</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.10</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/automata/without_properties/CMakeLists.txt
1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
3

  
4

  
5

  
6

  
7

  
8
#take all lustre files
9
set(GLOBAL_LUSTRE_FILES "")
10
LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )
11
list(APPEND GLOBAL_LUSTRE_FILES ${LFILES})
12
FOREACH(lfile ${LFILES})
13
	get_filename_component(L ${lfile} NAME_WE)
14
	set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/${L}")
15
	file(COPY ${lfile}   DESTINATION  ${LUSTRE_OUTPUT_DIR})
16
	if(EXISTS ${CMAKE_CURRENT_SOURCE_DIR}/${L}.lusi)
17
		file(COPY  ${L}.lusi DESTINATION  ${LUSTRE_OUTPUT_DIR})
18
	else()
19
		message("generate ${L}.lusi \n")
20
		Lustre_Compile(LUS_FILE ${lfile}
21
				NODE ""
22
				OPTS "-lusi")				
23
		set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
24
		execute_process(RESULT_VARIABLE res 
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff