second start of TorXExplorer (.tx) Model or Impl does not work (and JTorX crashes)
|Status:||Closed||Start date:||30 Jun 2009|
Typically, JTorX crashes with a null-pointer exception.
Still have to find out the exact details of why it does not work; either the TorXExplorer(s) is/are not started, or immediately fail(s).
Tried this with /Users/axel/src/torx-examples-3.9.1/confprot/SPEC/MCRL/confprot.mcrl.tx
as model and/or implementation.
We might interpret this as yet another indication that we have to fix the configuration (see related issues).
#1 Updated by Axel Belinfante about 11 years ago
- Status changed from New to Closed
- Target version set to 1.1.1
- % Done changed from 0 to 100
The problem seems to be that we try to be smart and avoid reloading a model (LTS) when the same model was used in a previous test run.
This works fine for models that are files (.aut, .graphml) but does not work for torx-explorer(5) models, because for such models a program must always be started
(unless we would keep the program running beyond the end of a test run, which we don't do).
crude fix in commit c6ea369b8ea227db34be9ce4deaf10036f3c7733
when we check whether to clear the model data, or reuse it, we always clear this data.
Also made JTorX slightly more robust: when we do not have a model-as-simulated-implementation we immediately abort the test run, instead of crashing.
TODO: inform the user why we aborted the test run: we do set an error verdict, but somehow that is not shown (we do not even show a verdict when we abort?)