diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index 54287c20ed5e603115ed4e2a179f1a19f0e78dd2..856f54ad76e94b1891ac33e793bbe6d5c1944bfa 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -464,7 +464,6 @@ public class TLAPrinter extends DepthFirstAdapter { moduleStringAppend(name); moduleStringAppend(" == "); } else { - moduleStringAppend(name); moduleStringAppend("Assertion" + (i + 1) + " == "); } } else { diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java index e8e6beee9701b5f173d095e0e5928376d2d07dc7..7830582a7605c8778a9ad42b9301d3f418af78b0 100644 --- a/src/main/java/de/tlc4b/tlc/TLCResults.java +++ b/src/main/java/de/tlc4b/tlc/TLCResults.java @@ -293,11 +293,9 @@ public class TLCResults implements ToolGlobals { // get the violated assumption expr from the OutputCollector ArrayList<ExprNode> violatedAssumptions = OutputCollector .getViolatedAssumptions(); - System.out.println(violatedAssumptions.size()); if (violatedAssumptions.size() > 0) { // try to find the assume node contain the expr in order to get // the name of the assumption - for (ExprNode exprNode : violatedAssumptions) { AssumeNode assumeNode = findAssumeNode(exprNode); ThmOrAssumpDefNode def = assumeNode.getDef(); @@ -315,7 +313,7 @@ public class TLCResults implements ToolGlobals { } } - if(tlcResult!= null){ + if(tlcResult == null){ // otherwise, it is normal properties error tlcResult = TLCResult.PropertiesError; }