From 576832fc399a4be4de13518a26a115cc0bab94e4 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 30 Jul 2015 21:48:44 +0200
Subject: [PATCH] minor changes
---
src/main/java/de/tlc4b/prettyprint/TLAPrinter.java | 1 -
src/main/java/de/tlc4b/tlc/TLCResults.java | 4 +---
2 files changed, 1 insertion(+), 4 deletions(-)
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 54287c2..856f54a 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 e8e6bee..7830582 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;
}
--
GitLab