First Last Prev Next    No search results available      Search page      Enter new bug
Bug#: 456
Product:
Component:
Status: RESOLVED
Resolution: FIXED
Assigned To: Alexandre David <adavid@cs.aau.dk>
Hardware:
OS:
Version:
Priority:
Severity:
Reporter: Marius Mikucionis <marius@cs.aau.dk>
Add CC:
CC:
URL:
Summary:

Attachment Type Creator Created Size Actions
the model (hopefully deadlock free) text/xml Marius Mikucionis 2008-12-30 14:24 10.92 KB Details
the list of properties in specific order application/octet-stream Marius Mikucionis 2008-12-30 14:24 1012 bytes Details
Create a New Attachment (proposed patch, testcase, etc.) View All

Bug 456 depends on: Show dependency tree
Show dependency graph
Bug 456 blocks:
Votes: 0    Show votes for this bug    Vote for this bug

Additional Comments:







View Bug Activity   |   Format For Printing   |   XML   |   Clone This Bug

Description:   Opened: 2008-12-30 14:22 
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 From Marius Mikucionis 2008-12-30 14:24:04 ------- 
Created an attachment (id=208) [details]
the model (hopefully deadlock free)

------- Comment #2 From Marius Mikucionis 2008-12-30 14:24:38 ------- 
Created an attachment (id=209) [details]
the list of properties in specific order

------- Comment #3 From Marius Mikucionis 2008-12-30 17:08:43 ------- 
the bug does not show up in 4.0.7, it seems to be local to Uppaal version in
trunk.

------- Comment #4 From Alexandre David 2009-03-02 18:50:32 ------- 
Fixed in rev. 4227.
First Last Prev Next    No search results available      Search page      Enter new bug