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.
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.
Revision 3932 should fix it.
The liveness checker of the trunk seems to work fine in 4.0.