From dc53456c86c4f61c5590dc18391d8984ac8898cb Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 1 Jun 2015 18:09:54 +0200
Subject: [PATCH] minor fix
---
tlatools/src/tlc2/output/OutputCollector.java | 6 +++---
tlatools/src/tlc2/tool/AbstractChecker.java | 7 ++++++-
tlatools/src/tlc2/tool/Spec.java | 2 --
3 files changed, 9 insertions(+), 6 deletions(-)
diff --git a/tlatools/src/tlc2/output/OutputCollector.java b/tlatools/src/tlc2/output/OutputCollector.java
index 4c237f703..93b5eb6e3 100644
--- a/tlatools/src/tlc2/output/OutputCollector.java
+++ b/tlatools/src/tlc2/output/OutputCollector.java
@@ -4,6 +4,7 @@ import java.util.ArrayList;
import java.util.Date;
import java.util.Hashtable;
+import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.st.Location;
import tlc2.module.TLC;
@@ -14,12 +15,11 @@ import tlc2.util.ObjLongTable;
public class OutputCollector {
-
private static TLCState initialState = null;
private static ArrayList<TLCStateInfo> trace = null;
private static ArrayList<Message> allMessages = new ArrayList<Message>();
- public static Action nextPred = null;
- public static Hashtable<Location, Long> lineCount= new Hashtable<Location, Long>();
+ public static ModuleNode moduleNode = null;
+ public static Hashtable<Location, Long> lineCount = null;
public static ArrayList<TLCStateInfo> getTrace() {
return trace;
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index 7d9ac8dad..1c8d430dc 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -154,6 +154,7 @@ public abstract class AbstractChecker implements Cancelable
MP.printMessage(EC.TLC_COVERAGE_START);
// First collecting all counts from all workers:
ObjLongTable counts = this.tool.getPrimedLocs();
+ OutputCollector.moduleNode = this.tool.rootModule;
Hashtable<String, Location> locationTable = new Hashtable<String, Location>();
for (int i = 0; i < workers.length; i++)
{
@@ -169,11 +170,15 @@ public abstract class AbstractChecker implements Cancelable
}
// Reporting:
Object[] skeys = counts.sortStringKeys();
+ OutputCollector.lineCount = new Hashtable<Location, Long>();
for (int i = 0; i < skeys.length; i++)
{
long val = counts.get(skeys[i]);
MP.printMessage(EC.TLC_COVERAGE_VALUE, new String[] { skeys[i].toString(), String.valueOf(val) });
- OutputCollector.lineCount.put(locationTable.get(skeys[i]), val);
+ Location location = locationTable.get(skeys[i]);
+ if(location != null){
+ OutputCollector.lineCount.put(location, val);
+ }
}
MP.printMessage(EC.TLC_COVERAGE_END);
}
diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java
index 48b1f0f4e..1094f2586 100644
--- a/tlatools/src/tlc2/tool/Spec.java
+++ b/tlatools/src/tlc2/tool/Spec.java
@@ -42,7 +42,6 @@ import tla2sany.semantic.ThmOrAssumpDefNode;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
-import tlc2.output.OutputCollector;
import tlc2.util.Context;
import tlc2.util.List;
import tlc2.util.ObjLongTable;
@@ -916,7 +915,6 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
Assert.fail(EC.TLC_CONFIG_ID_REQUIRES_NO_ARG, new String[] { "next state action", name });
}
this.nextPred = new Action(def.getBody(), Context.Empty);
- OutputCollector.nextPred = this.nextPred;
}
}
--
GitLab