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:	Engine	Assignee:	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