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

Adapted the translation of the modulo operator

parent e13611ad
Branches
Tags
No related merge requests found
......@@ -62,7 +62,7 @@ public class TLA2B implements TranslationGlobals {
System.err.println(e.getMessage());
System.exit(-1);
}
translator.createMachineFile();
//translator.createMachineFile();
translator.createProbFile();
}
......
......@@ -13,6 +13,7 @@ import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AFlooredDivExpression;
import de.be4.classicalb.core.parser.node.AGeneralSumExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AIfThenElseExpression;
......@@ -640,6 +641,13 @@ public class ASTPrettyPrinter extends ExtendedDFAdapter {
sb.append(" ))(0)");
}
@Override
public void caseAFlooredDivExpression(AFlooredDivExpression node) {
node.getLeft().apply(this);
sb.append(" \\div ");
node.getRight().apply(this);
}
@Override
public void caseAGeneralSumExpression(AGeneralSumExpression node) {
List<PExpression> copy = new ArrayList<PExpression>(
......
......@@ -1178,17 +1178,17 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
visitExprOrOpArgNodeExpression(n.getArgs()[0]),
visitExprOrOpArgNodeExpression(n.getArgs()[1])));
case B_OPCODE_mod: // modulo
case B_OPCODE_mod: // modulo a % b = a - b* (a/b)
{
PExpression f = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
PExpression s = visitExprOrOpArgNodeExpression(n.getArgs()[1]);
PExpression f2 = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
PExpression s2 = visitExprOrOpArgNodeExpression(n.getArgs()[1]);
PExpression a = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
PExpression b = visitExprOrOpArgNodeExpression(n.getArgs()[1]);
PExpression a2 = visitExprOrOpArgNodeExpression(n.getArgs()[0]);
PExpression b2 = visitExprOrOpArgNodeExpression(n.getArgs()[1]);
ADivExpression div = new ADivExpression(f, s);
AMultOrCartExpression mult = new AMultOrCartExpression(s2, div);
AFlooredDivExpression div = new AFlooredDivExpression(a, b);
AMultOrCartExpression mult = new AMultOrCartExpression(b2, div);
AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression(
f2, mult);
a2, mult);
return minus;
}
......
......@@ -6,6 +6,7 @@ package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Ignore;
import org.junit.Test;
......@@ -82,14 +83,15 @@ public class ModuleNaturalsTest {
compare(expected, module);
}
@Ignore
@Test
public void testMod() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals, Integers \n"
+ "ASSUME -3 % 2 = 1 \n"
+ "ASSUME (-3) % 2 = 1 \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
+ "PROPERTIES -3 - 2 * (-3 / 2) = 1 \n"
+ "PROPERTIES -3 - 2 * (-3 \\div 2) = 1 \n"
+ "END";
compare(expected, module);
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment