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

Bug 464

Summary: Liveness trace is too permissive
Product: UPPAAL Reporter: Alexandre David <adavid>
Component: EngineAssignee: Alexandre David <adavid>
Status: ASSIGNED ---    
Severity: normal CC: marius
Priority: P2    
Version: unspecified   
Hardware: PC   
OS: Linux   
Attachments: Model
another example with counter example to A<>

Description Alexandre David 2009-03-11 15:45:46 CET
In the following example, the engine allows states that do not satisfy the property to be in the trace.
Comment 1 Alexandre David 2009-03-11 15:46:09 CET
Created attachment 211 [details]
Comment 2 Alexandre David 2009-03-11 15:46:26 CET
Created attachment 212 [details]
Comment 3 Marius Mikuńćionis 2010-04-23 18:43:25 CEST
Created attachment 232 [details]
another example with counter example to A<>

the following model from Danny & Jiri seems to suffer from the same problem.
it seems that at least the last symbolic state is not completely stabilized.
or maybe the loop part of the trace is not stabilized?
the query for this model is:
A<> Process.bad