XML file generation

[hbourbouh]

The following error:
(Error)[Verification] Java exception occurred:
org.xml.sax.SAXParseException; systemId: file:/home/bourbouh/Documents/coco-team/cocoSim/test/properties/lustre_files/src_safe_math_functions/safe_math_functions.property_safe_math_functions_Property.xml; lineNumber: 1; columnNumber: 1; Content is not allowed in prolog.
at org.apache.xerces.parsers.DOMParser.parse(Unknown Source)
at org.apache.xerces.jaxp.DocumentBuilderImpl.parse(Unknown Source)
at javax.xml.parsers.DocumentBuilder.parse(Unknown Source)

is related to the generation of xml file that contains the Answer:

Python bool, int, long or float expected
xml version="1.0"?
Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
Property name="safe_math_functions_Property"
Date>2017-02-06 11:47</Date
Lustre2Horn unit="sec">0.00</Lustre2Horn
Parse unit="sec">0.00</Parse
Query unit="sec">0.01</Query
Answer>SAFE</Answer
Property
Results

As you see the first line is the cause of the error,

[lememta]

Can you attach the lustre file that triggers this error?

[hbourbouh]

safe_1_integers (copie).lus.txt

[hbourbouh]

zustre --node safe_1_integers --matlab safe_1_integers.lus
[INFO] 2017-02-06 15:24:33,156 zustre 162 [No pre-processing ]
[INFO] 2017-02-06 15:24:33,156 zustre 83 [Hornifiying ... safe_1_integers.lus ]
[INFO] 2017-02-06 15:24:33,299 zustre 177 [Successful Horn Generation ... /home/bourbouh/Documents/coco-team/regression-test/simulink/property_test/lustre_files/src_safe_1_integers/safe_1_integers.smt2 ]
(error "line 233 column 7: Sort mismatch at argument #1 for function (declare-fun and (Bool Bool) Bool) supplied sort is Int")
Process Process-1:
Traceback (most recent call last):
File "/usr/lib/python2.7/multiprocessing/process.py", line 258, in _bootstrap
self.run()
File "/usr/lib/python2.7/multiprocessing/process.py", line 114, in run
self._target(*self._args, **self._kwargs)
File "/home/bourbouh/Documents/cavale/local/bin/zustre", line 78, in main
zus.encodeAndSolve()
File "/home/bourbouh/Documents/cavale/local/lib/zustrepy/src/zustre.py", line 178, in encodeAndSolve
q = self.fp.parse_file (hornFormulas)
File "src/api/python/z3.py", line 6444, in parse_file
File "src/api/python/z3core.py", line 4734, in Z3_fixedpoint_from_file
Z3Exception: parser error

[lememta]

The observer node has to have one boolean output.

[lememta]

The only observer I see is 'zustre --node safe_1_integers_outside --matlab test.lus'

[hbourbouh]

Sorry for that yeah there is two observers/
safe_1_integers_Subsystem_inside

[hbourbouh]

Zustre command is working, it's CEX parsing XML in Cocosim that is not working

[lememta]

Both safe_1_integers_Subsystem_inside and safe_1_integers_outside are safe. Can you please send me the correct lustre and command that you used?

[hbourbouh]

the file is good and zustre is good,
the error is in xml generation,
Python bool, int, long or float expected
is in the xml file

[lememta]

OK, I can now replicate the error with zustre --node safe_1_integers_outside --matlab test.lus --xml --cg

[lememta]

I have fixed this issue in the latest version of zustre from devel branch. Please try it out.

[hbourbouh]

It is good now, we still have the problem in matlab.emf generation, we generate only one node