Collecting action coverage

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,6 +18,8 @@ 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;

tlatools/src/tlc2/tool/AbstractChecker.java

 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);
         }

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;
         }
     }