|Summary:||Liveness trace is too permissive|
|Product:||UPPAAL||Reporter:||Alexandre David <adavid>|
|Component:||Engine||Assignee:||Alexandre David <adavid>|
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 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