From 2d4b4fb27091db615e7fce1d77a412d5d3282d57 Mon Sep 17 00:00:00 2001
From: hansene <dominik_hansen@web.de>
Date: Thu, 30 Jul 2015 20:51:51 +0200
Subject: [PATCH] Collecting all assumption errors

---
 tlatools/build.gradle                         |  1 -
 tlatools/src/tlc2/output/OutputCollector.java | 10 +++++-----
 tlatools/src/tlc2/tool/ModelChecker.java      | 13 +++++++++----
 3 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/tlatools/build.gradle b/tlatools/build.gradle
index 0cb17c7d6..ce9afa0e8 100644
--- a/tlatools/build.gradle
+++ b/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()
diff --git a/tlatools/src/tlc2/output/OutputCollector.java b/tlatools/src/tlc2/output/OutputCollector.java
index 00636aaca..6a7db4b5d 100644
--- a/tlatools/src/tlc2/output/OutputCollector.java
+++ b/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,
diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java
index 84b950e13..f5fe5a09d 100644
--- a/tlatools/src/tlc2/tool/ModelChecker.java
+++ b/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;
     }
 
     /**
-- 
GitLab