Project

General

Profile

Revision b7026160

View differences:

regression_tests/CMakeLists.txt
19 19
else()
20 20
	message("javac not found")
21 21
endif()
22

  
23

  
22 24
add_subdirectory(lustre_files)
23 25

  
24 26
    
regression_tests/lustre_files/success/kind_fmcad08/CMakeLists.txt
1 1
cmake_minimum_required(VERSION 2.8.4)
2 2

  
3 3
add_subdirectory(large)
4
add_subdirectory(memory1)
regression_tests/lustre_files/success/kind_fmcad08/large/CEX/CMakeLists.txt
77 77
					OPTS "-horn")
78 78
					
79 79
	set(LUS_OPTS_CUT ${LUSTRE_OPTS_POSTFIX_${L}})
80
	add_test(NAME Kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
81
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}_${LUSTRE_NODE_OPT}_${LUS_OPTS_CUT}} 
80
	add_test(NAME Kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT}
81
			COMMAND  ${LUSTRE_COMPILER} ${LUSTREC_ARGS_${L}__${LUS_OPTS_CUT}} 
82 82
	)
83 83

  
84 84
	Zustre_Compile(LUS_FILE ${lus_file}
......
96 96
	)
97 97
	SET_TESTS_PROPERTIES (  Kind_fmcad08_large_CEX_COMPIL_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
98 98
			PROPERTIES FAIL_REGULAR_EXPRESSION "AssertionError;ERROR;Failed"
99
					DEPENDS Kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT})
99
					DEPENDS Kind_fmcad08_large_CEX_COMPIL_LUSTRE_${L}__${LUS_OPTS_CUT})
100 100
			
101 101
			
102 102
	add_test(NAME Kind_fmcad08_large_CEX_TAIL1_ZUSTRE_${L}_${ZUSTRE_NODE_OPT}_${ZUS_OPTS_CUT}
regression_tests/lustre_files/success/kind_fmcad08/memory1/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
	endif()
59
    if( ${${L}_zustre_output} MATCHES "<Answer>CEX</Answer>")
60
		#message("${L}.xml is CEX")
61
		set(ZUSTRE_ANSWER_${L} "CEX")
62
	elseif( ${${L}_zustre_output} MATCHES "<Answer>SAFE</Answer>")
63
		#message("${L}.xml is SAFE")
64
		set(ZUSTRE_ANSWER_${L} "SAFE")
65
	elseif( ${${L}_zustre_output} MATCHES "<Answer>TIMEOUT</Answer>")
66
		#message("${L}.xml is TIMEOUT")
67
		set(ZUSTRE_ANSWER_${L} "TIMEOUT")
68
	else()
69
		#message("${L}.xml is Error")
70
		set(ZUSTRE_ANSWER_${L} "ERROR")
71
	endif()
72
ENDFOREACH()
73

  
74

  
75

  
76

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

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

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

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

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

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

  
194
	endif()
195
	
196
ENDFOREACH()
197
add_custom_target(Kind_fmcad08_memory1 COMMAND ${CMAKE_CTEST_COMMAND} -R Kind_fmcad08_memory1)
198

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_1.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-19 15:52</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.13</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10.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-19 15:46</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.25</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e1_3587_e3_2749.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-19 16:05</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.16</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e1_3587_e7_872.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-19 16:06</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.30</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="Sofar">
11
            <Stream name="Sofar" type="bool">
12
                <Value instant="0">1</Value>
13
                <Value instant="1">1</Value>
14
           </Stream>
15
            <Stream name="X" type="bool">
16
                <Value instant="0">1</Value>
17
                <Value instant="1">1</Value>
18
           </Stream>
19
            <Stream name="X" type="bool">
20
                <Value instant="0">1</Value>
21
                <Value instant="1">1</Value>
22
           </Stream>
23
         </Node>
24
 <Node name ="top">
25
            <Stream name="exclusive" type="int">
26
                <Value instant="0">0</Value>
27
                <Value instant="1">0</Value>
28
           </Stream>
29
            <Stream name="exclusive" type="int">
30
                <Value instant="0">0</Value>
31
                <Value instant="1">0</Value>
32
           </Stream>
33
            <Stream name="e05" type="bool">
34
                <Value instant="0">1</Value>
35
                <Value instant="1">1</Value>
36
           </Stream>
37
            <Stream name="e05" type="bool">
38
                <Value instant="0">1</Value>
39
                <Value instant="1">1</Value>
40
           </Stream>
41
            <Stream name="init_invalid" type="int">
42
                <Value instant="0">-1</Value>
43
                <Value instant="1">1</Value>
44
           </Stream>
45
            <Stream name="init_invalid" type="int">
46
                <Value instant="0">-1</Value>
47
                <Value instant="1">1</Value>
48
           </Stream>
49
            <Stream name="Sofar" type="bool">
50
                <Value instant="0">1</Value>
51
                <Value instant="1">1</Value>
52
           </Stream>
53
            <Stream name="mem_init" type="int">
54
                <Value instant="0">-1</Value>
55
                <Value instant="1">-1</Value>
56
           </Stream>
57
            <Stream name="shared_dirty" type="int">
58
                <Value instant="0">0</Value>
59
                <Value instant="1">0</Value>
60
           </Stream>
61
            <Stream name="shared_dirty" type="int">
62
                <Value instant="0">0</Value>
63
                <Value instant="1">0</Value>
64
           </Stream>
65
            <Stream name="shared_dirty" type="int">
66
                <Value instant="0">0</Value>
67
                <Value instant="1">0</Value>
68
           </Stream>
69
            <Stream name="OK" type="bool">
70
                <Value instant="0">1</Value>
71
                <Value instant="1">1</Value>
72
           </Stream>
73
            <Stream name="e08" type="bool">
74
                <Value instant="0">1</Value>
75
                <Value instant="1">1</Value>
76
           </Stream>
77
            <Stream name="e09" type="bool">
78
                <Value instant="0">1</Value>
79
                <Value instant="1">1</Value>
80
           </Stream>
81
            <Stream name="e06" type="bool">
82
                <Value instant="0">1</Value>
83
                <Value instant="1">1</Value>
84
           </Stream>
85
            <Stream name="e10" type="bool">
86
                <Value instant="0">1</Value>
87
                <Value instant="1">1</Value>
88
           </Stream>
89
            <Stream name="e04" type="bool">
90
                <Value instant="0">1</Value>
91
                <Value instant="1">1</Value>
92
           </Stream>
93
            <Stream name="e12" type="bool">
94
                <Value instant="0">1</Value>
95
                <Value instant="1">1</Value>
96
           </Stream>
97
            <Stream name="e02" type="bool">
98
                <Value instant="0">1</Value>
99
                <Value instant="1">1</Value>
100
           </Stream>
101
            <Stream name="e03" type="bool">
102
                <Value instant="0">1</Value>
103
                <Value instant="1">1</Value>
104
           </Stream>
105
            <Stream name="invalid" type="int">
106
                <Value instant="0">-1</Value>
107
                <Value instant="1">-1</Value>
108
           </Stream>
109
            <Stream name="e01" type="bool">
110
                <Value instant="0">1</Value>
111
                <Value instant="1">1</Value>
112
           </Stream>
113
            <Stream name="e11" type="bool">
114
                <Value instant="0">1</Value>
115
                <Value instant="1">1</Value>
116
           </Stream>
117
            <Stream name="dirty" type="int">
118
                <Value instant="0">0</Value>
119
                <Value instant="1">0</Value>
120
           </Stream>
121
            <Stream name="e07" type="bool">
122
                <Value instant="0">1</Value>
123
                <Value instant="1">1</Value>
124
           </Stream>
125
            <Stream name="e07" type="bool">
126
                <Value instant="0">1</Value>
127
                <Value instant="1">1</Value>
128
           </Stream>
129
            <Stream name="shared" type="int">
130
                <Value instant="0">0</Value>
131
                <Value instant="1">0</Value>
132
           </Stream>
133
            <Stream name="shared" type="int">
134
                <Value instant="0">0</Value>
135
                <Value instant="1">0</Value>
136
           </Stream>
137
         </Node>
138
 <Node name ="excludes12">
139
            <Stream name="excludes" type="bool">
140
                <Value instant="0">1</Value>
141
                <Value instant="1">1</Value>
142
           </Stream>
143
            <Stream name="X2" type="bool">
144
                <Value instant="0">1</Value>
145
                <Value instant="1">1</Value>
146
           </Stream>
147
            <Stream name="X8" type="bool">
148
                <Value instant="0">1</Value>
149
                <Value instant="1">1</Value>
150
           </Stream>
151
            <Stream name="X9" type="bool">
152
                <Value instant="0">1</Value>
153
                <Value instant="1">1</Value>
154
           </Stream>
155
            <Stream name="X11" type="bool">
156
                <Value instant="0">1</Value>
157
                <Value instant="1">1</Value>
158
           </Stream>
159
            <Stream name="X10" type="bool">
160
                <Value instant="0">1</Value>
161
                <Value instant="1">1</Value>
162
           </Stream>
163
            <Stream name="X3" type="bool">
164
                <Value instant="0">1</Value>
165
                <Value instant="1">1</Value>
166
           </Stream>
167
            <Stream name="X12" type="bool">
168
                <Value instant="0">1</Value>
169
                <Value instant="1">1</Value>
170
           </Stream>
171
            <Stream name="X1" type="bool">
172
                <Value instant="0">1</Value>
173
                <Value instant="1">1</Value>
174
           </Stream>
175
            <Stream name="X6" type="bool">
176
                <Value instant="0">1</Value>
177
                <Value instant="1">1</Value>
178
           </Stream>
179
            <Stream name="X7" type="bool">
180
                <Value instant="0">1</Value>
181
                <Value instant="1">1</Value>
182
           </Stream>
183
            <Stream name="X4" type="bool">
184
                <Value instant="0">1</Value>
185
                <Value instant="1">1</Value>
186
           </Stream>
187
            <Stream name="X5" type="bool">
188
                <Value instant="0">1</Value>
189
                <Value instant="1">1</Value>
190
           </Stream>
191
         </Node>
192
 <Node name ="DRAGON">
193
            <Stream name="exclusive" type="int">
194
                <Value instant="0">0</Value>
195
                <Value instant="1">0</Value>
196
           </Stream>
197
            <Stream name="exclusive" type="int">
198
                <Value instant="0">0</Value>
199
                <Value instant="1">0</Value>
200
           </Stream>
201
            <Stream name="e05" type="bool">
202
                <Value instant="0">1</Value>
203
                <Value instant="1">1</Value>
204
           </Stream>
205
            <Stream name="init_invalid" type="int">
206
                <Value instant="0">-1</Value>
207
                <Value instant="1">1</Value>
208
           </Stream>
209
            <Stream name="init_invalid" type="int">
210
                <Value instant="0">-1</Value>
211
                <Value instant="1">1</Value>
212
           </Stream>
213
            <Stream name="mem_init" type="int">
214
                <Value instant="0">-1</Value>
215
                <Value instant="1">-1</Value>
216
           </Stream>
217
            <Stream name="invalid" type="int">
218
                <Value instant="0">-1</Value>
219
                <Value instant="1">-1</Value>
220
           </Stream>
221
            <Stream name="invalid" type="int">
222
                <Value instant="0">-1</Value>
223
                <Value instant="1">-1</Value>
224
           </Stream>
225
            <Stream name="invalid" type="int">
226
                <Value instant="0">-1</Value>
227
                <Value instant="1">-1</Value>
228
           </Stream>
229
            <Stream name="e08" type="bool">
230
                <Value instant="0">1</Value>
231
                <Value instant="1">1</Value>
232
           </Stream>
233
            <Stream name="e09" type="bool">
234
                <Value instant="0">1</Value>
235
                <Value instant="1">1</Value>
236
           </Stream>
237
            <Stream name="e06" type="bool">
238
                <Value instant="0">1</Value>
239
                <Value instant="1">1</Value>
240
           </Stream>
241
            <Stream name="e10" type="bool">
242
                <Value instant="0">1</Value>
243
                <Value instant="1">1</Value>
244
           </Stream>
245
            <Stream name="e04" type="bool">
246
                <Value instant="0">1</Value>
247
                <Value instant="1">1</Value>
248
           </Stream>
249
            <Stream name="e12" type="bool">
250
                <Value instant="0">1</Value>
251
                <Value instant="1">1</Value>
252
           </Stream>
253
            <Stream name="e02" type="bool">
254
                <Value instant="0">1</Value>
255
                <Value instant="1">1</Value>
256
           </Stream>
257
            <Stream name="e03" type="bool">
258
                <Value instant="0">1</Value>
259
                <Value instant="1">1</Value>
260
           </Stream>
261
            <Stream name="shared_dirty" type="int">
262
                <Value instant="0">0</Value>
263
                <Value instant="1">0</Value>
264
           </Stream>
265
            <Stream name="e01" type="bool">
266
                <Value instant="0">1</Value>
267
                <Value instant="1">1</Value>
268
           </Stream>
269
            <Stream name="e11" type="bool">
270
                <Value instant="0">1</Value>
271
                <Value instant="1">1</Value>
272
           </Stream>
273
            <Stream name="dirty" type="int">
274
                <Value instant="0">0</Value>
275
                <Value instant="1">0</Value>
276
           </Stream>
277
            <Stream name="e07" type="bool">
278
                <Value instant="0">1</Value>
279
                <Value instant="1">1</Value>
280
           </Stream>
281
            <Stream name="e07" type="bool">
282
                <Value instant="0">1</Value>
283
                <Value instant="1">1</Value>
284
           </Stream>
285
            <Stream name="shared" type="int">
286
                <Value instant="0">0</Value>
287
                <Value instant="1">0</Value>
288
           </Stream>
289
            <Stream name="shared" type="int">
290
                <Value instant="0">0</Value>
291
                <Value instant="1">0</Value>
292
           </Stream>
293
            <Stream name="erreur" type="bool">
294
                <Value instant="0">1</Value>
295
                <Value instant="1">1</Value>
296
           </Stream>
297
         </Node>
298

  
299
      </Counterexample>
300
     </Property>
301
   </Results>
302

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e1_998.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-19 16:05</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.17</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e2_2785_e3_1744.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-19 15:54</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.18</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e2_402.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-19 16:05</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.22</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e3_144_e5_2046.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-19 15:52</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.16</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e3_144_e7_523.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-19 15:46</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.38</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="Sofar">
11
            <Stream name="Sofar" type="bool">
12
                <Value instant="0">1</Value>
13
                <Value instant="1">1</Value>
14
           </Stream>
15
            <Stream name="X" type="bool">
16
                <Value instant="0">1</Value>
17
                <Value instant="1">1</Value>
18
           </Stream>
19
            <Stream name="X" type="bool">
20
                <Value instant="0">1</Value>
21
                <Value instant="1">1</Value>
22
           </Stream>
23
         </Node>
24
 <Node name ="top">
25
            <Stream name="exclusive" type="int">
26
                <Value instant="0">0</Value>
27
                <Value instant="1">0</Value>
28
           </Stream>
29
            <Stream name="exclusive" type="int">
30
                <Value instant="0">0</Value>
31
                <Value instant="1">0</Value>
32
           </Stream>
33
            <Stream name="e05" type="bool">
34
                <Value instant="0">1</Value>
35
                <Value instant="1">1</Value>
36
           </Stream>
37
            <Stream name="e05" type="bool">
38
                <Value instant="0">1</Value>
39
                <Value instant="1">1</Value>
40
           </Stream>
41
            <Stream name="init_invalid" type="int">
42
                <Value instant="0">-1</Value>
43
                <Value instant="1">1</Value>
44
           </Stream>
45
            <Stream name="init_invalid" type="int">
46
                <Value instant="0">-1</Value>
47
                <Value instant="1">1</Value>
48
           </Stream>
49
            <Stream name="Sofar" type="bool">
50
                <Value instant="0">1</Value>
51
                <Value instant="1">1</Value>
52
           </Stream>
53
            <Stream name="mem_init" type="int">
54
                <Value instant="0">-1</Value>
55
                <Value instant="1">-1</Value>
56
           </Stream>
57
            <Stream name="shared_dirty" type="int">
58
                <Value instant="0">0</Value>
59
                <Value instant="1">0</Value>
60
           </Stream>
61
            <Stream name="shared_dirty" type="int">
62
                <Value instant="0">0</Value>
63
                <Value instant="1">0</Value>
64
           </Stream>
65
            <Stream name="shared_dirty" type="int">
66
                <Value instant="0">0</Value>
67
                <Value instant="1">0</Value>
68
           </Stream>
69
            <Stream name="OK" type="bool">
70
                <Value instant="0">1</Value>
71
                <Value instant="1">1</Value>
72
           </Stream>
73
            <Stream name="e08" type="bool">
74
                <Value instant="0">1</Value>
75
                <Value instant="1">1</Value>
76
           </Stream>
77
            <Stream name="e09" type="bool">
78
                <Value instant="0">1</Value>
79
                <Value instant="1">1</Value>
80
           </Stream>
81
            <Stream name="e06" type="bool">
82
                <Value instant="0">1</Value>
83
                <Value instant="1">1</Value>
84
           </Stream>
85
            <Stream name="e10" type="bool">
86
                <Value instant="0">1</Value>
87
                <Value instant="1">1</Value>
88
           </Stream>
89
            <Stream name="e04" type="bool">
90
                <Value instant="0">1</Value>
91
                <Value instant="1">1</Value>
92
           </Stream>
93
            <Stream name="e12" type="bool">
94
                <Value instant="0">1</Value>
95
                <Value instant="1">1</Value>
96
           </Stream>
97
            <Stream name="e02" type="bool">
98
                <Value instant="0">1</Value>
99
                <Value instant="1">1</Value>
100
           </Stream>
101
            <Stream name="e03" type="bool">
102
                <Value instant="0">1</Value>
103
                <Value instant="1">1</Value>
104
           </Stream>
105
            <Stream name="invalid" type="int">
106
                <Value instant="0">-1</Value>
107
                <Value instant="1">-1</Value>
108
           </Stream>
109
            <Stream name="e01" type="bool">
110
                <Value instant="0">1</Value>
111
                <Value instant="1">1</Value>
112
           </Stream>
113
            <Stream name="e11" type="bool">
114
                <Value instant="0">1</Value>
115
                <Value instant="1">1</Value>
116
           </Stream>
117
            <Stream name="dirty" type="int">
118
                <Value instant="0">0</Value>
119
                <Value instant="1">0</Value>
120
           </Stream>
121
            <Stream name="e07" type="bool">
122
                <Value instant="0">1</Value>
123
                <Value instant="1">1</Value>
124
           </Stream>
125
            <Stream name="e07" type="bool">
126
                <Value instant="0">1</Value>
127
                <Value instant="1">1</Value>
128
           </Stream>
129
            <Stream name="shared" type="int">
130
                <Value instant="0">0</Value>
131
                <Value instant="1">0</Value>
132
           </Stream>
133
            <Stream name="shared" type="int">
134
                <Value instant="0">0</Value>
135
                <Value instant="1">0</Value>
136
           </Stream>
137
         </Node>
138
 <Node name ="excludes12">
139
            <Stream name="excludes" type="bool">
140
                <Value instant="0">1</Value>
141
                <Value instant="1">1</Value>
142
           </Stream>
143
            <Stream name="X2" type="bool">
144
                <Value instant="0">1</Value>
145
                <Value instant="1">1</Value>
146
           </Stream>
147
            <Stream name="X8" type="bool">
148
                <Value instant="0">1</Value>
149
                <Value instant="1">1</Value>
150
           </Stream>
151
            <Stream name="X9" type="bool">
152
                <Value instant="0">1</Value>
153
                <Value instant="1">1</Value>
154
           </Stream>
155
            <Stream name="X11" type="bool">
156
                <Value instant="0">1</Value>
157
                <Value instant="1">1</Value>
158
           </Stream>
159
            <Stream name="X10" type="bool">
160
                <Value instant="0">1</Value>
161
                <Value instant="1">1</Value>
162
           </Stream>
163
            <Stream name="X3" type="bool">
164
                <Value instant="0">1</Value>
165
                <Value instant="1">1</Value>
166
           </Stream>
167
            <Stream name="X12" type="bool">
168
                <Value instant="0">1</Value>
169
                <Value instant="1">1</Value>
170
           </Stream>
171
            <Stream name="X1" type="bool">
172
                <Value instant="0">1</Value>
173
                <Value instant="1">1</Value>
174
           </Stream>
175
            <Stream name="X6" type="bool">
176
                <Value instant="0">1</Value>
177
                <Value instant="1">1</Value>
178
           </Stream>
179
            <Stream name="X7" type="bool">
180
                <Value instant="0">1</Value>
181
                <Value instant="1">1</Value>
182
           </Stream>
183
            <Stream name="X4" type="bool">
184
                <Value instant="0">1</Value>
185
                <Value instant="1">1</Value>
186
           </Stream>
187
            <Stream name="X5" type="bool">
188
                <Value instant="0">1</Value>
189
                <Value instant="1">1</Value>
190
           </Stream>
191
         </Node>
192
 <Node name ="DRAGON">
193
            <Stream name="exclusive" type="int">
194
                <Value instant="0">0</Value>
195
                <Value instant="1">0</Value>
196
           </Stream>
197
            <Stream name="exclusive" type="int">
198
                <Value instant="0">0</Value>
199
                <Value instant="1">0</Value>
200
           </Stream>
201
            <Stream name="e05" type="bool">
202
                <Value instant="0">1</Value>
203
                <Value instant="1">1</Value>
204
           </Stream>
205
            <Stream name="init_invalid" type="int">
206
                <Value instant="0">-1</Value>
207
                <Value instant="1">1</Value>
208
           </Stream>
209
            <Stream name="init_invalid" type="int">
210
                <Value instant="0">-1</Value>
211
                <Value instant="1">1</Value>
212
           </Stream>
213
            <Stream name="mem_init" type="int">
214
                <Value instant="0">-1</Value>
215
                <Value instant="1">-1</Value>
216
           </Stream>
217
            <Stream name="invalid" type="int">
218
                <Value instant="0">-1</Value>
219
                <Value instant="1">-1</Value>
220
           </Stream>
221
            <Stream name="invalid" type="int">
222
                <Value instant="0">-1</Value>
223
                <Value instant="1">-1</Value>
224
           </Stream>
225
            <Stream name="invalid" type="int">
226
                <Value instant="0">-1</Value>
227
                <Value instant="1">-1</Value>
228
           </Stream>
229
            <Stream name="e08" type="bool">
230
                <Value instant="0">1</Value>
231
                <Value instant="1">1</Value>
232
           </Stream>
233
            <Stream name="e09" type="bool">
234
                <Value instant="0">1</Value>
235
                <Value instant="1">1</Value>
236
           </Stream>
237
            <Stream name="e06" type="bool">
238
                <Value instant="0">1</Value>
239
                <Value instant="1">1</Value>
240
           </Stream>
241
            <Stream name="e10" type="bool">
242
                <Value instant="0">1</Value>
243
                <Value instant="1">1</Value>
244
           </Stream>
245
            <Stream name="e04" type="bool">
246
                <Value instant="0">1</Value>
247
                <Value instant="1">1</Value>
248
           </Stream>
249
            <Stream name="e12" type="bool">
250
                <Value instant="0">1</Value>
251
                <Value instant="1">1</Value>
252
           </Stream>
253
            <Stream name="e02" type="bool">
254
                <Value instant="0">1</Value>
255
                <Value instant="1">1</Value>
256
           </Stream>
257
            <Stream name="e03" type="bool">
258
                <Value instant="0">1</Value>
259
                <Value instant="1">1</Value>
260
           </Stream>
261
            <Stream name="shared_dirty" type="int">
262
                <Value instant="0">0</Value>
263
                <Value instant="1">0</Value>
264
           </Stream>
265
            <Stream name="e01" type="bool">
266
                <Value instant="0">1</Value>
267
                <Value instant="1">1</Value>
268
           </Stream>
269
            <Stream name="e11" type="bool">
270
                <Value instant="0">1</Value>
271
                <Value instant="1">1</Value>
272
           </Stream>
273
            <Stream name="dirty" type="int">
274
                <Value instant="0">0</Value>
275
                <Value instant="1">0</Value>
276
           </Stream>
277
            <Stream name="e07" type="bool">
278
                <Value instant="0">1</Value>
279
                <Value instant="1">1</Value>
280
           </Stream>
281
            <Stream name="e07" type="bool">
282
                <Value instant="0">1</Value>
283
                <Value instant="1">1</Value>
284
           </Stream>
285
            <Stream name="shared" type="int">
286
                <Value instant="0">0</Value>
287
                <Value instant="1">0</Value>
288
           </Stream>
289
            <Stream name="shared" type="int">
290
                <Value instant="0">0</Value>
291
                <Value instant="1">0</Value>
292
           </Stream>
293
            <Stream name="erreur" type="bool">
294
                <Value instant="0">1</Value>
295
                <Value instant="1">1</Value>
296
           </Stream>
297
         </Node>
298

  
299
      </Counterexample>
300
     </Property>
301
   </Results>
302

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e3_3429.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-19 15:49</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.16</Query>
8
      <Answer>SAFE</Answer>
9
     </Property>
10
   </Results>
11

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e7_3861_e2_1020.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-19 15:52</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.30</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="Sofar">
11
            <Stream name="Sofar" type="bool">
12
                <Value instant="0">1</Value>
13
                <Value instant="1">1</Value>
14
           </Stream>
15
            <Stream name="X" type="bool">
16
                <Value instant="0">1</Value>
17
                <Value instant="1">1</Value>
18
           </Stream>
19
            <Stream name="X" type="bool">
20
                <Value instant="0">1</Value>
21
                <Value instant="1">1</Value>
22
           </Stream>
23
         </Node>
24
 <Node name ="top">
25
            <Stream name="exclusive" type="int">
26
                <Value instant="0">0</Value>
27
                <Value instant="1">0</Value>
28
           </Stream>
29
            <Stream name="exclusive" type="int">
30
                <Value instant="0">0</Value>
31
                <Value instant="1">0</Value>
32
           </Stream>
33
            <Stream name="e05" type="bool">
34
                <Value instant="0">1</Value>
35
                <Value instant="1">1</Value>
36
           </Stream>
37
            <Stream name="e05" type="bool">
38
                <Value instant="0">1</Value>
39
                <Value instant="1">1</Value>
40
           </Stream>
41
            <Stream name="init_invalid" type="int">
42
                <Value instant="0">-1</Value>
43
                <Value instant="1">1</Value>
44
           </Stream>
45
            <Stream name="init_invalid" type="int">
46
                <Value instant="0">-1</Value>
47
                <Value instant="1">1</Value>
48
           </Stream>
49
            <Stream name="Sofar" type="bool">
50
                <Value instant="0">1</Value>
51
                <Value instant="1">1</Value>
52
           </Stream>
53
            <Stream name="mem_init" type="int">
54
                <Value instant="0">-1</Value>
55
                <Value instant="1">-1</Value>
56
           </Stream>
57
            <Stream name="shared_dirty" type="int">
58
                <Value instant="0">0</Value>
59
                <Value instant="1">0</Value>
60
           </Stream>
61
            <Stream name="shared_dirty" type="int">
62
                <Value instant="0">0</Value>
63
                <Value instant="1">0</Value>
64
           </Stream>
65
            <Stream name="shared_dirty" type="int">
66
                <Value instant="0">0</Value>
67
                <Value instant="1">0</Value>
68
           </Stream>
69
            <Stream name="OK" type="bool">
70
                <Value instant="0">1</Value>
71
                <Value instant="1">1</Value>
72
           </Stream>
73
            <Stream name="e08" type="bool">
74
                <Value instant="0">1</Value>
75
                <Value instant="1">1</Value>
76
           </Stream>
77
            <Stream name="e09" type="bool">
78
                <Value instant="0">1</Value>
79
                <Value instant="1">1</Value>
80
           </Stream>
81
            <Stream name="e06" type="bool">
82
                <Value instant="0">1</Value>
83
                <Value instant="1">1</Value>
84
           </Stream>
85
            <Stream name="e10" type="bool">
86
                <Value instant="0">1</Value>
87
                <Value instant="1">1</Value>
88
           </Stream>
89
            <Stream name="e04" type="bool">
90
                <Value instant="0">1</Value>
91
                <Value instant="1">1</Value>
92
           </Stream>
93
            <Stream name="e12" type="bool">
94
                <Value instant="0">1</Value>
95
                <Value instant="1">1</Value>
96
           </Stream>
97
            <Stream name="e02" type="bool">
98
                <Value instant="0">1</Value>
99
                <Value instant="1">1</Value>
100
           </Stream>
101
            <Stream name="e03" type="bool">
102
                <Value instant="0">1</Value>
103
                <Value instant="1">1</Value>
104
           </Stream>
105
            <Stream name="invalid" type="int">
106
                <Value instant="0">-1</Value>
107
                <Value instant="1">-1</Value>
108
           </Stream>
109
            <Stream name="e01" type="bool">
110
                <Value instant="0">1</Value>
111
                <Value instant="1">1</Value>
112
           </Stream>
113
            <Stream name="e11" type="bool">
114
                <Value instant="0">1</Value>
115
                <Value instant="1">1</Value>
116
           </Stream>
117
            <Stream name="dirty" type="int">
118
                <Value instant="0">0</Value>
119
                <Value instant="1">0</Value>
120
           </Stream>
121
            <Stream name="e07" type="bool">
122
                <Value instant="0">1</Value>
123
                <Value instant="1">1</Value>
124
           </Stream>
125
            <Stream name="e07" type="bool">
126
                <Value instant="0">1</Value>
127
                <Value instant="1">1</Value>
128
           </Stream>
129
            <Stream name="shared" type="int">
130
                <Value instant="0">0</Value>
131
                <Value instant="1">0</Value>
132
           </Stream>
133
            <Stream name="shared" type="int">
134
                <Value instant="0">0</Value>
135
                <Value instant="1">0</Value>
136
           </Stream>
137
         </Node>
138
 <Node name ="excludes12">
139
            <Stream name="excludes" type="bool">
140
                <Value instant="0">1</Value>
141
                <Value instant="1">1</Value>
142
           </Stream>
143
            <Stream name="X2" type="bool">
144
                <Value instant="0">1</Value>
145
                <Value instant="1">1</Value>
146
           </Stream>
147
            <Stream name="X8" type="bool">
148
                <Value instant="0">1</Value>
149
                <Value instant="1">1</Value>
150
           </Stream>
151
            <Stream name="X9" type="bool">
152
                <Value instant="0">1</Value>
153
                <Value instant="1">1</Value>
154
           </Stream>
155
            <Stream name="X11" type="bool">
156
                <Value instant="0">1</Value>
157
                <Value instant="1">1</Value>
158
           </Stream>
159
            <Stream name="X10" type="bool">
160
                <Value instant="0">1</Value>
161
                <Value instant="1">1</Value>
162
           </Stream>
163
            <Stream name="X3" type="bool">
164
                <Value instant="0">1</Value>
165
                <Value instant="1">1</Value>
166
           </Stream>
167
            <Stream name="X12" type="bool">
168
                <Value instant="0">1</Value>
169
                <Value instant="1">1</Value>
170
           </Stream>
171
            <Stream name="X1" type="bool">
172
                <Value instant="0">1</Value>
173
                <Value instant="1">1</Value>
174
           </Stream>
175
            <Stream name="X6" type="bool">
176
                <Value instant="0">1</Value>
177
                <Value instant="1">1</Value>
178
           </Stream>
179
            <Stream name="X7" type="bool">
180
                <Value instant="0">1</Value>
181
                <Value instant="1">1</Value>
182
           </Stream>
183
            <Stream name="X4" type="bool">
184
                <Value instant="0">1</Value>
185
                <Value instant="1">1</Value>
186
           </Stream>
187
            <Stream name="X5" type="bool">
188
                <Value instant="0">1</Value>
189
                <Value instant="1">1</Value>
190
           </Stream>
191
         </Node>
192
 <Node name ="DRAGON">
193
            <Stream name="exclusive" type="int">
194
                <Value instant="0">0</Value>
195
                <Value instant="1">0</Value>
196
           </Stream>
197
            <Stream name="exclusive" type="int">
198
                <Value instant="0">0</Value>
199
                <Value instant="1">0</Value>
200
           </Stream>
201
            <Stream name="e05" type="bool">
202
                <Value instant="0">1</Value>
203
                <Value instant="1">1</Value>
204
           </Stream>
205
            <Stream name="init_invalid" type="int">
206
                <Value instant="0">-1</Value>
207
                <Value instant="1">1</Value>
208
           </Stream>
209
            <Stream name="init_invalid" type="int">
210
                <Value instant="0">-1</Value>
211
                <Value instant="1">1</Value>
212
           </Stream>
213
            <Stream name="mem_init" type="int">
214
                <Value instant="0">-1</Value>
215
                <Value instant="1">-1</Value>
216
           </Stream>
217
            <Stream name="invalid" type="int">
218
                <Value instant="0">-1</Value>
219
                <Value instant="1">-1</Value>
220
           </Stream>
221
            <Stream name="invalid" type="int">
222
                <Value instant="0">-1</Value>
223
                <Value instant="1">-1</Value>
224
           </Stream>
225
            <Stream name="invalid" type="int">
226
                <Value instant="0">-1</Value>
227
                <Value instant="1">-1</Value>
228
           </Stream>
229
            <Stream name="e08" type="bool">
230
                <Value instant="0">1</Value>
231
                <Value instant="1">1</Value>
232
           </Stream>
233
            <Stream name="e09" type="bool">
234
                <Value instant="0">1</Value>
235
                <Value instant="1">1</Value>
236
           </Stream>
237
            <Stream name="e06" type="bool">
238
                <Value instant="0">1</Value>
239
                <Value instant="1">1</Value>
240
           </Stream>
241
            <Stream name="e10" type="bool">
242
                <Value instant="0">1</Value>
243
                <Value instant="1">1</Value>
244
           </Stream>
245
            <Stream name="e04" type="bool">
246
                <Value instant="0">1</Value>
247
                <Value instant="1">1</Value>
248
           </Stream>
249
            <Stream name="e12" type="bool">
250
                <Value instant="0">1</Value>
251
                <Value instant="1">1</Value>
252
           </Stream>
253
            <Stream name="e02" type="bool">
254
                <Value instant="0">1</Value>
255
                <Value instant="1">1</Value>
256
           </Stream>
257
            <Stream name="e03" type="bool">
258
                <Value instant="0">1</Value>
259
                <Value instant="1">1</Value>
260
           </Stream>
261
            <Stream name="shared_dirty" type="int">
262
                <Value instant="0">0</Value>
263
                <Value instant="1">0</Value>
264
           </Stream>
265
            <Stream name="e01" type="bool">
266
                <Value instant="0">1</Value>
267
                <Value instant="1">1</Value>
268
           </Stream>
269
            <Stream name="e11" type="bool">
270
                <Value instant="0">1</Value>
271
                <Value instant="1">1</Value>
272
           </Stream>
273
            <Stream name="dirty" type="int">
274
                <Value instant="0">0</Value>
275
                <Value instant="1">0</Value>
276
           </Stream>
277
            <Stream name="e07" type="bool">
278
                <Value instant="0">1</Value>
279
                <Value instant="1">1</Value>
280
           </Stream>
281
            <Stream name="e07" type="bool">
282
                <Value instant="0">1</Value>
283
                <Value instant="1">1</Value>
284
           </Stream>
285
            <Stream name="shared" type="int">
286
                <Value instant="0">0</Value>
287
                <Value instant="1">0</Value>
288
           </Stream>
289
            <Stream name="shared" type="int">
290
                <Value instant="0">0</Value>
291
                <Value instant="1">0</Value>
292
           </Stream>
293
            <Stream name="erreur" type="bool">
294
                <Value instant="0">1</Value>
295
                <Value instant="1">1</Value>
296
           </Stream>
297
         </Node>
298

  
299
      </Counterexample>
300
     </Property>
301
   </Results>
302

  
regression_tests/lustre_files/success/kind_fmcad08/memory1/DRAGON_10_e7_3861_e7_2180.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-19 15:52</Date>
5
      <Lustre2Horn unit="sec">0.00</Lustre2Horn>
6
      <Parse unit="sec">0.00</Parse>
7
      <Query unit="sec">0.26</Query>
8
      <Answer>CEX</Answer>
9
      <Counterexample>
10
         <Node name ="Sofar">
11
            <Stream name="Sofar" type="bool">
12
                <Value instant="0">1</Value>
13
                <Value instant="1">1</Value>
14
           </Stream>
15
            <Stream name="X" type="bool">
16
                <Value instant="0">1</Value>
17
                <Value instant="1">1</Value>
18
           </Stream>
19
            <Stream name="X" type="bool">
20
                <Value instant="0">1</Value>
21
                <Value instant="1">1</Value>
22
           </Stream>
23
         </Node>
24
 <Node name ="top">
25
            <Stream name="exclusive" type="int">
26
                <Value instant="0">0</Value>
27
                <Value instant="1">0</Value>
28
           </Stream>
29
            <Stream name="exclusive" type="int">
30
                <Value instant="0">0</Value>
31
                <Value instant="1">0</Value>
32
           </Stream>
33
            <Stream name="e05" type="bool">
34
                <Value instant="0">1</Value>
35
                <Value instant="1">1</Value>
36
           </Stream>
37
            <Stream name="e05" type="bool">
38
                <Value instant="0">1</Value>
39
                <Value instant="1">1</Value>
40
           </Stream>
41
            <Stream name="init_invalid" type="int">
42
                <Value instant="0">-1</Value>
43
                <Value instant="1">1</Value>
44
           </Stream>
45
            <Stream name="init_invalid" type="int">
46
                <Value instant="0">-1</Value>
47
                <Value instant="1">1</Value>
48
           </Stream>
49
            <Stream name="Sofar" type="bool">
50
                <Value instant="0">1</Value>
51
                <Value instant="1">1</Value>
52
           </Stream>
53
            <Stream name="mem_init" type="int">
54
                <Value instant="0">-1</Value>
55
                <Value instant="1">-1</Value>
56
           </Stream>
57
            <Stream name="shared_dirty" type="int">
58
                <Value instant="0">0</Value>
59
                <Value instant="1">0</Value>
60
           </Stream>
61
            <Stream name="shared_dirty" type="int">
62
                <Value instant="0">0</Value>
63
                <Value instant="1">0</Value>
64
           </Stream>
65
            <Stream name="shared_dirty" type="int">
66
                <Value instant="0">0</Value>
67
                <Value instant="1">0</Value>
68
           </Stream>
69
            <Stream name="OK" type="bool">
70
                <Value instant="0">1</Value>
71
                <Value instant="1">1</Value>
72
           </Stream>
73
            <Stream name="e08" type="bool">
74
                <Value instant="0">1</Value>
75
                <Value instant="1">1</Value>
76
           </Stream>
77
            <Stream name="e09" type="bool">
78
                <Value instant="0">1</Value>
79
                <Value instant="1">1</Value>
80
           </Stream>
81
            <Stream name="e06" type="bool">
82
                <Value instant="0">1</Value>
83
                <Value instant="1">1</Value>
84
           </Stream>
85
            <Stream name="e10" type="bool">
86
                <Value instant="0">1</Value>
87
                <Value instant="1">1</Value>
88
           </Stream>
89
            <Stream name="e04" type="bool">
90
                <Value instant="0">1</Value>
91
                <Value instant="1">1</Value>
92
           </Stream>
93
            <Stream name="e12" type="bool">
94
                <Value instant="0">1</Value>
95
                <Value instant="1">1</Value>
96
           </Stream>
97
            <Stream name="e02" type="bool">
98
                <Value instant="0">1</Value>
99
                <Value instant="1">1</Value>
100
           </Stream>
101
            <Stream name="e03" type="bool">
102
                <Value instant="0">1</Value>
103
                <Value instant="1">1</Value>
104
           </Stream>
105
            <Stream name="invalid" type="int">
106
                <Value instant="0">-1</Value>
107
                <Value instant="1">-1</Value>
108
           </Stream>
109
            <Stream name="e01" type="bool">
110
                <Value instant="0">1</Value>
111
                <Value instant="1">1</Value>
112
           </Stream>
113
            <Stream name="e11" type="bool">
114
                <Value instant="0">1</Value>
115
                <Value instant="1">1</Value>
116
           </Stream>
117
            <Stream name="dirty" type="int">
118
                <Value instant="0">0</Value>
119
                <Value instant="1">0</Value>
120
           </Stream>
121
            <Stream name="e07" type="bool">
122
                <Value instant="0">1</Value>
123
                <Value instant="1">1</Value>
124
           </Stream>
125
            <Stream name="e07" type="bool">
126
                <Value instant="0">1</Value>
127
                <Value instant="1">1</Value>
128
           </Stream>
129
            <Stream name="shared" type="int">
130
                <Value instant="0">0</Value>
131
                <Value instant="1">0</Value>
132
           </Stream>
133
            <Stream name="shared" type="int">
134
                <Value instant="0">0</Value>
135
                <Value instant="1">0</Value>
136
           </Stream>
137
         </Node>
138
 <Node name ="excludes12">
139
            <Stream name="excludes" type="bool">
140
                <Value instant="0">1</Value>
141
                <Value instant="1">1</Value>
142
           </Stream>
143
            <Stream name="X2" type="bool">
144
                <Value instant="0">1</Value>
145
                <Value instant="1">1</Value>
146
           </Stream>
147
            <Stream name="X8" type="bool">
148
                <Value instant="0">1</Value>
149
                <Value instant="1">1</Value>
150
           </Stream>
151
            <Stream name="X9" type="bool">
152
                <Value instant="0">1</Value>
153
                <Value instant="1">1</Value>
154
           </Stream>
155
            <Stream name="X11" type="bool">
156
                <Value instant="0">1</Value>
157
                <Value instant="1">1</Value>
158
           </Stream>
159
            <Stream name="X10" type="bool">
160
                <Value instant="0">1</Value>
161
                <Value instant="1">1</Value>
162
           </Stream>
163
            <Stream name="X3" type="bool">
164
                <Value instant="0">1</Value>
165
                <Value instant="1">1</Value>
166
           </Stream>
167
            <Stream name="X12" type="bool">
168
                <Value instant="0">1</Value>
169
                <Value instant="1">1</Value>
170
           </Stream>
171
            <Stream name="X1" type="bool">
172
                <Value instant="0">1</Value>
173
                <Value instant="1">1</Value>
174
           </Stream>
175
            <Stream name="X6" type="bool">
176
                <Value instant="0">1</Value>
177
                <Value instant="1">1</Value>
178
           </Stream>
179
            <Stream name="X7" type="bool">
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff