| Summary: | Different verification results when verifying a single vs multiple quries | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | tgunde13 |
| Component: | GUI | Assignee: | Marius Mikučionis <marius> |
| Status: | RESOLVED FIXED | ||
| Severity: | critical | CC: | adavid, tgunde13 |
| Priority: | P5 | ||
| Version: | 4.1.19 | ||
| Hardware: | PC | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | The systems used to reproduce | ||
I believe this has been fixed in release 4.1.20. |
Created attachment 308 [details] The systems used to reproduce Observed: For a query I get a fail (red circle) when verifying all my queries at the same time. When I verify the query alone, I get a pass (green circle). The query: A[] forall(i:id_t) (ServerThread(i).Cal imply forall(j:id_t) (ServerThread(i).movesCopy[j] == ClientMinion(j).move)) Expected: The verifications show show the same result. Note: I do not know the correct answer for the query. I do not know if this is a problem with the GUI or the Engine. Steps: 1. Start UPPAAL 2. Open the attached system 3. Go to the "Verifier" tab 4. Mark all queries (shift click them all from top to bottom or click the first one and then Ctrl + A) 5. Click the "Check" button". I get Pass, Pass, Pass, Fail, Fail 6. Click the fourth query 7. Click the "Check" button". I get a Pass. Build: UPPAAL 4.1.19 (rev. 5649), September 2014 Academic and non-commercial use only Frequency: 10/10