| Summary: | Produced legible .xtr file with wrong "transition" data | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | DejaniraAI <da13683> |
| Component: | libutap | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | critical | CC: | adavid |
| Priority: | P5 | ||
| Version: | unspecified | ||
| Hardware: | Other | ||
| OS: | All | ||
| Architecture: | x86_64 (64bit) | ||
| Attachments: | Model, property and trace with bug, produced with cover and libutap tracer | ||
Hi, the UTAP library has changed a lot, could you try the new snapshot? http://people.cs.aau.dk/~marius/beta/libutap-0.92.tar.gz Created attachment 276 [details]
Model, property and trace with bug, produced with cover and libutap tracer
(In reply to Marius Mikučionis from comment #1) > Hi, the UTAP library has changed a lot, > could you try the new snapshot? > http://people.cs.aau.dk/~marius/beta/libutap-0.92.tar.gz Hi Marius, I just tried the new libutap snapshot, with the same results. Additionally, I had a compilation error: in the pretty.cpp file, line #include "utap/sbmlconverter.h" refers to a file that is not there, in the /src/utap folder. I commented this line out, and libutap compiled without any problem. When running the commands: UPPAAL_COMPILE_ONLY=1 ./verifyta prism.xml - | tracer - trace-file-2.xtr >> legible.tr the same bug I previously reported continues to appear. I am attaching here my UPPAAL model, the property, the computed trace (with cover), the output from tracer, and an annotated version where I point out the errors, for reproducibility. Thank you, Dejanira I cannot load your trace with your model in Uppaal 4.1.19 -- they don't seem to match, probably the order of edges has changed and thus impossible to read. One has to have the very same engine producing the system description (UPPAAL_COMPILE_ONLY part) in order to read the trace. Now that you mention CORA, I think that it is a bug in CORAs output of a trace: I tried loading trace-2.xtr into uppaal-cora-060910 and saving it again and it produces a different trace file. It seems to output larger variable table. So at least the model and trace files do not agree on a variable count. A few remarks on why it is CORAs issue and not tracer's: the xtr file contains state dumps and transition identifiers so in principle one can read the state dumps and match variable values one-by-one (the variable values are enumerated in the same order as they are declared, or as shown in simulator). There are the following problems with your trace file: 1) the transition numbers do not match the model: the very first transition is impossible with respect to process Robot (Robot should start from initial location, but the first transition is different). 2) the variable values also seem to be out-of-order, e.g. h_pressureOk becomes true on 10th transition in CORA, but in the trace dump it is already in the 6th transition, so at least the variable names do not match. I tried with libutap 0.90, 0.91, 0.92 (the latest snapshot) using "./configure --enable-cora" and they show identical symptoms. (0.80 crashes with segfault -- so not sure I've fixed compile errors properly). > When running the commands:
> UPPAAL_COMPILE_ONLY=1 ./verifyta prism.xml - | tracer - trace-file-2.xtr >>
> legible.tr
> the same bug I previously reported continues to appear. I am attaching here
> my UPPAAL model, the property, the computed trace (with cover), the output
> from tracer, and an annotated version where I point out the errors, for
> reproducibility.
Now I noticed it's not CORA but Cover: you need to use the same verifyta engine as Cover to compile the system description. Perhaps a very close version of Uppaal would do. It might be that Cover adds some variables to the system and/or parsers the edges in different order and thus tracer fails to match them.
The trace file traces-2.xtr can be opened without any problem in UPPAAL 4.0.14, although the model was generated in UPPAAL 4.1.19. I used COVER 1.4 to generate the trace (the most recent version of COVER according to the webpage). Indeed, UPPAAL 4.1.19 cannot open the trace. UPPAAL 4.0.14 correctly displays all the transitions and variable values in the trace. Then, I used verifyta supplied in the .zip file for the UPPAAL 4.0.14 installation. I also tried the verifyta and verifyta-openmpi, supplied in the UPPAAL 4.1.19, and I still get the same issue with the produced legible trace (using the same libutap 0.92). I even tried with the verifyta in version 4.1.20.beta6 (others such as 4.1.20.beta4 did not work at all). If you think the problem is in COVER, is there any other version of it (besides 1.4) that I could try? What would be the best match between the COVER version and the verifyta version? Thank you for your time. |
I used "tracer" to translate a trace from numerical format to string format (thus, legible). I keep encountering that the wrong "transition" is printed, although the "state" field (and all the current locations and variable values) are correct. E.g. (to illustrate the kind of error, not run in reality): state: a1.0 a2.0 a3.0 v=0 w=0 x=0 transition a1.3 -> a1.4 {guards;...; v=3} state: a1.1 a2.0 a3.0 v=1 w=0 x=0 The correct "transition" would have been: a1.0 -> a1.1 {guards;...; v=1} I am guessing the error could be in the reading of the "choice of transition", that might be offset, since the automata that has transitioned is correct. Also, I have noticed that sometimes the transitions that are shown subsequently correspond to rewritting the previous transition with other choice, e.g.: state: a1.0 a2.0 a3.0 v=0 w=0 x=0 transition a1.0 -> a1.1 {guards;...; v=1} state: a1.1 a2.0 a3.0 v=1 w=0 x=0 transition a1.0 -> a1.1 {guards;...; v=100} state: a1.2 a2.0 a3.0 v=2 w=0 x=0 the second transition should have been: transition a1.1 -> a1.2 {guards;...; v=2}