Collecting all assumption errors

tlatools/build.gradle

@@ -5,7 +5,6 @@ apply plugin: 'maven'
 project.version = '1.0.0-SNAPSHOT'
 project.group = 'de.tla'
 
-sourceCompatibility = 1.5
 
 repositories {
 	mavenCentral()

tlatools/src/tlc2/output/OutputCollector.java

@@ -17,7 +17,7 @@ public class OutputCollector {
 	private static ArrayList<Message> allMessages = new ArrayList<Message>();
 	private static Hashtable<Location, Long> lineCount = new Hashtable<Location, Long>();
 	private static ModuleNode moduleNode = null;
-	private static ExprNode violatedAssumption = null;
+	private static ArrayList<ExprNode> violatedAssumptions = new ArrayList<>();
 
 	public static ArrayList<TLCStateInfo> getTrace() {
 		return trace;
@@ -46,12 +46,12 @@ public class OutputCollector {
 		return allMessages;
 	}
 
-	public static void setViolatedAssumption(ExprNode assumption) {
-		violatedAssumption = assumption;
+	public static void addViolatedAssumption(ExprNode assumption) {
+			violatedAssumptions.add(assumption);
 	}
 
-	public static ExprNode getViolatedAssumption() {
-		return violatedAssumption;
+	public static ArrayList<ExprNode> getViolatedAssumptions() {
+		return violatedAssumptions;
 	}
 
 	public synchronized static void saveMessage(int messageClass,

tlatools/src/tlc2/tool/ModelChecker.java

@@ -267,25 +267,30 @@ public class ModelChecker extends AbstractChecker
     {
         ExprNode[] assumps = this.tool.getAssumptions();
         boolean[] isAxiom = this.tool.getAssumptionIsAxiom();
+        boolean assumptionsAreTRUE = true;
         for (int i = 0; i < assumps.length; i++)
         {
             try
             {
                 if ((!isAxiom[i]) && !this.tool.isValid(assumps[i]))
                 {
-                	OutputCollector.setViolatedAssumption(assumps[i]);
+                	OutputCollector.addViolatedAssumption(assumps[i]);
                     MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
-                    return false;
+                    //return false;
+                    assumptionsAreTRUE = false;
                 }
             } catch (Exception e)
             {
                 // Assert.printStack(e);
+            	OutputCollector.addViolatedAssumption(assumps[i]);
                 MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
                         new String[] { assumps[i].toString(), e.getMessage() });
-                return false;
+                //return false;
+                assumptionsAreTRUE = false;
             }
         }
-        return true;
+        //return true;
+        return assumptionsAreTRUE;
     }
 
     /**