Skip to content
Snippets Groups Projects
Commit ec3949d8 authored by hansen's avatar hansen
Browse files

removed redundant brackets in the translated specification

parent e1baa649
No related branches found
No related tags found
No related merge requests found
...@@ -48,6 +48,7 @@ public class PrecedenceCollector extends DepthFirstAdapter { ...@@ -48,6 +48,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("AGreaterEqualPredicate", 5, 5, false); put("AGreaterEqualPredicate", 5, 5, false);
put("ANotEqualPredicate", 5, 5, false); put("ANotEqualPredicate", 5, 5, false);
put("APowerOfExpression", 14, 14, false); put("APowerOfExpression", 14, 14, false);
put("ASubsetPredicate", 5, 5, false);
// put("ANatural1SetExpression", 8, 8, false); // NAT \ {0} // put("ANatural1SetExpression", 8, 8, false); // NAT \ {0}
put("AUnionExpression", 8, 8, true); put("AUnionExpression", 8, 8, true);
......
...@@ -2018,10 +2018,10 @@ public class TLAPrinter extends DepthFirstAdapter { ...@@ -2018,10 +2018,10 @@ public class TLAPrinter extends DepthFirstAdapter {
inASubsetPredicate(node); inASubsetPredicate(node);
node.getLeft().apply(this); node.getLeft().apply(this);
tlaModuleString.append(" \\in SUBSET("); //tlaModuleString.append(" \\in SUBSET(");
// tlaModuleString.append(" \\subseteq "); tlaModuleString.append(" \\subseteq ");
node.getRight().apply(this); node.getRight().apply(this);
tlaModuleString.append(")"); //tlaModuleString.append(")");
outASubsetPredicate(node); outASubsetPredicate(node);
} }
......
...@@ -115,7 +115,7 @@ public class ConstantsTest { ...@@ -115,7 +115,7 @@ public class ConstantsTest {
String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n" String expected = "---- MODULE test----\n" + "EXTENDS Naturals\n"
+ "N == {1,2,3,4}\n" + "N == {1,2,3,4}\n"
+ "ASSUME N \\in SUBSET(Nat) \n" + "ASSUME N \\subseteq Nat \n"
+ "======"; + "======";
compare(expected, machine); compare(expected, machine);
} }
......
...@@ -154,7 +154,7 @@ public class SetTest { ...@@ -154,7 +154,7 @@ public class SetTest {
String machine = "MACHINE test\n" String machine = "MACHINE test\n"
+ "PROPERTIES {1} <: {1} \n" + "END"; + "PROPERTIES {1} <: {1} \n" + "END";
String expected = "---- MODULE test----\n" String expected = "---- MODULE test----\n"
+ "ASSUME {1} \\in SUBSET({1}) \n" + "ASSUME {1} \\subseteq {1} \n"
+ "======"; + "======";
compare(expected, machine); compare(expected, machine);
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment