Project

General

Profile

Revision 5600dad4

View differences:

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)
8
add_subdirectory(clocks)
7
add_subdirectory(automata)
8
#[[add_subdirectory(clocks)
9 9
add_subdirectory(lego_robot)
10 10
add_subdirectory(linear_ctl)
11 11
add_subdirectory(mpfr)
regression_tests/lustre_files/success/Simulink/CMakeLists.txt
7 7

  
8 8
#proceed all subdirectories
9 9
SUBDIRLIST(SUBDIRS ${CMAKE_CURRENT_SOURCE_DIR}  "src_")
10
set(DST_DIR "${CMAKE_CURRENT_BINARY_DIR}")
10 11
FOREACH(subdir ${SUBDIRS})
11 12
  LUSTREFILES(LFILES ${subdir} )
12 13
  set(TESTS_PREFIX "Simulink")
13 14
  set(SRC_DIR "${CMAKE_CURRENT_SOURCE_DIR}/${subdir}")
14
  set(DST_DIR "${CMAKE_CURRENT_BINARY_DIR}")
15
  
15 16
  FOREACH(lus_file ${LFILES})
16 17
	get_filename_component(L ${lus_file} NAME_WE)
17 18
	set(NODE_NAME  "${L}")
regression_tests/lustre_files/success/Stateflow/CMakeLists.txt
7 7

  
8 8
#proceed all subdirectories
9 9
SUBDIRLIST(SUBDIRS ${CMAKE_CURRENT_SOURCE_DIR}  "src_")
10
  set(DST_DIR "${CMAKE_CURRENT_BINARY_DIR}")
10 11
FOREACH(subdir ${SUBDIRS})
11 12
  LUSTREFILES(LFILES ${subdir} )
12 13
  set(TESTS_PREFIX "Steteflow")
13 14
  set(SRC_DIR "${CMAKE_CURRENT_SOURCE_DIR}/${subdir}")
14
  set(DST_DIR "${CMAKE_CURRENT_BINARY_DIR}")
15

  
15 16
  FOREACH(lus_file ${LFILES})
16 17
	get_filename_component(L ${lus_file} NAME_WE)
17 18
	set(NODE_NAME  "${L}")
regression_tests/lustre_files/success/automata/with_properties/CMakeLists.txt
1 1
cmake_minimum_required(VERSION 2.8.4)
2
include(FindUnixCommands)
3 2

  
4 3

  
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 4

  
11

  
12

  
13

  
14
#first combination :no option
15 5
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()
6
set(LUSTRE_OPTIONS_OPT "" )
7
set(NODE_NAME  "top")
8
set(MAX_INPUT_VALUE 100)
74 9

  
75 10

  
76 11

  
77 12

  
78
FOREACH(lus_file ${GLOBAL_LUSTRE_FILES})
13
set(SRC_DIR "${CMAKE_CURRENT_SOURCE_DIR}")
14
set(DST_DIR "${CMAKE_CURRENT_BINARY_DIR}")
15
set(subdir ${CMAKE_CURRENT_SOURCE_DIR})
16
LUSTREFILES(LFILES ${subdir} )
17
set(TESTS_PREFIX "automata_with_properties")
18
FOREACH(lus_file ${LFILES})
79 19
	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}
20
	Copy_or_generate_lusi_input_and_output_values_for_reference(
21
		LUS_FILE ${lus_file}
22
		NODE ${NODE_NAME}
23
		OPTS ${LUSTRE_OPTIONS_OPT}
24
		MAX ${MAX_INPUT_VALUE}  	#maximum value for input values.
25
		SRC_DIR ${SRC_DIR}
26
		DST_DIR ${DST_DIR}
103 27
	)
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}
28
	Copy_or_generate_zustre_output_xml_for_reference(
29
		LUS_FILE ${lus_file}
30
		NODE ${NODE_NAME}
31
		OPTS ${ZUSTRE_OPTIONS_OPT}
32
		SRC_DIR ${SRC_DIR}
33
		DST_DIR ${DST_DIR}
113 34
	)
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 35

  
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}
36
	Zustre_compile_and_compare_to_reference(
37
		LUS_FILE ${lus_file}
38
		NODE ${NODE_NAME}
39
		TESTS_PREFIX ${TESTS_PREFIX}
40
		OPTS ${ZUSTRE_OPTIONS_OPT}
41
		CALL_ID "1"
42
		SRC_DIR ${SRC_DIR}
43
		DST_DIR ${DST_DIR}
44
	)
45
	if(EXISTS ${CMAKE_BINARY_DIR}/modules/XPathParser_lusi.class 
46
		AND ${ZUSTRE_ANSWER_${L}_${NODE_NAME}} STREQUAL "CEX" 
47
		AND EXISTS ${CMAKE_CURRENT_BINARY_DIR}/${L}/${L}.lusi)
48
		Compare_Zustre_and_Lustrec_outputs(
49
			LUS_FILE ${lus_file}
50
			NODE ${NODE_NAME}
51
			TESTS_PREFIX ${TESTS_PREFIX}
52
			OPTS ${ZUSTRE_OPTIONS_OPT}
53
			CALL_ID "2"
54
			SRC_DIR ${SRC_DIR}
55
			DST_DIR ${DST_DIR}
157 56
		)
57
	endif()
58
	Lustre_compile_and_compare_to_reference(
59
		LUS_FILE ${lus_file}
60
		NODE ${NODE_NAME}
61
		TESTS_PREFIX ${TESTS_PREFIX}
62
		OPTS ${LUSTRE_OPTIONS_OPT}
63
		CALL_ID "3"
64
		SRC_DIR ${SRC_DIR}
65
		DST_DIR ${DST_DIR}
66
	)
158 67

  
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()
68
ENDFOREACH()
183 69

  
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 70

  
195
	endif()
196
	
197
ENDFOREACH()
198 71
add_custom_target(automata_with_properties COMMAND ${CMAKE_CTEST_COMMAND} -R automata_with_properties)
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.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/counters_top__output_values
1
'OK': '1' 
2
'OK': '1' 
3
'OK': '1' 
4
'OK': '1' 
5
'OK': '1' 
6
'OK': '1' 
7
'OK': '1' 
8
'OK': '1' 
9
'OK': '1' 
10
'OK': '1' 
11
'OK': '1' 
12
'OK': '1' 
13
'OK': '1' 
14
'OK': '1' 
15
'OK': '1' 
16
'OK': '1' 
17
'OK': '1' 
18
'OK': '1' 
19
'OK': '1' 
20
'OK': '1' 
21
'OK': '1' 
22
'OK': '1' 
23
'OK': '1' 
24
'OK': '1' 
25
'OK': '1' 
26
'OK': '1' 
27
'OK': '1' 
28
'OK': '1' 
29
'OK': '1' 
30
'OK': '1' 
31
'OK': '1' 
32
'OK': '1' 
33
'OK': '1' 
34
'OK': '1' 
35
'OK': '1' 
36
'OK': '1' 
37
'OK': '1' 
38
'OK': '1' 
39
'OK': '1' 
40
'OK': '1' 
41
'OK': '1' 
42
'OK': '1' 
43
'OK': '1' 
44
'OK': '1' 
45
'OK': '1' 
46
'OK': '1' 
47
'OK': '1' 
48
'OK': '1' 
49
'OK': '1' 
50
'OK': '1' 
51
'OK': '1' 
52
'OK': '1' 
53
'OK': '1' 
54
'OK': '1' 
55
'OK': '1' 
56
'OK': '1' 
57
'OK': '1' 
58
'OK': '1' 
59
'OK': '1' 
60
'OK': '1' 
61
'OK': '1' 
62
'OK': '1' 
63
'OK': '1' 
64
'OK': '1' 
65
'OK': '1' 
66
'OK': '1' 
67
'OK': '1' 
68
'OK': '1' 
69
'OK': '1' 
70
'OK': '1' 
71
'OK': '1' 
72
'OK': '1' 
73
'OK': '1' 
74
'OK': '1' 
75
'OK': '1' 
76
'OK': '1' 
77
'OK': '1' 
78
'OK': '1' 
79
'OK': '1' 
80
'OK': '1' 
81
'OK': '1' 
82
'OK': '1' 
83
'OK': '1' 
84
'OK': '1' 
85
'OK': '1' 
86
'OK': '1' 
87
'OK': '1' 
88
'OK': '1' 
89
'OK': '1' 
90
'OK': '1' 
91
'OK': '1' 
92
'OK': '1' 
93
'OK': '1' 
94
'OK': '1' 
95
'OK': '1' 
96
'OK': '1' 
97
'OK': '1' 
98
'OK': '1' 
99
'OK': '1' 
100
'OK': '1' 
regression_tests/lustre_files/success/automata/with_properties/counters_top__timeout60_xml.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-30 00:26</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.65</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/automata/with_properties/counters_top_input_values
1
1
2
0
3
1
4
1
5
1
6
0
7
1
8
0
9
1
10
1
11
0
12
0
13
1
14
0
15
0
16
1
17
1
18
0
19
0
20
0
21
1
22
1
23
1
24
0
25
1
26
0
27
1
28
1
29
1
30
1
31
1
32
1
33
0
34
1
35
1
36
0
37
0
38
0
39
1
40
0
41
0
42
0
43
0
44
1
45
0
46
1
47
0
48
1
49
0
50
0
51
0
52
1
53
0
54
0
55
1
56
1
57
0
58
1
59
0
60
0
61
0
62
1
63
1
64
0
65
1
66
1
67
0
68
1
69
1
70
1
71
0
72
1
73
1
74
1
75
0
76
0
77
0
78
0
79
1
80
0
81
1
82
0
83
1
84
0
85
0
86
1
87
0
88
1
89
1
90
0
91
0
92
0
93
0
94
0
95
0
96
1
97
1
98
0
99
0
100
0
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.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/heater4_top__output_values
1
'open_light': '1' 
2
'open_light': '1' 
3
'open_light': '1' 
4
'open_light': '1' 
5
'open_light': '1' 
6
'open_light': '1' 
7
'open_light': '1' 
8
'open_light': '1' 
9
'open_light': '1' 
10
'open_light': '1' 
11
'open_light': '1' 
12
'open_light': '1' 
13
'open_light': '1' 
14
'open_light': '1' 
15
'open_light': '1' 
16
'open_light': '1' 
17
'open_light': '1' 
18
'open_light': '1' 
19
'open_light': '1' 
20
'open_light': '1' 
21
'open_light': '1' 
22
'open_light': '1' 
23
'open_light': '1' 
24
'open_light': '1' 
25
'open_light': '1' 
26
'open_light': '1' 
27
'open_light': '1' 
28
'open_light': '1' 
29
'open_light': '1' 
30
'open_light': '1' 
31
'open_light': '1' 
32
'open_light': '1' 
33
'open_light': '1' 
34
'open_light': '1' 
35
'open_light': '1' 
36
'open_light': '1' 
37
'open_light': '1' 
38
'open_light': '1' 
39
'open_light': '1' 
40
'open_light': '1' 
41
'open_light': '1' 
42
'open_light': '1' 
43
'open_light': '1' 
44
'open_light': '1' 
45
'open_light': '1' 
46
'open_light': '1' 
47
'open_light': '1' 
48
'open_light': '1' 
49
'open_light': '1' 
50
'open_light': '1' 
51
'open_light': '1' 
52
'open_light': '1' 
53
'open_light': '1' 
54
'open_light': '1' 
55
'open_light': '1' 
56
'open_light': '1' 
57
'open_light': '1' 
58
'open_light': '1' 
59
'open_light': '1' 
60
'open_light': '1' 
61
'open_light': '1' 
62
'open_light': '1' 
63
'open_light': '1' 
64
'open_light': '1' 
65
'open_light': '1' 
66
'open_light': '1' 
67
'open_light': '1' 
68
'open_light': '1' 
69
'open_light': '1' 
70
'open_light': '1' 
71
'open_light': '1' 
72
'open_light': '1' 
73
'open_light': '1' 
74
'open_light': '1' 
75
'open_light': '1' 
76
'open_light': '1' 
77
'open_light': '1' 
78
'open_light': '1' 
79
'open_light': '1' 
80
'open_light': '1' 
81
'open_light': '1' 
82
'open_light': '1' 
83
'open_light': '1' 
84
'open_light': '1' 
85
'open_light': '1' 
86
'open_light': '1' 
87
'open_light': '1' 
88
'open_light': '1' 
89
'open_light': '1' 
90
'open_light': '1' 
91
'open_light': '1' 
92
'open_light': '1' 
93
'open_light': '1' 
94
'open_light': '1' 
95
'open_light': '1' 
96
'open_light': '1' 
97
'open_light': '1' 
98
'open_light': '1' 
99
'open_light': '1' 
100
'open_light': '1' 
regression_tests/lustre_files/success/automata/with_properties/heater4_top__timeout60_xml.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-30 00:26</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/heater4_top_input_values
1
0
2
1
3
1
4
0
5
1
6
1
7
0
8
1
9
0
10
1
11
0
12
1
13
0
14
0
15
0
16
1
17
0
18
0
19
0
20
0
21
0
22
0
23
0
24
1
25
1
26
1
27
1
28
0
29
0
30
0
31
0
32
0
33
1
34
0
35
1
36
0
37
0
38
1
39
1
40
0
41
1
42
1
43
0
44
0
45
1
46
1
47
0
48
0
49
0
50
0
51
1
52
1
53
0
54
1
55
0
56
0
57
1
58
0
59
0
60
1
61
1
62
0
63
0
64
1
65
0
66
0
67
0
68
1
69
0
70
0
71
1
72
1
73
0
74
0
75
1
76
1
77
1
78
1
79
1
80
1
81
1
82
0
83
1
84
0
85
0
86
0
87
1
88
1
89
1
90
1
91
1
92
1
93
0
94
0
95
0
96
0
97
1
98
0
99
0
100
0
regression_tests/lustre_files/success/automata/with_properties/heater_top__output_values
1
'ok': '1' 
2
'ok': '1' 
3
'ok': '1' 
4
'ok': '1' 
5
'ok': '1' 
6
'ok': '1' 
7
'ok': '1' 
8
'ok': '1' 
9
'ok': '1' 
10
'ok': '1' 
11
'ok': '1' 
12
'ok': '1' 
13
'ok': '1' 
14
'ok': '1' 
15
'ok': '1' 
16
'ok': '1' 
17
'ok': '1' 
18
'ok': '1' 
19
'ok': '1' 
20
'ok': '1' 
21
'ok': '1' 
22
'ok': '1' 
23
'ok': '1' 
24
'ok': '1' 
25
'ok': '1' 
26
'ok': '1' 
27
'ok': '1' 
28
'ok': '1' 
29
'ok': '1' 
30
'ok': '1' 
31
'ok': '1' 
32
'ok': '1' 
33
'ok': '1' 
34
'ok': '1' 
35
'ok': '1' 
36
'ok': '1' 
37
'ok': '1' 
38
'ok': '1' 
39
'ok': '0' 
40
'ok': '1' 
41
'ok': '1' 
42
'ok': '1' 
43
'ok': '1' 
44
'ok': '1' 
45
'ok': '1' 
46
'ok': '1' 
47
'ok': '1' 
48
'ok': '1' 
49
'ok': '1' 
50
'ok': '1' 
51
'ok': '1' 
52
'ok': '1' 
53
'ok': '1' 
54
'ok': '1' 
55
'ok': '1' 
56
'ok': '1' 
57
'ok': '1' 
58
'ok': '1' 
59
'ok': '1' 
60
'ok': '1' 
61
'ok': '1' 
62
'ok': '1' 
63
'ok': '1' 
64
'ok': '1' 
65
'ok': '1' 
66
'ok': '1' 
67
'ok': '1' 
68
'ok': '1' 
69
'ok': '1' 
70
'ok': '1' 
71
'ok': '1' 
72
'ok': '1' 
73
'ok': '1' 
74
'ok': '1' 
75
'ok': '1' 
76
'ok': '1' 
77
'ok': '1' 
78
'ok': '1' 
79
'ok': '1' 
80
'ok': '1' 
81
'ok': '1' 
82
'ok': '1' 
83
'ok': '1' 
84
'ok': '1' 
85
'ok': '1' 
86
'ok': '1' 
87
'ok': '1' 
88
'ok': '1' 
89
'ok': '1' 
90
'ok': '1' 
91
'ok': '1' 
92
'ok': '1' 
93
'ok': '1' 
94
'ok': '1' 
95
'ok': '1' 
96
'ok': '1' 
97
'ok': '1' 
98
'ok': '1' 
99
'ok': '1' 
100
'ok': '1' 
regression_tests/lustre_files/success/automata/with_properties/heater_top__timeout60_xml.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/heater_top_input_values
1
0
2
1
3
88
4
75
5
0
6
0
7
1
8
57
9
41
10
1
11
1
12
1
13
5
14
68
15
1
16
0
17
1
18
92
19
89
20
1
21
0
22
0
23
35
24
41
25
1
26
0
27
1
28
57
29
69
30
0
31
0
32
0
33
28
34
74
35
1
36
0
37
1
38
73
39
63
40
1
41
1
42
0
43
18
44
77
45
1
46
1
47
0
48
56
49
97
50
1
51
1
52
0
53
8
54
74
55
0
56
1
57
1
58
15
59
95
60
0
61
1
62
0
63
5
64
61
65
0
66
1
67
1
68
87
69
87
70
0
71
1
72
1
73
24
74
74
75
0
76
0
77
0
78
95
79
32
80
0
81
0
82
0
83
10
84
96
85
0
86
1
87
1
88
79
89
15
90
0
91
0
92
1
93
34
94
27
95
0
96
1
97
0
98
0
99
56
100
0
101
0
102
1
103
2
104
87
105
1
106
0
107
0
108
78
109
40
110
1
111
1
112
0
113
12
114
25
115
1
116
1
117
1
118
84
119
83
120
0
121
0
122
0
123
77
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff