diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java index 3c535b210385c223c7d79f052cc2d2cdaea969ee..c03d212a8da5c4fbc13b8c5daffa7eb71c8bbddb 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 f3d27de09ff155c9b0346d48a6adb4ac5c1c1829..3f62753cc6b182b9a0e3d36424b33691e22993f8 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 7cf4e941202aa8757532a055086e5b66cdbc0255..11231b3764f532be4a5e90701236fba955dd80e5 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 e2fbe0610af2810d70e34158e46a43d2cd2232f1..5b087cb448bd69ee180d5ed04ed34081cdb6fb11 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); }