Revision 02d89bbb
Added by Hamza Bourbouh about 8 years ago
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 |
Also available in: Unified diff
add automata folder to tests