Collecting the exprNode of the violated assumption in case of an assumption error.

tlatools/src/tlc2/output/OutputCollector.java

@@ -4,22 +4,20 @@ import java.util.ArrayList;
 import java.util.Date;
 import java.util.Hashtable;
 
+import tla2sany.semantic.ExprNode;
 import tla2sany.semantic.ModuleNode;
-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 {
 
 	private static TLCState initialState = null;
 	private static ArrayList<TLCStateInfo> trace = null;
 	private static ArrayList<Message> allMessages = new ArrayList<Message>();
-	public static ModuleNode moduleNode = null;
-	public static Hashtable<Location, Long> lineCount = null;
+	private static Hashtable<Location, Long> lineCount = new Hashtable<Location, Long>();
+	private static ModuleNode moduleNode = null;
+	private static ExprNode violatedAssumption = null;
 
 	public static ArrayList<TLCStateInfo> getTrace() {
 		return trace;
@@ -48,6 +46,14 @@ public class OutputCollector {
 		return allMessages;
 	}
 
+	public static void setViolatedAssumption(ExprNode assumption) {
+		violatedAssumption = assumption;
+	}
+
+	public static ExprNode getViolatedAssumption() {
+		return violatedAssumption;
+	}
+
 	public synchronized static void saveMessage(int messageClass,
 			int messageCode, String[] parameters) {
 
@@ -55,4 +61,20 @@ public class OutputCollector {
 				new Date());
 		allMessages.add(m);
 	}
+
+	public static ModuleNode getModuleNode() {
+		return moduleNode;
+	}
+
+	public static void setModuleNode(ModuleNode moduleNode) {
+		OutputCollector.moduleNode = moduleNode;
+	}
+
+	public static Hashtable<Location, Long> getLineCountTable() {
+		return new Hashtable<Location, Long>(lineCount);
+	}
+
+	public static void putLineCount(Location location, long val) {
+		lineCount.put(location, val);
+	}
 }

tlatools/src/tlc2/tool/AbstractChecker.java

@@ -81,6 +81,8 @@ public abstract class AbstractChecker implements Cancelable
         this.specObj = this.tool.init(preprocess, spec);
         this.checkLiveness = !this.tool.livenessIsTrue();
 
+        OutputCollector.setModuleNode(this.tool.rootModule);
+        
         // moved to file utilities
         this.metadir = FileUtil.makeMetaDir(specDir, fromChkpt);
         
@@ -154,7 +156,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;
+            OutputCollector.setModuleNode(this.tool.rootModule);
             Hashtable<String, Location> locationTable = new Hashtable<String, Location>();
             for (int i = 0; i < workers.length; i++)
             {
@@ -170,14 +172,13 @@ 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) });
                 Location location = locationTable.get(skeys[i]);
                 if(location != null){
-                    OutputCollector.lineCount.put(location, val);
+                    OutputCollector.putLineCount(location, val);
                 }
             }
             MP.printMessage(EC.TLC_COVERAGE_END);

tlatools/src/tlc2/tool/ModelChecker.java

@@ -273,6 +273,7 @@ public class ModelChecker extends AbstractChecker
             {
                 if ((!isAxiom[i]) && !this.tool.isValid(assumps[i]))
                 {
+                	OutputCollector.setViolatedAssumption(assumps[i]);
                     MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
                     return false;
                 }