diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 3d2d5b6e508f61b54fcf7110c46ae42c1f834fdc..76ef31d8a560291e45f9a4c05c0a26684e422b7d 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -198,6 +198,7 @@ public final class StandardMadules {
public static final String POW_1 = "Pow1";
public static final String FINITE_SUBSETS = "Fin";
public static final String FINITE_1_SUBSETS = "Fin1";
+ public static final String B_POWER_Of = "BPowerOf";
public static final String B_MODULO = "BModulo";
public static final String B_DIVISION = "BDivision";
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 10d65ec3e98f36731421ff1431a464e015417376..3eaa3126d9035a15ed1657bc5ec56ad6fbb8c951 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -275,9 +275,6 @@ public class UsedStandardModules extends DepthFirstAdapter {
extendedStandardModules.add(STANDARD_MODULES.Naturals);
}
- public void inAPowerOfExpression(APowerOfExpression node) {
- extendedStandardModules.add(STANDARD_MODULES.Naturals);
- }
public void inAMinusOrSetSubtractExpression(
AMinusOrSetSubtractExpression node) {
@@ -327,6 +324,10 @@ public class UsedStandardModules extends DepthFirstAdapter {
* BBuiltIns
*/
+ public void inAPowerOfExpression(APowerOfExpression node) {
+ extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
+ }
+
public void inAMinExpression(AMinExpression node) {
extendedStandardModules.add(STANDARD_MODULES.BBuiltIns);
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 3afd929d53bc04865bc681eafd7cda71c4d66a6d..b5f74ddf0eb6b2aac4006e6b487a57f4177609e4 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -458,25 +458,24 @@ public class TLAPrinter extends DepthFirstAdapter {
ALabelPredicate label = (ALabelPredicate) assertion;
name = label.getName().getText();
}
-
- if(name == null){
+
+ if (name == null) {
name = "Assertion" + (i + 1);
}
-
if (tlaModule.hasInitPredicate()) {
- moduleStringAppend(name);
- moduleStringAppend(" == ");
+ moduleStringAppend(name);
+ moduleStringAppend(" == ");
} else {
moduleStringAppend("ASSUME ");
- moduleStringAppend(name);
- moduleStringAppend(" == ");
+ moduleStringAppend(name);
+ moduleStringAppend(" == ");
}
- //assertionMode = true;
- //assertionName = name;
- //parameterCounter = 0;
+ // assertionMode = true;
+ // assertionName = name;
+ // parameterCounter = 0;
assertion.apply(this);
- //assertionMode = false;
+ // assertionMode = false;
moduleStringAppend("\n");
}
}
@@ -1279,7 +1278,7 @@ public class TLAPrinter extends DepthFirstAdapter {
moduleStringAppend("(");
moduleStringAppend("TLCSet(");
- moduleStringAppend(""+start);
+ moduleStringAppend("" + start);
moduleStringAppend(", TRUE) /\\ ");
for (int i = start; i < end; i++) {
moduleStringAppend("TLCSet(");
@@ -1312,7 +1311,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
assertionMode = false;
-
+
moduleStringAppend(" IF ");
node.getImplication().apply(this);
moduleStringAppend(" THEN TRUE ");
@@ -1323,14 +1322,14 @@ public class TLAPrinter extends DepthFirstAdapter {
moduleStringAppend("TLCGet(");
moduleStringAppend("" + (i + 1));
moduleStringAppend(")");
- if(i<copy.size()-1){
+ if (i < copy.size() - 1) {
moduleStringAppend(", ");
}
-
+
}
moduleStringAppend(" >>) ");
moduleStringAppend("/\\ TLCSet(");
- moduleStringAppend(""+start);
+ moduleStringAppend("" + start);
moduleStringAppend(", FALSE)");
moduleStringAppend(")");
moduleStringAppend(" /\\ TLCGet(");
@@ -1648,11 +1647,12 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAPowerOfExpression(APowerOfExpression node) {
- inAPowerOfExpression(node);
+ moduleStringAppend(B_POWER_Of);
+ moduleStringAppend("(");
node.getLeft().apply(this);
- moduleStringAppend(" ^ ");
+ moduleStringAppend(", ");
node.getRight().apply(this);
- outAPowerOfExpression(node);
+ moduleStringAppend(")");
}
@Override
diff --git a/src/main/resources/standardModules/BBuiltIns.tla b/src/main/resources/standardModules/BBuiltIns.tla
index 392ca03e331a37c2587cd6163869e379e842944f..688ba0f068ff90261fcc4d153642d1fa1d53562d 100644
--- a/src/main/resources/standardModules/BBuiltIns.tla
+++ b/src/main/resources/standardModules/BBuiltIns.tla
@@ -12,6 +12,7 @@ succ[x \in Int] == x + 1
pred[x \in Int] == x - 1
\* The predecessor function
+BPowerOf(a,b) == IF a = 0 /\ b = 0 THEN 1 ELSE a ^ b
BDivision(a,b) ==
CASE a >= 0 /\ b > 0 -> a \div b
@@ -19,21 +20,38 @@ BDivision(a,b) ==
[] a >= 0 /\ b < 0 -> -(a \div (-b))
[] a < 0 /\ b < 0 -> (-a) \div (-b)
[] b = 0 -> Assert(FALSE, "Error: Division by zero.")
+ [] OTHER -> Assert(FALSE, "Error: Modulo Operator.")
\* Rules from AtelierB reference manual (see page 40)
BModulo(a,b) ==
- IF a > 0 /\ b > 0
+ IF a >= 0 /\ b > 0
THEN a % b
ELSE Assert(FALSE, "Error: Both operands of the modulo operator must be natural numbers.")
RECURSIVE Sigma(_)
-Sigma(S) == LET e == CHOOSE e \in S: TRUE
- IN IF S = {} THEN 0 ELSE e[2] + Sigma(S \ {e})
+Sigma(S) ==
+ IF S = {} THEN 0
+ ELSE
+ LET
+ e == CHOOSE e \in S: TRUE
+ newS == S \ {e}
+ IN
+ IF newS = {}
+ THEN e[2]
+ ELSE e[2] + Sigma(S \ {e})
\* The sum of all second components of pairs which are elements of S
RECURSIVE Pi(_)
-Pi(S) == LET e == CHOOSE e \in S: TRUE
- IN IF S = {} THEN 0 ELSE e[2] + Pi(S \ {e})
+Pi(S) ==
+ IF S = {} THEN 0
+ ELSE
+ LET
+ e == CHOOSE e \in S: TRUE
+ newS == S \ {e}
+ IN
+ IF newS = {}
+ THEN e[2]
+ ELSE e[2] * Pi(S \ {e})
\* The product of all second components of pairs which are elements of S
Pow1(S) == (SUBSET S) \ {{}}