diff --git a/tlatools/build.gradle b/tlatools/build.gradle index 0cb17c7d68c0ce8270b1f6fd48d9841240c15185..ce9afa0e83cce72673ed5f9424188623454fb7e1 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 00636aaca758b44508cc02c1a2dde7f83a5bd2bb..6a7db4b5d56329dcd53f597be182766e6bd9983c 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 84b950e13eea76035faaf68b52607951da35f969..f5fe5a09d3c13b1e142579adc5549f9a0c02ee67 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; } /**