From 23e3af26243497c723e756eb890d5ff1232d2cd2 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Wed, 6 May 2015 13:56:09 +0200
Subject: [PATCH] [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).
---
tlatools/src/tlc2/tool/liveness/LiveCheck.java | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck.java b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
index 56e00b2f3..62eedbe80 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveCheck.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
@@ -641,12 +641,17 @@ public class LiveCheck implements ILiveCheck {
// Intended to be used in unit tests only!!! This is not part of the API!!!
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
// (Arguments tab) to the parent directory of the folder containing the
// nodes_* and ptrs_* files. The parent folder has to contain the spec
// and config file both named "MC".
// 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.
public static ILiveCheck recreateFromDisk(final String path) throws Exception {
// Don't know with which Polynomial the FP64 has been initialized, but
@@ -661,6 +666,11 @@ public class LiveCheck implements ILiveCheck {
final Tool tool = new Tool("", "MC", "MC", new SimpleFilenameToStream());
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());
// Calling recover requires a .chkpt file to be able to re-create the
--
GitLab