diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index 64d28f892a43ca736be42ee93d6992ad6631d02e..73d1a8e2dd43c0e8f173fb62c8afdb6b51c051be 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -1,6 +1,6 @@
package de.tla2b;
-import de.tla2b.exceptions.FrontEndException;
+import de.tla2b.exceptions.TLA2BFrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
@@ -50,13 +50,12 @@ public class TLA2B implements TranslationGlobals {
public static void main(String[] args) {
// To indicate an error we use the exit code -1
TLA2B tla2b = new TLA2B();
-
tla2b.handleParameter(args);
Translator translator = null;
try {
translator = new Translator(tla2b.mainFile);
- } catch (FrontEndException e) {
+ } catch (TLA2BFrontEndException e) {
System.exit(-1);
}
try {
diff --git a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
index 9198572ef0388cca6cd9ebaa385d3c5b2e38b2e7..3c703ed98cb143352658164b9f670cf0d0d870d8 100644
--- a/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
+++ b/src/main/java/de/tla2b/analysis/AbstractASTVisitor.java
@@ -7,9 +7,7 @@ import tlc2.tool.BuiltInOPs;
public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
public void visitModuleNode(ModuleNode moduleNode) {
-
visitDefinitions(moduleNode.getOpDefs());
-
visitAssumptions(moduleNode.getAssumptions());
}
@@ -19,6 +17,10 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
}
}
+ public void visitDefinition(OpDefNode opDefNode) {
+ visitExprNode(opDefNode.getBody());
+ }
+
public void visitAssumptions(AssumeNode[] assumptions) {
for (AssumeNode assumeNode : assumptions) {
visitAssumeNode(assumeNode);
@@ -29,17 +31,12 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
visitExprNode(assumeNode.getAssume());
}
- public void visitDefinition(OpDefNode opDefNode) {
- visitExprNode(opDefNode.getBody());
- }
-
public void visitExprOrOpArgNode(ExprOrOpArgNode n) {
if (n instanceof ExprNode) {
visitExprNode((ExprNode) n);
} else {
throw new RuntimeException("Should not appear.");
}
-
}
public void visitExprNode(ExprNode node) {
@@ -101,10 +98,8 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
} else {
visitUserDefinedNode(node);
}
-
}
}
-
}
public void visitBBuiltinsNode(OpApplNode n) {
@@ -131,7 +126,6 @@ public class AbstractASTVisitor extends BuiltInOPs implements ASTConstants {
if (exprOrOpArgNode != null) {
visitExprOrOpArgNode(exprOrOpArgNode);
}
-
}
}
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 486b6daf9d99066ccfdd72dda2ddf6618a2d3e37..8b285d8f11a879603ab7626159c6ecfc3315e97d 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -224,10 +224,8 @@ public class BOperation extends BuiltInOPs implements ASTConstants, ToolGlobals,
}
public SymbolNode getSymbolNode() {
- if (node != null) {
- if (node.getOperator().getKind() == UserDefinedOpKind) {
- return node.getOperator();
- }
+ if (node != null && node.getOperator().getKind() == UserDefinedOpKind) {
+ return node.getOperator();
}
return null;
}
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index b5dccfaefc7ef3008b02bace5c81ada736cf8280..47593bf67d49224157ea4645e8ca5c454e74944a 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -5,17 +5,19 @@ import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import util.UniqueString;
-import java.util.Hashtable;
+import java.util.Arrays;
+import java.util.Map;
+import java.util.stream.Collectors;
public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
private final OpDefNode[] defs;
- private final Hashtable<String, OpDefNode> defsHash;
+ private final Map<String, OpDefNode> defsHash;
private final int substitutionId = 11;
private InstanceTransformation(ModuleNode moduleNode) {
this.defs = moduleNode.getOpDefs();
- this.defsHash = SymbolSorter.getDefsHashTable(defs);
+ this.defsHash = SymbolSorter.getDefsMap(defs);
}
public static void run(ModuleNode moduleNode) {
@@ -58,8 +60,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
case NumeralKind: {
- NumeralNode num = (NumeralNode) n;
- return new NumeralNode(num.toString(), n.getTreeNode());
+ return new NumeralNode(n.toString(), n.getTreeNode());
}
case DecimalKind: {
@@ -71,28 +72,21 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
case StringKind: {
- StringNode str = (StringNode) n;
- return new StringNode(str.getTreeNode(), false);
+ return new StringNode(n.getTreeNode(), false);
}
case SubstInKind: {
SubstInNode substInNode = (SubstInNode) n;
-
- Subst[] subs = substInNode.getSubsts();
- for (Subst sub : subs) {
- OpDeclNode op = sub.getOp();
- ExprOrOpArgNode expr = sub.getExpr();
- op.setToolObject(substitutionId, expr);
+ for (Subst sub : substInNode.getSubsts()) {
+ sub.getOp().setToolObject(substitutionId, sub.getExpr());
}
return generateNewExprNode(substInNode.getBody(), prefix);
}
+
case AtNodeKind: { // @
AtNode old = (AtNode) n;
- OpApplNode oldExcept = old.getExceptRef();
- OpApplNode newExcept = (OpApplNode) oldExcept.getToolObject(substitutionId);
- OpApplNode oldComponent = old.getExceptComponentRef();
- OpApplNode newComponent = (OpApplNode) oldComponent.getToolObject(substitutionId);
- return new AtNode(newExcept, newComponent);
+ return new AtNode((OpApplNode) old.getExceptRef().getToolObject(substitutionId),
+ (OpApplNode) old.getExceptComponentRef().getToolObject(substitutionId));
}
case LetInKind: {
@@ -112,12 +106,11 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
cc.addSymbolToContext(newName, newLet);
}
- return new LetInNode(oldLetNode.getTreeNode(),
- newLets, null, generateNewExprNode(oldLetNode.getBody(),
- prefix), cc);
+ return new LetInNode(oldLetNode.getTreeNode(), newLets, null,
+ generateNewExprNode(oldLetNode.getBody(), prefix), cc);
}
}
- throw new RuntimeException();
+ throw new IllegalArgumentException("unknown ExprNode kind " + n.getKind());
}
private ExprNode generateNewOpApplNode(OpApplNode n, String prefix) throws AbortException {
@@ -144,8 +137,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
case FormalParamKind: {
- FormalParamNode f = (FormalParamNode) n.getOperator()
- .getToolObject(substitutionId);
+ FormalParamNode f = (FormalParamNode) n.getOperator().getToolObject(substitutionId);
if (f == null) {
throw new RuntimeException();
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index d4e815aa59cc4b285ed5ded6f7be882d3d139446..75ab20d472cefd96e6e9cffd60540e68c9e82f49 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -2,7 +2,7 @@ package de.tla2b.analysis;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.exceptions.ConfigFileErrorException;
-import de.tla2b.exceptions.FrontEndException;
+import de.tla2b.exceptions.TLA2BFrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.SemanticErrorException;
import de.tla2b.global.BBuiltInOPs;
@@ -159,7 +159,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
public void start()
- throws SemanticErrorException, FrontEndException, ConfigFileErrorException, NotImplementedException {
+ throws SemanticErrorException, TLA2BFrontEndException, ConfigFileErrorException, NotImplementedException {
if (spec != null) {
evalSpec();
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index b457ac933d1c671d15333a496bbba09998cb6f01..db0def3155deaff623d0de76976f88ed912228bf 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -6,7 +6,8 @@ import tla2sany.semantic.OpDefNode;
import java.util.Arrays;
import java.util.Comparator;
-import java.util.Hashtable;
+import java.util.HashMap;
+import java.util.Map;
public class SymbolSorter {
@@ -27,8 +28,8 @@ public class SymbolSorter {
Arrays.sort(opDefNodes, new OpDefNodeComparator());
}
- public static Hashtable<String, OpDefNode> getDefsHashTable(OpDefNode[] opDefNodes) {
- Hashtable<String, OpDefNode> definitions = new Hashtable<>();
+ public static Map<String, OpDefNode> getDefsMap(OpDefNode[] opDefNodes) {
+ Map<String, OpDefNode> definitions = new HashMap<>();
for (OpDefNode def : opDefNodes) {
// Definition in this module
// if (StandardModules.contains(def.getOriginallyDefinedInModuleNode()
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index e0da24efc6d75d90d8e5dd391fb3f4e599d875a9..4f6d48b80f0579bc7ea3153ea89c7abdbb4e4a56 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -191,7 +191,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
FormalParamNode[] params = def.getParams();
for (FormalParamNode p : params) {
if (p.getArity() > 0) {
- throw new FrontEndException(String.format("TLA2B do not support 2nd-order operators: '%s'%n %s ",
+ throw new TLA2BFrontEndException(String.format("TLA2B do not support 2nd-order operators: '%s'%n %s ",
def.getName(), def.getLocation()));
}
UntypedType u = new UntypedType();
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index f6c4080b6f28351894dde8e955b63cf839fe2624..ea9f0887655e3fe8f108059db6e43ee56f2ecece 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -12,25 +12,18 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private final Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
private final Hashtable<OpDefNode, ValueObj> operatorAssignments;
- public ModuleOverrider(ModuleNode moduleNode,
- Hashtable<OpDeclNode, OpDefNode> constantOverrideTable,
- Hashtable<OpDefNode, OpDefNode> operatorOverrideTable,
- Hashtable<OpDefNode, ValueObj> operatorAssignments) {
- this.moduleNode = moduleNode;
- this.constantOverrideTable = constantOverrideTable;
- this.operatorOverrideTable = operatorOverrideTable;
- this.operatorAssignments = operatorAssignments;
- }
-
- public ModuleOverrider(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
+ private ModuleOverrider(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
this.moduleNode = moduleNode;
this.constantOverrideTable = conEval.getConstantOverrideTable();
this.operatorOverrideTable = conEval.getOperatorOverrideTable();
this.operatorAssignments = conEval.getOperatorAssignments();
+ }
+ public static void run(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
+ new ModuleOverrider(moduleNode, conEval).start();
}
- public void start() {
+ private void start() {
OpDefNode[] defs = moduleNode.getOpDefs();
for (OpDefNode def : defs) {
if (operatorAssignments.containsKey(def)) {
diff --git a/src/main/java/de/tla2b/exceptions/FrontEndException.java b/src/main/java/de/tla2b/exceptions/FrontEndException.java
deleted file mode 100644
index e2588b9861f31fa4a903cde0d0d38d4c3115e2a3..0000000000000000000000000000000000000000
--- a/src/main/java/de/tla2b/exceptions/FrontEndException.java
+++ /dev/null
@@ -1,18 +0,0 @@
-package de.tla2b.exceptions;
-
-import tla2sany.modanalyzer.SpecObj;
-
-@SuppressWarnings("serial")
-public class FrontEndException extends TLA2BException {
-
- public SpecObj spec;
-
- public FrontEndException(String e) {
- super(e);
- }
-
- public FrontEndException(String string, SpecObj spec) {
- super(string);
- this.spec = spec;
- }
-}
diff --git a/src/main/java/de/tla2b/exceptions/TLA2BFrontEndException.java b/src/main/java/de/tla2b/exceptions/TLA2BFrontEndException.java
new file mode 100644
index 0000000000000000000000000000000000000000..0066b1a8fe5fef9f883c9aedf0613cc4f2c77e37
--- /dev/null
+++ b/src/main/java/de/tla2b/exceptions/TLA2BFrontEndException.java
@@ -0,0 +1,17 @@
+package de.tla2b.exceptions;
+
+import tla2sany.modanalyzer.SpecObj;
+
+public class TLA2BFrontEndException extends TLA2BException {
+
+ public SpecObj spec;
+
+ public TLA2BFrontEndException(String e) {
+ super(e);
+ }
+
+ public TLA2BFrontEndException(String string, SpecObj spec) {
+ super(string);
+ this.spec = spec;
+ }
+}
diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java
index f9252a40a6bc9a3f602b5b08da7389637be3c5ec..33726f4e17e8e17a74f16a41f73c6abe67b3a038 100644
--- a/src/main/java/de/tla2b/global/BBuildIns.java
+++ b/src/main/java/de/tla2b/global/BBuildIns.java
@@ -3,91 +3,58 @@ package de.tla2b.global;
import util.UniqueString;
public interface BBuildIns {
- UniqueString OP_dotdot = UniqueString
- .uniqueStringOf("..");
+ UniqueString OP_dotdot = UniqueString.uniqueStringOf("..");
UniqueString OP_plus = UniqueString.uniqueStringOf("+");
- UniqueString OP_minus = UniqueString
- .uniqueStringOf("-");
- UniqueString OP_times = UniqueString
- .uniqueStringOf("*");
- UniqueString OP_div = UniqueString
- .uniqueStringOf("\\div");
- UniqueString OP_realdiv = UniqueString
- .uniqueStringOf("/");
+ UniqueString OP_minus = UniqueString.uniqueStringOf("-");
+ UniqueString OP_times = UniqueString.uniqueStringOf("*");
+ UniqueString OP_div = UniqueString.uniqueStringOf("\\div");
+ UniqueString OP_realdiv = UniqueString.uniqueStringOf("/");
UniqueString OP_mod = UniqueString.uniqueStringOf("%");
UniqueString OP_exp = UniqueString.uniqueStringOf("^");
- UniqueString OP_uminus = UniqueString
- .uniqueStringOf("-.");
+ UniqueString OP_uminus = UniqueString.uniqueStringOf("-.");
UniqueString OP_lt = UniqueString.uniqueStringOf("<");
- UniqueString OP_leq = UniqueString
- .uniqueStringOf("\\leq");
+ UniqueString OP_leq = UniqueString.uniqueStringOf("\\leq");
UniqueString OP_gt = UniqueString.uniqueStringOf(">");
- UniqueString OP_geq = UniqueString
- .uniqueStringOf("\\geq");
-
- UniqueString OP_nat = UniqueString
- .uniqueStringOf("Nat");
- UniqueString OP_int = UniqueString
- .uniqueStringOf("Int");
- UniqueString OP_real = UniqueString
- .uniqueStringOf("Real");
- UniqueString OP_bool = UniqueString
- .uniqueStringOf("BOOLEAN");
- UniqueString OP_true = UniqueString
- .uniqueStringOf("TRUE");
- UniqueString OP_false = UniqueString
- .uniqueStringOf("FALSE");
- UniqueString OP_string = UniqueString
- .uniqueStringOf("STRING");
+ UniqueString OP_geq = UniqueString.uniqueStringOf("\\geq");
+
+ UniqueString OP_nat = UniqueString.uniqueStringOf("Nat");
+ UniqueString OP_int = UniqueString.uniqueStringOf("Int");
+ UniqueString OP_real = UniqueString.uniqueStringOf("Real");
+ UniqueString OP_bool = UniqueString.uniqueStringOf("BOOLEAN");
+ UniqueString OP_true = UniqueString.uniqueStringOf("TRUE");
+ UniqueString OP_false = UniqueString.uniqueStringOf("FALSE");
+ UniqueString OP_string = UniqueString.uniqueStringOf("STRING");
// Sets
- UniqueString OP_card = UniqueString
- .uniqueStringOf("Cardinality");
- UniqueString OP_finite = UniqueString
- .uniqueStringOf("IsFiniteSet");
+ UniqueString OP_card = UniqueString.uniqueStringOf("Cardinality");
+ UniqueString OP_finite = UniqueString.uniqueStringOf("IsFiniteSet");
// Sequences
- UniqueString OP_len = UniqueString
- .uniqueStringOf("Len");
- UniqueString OP_append = UniqueString
- .uniqueStringOf("Append");
- UniqueString OP_seq = UniqueString
- .uniqueStringOf("Seq");
- UniqueString OP_head = UniqueString
- .uniqueStringOf("Head");
- UniqueString OP_tail = UniqueString
- .uniqueStringOf("Tail");
- UniqueString OP_subseq = UniqueString
- .uniqueStringOf("SubSeq");
- UniqueString OP_conc = UniqueString
- .uniqueStringOf("\\o");
+ UniqueString OP_len = UniqueString.uniqueStringOf("Len");
+ UniqueString OP_append = UniqueString.uniqueStringOf("Append");
+ UniqueString OP_seq = UniqueString.uniqueStringOf("Seq");
+ UniqueString OP_head = UniqueString.uniqueStringOf("Head");
+ UniqueString OP_tail = UniqueString.uniqueStringOf("Tail");
+ UniqueString OP_subseq = UniqueString.uniqueStringOf("SubSeq");
+ UniqueString OP_conc = UniqueString.uniqueStringOf("\\o");
//TLA2B
- UniqueString OP_min = UniqueString
- .uniqueStringOf("MinOfSet");
- UniqueString OP_max = UniqueString
- .uniqueStringOf("MaxOfSet");
- UniqueString OP_setprod = UniqueString
- .uniqueStringOf("SetProduct");
- UniqueString OP_setsum = UniqueString
- .uniqueStringOf("SetSummation");
- UniqueString OP_permseq = UniqueString
- .uniqueStringOf("PermutedSequences");
+ UniqueString OP_min = UniqueString.uniqueStringOf("MinOfSet");
+ UniqueString OP_max = UniqueString.uniqueStringOf("MaxOfSet");
+ UniqueString OP_setprod = UniqueString.uniqueStringOf("SetProduct");
+ UniqueString OP_setsum = UniqueString.uniqueStringOf("SetSummation");
+ UniqueString OP_permseq = UniqueString.uniqueStringOf("PermutedSequences");
//BBuildIns
- UniqueString OP_pow1 = UniqueString
- .uniqueStringOf("POW1");
-
+ UniqueString OP_pow1 = UniqueString.uniqueStringOf("POW1");
//Relations
- UniqueString OP_rel_inverse = UniqueString
- .uniqueStringOf("rel_inverse");
+ UniqueString OP_rel_inverse = UniqueString.uniqueStringOf("rel_inverse");
//TLC
- UniqueString OP_assert = UniqueString
- .uniqueStringOf("Assert");
+ UniqueString OP_assert = UniqueString.uniqueStringOf("Assert");
int B_OPCODE_dotdot = 1;
int B_OPCODE_plus = 2;
@@ -129,11 +96,10 @@ public interface BBuildIns {
int B_OPCODE_pow1 = B_OPCODE_permseq + 1;
-
int B_OPCODE_rel_inverse = B_OPCODE_pow1 + 1;
int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
int B_OPCODE_real = B_OPCODE_assert + 1;
- int B_OPCODE_realdiv = B_OPCODE_real + 1;
+ int B_OPCODE_realdiv = B_OPCODE_assert + 2;
}
diff --git a/src/main/java/de/tla2b/global/BBuiltInOPs.java b/src/main/java/de/tla2b/global/BBuiltInOPs.java
index d82c68f94509407f76ceb017af2b2c80c9b24628..9fdc564cc960817fa56dfd54a2c2469c576c787b 100644
--- a/src/main/java/de/tla2b/global/BBuiltInOPs.java
+++ b/src/main/java/de/tla2b/global/BBuiltInOPs.java
@@ -2,13 +2,14 @@ package de.tla2b.global;
import util.UniqueString;
-import java.util.Hashtable;
+import java.util.HashMap;
+import java.util.Map;
public class BBuiltInOPs implements BBuildIns {
- private static final Hashtable<UniqueString, Integer> B_Opcode_Table;
+ private static final Map<UniqueString, Integer> B_Opcode_Table;
static {
- B_Opcode_Table = new Hashtable<>();
+ B_Opcode_Table = new HashMap<>();
B_Opcode_Table.put(OP_dotdot, B_OPCODE_dotdot);
B_Opcode_Table.put(OP_plus, B_OPCODE_plus);
B_Opcode_Table.put(OP_minus, B_OPCODE_minus);
diff --git a/src/main/java/de/tla2b/translation/OperationsFinder.java b/src/main/java/de/tla2b/translation/OperationsFinder.java
index 77f53e92ae3416fe7ee74de274b623402036cd27..4bb59e017f063afdc5967ca7a89a3c9694258d4f 100644
--- a/src/main/java/de/tla2b/translation/OperationsFinder.java
+++ b/src/main/java/de/tla2b/translation/OperationsFinder.java
@@ -19,16 +19,13 @@ public class OperationsFinder extends AbstractASTVisitor implements
private String currentName;
private ArrayList<OpApplNode> exists;
- // a list containing all existential quantifier which will be parameters in
- // the resulting B Maschine
-
+ // a list containing all existential quantifier which will be parameters in the resulting B Machine
private final ArrayList<BOperation> bOperations;
public OperationsFinder(SpecAnalyser specAnalyser) {
this.specAnalyser = specAnalyser;
this.bOperations = new ArrayList<>();
if (specAnalyser.getNext() != null) {
-
currentName = "Next";
exists = new ArrayList<>();
visitExprNode(specAnalyser.getNext());
@@ -150,11 +147,9 @@ public class OperationsFinder extends AbstractASTVisitor implements
}
throw new RuntimeException(String.format(
"Expected an action at '%s' :%n%s", n.getOperator().getName(), n.getLocation().toString()));
-
}
public ArrayList<BOperation> getBOperations() {
return bOperations;
}
-
}
diff --git a/src/main/java/de/tla2b/util/FileUtils.java b/src/main/java/de/tla2b/util/FileUtils.java
index 91fb30edc5bb3ce8069882c6ced2038596aa08c3..1a73bc1c59b517658b6aa9fa9184c0715d84faf8 100644
--- a/src/main/java/de/tla2b/util/FileUtils.java
+++ b/src/main/java/de/tla2b/util/FileUtils.java
@@ -21,8 +21,7 @@ public class FileUtils {
return filePath;
} else {
// Remove the last period and everything after it
- File renamed = new File(f.getParent(), name.substring(0,
- lastPeriodPos));
+ File renamed = new File(f.getParent(), name.substring(0, lastPeriodPos));
return renamed.getPath();
}
}
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 05e10926c6a302b8a455b47ce8aa9aa28af53a6a..2d7525b08452219088ed6adf9d961ebd4706a17e 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -1810,26 +1810,14 @@ public class BAstCreator extends BuiltInOPs
return new ARecExpression(list);
} else {
- FunctionType func = (FunctionType) tlaType;
-
- ACoupleExpression couple = new ACoupleExpression();
- List<PExpression> coupleList = new ArrayList<>();
- coupleList.add(visitExprOrOpArgNodeExpression(head));
-
- AFunctionExpression funcCall = new AFunctionExpression();
- funcCall.setIdentifier(prefix);
- List<PExpression> argList = new ArrayList<>();
- argList.add(visitExprOrOpArgNodeExpression(head));
- funcCall.setParameters(argList);
- coupleList.add(evalExceptValue(funcCall, seqList, func.getRange(), val));
- couple.setList(coupleList);
- List<PExpression> setList = new ArrayList<>();
- setList.add(couple);
- ASetExtensionExpression setExtension = new ASetExtensionExpression(setList);
- AOverwriteExpression overwrite = new AOverwriteExpression();
- overwrite.setLeft(prefix.clone());
- overwrite.setRight(setExtension);
- return overwrite;
+ AFunctionExpression funcCall = new AFunctionExpression(prefix,
+ Collections.singletonList(visitExprOrOpArgNodeExpression(head)));
+ List<PExpression> coupleList = Arrays.asList(visitExprOrOpArgNodeExpression(head),
+ evalExceptValue(funcCall, seqList, ((FunctionType) tlaType).getRange(), val));
+ return new AOverwriteExpression(
+ prefix.clone(),
+ new ASetExtensionExpression(Collections.singletonList(new ACoupleExpression(coupleList)))
+ );
}
}
@@ -1841,10 +1829,10 @@ public class BAstCreator extends BuiltInOPs
int index;
if (field == 1) {
index = 2;
- AFirstProjectionExpression first = new AFirstProjectionExpression();
- first.setExp1(tuple.getTypes().get(0).getBNode());
- first.setExp2(tuple.getTypes().get(1).getBNode());
- returnFunc.setIdentifier(first);
+ returnFunc.setIdentifier(new AFirstProjectionExpression(
+ tuple.getTypes().get(0).getBNode(),
+ tuple.getTypes().get(1).getBNode()
+ ));
} else {
index = field;
ASecondProjectionExpression second = new ASecondProjectionExpression();
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index 934b3716fa647991bf02e648625edc557f508cce..70df795009c7670deaaff2c0df87ade88adea6bd 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -6,6 +6,7 @@ import de.tla2b.analysis.SymbolRenamer;
import de.tla2b.analysis.TypeChecker;
import de.tla2b.exceptions.ExpressionTranslationException;
import de.tla2b.exceptions.TLA2BException;
+import de.tla2b.exceptions.TLA2BFrontEndException;
import de.tla2b.exceptions.TypeErrorException;
import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.InitException;
@@ -106,7 +107,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
this.moduleNode = null;
try {
moduleNode = parseModule(moduleName, sb.toString());
- } catch (de.tla2b.exceptions.FrontEndException e) {
+ } catch (TLA2BFrontEndException e) {
throw new ExpressionTranslationException(e.getLocalizedMessage());
}
}
@@ -162,35 +163,35 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
}
public static ModuleNode parseModule(String moduleName, String module)
- throws de.tla2b.exceptions.FrontEndException {
+ throws TLA2BFrontEndException {
SpecObj spec = new SpecObj(moduleName, null);
try {
SANY.frontEndMain(spec, moduleName, ToolIO.out);
} catch (FrontEndException e) {
// Error in Frontend, should never happen
- throw new de.tla2b.exceptions.FrontEndException("Frontend error! This should never happen.", spec);
+ throw new TLA2BFrontEndException("Frontend error! This should never happen.", spec);
}
if (spec.parseErrors.isFailure()) {
String message = module + "\n\n" + spec.parseErrors + allMessagesToString(ToolIO.getAllMessages());
- throw new de.tla2b.exceptions.FrontEndException(message, spec);
+ throw new TLA2BFrontEndException(message, spec);
}
if (spec.semanticErrors.isFailure()) {
String message = module + "\n\n" + spec.semanticErrors + allMessagesToString(ToolIO.getAllMessages());
- throw new de.tla2b.exceptions.FrontEndException(message, spec);
+ throw new TLA2BFrontEndException(message, spec);
}
// RootModule
ModuleNode n = spec.getExternalModuleTable().rootModule;
if (spec.getInitErrors().isFailure()) {
System.err.println(spec.getInitErrors());
- throw new de.tla2b.exceptions.FrontEndException(allMessagesToString(ToolIO.getAllMessages()), spec);
+ throw new TLA2BFrontEndException(allMessagesToString(ToolIO.getAllMessages()), spec);
}
if (n == null) { // Parse Error
// System.out.println("Rootmodule null");
- throw new de.tla2b.exceptions.FrontEndException(
+ throw new TLA2BFrontEndException(
allMessagesToString(ToolIO.getAllMessages()), spec);
}
return n;
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 5f09fde2f449676c200f8b968592a4680dc303a4..79c2d965f1e7357372772d389f8ec16c061658ca 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -12,7 +12,7 @@ import de.be4.classicalb.core.parser.util.SuffixIdentifierRenaming;
import de.tla2b.analysis.*;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.ModuleOverrider;
-import de.tla2b.exceptions.FrontEndException;
+import de.tla2b.exceptions.TLA2BFrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.output.PrologPrinter;
@@ -20,6 +20,7 @@ import de.tla2b.translation.BMacroHandler;
import de.tla2b.translation.RecursiveFunctionHandler;
import de.tla2b.types.TLAType;
import de.tla2b.util.FileUtils;
+import tla2sany.drivers.FrontEndException;
import tla2sany.drivers.SANY;
import tla2sany.modanalyzer.SpecObj;
import tla2sany.semantic.ModuleNode;
@@ -49,34 +50,25 @@ public class Translator implements TranslationGlobals {
private SpecAnalyser specAnalyser;
private TypeChecker typechecker;
- public Translator(String moduleFileName) throws FrontEndException {
+ public Translator(String moduleFileName) throws TLA2BFrontEndException {
this.moduleFileName = moduleFileName;
- findModuleFile();
- findConfigFile();
-
- parse();
- }
-
- private void findConfigFile() {
- String configFileName = FileUtils.removeExtension(moduleFile.getAbsolutePath());
- configFileName = configFileName + ".cfg";
- configFile = new File(configFileName);
- if (!configFile.exists()) {
- configFile = null;
- }
- }
-
- private void findModuleFile() {
- moduleFile = new File(moduleFileName);
+ this.moduleFile = new File(moduleFileName);
if (!moduleFile.exists()) {
throw new RuntimeException("Can not find module file: '" + moduleFileName + "'");
}
try {
- moduleFile = moduleFile.getCanonicalFile();
+ this.moduleFile = moduleFile.getCanonicalFile();
} catch (IOException e) {
throw new RuntimeException("Can not access module file: '" + moduleFileName + "'");
}
+
+ this.configFile = new File(FileUtils.removeExtension(moduleFile.getAbsolutePath()) + ".cfg");
+ if (!configFile.exists()) {
+ this.configFile = null;
+ }
+
+ parse();
}
/**
@@ -100,13 +92,30 @@ public class Translator implements TranslationGlobals {
}
// Used for Testing in tla2bAST project
- public Translator(String moduleString, String configString) throws FrontEndException {
+ public Translator(String moduleString, String configString) throws TLA2BFrontEndException {
String moduleName = "Testing";
createTLATempFile(moduleString, moduleName);
createCfgFile(configString, moduleName);
parse();
}
+ private void createTLATempFile(String moduleString, String moduleName) {
+ File dir = new File("temp/");
+ dir.mkdirs();
+ dir.deleteOnExit();
+
+ try {
+ moduleFile = new File("temp/" + moduleName + ".tla");
+ moduleFile.createNewFile();
+ try (BufferedWriter out = new BufferedWriter(new OutputStreamWriter(Files.newOutputStream(moduleFile.toPath()), StandardCharsets.UTF_8))) {
+ out.write(moduleString);
+ }
+ moduleFileName = moduleFile.getAbsolutePath();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
+
private void createCfgFile(String configString, String moduleName) {
modelConfig = null;
if (configString != null) {
@@ -114,7 +123,7 @@ public class Translator implements TranslationGlobals {
try {
configFile.createNewFile();
try (BufferedWriter out = new BufferedWriter(
- new OutputStreamWriter(Files.newOutputStream(configFile.toPath()), StandardCharsets.UTF_8))) {
+ new OutputStreamWriter(Files.newOutputStream(configFile.toPath()), StandardCharsets.UTF_8))) {
out.write(configString);
}
} catch (IOException e) {
@@ -123,78 +132,51 @@ public class Translator implements TranslationGlobals {
}
}
- private void createTLATempFile(String moduleString, String moduleName) {
- File dir = new File("temp/");
- dir.mkdirs();
- dir.deleteOnExit();
+ private void parse() throws TLA2BFrontEndException {
+ moduleNode = parseModule();
- try {
- moduleFile = new File("temp/" + moduleName + ".tla");
- moduleFile.createNewFile();
- try (BufferedWriter out = new BufferedWriter(new OutputStreamWriter(Files.newOutputStream(moduleFile.toPath()), StandardCharsets.UTF_8))) {
- out.write(moduleString);
- }
- moduleFileName = moduleFile.getAbsolutePath();
- } catch (IOException e) {
- e.printStackTrace();
+ modelConfig = null;
+ if (configFile != null) {
+ modelConfig = new ModelConfig(configFile.getAbsolutePath(), new SimpleResolver());
+ modelConfig.parse();
}
}
- public ModuleNode parseModule() throws de.tla2b.exceptions.FrontEndException {
+ public ModuleNode parseModule() throws TLA2BFrontEndException {
String fileName = moduleFile.getName();
ToolIO.setUserDir(moduleFile.getParent());
SpecObj spec = new SpecObj(fileName, null);
try {
SANY.frontEndMain(spec, fileName, ToolIO.out);
- } catch (tla2sany.drivers.FrontEndException e) {
+ } catch (FrontEndException e) {
// should never happen
- e.printStackTrace();
+ throw new RuntimeException("Could not parse module: '" + fileName + "'", e);
}
- if (spec.parseErrors.isFailure()) {
- throw new de.tla2b.exceptions.FrontEndException(
- allMessagesToString(ToolIO.getAllMessages()) + spec.parseErrors, spec);
+ if (spec.getParseErrors().isFailure()) {
+ throw new TLA2BFrontEndException(allMessagesToString(ToolIO.getAllMessages()) + spec.getParseErrors(), spec);
}
- if (spec.semanticErrors.isFailure()) {
- throw new de.tla2b.exceptions.FrontEndException(
- // allMessagesToString(ToolIO.getAllMessages())
- "" + spec.semanticErrors, spec);
+ if (spec.getSemanticErrors().isFailure()) {
+ throw new TLA2BFrontEndException(allMessagesToString(ToolIO.getAllMessages()) + spec.getSemanticErrors(), spec);
}
// RootModule
- ModuleNode n = spec.getExternalModuleTable().rootModule;
+ ModuleNode n = spec.getExternalModuleTable().getRootModule();
if (spec.getInitErrors().isFailure()) {
- System.err.println(spec.getInitErrors());
- return null;
+ throw new TLA2BFrontEndException(spec.getInitErrors().toString(), spec);
}
if (n == null) { // Parse Error
- // System.out.println("Rootmodule null");
- throw new de.tla2b.exceptions.FrontEndException(allMessagesToString(ToolIO.getAllMessages()), spec);
+ throw new TLA2BFrontEndException(allMessagesToString(ToolIO.getAllMessages()), spec);
}
return n;
}
public static String allMessagesToString(String[] allMessages) {
- StringBuilder sb = new StringBuilder();
- for (int i = 0; i < allMessages.length - 1; i++) {
- sb.append(allMessages[i]).append("\n");
- }
- return sb.toString();
- }
-
- private void parse() throws FrontEndException {
- moduleNode = parseModule();
-
- modelConfig = null;
- if (configFile != null) {
- modelConfig = new ModelConfig(configFile.getAbsolutePath(), new SimpleResolver());
- modelConfig.parse();
- }
-
+ return String.join("\n", allMessages) + "\n";
}
public Start translate() throws TLA2BException {
@@ -206,8 +188,7 @@ public class Translator implements TranslationGlobals {
conEval = new ConfigfileEvaluator(modelConfig, moduleNode);
conEval.start();
- ModuleOverrider modOver = new ModuleOverrider(moduleNode, conEval);
- modOver.start();
+ ModuleOverrider.run(moduleNode, conEval);
specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode, conEval);
} else {
specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode);
@@ -222,10 +203,9 @@ public class Translator implements TranslationGlobals {
new BMacroHandler(specAnalyser, conEval),
new RecursiveFunctionHandler(specAnalyser));
- this.BAst = bAstCreator.getStartNode();
this.typeTable = bAstCreator.getTypeTable();
this.bDefinitions = bAstCreator.getBDefinitions();
- return BAst;
+ return this.BAst = bAstCreator.getStartNode();
}
public void createProbFile() {