"Cannot generate the trace" error when over-approximation and diagnostic trace are enabled

[mikucionisaau]

Describe the bug
Uppaal refuses to show traces by showing an error "Cannot generate the trace" on some models when over-approximation and diagnostic trace is enabled.

The issue is that

1. the error message is not descriptive enough (does not explain the reason) and
2. "EngineCrashException" part is misleading (the engine did not crash, it just issued this error).

Previous (e.g. 4.1.26) versions produce the counter example trace instead of error, so perhaps it's a regression.

To Reproduce
Steps to reproduce the behavior:

1. Open the model bonus2_advanced.xml.zip
2. Go to Verifier
3. Select the first query and click check.
4. Observe the error:
   

Expected behavior
Uppaal should either produce a trace (just like previous versions) or the error should provide a valid reason for not producing a trace.

Version(s) of UPPAAL tested
UPPAAL 5.0.0-rc2 (rev. 92306F488AF675BA), March 2023

Other
Older version UPPAAL 4.1.26-1 (rev. 7BCF30B7363A9518) loads the trace successfully.

[mikucionisaau]

The attached model is a minimal case to trigger the bug in static analysis.

Static analysis of the code is over-approximate and in this case treats clock x as being always reset, even though it is never reset due to the if condition being false. (The edge guards are analyzed precisely, hence does not have such issue.)
As a consequence, location-based extrapolations algorithms lose the constraints over such clocks (because their value is irrelevant after reset and hence the max and LU bounds are not propagated passed the reset) and therefore reaches location Run.

If a diagnostic trace is requested (Options > Diagnostic trace > Some), then UPPAAL fails with "Cannot generate trace"
(because the found sequence of edges is not realizable when UPPAAL attempts to reconstruct the trace without using the extrapolation).

If extrapolation is disabled (Options > Extrapolationn > None), then UPPAAL computes correct results (property E<> P.Run is not satisfied).

Affected versions:

• UPPAAL 5.1.0-beta5 (rev. C7C01B0740E14075), 2023-12-11
• UPPAAL 5.0.0 (rev. 714BA9DB36F49691), 2023-06-21
• UPPAAL 4.1.20-stratego-9 (rev. 67D95DBCE6B8B4ED), January 2022
• UPPAAL 4.1.20-stratego-8 (rev. 0D95F1A3F94D0519), January 2022
• UPPAAL 4.1.20-stratego-7 (rev. 2FAFB4835E702C0F), December 2019
• UPPAAL 4.1.20-stratego-5 (rev. 92B3A8B7C85C1101), February 2019

Not affected:

• UPPAAL 4.1.26-1 (rev. 7BCF30B7363A9518), February 2022
• UPPAAL 4.1.20-stratego-4 (rev. 7), November 2016

extrapolation.xml.zip