From 615a6961afb03fe348cde0e86c93219f5fe0a261 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 21 Nov 2014 12:18:34 +0100
Subject: [PATCH] fixed precedence Bug
---
src/main/java/de/tlc4b/TLC4B.java | 5 +++++
.../java/de/tlc4b/analysis/NotSupportedConstructs.java | 8 ++++++++
src/main/java/de/tlc4b/prettyprint/TLAPrinter.java | 3 ++-
src/test/java/testing/Testing2.java | 1 +
4 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 6817f71..b762f56 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -72,6 +72,11 @@ public class TLC4B {
private void printResults(TLCResults results, boolean createTraceFile) {
+ String s = "";
+ for (int i = 0; i < 10; i++) {
+ s += i;
+ }
+
System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
+ " ms");
System.out.println("Translation time: " + StopWatch.getRunTime("Pure")
diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
index 1798fb4..56372a5 100644
--- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
+++ b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
@@ -7,6 +7,7 @@ import de.be4.classicalb.core.parser.node.AImportsMachineClause;
import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
import de.be4.classicalb.core.parser.node.APromotesMachineClause;
import de.be4.classicalb.core.parser.node.ARefinesModelClause;
+import de.be4.classicalb.core.parser.node.ASeesMachineClause;
import de.be4.classicalb.core.parser.node.ASeesModelClause;
import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
import de.be4.classicalb.core.parser.node.AUsesMachineClause;
@@ -18,12 +19,19 @@ public class NotSupportedConstructs extends DepthFirstAdapter {
public NotSupportedConstructs(Start start) {
start.apply(this);
+ System.out.println(start.getPParseUnit().getClass());
}
public void inARefinesModelClause(ARefinesModelClause node) {
throw new NotSupportedException(
"Refines clause is currently not supported.");
}
+
+ public void inASeesMachineClause(ASeesMachineClause node)
+ {
+ throw new NotSupportedException(
+ "SEES clause is currently not supported.");
+ }
public void inAUsesMachineClause(AUsesMachineClause node) {
throw new NotSupportedException(
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index c1e861c..425a405 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -813,7 +813,7 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseASelectSubstitution(ASelectSubstitution node) {
inASelectSubstitution(node);
// TODO remove brackets
-
+ tlaModuleString.append("(");
List<PSubstitution> copy = new ArrayList<PSubstitution>(
node.getWhenSubstitutions());
@@ -857,6 +857,7 @@ public class TLAPrinter extends DepthFirstAdapter {
&& (copy.size() > 0 || node.getElse() != null)) {
tlaModuleString.append(")");
}
+ tlaModuleString.append(")");
printUnchangedVariables(node, true);
outASelectSubstitution(node);
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index 4a936a7..925ef7e 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -29,6 +29,7 @@ public class Testing2 extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath(), "-nodead", "-noinv" };
+ //String[] a = new String[] { "./src/test/resources/testing/Counter.mch" };
TLC4B.main(a);
//TLC4B.test(a, false);
// test(a);
--
GitLab