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

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.