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

Bug 64 - the nature of symbolic traces should be explained in the doc
Summary: the nature of symbolic traces should be explained in the doc
Status: CLOSED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Documentation (show other bugs)
Version: 3.4.1
Hardware: All All
: P2 normal
Assignee: Paul Pettersson
URL:
Depends on:
Blocks:
 
Reported: 2003-10-03 09:29 CEST by Juhan Ernits
Modified: 2005-06-29 21:23 CEST (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 Juhan Ernits 2003-10-03 09:29:44 CEST 
it seems to be unintuitive to understand the symbolic traces Uppaal gives
especially in the case they happen to be unstable, i.e. they contain reachable
states from where there is no path to the final state.

Therefore there should be a concise note in the documentation for clarifying
that Uppaal actually uses symbolic traces in the simulator and how a symbolic
trace should be interpreted.

In the same context, it would be nice to have a reference to the command line
option to generate concrete traces using verifyta.
Comment 1 Paul Pettersson 2004-05-07 14:13:54 CEST 
Text updated.