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   
Architecture:
Attachments: Model
Property
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]
Model
Comment 2 Alexandre David 2009-03-11 15:46:26 CET
Created attachment 212 [details]
Property
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