This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 630 - Different verification results when verifying a single vs multiple quries
Summary: Different verification results when verifying a single vs multiple quries
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.1.19
Hardware: PC All
: P5 critical
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2017-04-04 11:56 CEST by tgunde13
Modified: 2019-10-28 14:06 CET (History)
2 users (show)

See Also:
Architecture:

Attachments
The systems used to reproduce (8.96 KB, text/xml)
2017-04-04 11:56 CEST, tgunde13 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Description tgunde13 2017-04-04 11:56:27 CEST 
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
Comment 1 Marius Mikučionis 2019-10-28 14:06:24 CET 
I believe this has been fixed in release 4.1.20.