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.