Skip to content
Snippets Groups Projects
Commit 23e3af26 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

[Tests] Initialize Tool's actions which otherwise causes a NPE when

LiveCheck#TestHelper has re-created the liveness behavior graph, a
violation has been found and the error trace is printed
(LiveCheck#printTrace).
parent fbcfef92
No related branches found
No related tags found
No related merge requests found
...@@ -641,12 +641,17 @@ public class LiveCheck implements ILiveCheck { ...@@ -641,12 +641,17 @@ public class LiveCheck implements ILiveCheck {
// Intended to be used in unit tests only!!! This is not part of the API!!! // Intended to be used in unit tests only!!! This is not part of the API!!!
static class TestHelper { static class TestHelper {
/*
* * EWD840 (with tableau) spec with N = 11 and maxSetSize = 9.000.000 => 12GB nodes file, 46141438 distinct states
* * EWD840 (with tableau) spec with N = 12 and maxSetSize = 9.000.000 => TBD
*/
// The Eclipse Launch configuration has to set the working directory // The Eclipse Launch configuration has to set the working directory
// (Arguments tab) to the parent directory of the folder containing the // (Arguments tab) to the parent directory of the folder containing the
// nodes_* and ptrs_* files. The parent folder has to contain the spec // nodes_* and ptrs_* files. The parent folder has to contain the spec
// and config file both named "MC". // and config file both named "MC".
// metadir is the the name of the folder with the nodes_* and ptrs_* // metadir is the the name of the folder with the nodes_* and ptrs_*
// relative to the parent directory. It does *not* need to contain the // relative to the parent directory. The directory does *not* need to contain the
// backing file of the fingerprint set or the state queue files. // backing file of the fingerprint set or the state queue files.
public static ILiveCheck recreateFromDisk(final String path) throws Exception { public static ILiveCheck recreateFromDisk(final String path) throws Exception {
// Don't know with which Polynomial the FP64 has been initialized, but // Don't know with which Polynomial the FP64 has been initialized, but
...@@ -661,6 +666,11 @@ public class LiveCheck implements ILiveCheck { ...@@ -661,6 +666,11 @@ public class LiveCheck implements ILiveCheck {
final Tool tool = new Tool("", "MC", "MC", new SimpleFilenameToStream()); final Tool tool = new Tool("", "MC", "MC", new SimpleFilenameToStream());
tool.init(true, null); tool.init(true, null);
// Initialize tool's actions explicitly. LiveCheck#printTrace is
// going to access the actions and fails with a NPE unless
// initialized.
tool.getActions();
final ILiveCheck liveCheck = new LiveCheck(tool, null, path, new DummyBucketStatistics()); final ILiveCheck liveCheck = new LiveCheck(tool, null, path, new DummyBucketStatistics());
// Calling recover requires a .chkpt file to be able to re-create the // Calling recover requires a .chkpt file to be able to re-create the
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment