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

Bug 464 - Liveness trace is too permissive
Summary: Liveness trace is too permissive
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Linux
: P2 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2009-03-11 15:45 CET by Alexandre David
Modified: 2010-04-23 18:43 CEST (History)
1 user (show)

See Also:
Architecture:

Attachments
Model (1.10 KB, text/xml)
2009-03-11 15:46 CET, Alexandre David 		Details
Property (124 bytes, application/octet-stream)
2009-03-11 15:46 CET, Alexandre David 		Details
another example with counter example to A<> (2.24 KB, text/xml)
2010-04-23 18:43 CEST, Marius Mikučionis 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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