search

utwente-fmt / UrPal

UPPAAL Sanity Checker
5 stars 1 forks source link

Loading traces cause exception if simulator hasn't been opened previously #17

Closed ramononis closed 5 years ago

ramononis commented 5 years ago

To reproduce:

  1. Open Uppaal
  2. Open any Uppaal model with an deadlock/invariant violation
  3. Open the sanity checker tab (do not open the simulator beforehand).
  4. Run a check that returns a trace and load it.
  5. This results in a nullpointer.

Note that this exception does not happen if the simulator has been opened before loading the trace.

Probable cause/remedy:
Internally Uppaal tries to replace something in the view-model of the simulator when loading a trace. If the simulator has not been opened before, this 'something' will be null (probably an array).

ramononis commented 5 years ago

Related to #16

ramononis commented 5 years ago

Will be fixed in Uppaal 4.1.23 (fix available in 4.1.23-beta7).