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

Bug 454 - stopwatches undocumented
Summary: stopwatches undocumented
Status: RESOLVED FIXED
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: 2008-12-18 18:35 CET by Marius Mikučionis
Modified: 2009-03-10 11:19 CET (History)
0 users

See Also:
Architecture:

Attachments
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 Marius Mikučionis 2008-12-18 18:35:28 CET 
I think this bug is a release critical, so just for the record:

1) There is no documentation about stopwatches in the manual,
i.e. how to define, use them and what are consequences.

2) safety verification suddenly switches to "probably" and does not give any trace, although the verification terminates quite quickly, i.e. it clearly found something, but refuses to show it. 

I'd like to get that trace, even if that is an overapproximation, or at least show a reason in status why there is no trace when trace is requested.

Is it a fundamental/correctness problem or implementation limitation?
Comment 1 Alexandre David 2009-03-10 11:19:01 CET 
Fixed in rev. 4247.