Bug 456 - (at least) deadlock check is incorrect in batch verification when state space is reused
Summary: (at least) deadlock check is incorrect in batch verification when state space...
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Linux
: P2 major
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2008-12-30 14:22 CET by Marius Mikučionis
Modified: 2009-03-02 18:50 CET (History)
0 users

See Also:
Architecture:


Attachments
the model (hopefully deadlock free) (10.92 KB, text/xml)
2008-12-30 14:24 CET, Marius Mikučionis
Details
the list of properties in specific order (1012 bytes, application/octet-stream)
2008-12-30 14:24 CET, Marius Mikučionis
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2008-12-30 14:22:43 CET
Procedure to reproduce bug:
1) load the model (will upload shortly)
2) make sure diagnostic trace is turned off
3) state space reuse is turned on
4) select all queries in verifier and click verify

Result:
all properties satisfied except "A[] not deadlock"

If this property is rechecked with diagnostic trace turned on, or without state space reuse, then verifier says that this property is satisfied.

I guess that something goes wrong with state space reuse, perhaps the state space gets reduced due to some earlier property and hence deadlock situation is created.
Comment 1 Marius Mikučionis 2008-12-30 14:24:04 CET
Created attachment 208 [details]
the model (hopefully deadlock free)
Comment 2 Marius Mikučionis 2008-12-30 14:24:38 CET
Created attachment 209 [details]
the list of properties in specific order
Comment 3 Marius Mikučionis 2008-12-30 17:08:43 CET
the bug does not show up in 4.0.7, it seems to be local to Uppaal version in trunk.
Comment 4 Alexandre David 2009-03-02 18:50:32 CET
Fixed in rev. 4227.