From ec3949d82ad029c200644d6f62ff57fb78e35fbc Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Tue, 18 Mar 2014 15:39:30 +0100
Subject: [PATCH] removed redundant brackets in the translated specification
---
src/main/java/de/tlc4b/analysis/PrecedenceCollector.java | 1 +
src/main/java/de/tlc4b/prettyprint/TLAPrinter.java | 6 +++---
src/test/java/de/tlc4b/analysis/ConstantsTest.java | 2 +-
src/test/java/de/tlc4b/prettyprint/SetTest.java | 2 +-
4 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index 3c535b2..c03d212 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -48,6 +48,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("AGreaterEqualPredicate", 5, 5, false);
put("ANotEqualPredicate", 5, 5, false);
put("APowerOfExpression", 14, 14, false);
+ put("ASubsetPredicate", 5, 5, false);
// put("ANatural1SetExpression", 8, 8, false); // NAT \ {0}
put("AUnionExpression", 8, 8, true);
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index f3d27de..3f62753 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -2018,10 +2018,10 @@ public class TLAPrinter extends DepthFirstAdapter {
inASubsetPredicate(node);
node.getLeft().apply(this);
- tlaModuleString.append(" \\in SUBSET(");
- // tlaModuleString.append(" \\subseteq ");
+ //tlaModuleString.append(" \\in SUBSET(");
+ tlaModuleString.append(" \\subseteq ");
node.getRight().apply(this);
- tlaModuleString.append(")");
+ //tlaModuleString.append(")");
outASubsetPredicate(node);
}
diff --git a/src/test/java/de/tlc4b/analysis/ConstantsTest.java b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
index 7cf4e94..11231b3 100644
--- a/src/test/java/de/tlc4b/analysis/ConstantsTest.java
+++ b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
@@ -115,7 +115,7 @@ public class ConstantsTest {
String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ "N == {1,2,3,4}\n"
- + "ASSUME N \\in SUBSET(Nat) \n"
+ + "ASSUME N \\subseteq Nat \n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/SetTest.java b/src/test/java/de/tlc4b/prettyprint/SetTest.java
index e2fbe06..5b087cb 100644
--- a/src/test/java/de/tlc4b/prettyprint/SetTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SetTest.java
@@ -154,7 +154,7 @@ public class SetTest {
String machine = "MACHINE test\n"
+ "PROPERTIES {1} <: {1} \n" + "END";
String expected = "---- MODULE test----\n"
- + "ASSUME {1} \\in SUBSET({1}) \n"
+ + "ASSUME {1} \\subseteq {1} \n"
+ "======";
compare(expected, machine);
}
--
GitLab