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

Bug 431 - leads to property check is wrong
Summary: leads to property check is wrong
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.6
Hardware: PC All
: P2 critical
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2007-11-14 16:59 CET by Marius Mikučionis
Modified: 2008-09-12 11:49 CEST (History)
0 users

See Also:
Architecture:

Attachments
The model exhibiting the bug (1.50 KB, text/xml)
2007-11-14 17:01 CET, Marius Mikučionis 		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 Marius Mikučionis 2007-11-14 16:59:15 CET 
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 Marius Mikučionis 2007-11-14 17:01:01 CET 
Created attachment 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 Alexandre David 2008-09-11 16:31:18 CEST 
Revision 3932 should fix it.
Comment 3 Alexandre David 2008-09-12 11:49:19 CEST 
The liveness checker of the trunk seems to work fine in 4.0.