First Last Prev Next    No search results available      Search page      Enter new bug
Bug#: 431
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 exhibiting the bug text/xml Marius Mikucionis 2007-11-14 17:01 1.50 KB Details
Create a New Attachment (proposed patch, testcase, etc.) View All

Bug 431 depends on: Show dependency tree
Show dependency graph
Bug 431 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: 2007-11-14 16:59 
zhang Miaomiao reported a strange liveness check result (will attach it soon)
where the property "(impulse.x>0 && cpu_output==1) --> (impulse.x==0 &&
cpu_output==0)" is not satisfied on 4.0.6 release.

It looks like a bug to me, but I could not reproduce this on the trunk version
(it says the property is satisfied), so somehow it's fixed but the fix is not
released.

------- Comment #1 From Marius Mikucionis 2007-11-14 17:01:01 ------- 
Created an attachment (id=199) [details]
The model exhibiting the bug

UPPAAL 4.0.6 says the following property does not hold:
(impulse.x>0 && cpu_output== 1) --> (impulse.x==0 && cpu_output== 0)

Version from trunk says it holds.

------- Comment #2 From Alexandre David 2008-09-11 16:31:18 ------- 
Revision 3932 should fix it.

------- Comment #3 From Alexandre David 2008-09-12 11:49:19 ------- 
The liveness checker of the trunk seems to work fine in 4.0.
First Last Prev Next    No search results available      Search page      Enter new bug