From e4a1cdd05cfe7703fa788f349942d3b05af945f7 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 1 Jun 2015 16:22:21 +0200
Subject: [PATCH] Collecting action coverage
---
tlatools/src/tlc2/output/OutputCollector.java | 9 ++++++++-
tlatools/src/tlc2/tool/AbstractChecker.java | 6 ++++++
tlatools/src/tlc2/tool/Spec.java | 2 ++
3 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/tlatools/src/tlc2/output/OutputCollector.java b/tlatools/src/tlc2/output/OutputCollector.java
index dec13f686..4c237f703 100644
--- a/tlatools/src/tlc2/output/OutputCollector.java
+++ b/tlatools/src/tlc2/output/OutputCollector.java
@@ -2,10 +2,15 @@ package tlc2.output;
import java.util.ArrayList;
import java.util.Date;
+import java.util.Hashtable;
+import tla2sany.semantic.SemanticNode;
+import tla2sany.st.Location;
import tlc2.module.TLC;
+import tlc2.tool.Action;
import tlc2.tool.TLCState;
import tlc2.tool.TLCStateInfo;
+import tlc2.util.ObjLongTable;
public class OutputCollector {
@@ -13,7 +18,9 @@ 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 ArrayList<TLCStateInfo> getTrace() {
return trace;
}
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index cac020874..7d9ac8dad 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -1,13 +1,16 @@
package tlc2.tool;
import java.io.IOException;
+import java.util.Hashtable;
import java.util.concurrent.atomic.AtomicLong;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.SemanticNode;
+import tla2sany.st.Location;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.liveness.ILiveCheck;
import tlc2.tool.liveness.LiveCheck;
import tlc2.tool.liveness.Liveness;
@@ -151,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();
+ Hashtable<String, Location> locationTable = new Hashtable<String, Location>();
for (int i = 0; i < workers.length; i++)
{
ObjLongTable counts1 = workers[i].getCounts();
@@ -160,6 +164,7 @@ public abstract class AbstractChecker implements Cancelable
{
String loc = ((SemanticNode) key).getLocation().toString();
counts.add(loc, counts1.get(key));
+ locationTable.put(loc, ((SemanticNode) key).getLocation());
}
}
// Reporting:
@@ -168,6 +173,7 @@ public abstract class AbstractChecker implements Cancelable
{
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);
}
MP.printMessage(EC.TLC_COVERAGE_END);
}
diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java
index 1094f2586..48b1f0f4e 100644
--- a/tlatools/src/tlc2/tool/Spec.java
+++ b/tlatools/src/tlc2/tool/Spec.java
@@ -42,6 +42,7 @@ 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;
@@ -915,6 +916,7 @@ 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