| Summary: | Incorrect result for batch run in verifier | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Allan Munck <allmun> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | RESOLVED FIXED | ||
| Severity: | critical | CC: | adavid |
| Priority: | P5 | ||
| Version: | 4.1.19 | ||
| Hardware: | PC | ||
| OS: | Windows 7 | ||
| Architecture: | |||
| Attachments: | A simple model that illustrates the problem | ||
Also, the external verifier "verifyta" produces different results than shown in the verifier tab in UPPAAL. Dear Alan Munck, Thanks for the report. I am trying to reproduce it and I observe the strange behavior (not satisfied in individual checks and erroneously satisfied in batch) with the first query: A[] APP.ShowingList imply APP.listSize() == MaxRftListLength The other 3 queries are satisfied (correctly). There is no newer public release, but there's a beta snapshot: http://people.cs.aau.dk/~marius/beta/uppaal-4.1.20-beta7.zip (it seems that this particular issue is fixed over there) Marius Fixed in the 4.1.20 release |
Created attachment 279 [details] A simple model that illustrates the problem The verification results are incorrect, when the queries are run as a batch (all selected) in the verifier tab in UPPAAL. For the attached example, all queries (Q1 - Q4) pass when run as a batch. However, this is incorrect: We know that Q4 should fail! When we run the queries individually, we get the correct results. I have previously seen a similar problem (which is probably caused by the same problem): Changing one query may affect the results of other queries (and care has been taken to ensure that the queries are side-effect-free). I have marked the problem as critical because a formal verifier should never present wrong results. PS: How do we get a newer version than 4.19? Best regards, Allan Munck