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

adjusted min and max int configuration

parent 48161865
No related branches found
No related tags found
No related merge requests found
......@@ -157,9 +157,26 @@ public class TLC4B {
} else if (args[index].toLowerCase().equals("-testscript")) {
TLC4BGlobals.setRunTestscript(true);
} else if (args[index].toLowerCase().equals("-notrace")) {
TLC4BGlobals.setCreateTraceFile(false);
} else if (args[index].toLowerCase().equals("-del")) {
TLC4BGlobals.setDeleteOnExit(true);
} else if (args[index].toLowerCase().equals("-maxint")) {
index = index + 1;
if (index == args.length) {
throw new TLC4BIOException(
"Error: Number requiered after option '-maxnint'.");
}
int maxint = Integer.parseInt(args[index]);
TLC4BGlobals.setMAX_INT(maxint);
} else if (args[index].toLowerCase().equals("-minint")) {
index = index + 1;
if (index == args.length) {
throw new TLC4BIOException(
"Error: Number requiered after option '-minint'.");
}
int minint = Integer.parseInt(args[index]);
TLC4BGlobals.setMIN_INT(minint);
;
} else if (args[index].toLowerCase().equals("-workers")) {
index = index + 1;
if (index == args.length) {
......
......@@ -1323,21 +1323,22 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAIntSetExpression(AIntSetExpression node) {
inAIntSetExpression(node);
tlaModuleString.append("Int");
tlaModuleString.append("(" + TLC4BGlobals.getMIN_INT() + ".."
+ TLC4BGlobals.getMAX_INT() + ")");
outAIntSetExpression(node);
}
@Override
public void caseANatSetExpression(ANatSetExpression node) {
inANatSetExpression(node);
tlaModuleString.append("Nat");
tlaModuleString.append("(0.." + TLC4BGlobals.getMAX_INT() + ")");
outANatSetExpression(node);
}
@Override
public void caseANat1SetExpression(ANat1SetExpression node) {
inANat1SetExpression(node);
tlaModuleString.append("(Nat \\ {0})");
tlaModuleString.append("(1.." + TLC4BGlobals.getMAX_INT() + ")");
outANat1SetExpression(node);
}
......
......@@ -108,9 +108,6 @@ public class TestUtil {
//parse check
translateTLA2B(name, b2tlaTranslator.getModuleString(),
b2tlaTranslator.getConfigString());
// de.tla2b.translation.Tla2BTranslator.translateString(name,
// b2tlaTranslator.getModuleString(),
// b2tlaTranslator.getConfigString());
assertEquals(expectedModule, b2tlaTranslator.getModuleString());
assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment