diff --git a/build.gradle b/build.gradle
index f574f8b6d041249c860ad27c06ff1177d433463d..ac502c12521b0c93bfbee47ed32c893180e1b15e 100644
--- a/build.gradle
+++ b/build.gradle
@@ -4,7 +4,7 @@ apply plugin: 'maven'
apply plugin: 'jacoco'
apply plugin: 'findbugs'
-project.version = '1.0.9'
+project.version = '1.1.0'
project.group = 'de.hhu.stups'
project.archivesBaseName = "tla2bAST"
@@ -13,15 +13,15 @@ project.targetCompatibility = '1.7'
repositories {
- mavenCentral()
- maven {
- name "sonatype snapshots"
- url "https://oss.sonatype.org/content/repositories/snapshots"
- }
- maven {
- name "sonatype releases"
- url "https://oss.sonatype.org/content/repositories/releases"
- }
+ mavenCentral()
+ maven {
+ name "sonatype snapshots"
+ url "https://oss.sonatype.org/content/repositories/snapshots"
+ }
+ maven {
+ name "sonatype releases"
+ url "https://oss.sonatype.org/content/repositories/releases"
+ }
}
configurations.all {
@@ -30,22 +30,22 @@ configurations.all {
def parser_version
if (project.version.endsWith("-SNAPSHOT")) {
- parser_version = '2.9.7-SNAPSHOT'
+ parser_version = '2.9.13-SNAPSHOT'
}
else {
- parser_version = '2.9.6'
+ parser_version = '2.9.12'
}
def tlatools_version = '1.0.2'
dependencies {
- compile 'commons-cli:commons-cli:1.2'
- compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
- compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
- compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
- compile (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
- compile (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
+ compile (group: 'commons-cli', name: 'commons-cli', version: '1.4')
+ compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
+ compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
+ compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
+ compile (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
+ compile (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
testCompile (group: 'junit', name: 'junit', version: '4.12')
}
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index d25f0fe674df1cdc01a76c216e00348b473a380a..0dfe571d7721e6438eb9c3a500fa5852270c3f65 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -376,6 +376,10 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
// Tuple
for (int i = 0; i < k.getArgs().length; i++) {
OpApplNode var = (OpApplNode) k.getArgs()[i];
+ //findUnchangedVariablesInOpApplNode(var);
+ if(!(var.getOperator() instanceof OpDeclNode)) {
+ throw new RuntimeException(var.getOperator().getName() + " " + var.getLocation());
+ }
unchangedVariablesList.add((OpDeclNode) var
.getOperator());
String name = var.getOperator().getName().toString();
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 9412c11c26c1772461b7e0dc34466b0285928d9a..5e17ba396f27fc5f970cd3378c0d39b4311c1cc1 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -33,15 +33,14 @@ import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
-public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
- ToolGlobals, TranslationGlobals {
+public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals {
private OpDefNode spec;
private OpDefNode init;
private OpDefNode next;
- private ArrayList<OpDefNode> invariants = new ArrayList<OpDefNode>();
+ private ArrayList<OpDefNode> invariants = new ArrayList<>();
private OpDefNode expressionOpdefNode;
- private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<String, SymbolNode>();
+ private Hashtable<String, SymbolNode> namingHashTable = new Hashtable<>();
private final ModuleNode moduleNode;
private ExprNode nextExpr;
@@ -57,14 +56,14 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
// set of OpDefNodes which will appear in the resulting B Machine
private Set<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
// definitions which are used for the type inference algorithm
- private Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<OpDefNode, FormalParamNode[]>();
+ private Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>();
// additional parameters of an let Operator, these parameters are from the
// surrounding operator
- private ArrayList<String> definitionMacros = new ArrayList<String>();
+ private ArrayList<String> definitionMacros = new ArrayList<>();
- private ArrayList<OpDefNode> recursiveFunctions = new ArrayList<OpDefNode>();
+ private ArrayList<OpDefNode> recursiveFunctions = new ArrayList<>();
- private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<RecursiveDefinition>();
+ private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
private ConfigfileEvaluator configFileEvaluator;
@@ -73,8 +72,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
this.bConstants = new ArrayList<OpDeclNode>();
}
- public static SpecAnalyser createSpecAnalyser(ModuleNode m,
- ConfigfileEvaluator conEval) {
+ public static SpecAnalyser createSpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) {
SpecAnalyser specAnalyser = new SpecAnalyser(m);
specAnalyser.spec = conEval.getSpecNode();
specAnalyser.init = conEval.getInitNode();
@@ -99,8 +97,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
SpecAnalyser specAnalyser = new SpecAnalyser(m);
Hashtable<String, OpDefNode> definitions = new Hashtable<String, OpDefNode>();
for (int i = 0; i < m.getOpDefs().length; i++) {
- definitions.put(m.getOpDefs()[i].getName().toString(),
- m.getOpDefs()[i]);
+ definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]);
}
specAnalyser.spec = definitions.get("Spec");
specAnalyser.init = definitions.get("Init");
@@ -115,8 +112,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return specAnalyser;
}
- public void start() throws SemanticErrorException, FrontEndException,
- ConfigFileErrorException, NotImplementedException {
+ public void start()
+ throws SemanticErrorException, FrontEndException, ConfigFileErrorException, NotImplementedException {
if (spec != null) {
evalSpec();
@@ -131,8 +128,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
OpDefNode opDefNode = (OpDefNode) opApplNode.getOperator();
- if (opDefNode.getKind() == UserDefinedOpKind
- && !BBuiltInOPs.contains(opDefNode.getName())) {
+ if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())) {
int i = invariants.indexOf(inv);
invariants.set(i, opDefNode);
}
@@ -160,9 +156,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
OpDeclNode con = bConstants.get(i);
if (con.getArity() > 0) {
throw new ConfigFileErrorException(
- String.format(
- "Constant '%s' must be overriden in the configuration file.",
- con.getName()));
+ String.format("Constant '%s' must be overriden in the configuration file.", con.getName()));
}
}
findRecursiveConstructs();
@@ -198,8 +192,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
- private void processConfigSpec(ExprNode exprNode)
- throws SemanticErrorException, FrontEndException {
+ private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException, FrontEndException {
if (exprNode instanceof OpApplNode) {
OpApplNode opApp = (OpApplNode) exprNode;
@@ -217,8 +210,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
return;
}
- throw new SemanticErrorException(
- "Can not handle specification conjunction.");
+ throw new SemanticErrorException("Can not handle specification conjunction.");
}
int opcode = BuiltInOPs.getOpCode(opApp.getOperator().getName());
@@ -232,8 +224,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
if (opcode == OPCODE_box) {
SemanticNode boxArg = args[0];
if ((boxArg instanceof OpApplNode)
- && BuiltInOPs.getOpCode(((OpApplNode) boxArg)
- .getOperator().getName()) == OPCODE_sa) {
+ && BuiltInOPs.getOpCode(((OpApplNode) boxArg).getOperator().getName()) == OPCODE_sa) {
ExprNode next = (ExprNode) ((OpApplNode) boxArg).getArgs()[0];
this.nextExpr = next;
return;
@@ -247,8 +238,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
// temporal
} else {
- throw new SemanticErrorException(
- "Can not handle specification conjunction.");
+ throw new SemanticErrorException("Can not handle specification conjunction.");
}
}
@@ -257,8 +247,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
Set<OpDefNode> set = new HashSet<OpDefNode>(usedDefinitions);
for (OpDefNode def : set) {
if (def.getInRecursive()) {
- throw new NotImplementedException(
- "Recursive definitions are currently not supported: " + def.getName() + "\n" + def.getLocation() );
+ throw new NotImplementedException("Recursive definitions are currently not supported: " + def.getName()
+ + "\n" + def.getLocation());
// bDefinitionsSet.remove(def);
// RecursiveDefinition rd = new RecursiveDefinition(def);
// recursiveDefinitions.add(rd);
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 542e34cc1fb626484739ce1d13e93148b37b037c..70120d2d409ef18a4269837ff5c1b2468e44b802 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -42,15 +42,15 @@ import tla2sany.semantic.StringNode;
import tla2sany.semantic.SymbolNode;
import tlc2.tool.BuiltInOPs;
-public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
- TranslationGlobals {
+public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns, TranslationGlobals {
private static final int TEMP_TYPE_ID = 6;
private int paramId;
private ArrayList<ExprNode> inits;
private ExprNode nextExpr;
- private Set<OpDefNode> usedDefinitions;
+ private final Set<OpDefNode> usedDefinitions;
+ private final Set<OpDefNode> bDefinitions;
private ArrayList<SymbolNode> symbolNodeList = new ArrayList<SymbolNode>();
private ArrayList<SemanticNode> tupleNodeList = new ArrayList<SemanticNode>();
@@ -68,8 +68,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* @param conEval
* @param specAnalyser
*/
- public TypeChecker(ModuleNode moduleNode, ConfigfileEvaluator conEval,
- SpecAnalyser specAnalyser) {
+ public TypeChecker(ModuleNode moduleNode, ConfigfileEvaluator conEval, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
if (conEval != null) {
@@ -80,6 +79,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
this.inits = specAnalyser.getInits();
this.nextExpr = specAnalyser.getNext();
usedDefinitions = specAnalyser.getUsedDefinitions();
+ this.bDefinitions = specAnalyser.getBDefinitions();
paramId = TYPE_ID;
}
@@ -92,7 +92,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
// used the last definition of the module
usedDefinitions.add(defs[defs.length - 1]);
this.usedDefinitions = usedDefinitions;
-
+ this.bDefinitions = specAnalyser.getBDefinitions();
paramId = TYPE_ID;
}
@@ -100,8 +100,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
OpDeclNode[] cons = moduleNode.getConstantDecls();
for (int i = 0; i < cons.length; i++) {
OpDeclNode con = cons[i];
- if (constantAssignments != null
- && constantAssignments.containsKey(con)) {
+ if (constantAssignments != null && constantAssignments.containsKey(con)) {
TLAType t = constantAssignments.get(con).getType();
con.setToolObject(TYPE_ID, t);
@@ -126,8 +125,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
evalDefinitions(moduleNode.getOpDefs());
if (conEval != null) {
- Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval
- .getConstantOverrideTable().entrySet().iterator();
+ Iterator<Entry<OpDeclNode, OpDefNode>> iter = conEval.getConstantOverrideTable().entrySet().iterator();
while (iter.hasNext()) {
Entry<OpDeclNode, OpDefNode> entry = iter.next();
OpDeclNode con = entry.getKey();
@@ -142,9 +140,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType result = defType.unify(conType);
con.setToolObject(TYPE_ID, result);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at constant '%s'.", defType,
- conType, con.getName()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at constant '%s'.", defType, conType, con.getName()));
}
}
}
@@ -172,8 +169,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
OpDeclNode var = vars[i];
TLAType varType = (TLAType) var.getToolObject(TYPE_ID);
if (varType.isUntyped()) {
- throw new TypeErrorException("The type of the variable '" + var.getName()
- + "' can not be inferred: " + varType);
+ throw new TypeErrorException(
+ "The type of the variable '" + var.getName() + "' can not be inferred: " + varType);
}
}
@@ -185,8 +182,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
if (bConstList == null || bConstList.contains(con)) {
TLAType conType = (TLAType) con.getToolObject(TYPE_ID);
if (conType.isUntyped()) {
- throw new TypeErrorException("The type of constant "
- + con.getName() + " is still untyped: " + conType);
+ throw new TypeErrorException(
+ "The type of constant " + con.getName() + " is still untyped: " + conType);
}
}
}
@@ -194,8 +191,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
for (SymbolNode symbol : symbolNodeList) {
TLAType type = (TLAType) symbol.getToolObject(TYPE_ID);
if (type.isUntyped()) {
- throw new TypeErrorException("Symbol '" + symbol.getName()
- + "' has no type.\n" + symbol.getLocation());
+ throw new TypeErrorException("Symbol '" + symbol.getName() + "' has no type.\n" + symbol.getLocation());
}
}
@@ -213,16 +209,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
for (int i = 0; i < opDefs.length; i++) {
OpDefNode def = opDefs[i];
// Definition in this module
- String moduleName1 = def.getOriginallyDefinedInModuleNode()
- .getName().toString();
- String moduleName2 = def.getSource()
- .getOriginallyDefinedInModuleNode().getName().toString();
+ String moduleName1 = def.getOriginallyDefinedInModuleNode().getName().toString();
+ String moduleName2 = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
- if (STANDARD_MODULES.contains(moduleName1)
- || STANDARD_MODULES.contains(moduleName2)) {
+ if (STANDARD_MODULES.contains(moduleName1) || STANDARD_MODULES.contains(moduleName2)) {
continue;
}
- if (usedDefinitions.contains(def))
+ if (usedDefinitions.contains(def) || bDefinitions.contains(def))
visitOpDefNode(def);
}
@@ -237,8 +230,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
for (int i = 0; i < params.length; i++) {
FormalParamNode p = params[i];
if (p.getArity() > 0) {
- throw new FrontEndException(String.format(
- "TLA2B do not support 2nd-order operators: '%s'%n %s ",
+ throw new FrontEndException(String.format("TLA2B do not support 2nd-order operators: '%s'%n %s ",
def.getName(), def.getLocation()));
}
UntypedType u = new UntypedType();
@@ -256,8 +248,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- private void evalAssumptions(AssumeNode[] assumptions)
- throws TLA2BException {
+ private void evalAssumptions(AssumeNode[] assumptions) throws TLA2BException {
for (AssumeNode assumeNode : assumptions) {
visitExprNode(assumeNode.getAssume(), BoolType.getInstance());
}
@@ -269,8 +260,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* @throws TypeErrorException
* @throws NotImplementedException
*/
- private TLAType visitExprOrOpArgNode(ExprOrOpArgNode n, TLAType expected)
- throws TLA2BException {
+ private TLAType visitExprOrOpArgNode(ExprOrOpArgNode n, TLAType expected) throws TLA2BException {
if (n instanceof ExprNode) {
return visitExprNode((ExprNode) n, expected);
} else {
@@ -279,8 +269,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- private TLAType visitExprNode(ExprNode exprNode, TLAType expected)
- throws TLA2BException {
+ private TLAType visitExprNode(ExprNode exprNode, TLAType expected) throws TLA2BException {
switch (exprNode.getKind()) {
case TLCValueKind: {
@@ -289,10 +278,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return valueNode.getType().unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(
- String.format(
- "Expected %s, found %s at '%s'(assigned in the configuration file),%n%s ",
- expected, valueNode.getType(),
- valueNode.getValue(), exprNode.getLocation()));
+ String.format("Expected %s, found %s at '%s'(assigned in the configuration file),%n%s ",
+ expected, valueNode.getType(), valueNode.getValue(), exprNode.getLocation()));
}
}
@@ -304,18 +291,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
return IntType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '%s',%n%s ", expected,
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s ", expected,
((NumeralNode) exprNode).val(), exprNode.getLocation()));
}
case StringKind: {
try {
return StringType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found STRING at '%s',%n%s ", expected,
- ((StringNode) exprNode).getRep(),
- exprNode.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found STRING at '%s',%n%s ", expected,
+ ((StringNode) exprNode).getRep(), exprNode.getLocation()));
}
}
case AtNodeKind: { // @
@@ -328,9 +312,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
setType(exprNode, res);
return res;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at '@',%n%s ", expected, type,
- exprNode.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at '@',%n%s ", expected, type, exprNode.getLocation()));
}
}
@@ -344,8 +327,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
case SubstInKind: {
- throw new RuntimeException(
- "SubstInKind should never occur after InstanceTransformation");
+ throw new RuntimeException("SubstInKind should never occur after InstanceTransformation");
}
case DecimalKind: {
@@ -375,8 +357,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* @return {@link TLAType}
* @throws TLA2BException
*/
- private TLAType visitOpApplNode(OpApplNode n, TLAType expected)
- throws TLA2BException {
+ private TLAType visitOpApplNode(OpApplNode n, TLAType expected) throws TLA2BException {
switch (n.getOperator().getKind()) {
case ConstantDeclKind: {
@@ -391,9 +372,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
con.setToolObject(TYPE_ID, result);
return result;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at constant '%s',%n%s",
- expected, c, con.getName(), n.getLocation())
+ throw new TypeErrorException(String.format("Expected %s, found %s at constant '%s',%n%s", expected, c,
+ con.getName(), n.getLocation())
);
}
@@ -417,9 +397,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
symbolNode.setToolObject(TYPE_ID, result);
return result;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at variable '%s',%n%s",
- expected, v, vName, n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found %s at variable '%s',%n%s", expected, v,
+ vName, n.getLocation()));
}
}
@@ -437,16 +416,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
if (t == null) {
t = new UntypedType(); // TODO is this correct?
- //throw new RuntimeException();
+ // throw new RuntimeException();
}
try {
TLAType result = expected.unify(t);
symbolNode.setToolObject(paramId, result);
return result;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at parameter '%s',%n%s",
- expected, t, pName, n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found %s at parameter '%s',%n%s", expected, t,
+ pName, n.getLocation()));
}
}
@@ -454,10 +432,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
OpDefNode def = (OpDefNode) n.getOperator();
// Definition is a BBuilt-in definition
- String sourceModule = def.getSource()
- .getOriginallyDefinedInModuleNode().getName().toString();
- if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(sourceModule)) {
+ String sourceModule = def.getSource().getOriginallyDefinedInModuleNode().getName().toString();
+ if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(sourceModule)) {
return evalBBuiltIns(n, expected);
}
@@ -474,10 +450,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- e.printStackTrace();
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at definition '%s',%n%s",
- expected, found, def.getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found %s at definition '%s',%n%s", expected,
+ found, def.getName(), n.getLocation()));
}
boolean untyped = false;
FormalParamNode[] params = def.getParams();
@@ -517,8 +491,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
default: {
- throw new NotImplementedException(n.getOperator().getName()
- .toString());
+ throw new NotImplementedException(n.getOperator().getName().toString());
}
}
@@ -530,8 +503,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* @return {@link TLAType}
* @throws TLA2BException
*/
- private TLAType evalBuiltInKind(OpApplNode n, TLAType expected)
- throws TLA2BException {
+ private TLAType evalBuiltInKind(OpApplNode n, TLAType expected) throws TLA2BException {
switch (getOpCode(n.getOperator().getName())) {
@@ -544,12 +516,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
- TLAType left = visitExprOrOpArgNode(n.getArgs()[0],
- new de.tla2b.types.UntypedType());
+ TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new de.tla2b.types.UntypedType());
visitExprOrOpArgNode(n.getArgs()[1], left);
return BoolType.getInstance();
}
@@ -569,9 +539,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
visitExprOrOpArgNode(n.getArgs()[i], BoolType.getInstance());
@@ -588,9 +557,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
evalBoundedVariables(n);
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -606,9 +574,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at set enumeration,%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(_A) at set enumeration,%n%s", expected, n.getLocation()));
}
TLAType current = found.getSubType();
for (int i = 0; i < n.getArgs().length; i++) {
@@ -621,12 +588,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case OPCODE_notin: // \notin
{
if (!BoolType.getInstance().compare(expected)) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
- TLAType element = visitExprOrOpArgNode(n.getArgs()[0],
- new UntypedType());
+ TLAType element = visitExprOrOpArgNode(n.getArgs()[0], new UntypedType());
visitExprOrOpArgNode(n.getArgs()[1], new SetType(element));
return BoolType.getInstance();
@@ -640,9 +605,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found POW(_A) at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
TLAType left = visitExprOrOpArgNode(n.getArgs()[0], found);
TLAType right = visitExprOrOpArgNode(n.getArgs()[1], left);
@@ -654,12 +618,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
- TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new SetType(
- new UntypedType()));
+ TLAType left = visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
visitExprOrOpArgNode(n.getArgs()[1], left);
return BoolType.getInstance();
}
@@ -675,8 +637,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at '%s',%n%s", expected, found,
+ throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -689,9 +650,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found POW(_A) at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
evalBoundedVariables(n);
visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
@@ -704,9 +664,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at 'SUBSET',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(_A) at 'SUBSET',%n%s", expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], found.getSubType());
return found;
@@ -718,12 +677,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(_A) at 'SUBSET',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(_A) at 'SUBSET',%n%s", expected, n.getLocation()));
}
- SetType setOfSet = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(found));
+ SetType setOfSet = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(found));
return setOfSet.getSubType();
}
@@ -735,15 +692,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
OpApplNode node = (OpApplNode) n.getArgs()[0];
if (node.getOperator().getKind() != VariableDeclKind) {
- throw new TypeErrorException("Expected variable at \""
- + node.getOperator().getName() + "\":\n"
- + node.getLocation());
+ throw new TypeErrorException(
+ "Expected variable at \"" + node.getOperator().getName() + "\":\n" + node.getLocation());
}
return visitExprOrOpArgNode(n.getArgs()[0], expected);
} catch (ClassCastException e) {
throw new TypeErrorException(
- "Expected variable as argument of prime operator:\n"
- + n.getArgs()[0].getLocation());
+ "Expected variable as argument of prime operator:\n" + n.getArgs()[0].getLocation());
}
}
@@ -757,8 +712,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
TLAType found = null;
if (list.size() == 0) {
- found = new FunctionType(IntType.getInstance(),
- new UntypedType());
+ found = new FunctionType(IntType.getInstance(), new UntypedType());
} else if (list.size() == 1) {
found = new FunctionType(IntType.getInstance(), list.get(0));
} else {
@@ -768,9 +722,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at Tuple,%n%s", expected, found,
- n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at Tuple,%n%s", expected, found, n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
tupleNodeList.add(n);
@@ -800,8 +753,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected
- + "', found '" + found + "'.\n" + n.getLocation());
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n" + n.getLocation());
}
TLAType t = null;
@@ -809,8 +761,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
t = (TLAType) recFunc.getToolObject(TYPE_ID);
found = (FunctionType) found.unify(t);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected
- + "', found '" + t + "'.\n" + n.getLocation());
+ throw new TypeErrorException("Expected '" + expected + "', found '" + t + "'.\n" + n.getLocation());
}
return found;
@@ -826,8 +777,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected
- + "', found '" + found + "'.\n" + n.getLocation());
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n" + n.getLocation());
}
return found;
}
@@ -839,20 +789,16 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
{
TLAType domType;
ExprOrOpArgNode dom = n.getArgs()[1];
- if (dom instanceof OpApplNode
- && ((OpApplNode) dom).getOperator().getName().toString()
- .equals("$Tuple")) {
+ if (dom instanceof OpApplNode && ((OpApplNode) dom).getOperator().getName().toString().equals("$Tuple")) {
ArrayList<TLAType> domList = new ArrayList<TLAType>();
OpApplNode domOpAppl = (OpApplNode) dom;
for (int i = 0; i < domOpAppl.getArgs().length; i++) {
- TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[i],
- new UntypedType());
+ TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[i], new UntypedType());
domList.add(d);
}
if (domList.size() == 1) { // one-tuple
- domType = new FunctionType(IntType.getInstance(),
- domList.get(0));
+ domType = new FunctionType(IntType.getInstance(), domList.get(0));
FunctionType func = new FunctionType(domType, expected);
TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
return ((FunctionType) res).getRange();
@@ -869,30 +815,24 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
UntypedType u = new UntypedType();
n.setToolObject(TYPE_ID, u);
u.addFollower(n);
- TupleOrFunction tupleOrFunc = new TupleOrFunction(
- num.val(), u);
+ TupleOrFunction tupleOrFunc = new TupleOrFunction(num.val(), u);
- TLAType res = visitExprOrOpArgNode(n.getArgs()[0],
- tupleOrFunc);
+ TLAType res = visitExprOrOpArgNode(n.getArgs()[0], tupleOrFunc);
n.getArgs()[0].setToolObject(TYPE_ID, res);
tupleNodeList.add(n.getArgs()[0]);
if (res instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) res)
- .addFollower(n.getArgs()[0]);
+ ((AbstractHasFollowers) res).addFollower(n.getArgs()[0]);
}
TLAType found = (TLAType) n.getToolObject(TYPE_ID);
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected
- + "', found '" + found + "'.\n"
- + n.getArgs()[0].toString(2) + "\n"
- + n.getLocation());
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "'.\n"
+ + n.getArgs()[0].toString(2) + "\n" + n.getLocation());
}
return found;
}
- domType = visitExprOrOpArgNode(n.getArgs()[1],
- new UntypedType());
+ domType = visitExprOrOpArgNode(n.getArgs()[1], new UntypedType());
}
FunctionType func = new FunctionType(domType, expected);
TLAType res = visitExprOrOpArgNode(n.getArgs()[0], func);
@@ -905,16 +845,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
***********************************************************************/
case OPCODE_domain: {
- FunctionType func = new FunctionType(new UntypedType(),
- new UntypedType());
+ FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
TLAType res = null;
try {
res = new SetType(func.getDomain()).unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected '%s', found '%s' at 'DOMAIN(..)',%n%s",
- expected, func, n.getLocation()));
+ throw new TypeErrorException(String.format("Expected '%s', found '%s' at 'DOMAIN(..)',%n%s", expected,
+ func, n.getLocation()));
}
return res;
}
@@ -923,18 +861,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
***********************************************************************/
case OPCODE_sof: // [ A -> B]
{
- SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(new UntypedType()));
- SetType B = (SetType) visitExprOrOpArgNode(n.getArgs()[1],
- new SetType(new UntypedType()));
+ SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ SetType B = (SetType) visitExprOrOpArgNode(n.getArgs()[1], new SetType(new UntypedType()));
- SetType found = new SetType(new FunctionType(A.getSubType(),
- B.getSubType()));
+ SetType found = new SetType(new FunctionType(A.getSubType(), B.getSubType()));
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected '%s', found '%s' at Set of Function,%n%s",
+ throw new TypeErrorException(String.format("Expected '%s', found '%s' at Set of Function,%n%s",
expected, found, n.getLocation()));
}
return found;
@@ -955,17 +889,15 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
{
ArrayList<TLAType> list = new ArrayList<TLAType>();
for (int i = 0; i < n.getArgs().length; i++) {
- SetType t = (SetType) visitExprOrOpArgNode(n.getArgs()[i],
- new SetType(new UntypedType()));
+ SetType t = (SetType) visitExprOrOpArgNode(n.getArgs()[i], new SetType(new UntypedType()));
list.add(t.getSubType());
}
SetType found = new SetType(new TupleType(list));
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at Cartesian Product,%n%s",
- expected, found, n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found %s at Cartesian Product,%n%s", expected,
+ found, n.getLocation()));
}
return found;
@@ -980,8 +912,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
for (int i = 0; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
StringNode field = (StringNode) pair.getArgs()[0];
- SetType fieldType = (SetType) visitExprOrOpArgNode(
- pair.getArgs()[1], new SetType(new UntypedType()));
+ SetType fieldType = (SetType) visitExprOrOpArgNode(pair.getArgs()[1], new SetType(new UntypedType()));
struct.add(field.getRep().toString(), fieldType.getSubType());
}
@@ -989,9 +920,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at Set of Records,%n%s",
- expected, found, n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found %s at Set of Records,%n%s", expected,
+ found, n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
found.addFollower(n);
@@ -1004,16 +934,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
for (int i = 0; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
StringNode field = (StringNode) pair.getArgs()[0];
- TLAType fieldType = visitExprOrOpArgNode(pair.getArgs()[1],
- new UntypedType());
+ TLAType fieldType = visitExprOrOpArgNode(pair.getArgs()[1], new UntypedType());
found.add(field.getRep().toString(), fieldType);
}
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at Record,%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at Record,%n%s", expected, found, n.getLocation()));
}
n.setToolObject(TYPE_ID, found);
found.addFollower(n);
@@ -1024,10 +952,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
case OPCODE_rs: // $RcdSelect r.c
{
- String fieldName = ((StringNode) n.getArgs()[1]).getRep()
- .toString();
- StructType r = (StructType) visitExprOrOpArgNode(n.getArgs()[0],
- StructType.getIncompleteStruct());
+ String fieldName = ((StringNode) n.getArgs()[1]).getRep().toString();
+ StructType r = (StructType) visitExprOrOpArgNode(n.getArgs()[0], StructType.getIncompleteStruct());
StructType expectedStruct = StructType.getIncompleteStruct();
expectedStruct.add(fieldName, expected);
@@ -1035,9 +961,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
r = r.unify(expectedStruct);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Struct has no field %s with type %s: %s%n%s",
- fieldName, r.getType(fieldName), r, n.getLocation()));
+ throw new TypeErrorException(String.format("Struct has no field %s with type %s: %s%n%s", fieldName,
+ r.getType(fieldName), r, n.getLocation()));
}
n.getArgs()[0].setToolObject(TYPE_ID, r);
r.addFollower(n.getArgs()[0]);
@@ -1070,8 +995,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
for (int i = 0; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
if (pair.getArgs()[0] != null) {
- visitExprOrOpArgNode(pair.getArgs()[0],
- BoolType.getInstance());
+ visitExprOrOpArgNode(pair.getArgs()[0], BoolType.getInstance());
}
found = visitExprOrOpArgNode(pair.getArgs()[1], found);
}
@@ -1096,9 +1020,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'CHOOSE',%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'CHOOSE',%n%s", expected, found, n.getLocation()));
}
setType(n, found);
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -1112,9 +1035,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'CHOOSE',%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'CHOOSE',%n%s", expected, found, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
return found;
@@ -1132,8 +1054,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- throw new NotImplementedException("Not supported Operator: "
- + n.getOperator().getName().toString() + "\n" + n.getLocation());
+ throw new NotImplementedException(
+ "Not supported Operator: " + n.getOperator().getName().toString() + "\n" + n.getLocation());
}
private TLAType evalBoundedVariables(OpApplNode n) throws TLA2BException {
@@ -1141,37 +1063,31 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
ExprNode[] bounds = n.getBdedQuantBounds();
for (int i = 0; i < bounds.length; i++) {
- SetType boundType = (SetType) visitExprNode(bounds[i], new SetType(
- new UntypedType()));
+ SetType boundType = (SetType) visitExprNode(bounds[i], new SetType(new UntypedType()));
TLAType subType = boundType.getSubType();
if (n.isBdedQuantATuple()[i]) {
if (params[i].length == 1) {
FormalParamNode p = params[i][0];
- FunctionType expected = new FunctionType(
- IntType.getInstance(), new UntypedType());
+ FunctionType expected = new FunctionType(IntType.getInstance(), new UntypedType());
try {
expected = (FunctionType) expected.unify(subType);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at parameter %s,%n%s",
- expected, subType, p.getName().toString(),
- bounds[i].getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found %s at parameter %s,%n%s",
+ expected, subType, p.getName().toString(), bounds[i].getLocation()));
}
domList.add(expected);
symbolNodeList.add(p);
p.setToolObject(TYPE_ID, expected.getRange());
if (expected.getRange() instanceof AbstractHasFollowers) {
- ((AbstractHasFollowers) expected.getRange())
- .addFollower(p);
+ ((AbstractHasFollowers) expected.getRange()).addFollower(p);
}
} else {
TupleType tuple = new TupleType(params[i].length);
try {
tuple = (TupleType) tuple.unify(subType);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at tuple,%n%s", tuple,
+ throw new TypeErrorException(String.format("Expected %s, found %s at tuple,%n%s", tuple,
subType, bounds[i].getLocation()));
}
domList.add(tuple);
@@ -1216,8 +1132,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* @return
* @throws TLA2BException
*/
- private TLAType evalExcept(OpApplNode n, TLAType expected)
- throws TLA2BException {
+ private TLAType evalExcept(OpApplNode n, TLAType expected) throws TLA2BException {
TLAType t = visitExprOrOpArgNode(n.getArgs()[0], expected);
n.setToolObject(TYPE_ID, t);
if (t instanceof AbstractHasFollowers) {
@@ -1248,9 +1163,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
t = t.unify(s);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'EXCEPT',%n%s", t, s,
- pair.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, s, pair.getLocation()));
}
} else {
@@ -1259,13 +1173,11 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType domType;
TLAType rangeType;
if (domExpr instanceof OpApplNode
- && ((OpApplNode) domExpr).getOperator().getName()
- .toString().equals("$Tuple")) {
+ && ((OpApplNode) domExpr).getOperator().getName().toString().equals("$Tuple")) {
ArrayList<TLAType> domList = new ArrayList<TLAType>();
OpApplNode domOpAppl = (OpApplNode) domExpr;
for (int j = 0; j < domOpAppl.getArgs().length; j++) {
- TLAType d = visitExprOrOpArgNode(
- domOpAppl.getArgs()[j], new UntypedType());
+ TLAType d = visitExprOrOpArgNode(domOpAppl.getArgs()[j], new UntypedType());
domList.add(d);
}
domType = new TupleType(domList);
@@ -1278,9 +1190,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
t = t.unify(func);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'EXCEPT',%n%s", t, func,
- pair.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'EXCEPT',%n%s", t, func, pair.getLocation()));
}
}
}
@@ -1294,8 +1205,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
* @return
* @throws TLA2BException
*/
- private TLAType evalType(LinkedList<ExprOrOpArgNode> list, TLAType valueType)
- throws TLA2BException {
+ private TLAType evalType(LinkedList<ExprOrOpArgNode> list, TLAType valueType) throws TLA2BException {
if (list.size() == 0) {
return valueType;
}
@@ -1303,8 +1213,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
if (head instanceof StringNode) {
// record or function of strings
String name = ((StringNode) head).getRep().toString();
- StructOrFunctionType res = new StructOrFunctionType(name, evalType(
- list, valueType));
+ StructOrFunctionType res = new StructOrFunctionType(name, evalType(list, valueType));
return res;
}
TLAType t = visitExprOrOpArgNode(head, new UntypedType());
@@ -1312,8 +1221,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return res;
}
- private TLAType evalBBuiltIns(OpApplNode n, TLAType expected)
- throws TLA2BException {
+ private TLAType evalBBuiltIns(OpApplNode n, TLAType expected) throws TLA2BException {
switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
// B Builtins
@@ -1328,9 +1236,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
@@ -1347,9 +1254,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
visitExprOrOpArgNode(n.getArgs()[i], IntType.getInstance());
@@ -1362,9 +1268,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
expected.unify(new SetType(IntType.getInstance()));
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER) at '..',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(INTEGER) at '..',%n%s", expected, n.getLocation()));
}
for (int i = 0; i < n.getArgs().length; i++) {
@@ -1380,9 +1285,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
return found;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER) at 'Nat',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(INTEGER) at 'Nat',%n%s", expected, n.getLocation()));
}
}
@@ -1396,9 +1300,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
return found;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER) at 'Int',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(INTEGER) at 'Int',%n%s", expected, n.getLocation()));
}
}
@@ -1407,9 +1310,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '-',%n%s", expected,
- n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found INTEGER at '-',%n%s", expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], IntType.getInstance());
return IntType.getInstance();
@@ -1423,9 +1325,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
BoolType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at 'IsFiniteSet',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found BOOL at 'IsFiniteSet',%n%s", expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
return BoolType.getInstance();
@@ -1436,9 +1337,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at 'Cardinality',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found INTEGER at 'Cardinality',%n%s", expected, n.getLocation()));
}
visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
return IntType.getInstance();
@@ -1449,17 +1349,14 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
**********************************************************************/
case B_OPCODE_seq: { // Seq(S) - set of sequences, S must be a set
- SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(new UntypedType()));
+ SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
- SetType set_of_seq = new SetType(new FunctionType(
- IntType.getInstance(), S.getSubType()));
+ SetType set_of_seq = new SetType(new FunctionType(IntType.getInstance(), S.getSubType()));
try {
set_of_seq = set_of_seq.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Seq',%n%s", expected,
- set_of_seq, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'Seq',%n%s", expected, set_of_seq, n.getLocation()));
}
return set_of_seq;
}
@@ -1468,88 +1365,76 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at 'Len',%n%s", expected,
- n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found INTEGER at 'Len',%n%s", expected, n.getLocation()));
}
- visitExprOrOpArgNode(n.getArgs()[0],
- new FunctionType(IntType.getInstance(), new UntypedType()));
+ visitExprOrOpArgNode(n.getArgs()[0], new FunctionType(IntType.getInstance(), new UntypedType()));
return IntType.getInstance();
}
case B_OPCODE_conc: { // s \o s2 - concatenation of s and s2
- TLAType found = new FunctionType(IntType.getInstance(),
- new UntypedType());
- found = visitExprOrOpArgNode(n.getArgs()[0], found);
- found = visitExprOrOpArgNode(n.getArgs()[1], found);
+ TLAType found = new FunctionType(IntType.getInstance(), new UntypedType());
+ found = visitExprOrOpArgNode(n.getArgs()[0], found);
+ found = visitExprOrOpArgNode(n.getArgs()[1], found);
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(INTEGER*_A) at '\\o',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(INTEGER*_A) at '\\o',%n%s", expected, n.getLocation()));
}
return found;
}
case B_OPCODE_append: // Append(s, e)
{
- FunctionType found = new FunctionType(IntType.getInstance(),
- new UntypedType());
+ FunctionType found = new FunctionType(IntType.getInstance(), new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
visitExprOrOpArgNode(n.getArgs()[1], found.getRange());
try {
found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Append',%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'Append',%n%s", expected, found, n.getLocation()));
}
return found;
}
case B_OPCODE_head: { // HEAD(s) - the first element of the sequence
- FunctionType func = new FunctionType(IntType.getInstance(),
- new UntypedType());
+ FunctionType func = new FunctionType(IntType.getInstance(), new UntypedType());
func = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], func);
TLAType found = func.getRange();
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Head',%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'Head',%n%s", expected, found, n.getLocation()));
}
return found;
}
case B_OPCODE_tail: { // Tail(s)
- FunctionType found = new FunctionType(IntType.getInstance(),
- new UntypedType());
+ FunctionType found = new FunctionType(IntType.getInstance(), new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
try {
found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'Tail',%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'Tail',%n%s", expected, found, n.getLocation()));
}
return found;
}
case B_OPCODE_subseq: { // SubSeq(s,m,n)
- TLAType found = new FunctionType(IntType.getInstance(),
- new UntypedType());
+ TLAType found = new FunctionType(IntType.getInstance(), new UntypedType());
found = visitExprOrOpArgNode(n.getArgs()[0], found);
visitExprOrOpArgNode(n.getArgs()[1], IntType.getInstance());
visitExprOrOpArgNode(n.getArgs()[2], IntType.getInstance());
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'SubSeq',%n%s", expected,
- found, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found %s at 'SubSeq',%n%s", expected, found, n.getLocation()));
}
return found;
}
@@ -1568,25 +1453,20 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
IntType.getInstance().unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found INTEGER at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found INTEGER at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
- visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(IntType.getInstance()));
+ visitExprOrOpArgNode(n.getArgs()[0], new SetType(IntType.getInstance()));
return IntType.getInstance();
}
case B_OPCODE_permseq: { // PermutedSequences(S)
- SetType argType = (SetType) visitExprOrOpArgNode(n.getArgs()[0],
- new SetType(new UntypedType()));
- SetType found = new SetType(new FunctionType(IntType.getInstance(),
- argType.getSubType()));
+ SetType argType = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
+ SetType found = new SetType(new FunctionType(IntType.getInstance(), argType.getSubType()));
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at 'PermutedSequences',%n%s",
+ throw new TypeErrorException(String.format("Expected %s, found %s at 'PermutedSequences',%n%s",
expected, found, n.getLocation()));
}
return found;
@@ -1604,8 +1484,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at '%s',%n%s", expected, found,
+ throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
}
return found;
@@ -1626,8 +1505,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found %s at '%s',%n%s", expected, found,
+ throw new TypeErrorException(String.format("Expected %s, found %s at '%s',%n%s", expected, found,
n.getOperator().getName(), n.getLocation()));
}
return found;
@@ -1642,9 +1520,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
return found;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(BOOL) at 'BOOLEAN',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(BOOL) at 'BOOLEAN',%n%s", expected, n.getLocation()));
}
case B_OPCODE_string: // STRING
@@ -1653,9 +1530,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = found.unify(expected);
return found;
} catch (UnificationException e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found POW(STRING) at 'STRING',%n%s",
- expected, n.getLocation()));
+ throw new TypeErrorException(
+ String.format("Expected %s, found POW(STRING) at 'STRING',%n%s", expected, n.getLocation()));
}
case B_OPCODE_true:
@@ -1664,9 +1540,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
return BoolType.getInstance();
} catch (Exception e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
case B_OPCODE_assert: {
@@ -1674,15 +1549,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
BoolType.getInstance().unify(expected);
return BoolType.getInstance();
} catch (Exception e) {
- throw new TypeErrorException(String.format(
- "Expected %s, found BOOL at '%s',%n%s", expected, n
- .getOperator().getName(), n.getLocation()));
+ throw new TypeErrorException(String.format("Expected %s, found BOOL at '%s',%n%s", expected,
+ n.getOperator().getName(), n.getLocation()));
}
}
default: {
- throw new NotImplementedException(n.getOperator().getName()
- .toString());
+ throw new NotImplementedException(n.getOperator().getName().toString());
}
}
}
diff --git a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
index 3c98c6c0c73a4424df597484d8088a70ed5be773..6c3ba3d178bea0e7889325cee944ea4ea0bd98a9 100644
--- a/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/BDefinitionsFinder.java
@@ -2,6 +2,7 @@ package de.tla2b.translation;
import java.util.ArrayList;
import java.util.HashSet;
+import java.util.Set;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
@@ -15,16 +16,13 @@ import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.TranslationGlobals;
-public class BDefinitionsFinder extends AbstractASTVisitor implements
- ASTConstants, ToolGlobals, TranslationGlobals {
- private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<OpDefNode>();
+public class BDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
+ private final HashSet<OpDefNode> bDefinitionsSet = new HashSet<>();
public BDefinitionsFinder(SpecAnalyser specAnalyser) {
if (specAnalyser.getConfigFileEvaluator() != null) {
- bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
- .getConstantOverrideTable().values());
- bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator()
- .getOperatorOverrideTable().values());
+ bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values());
+ bDefinitionsSet.addAll(specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values());
}
for (BOperation op : specAnalyser.getBOperations()) {
@@ -52,15 +50,28 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
bDefinitionsSet.add(def);
}
- HashSet<OpDefNode> temp = new HashSet<OpDefNode>(bDefinitionsSet);
+ for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
+ String defName = opDef.getName().toString();
+ // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx,
+ if (defName.equals("GOAL") || defName.startsWith("ANIMATION_") || defName.startsWith("CUSTOM_GRAPH_")
+ || defName.startsWith("SET_PREF_") || defName.startsWith("HEURISTIC_FUNCTION")
+ || defName.startsWith("SCOPE") || defName.startsWith("scope_")) {
+ bDefinitionsSet.add(opDef);
+ }
+ }
+
+ HashSet<OpDefNode> temp = new HashSet<>(bDefinitionsSet);
for (OpDefNode opDefNode : temp) {
visitExprNode(opDefNode.getBody());
}
+
}
+ @Override
public void visitUserDefinedNode(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator();
if (bDefinitionsSet.add(def)) {
+ // visit body only once
visitExprNode(def.getBody());
}
for (ExprOrOpArgNode exprOrOpArgNode : n.getArgs()) {
@@ -68,7 +79,7 @@ public class BDefinitionsFinder extends AbstractASTVisitor implements
}
}
- public HashSet<OpDefNode> getBDefinitionsSet() {
+ public Set<OpDefNode> getBDefinitionsSet() {
return bDefinitionsSet;
}
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 933423dac2e62da9bfc13bc32e13e3f8a775fae7..dced95d2e4027e847ba7637d76f324a87f050db8 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -13,22 +13,18 @@ import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-public class UsedDefinitionsFinder extends AbstractASTVisitor implements
- ASTConstants, ToolGlobals, TranslationGlobals {
+public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTConstants, ToolGlobals, TranslationGlobals {
+
+ private final HashSet<OpDefNode> usedDefinitions = new HashSet<>();
- private final HashSet<OpDefNode> usedDefinitions = new HashSet<OpDefNode>();
-
-
public UsedDefinitionsFinder(SpecAnalyser specAnalyser) {
if (specAnalyser.getConfigFileEvaluator() != null) {
- Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator()
- .getConstantOverrideTable().values();
+ Collection<OpDefNode> cons = specAnalyser.getConfigFileEvaluator().getConstantOverrideTable().values();
for (OpDefNode def : cons) {
visitExprNode(def.getBody());
}
- Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator()
- .getOperatorOverrideTable().values();
+ Collection<OpDefNode> ops = specAnalyser.getConfigFileEvaluator().getOperatorOverrideTable().values();
for (OpDefNode def : cons) {
visitExprNode(def.getBody());
}
@@ -37,7 +33,7 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
}
visitAssumptions(specAnalyser.getModuleNode().getAssumptions());
-
+
if (specAnalyser.getNext() != null) {
visitExprNode(specAnalyser.getNext());
}
@@ -59,6 +55,15 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
visitExprNode(def.getBody());
}
}
+
+ for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
+ String defName = opDef.getName().toString();
+ // GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx,
+ if (defName.equals("GOAL") || defName.startsWith("ANIMATION_FUNCTION")
+ || defName.startsWith("ANIMATION_IMG") || defName.startsWith("SET_PREF_")) {
+ usedDefinitions.add(opDef);
+ }
+ }
}
public HashSet<OpDefNode> getUsedDefinitions() {
@@ -70,15 +75,12 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
super.visitUserDefinedNode(n);
OpDefNode def = (OpDefNode) n.getOperator();
- ModuleNode moduleNode = def.getSource()
- .getOriginallyDefinedInModuleNode();
+ ModuleNode moduleNode = def.getSource().getOriginallyDefinedInModuleNode();
if (moduleNode.getName().toString().equals("TLA2B")) {
return;
}
if (BBuiltInOPs.contains(def.getName())
- && STANDARD_MODULES.contains(def.getSource()
- .getOriginallyDefinedInModuleNode().getName()
- .toString())) {
+ && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) {
return;
}
if (usedDefinitions.add(def)) {
diff --git a/src/main/java/de/tla2b/types/StructType.java b/src/main/java/de/tla2b/types/StructType.java
index 61dd2cae8ffbc8cabfda2f946b6f13171632df08..50fca87cfc00fade1b42da58486fc7a096e58769 100644
--- a/src/main/java/de/tla2b/types/StructType.java
+++ b/src/main/java/de/tla2b/types/StructType.java
@@ -81,8 +81,9 @@ public class StructType extends AbstractHasFollowers {
}
public boolean compare(TLAType o) {
- if (this.contains(o) || o.contains(this))
+ if (this.contains(o) || o.contains(this)) {
return false;
+ }
if (o.getKind() == UNTYPED)
return true;
@@ -119,32 +120,32 @@ public class StructType extends AbstractHasFollowers {
}
if (o instanceof StructType) {
- StructType s = (StructType) o;
+ StructType otherStruct = (StructType) o;
boolean extendStruct = false;
- if (this.incompleteStruct && s.incompleteStruct) {
+ if (this.incompleteStruct && otherStruct.incompleteStruct) {
extendStruct = false;
} else if (this.incompleteStruct) {
- if (s.types.keySet().containsAll(this.types.keySet())) {
+ if (otherStruct.types.keySet().containsAll(this.types.keySet())) {
extendStruct = false;
} else {
extendStruct = true;
}
- } else if (s.incompleteStruct) {
- if (this.types.keySet().containsAll(s.types.keySet())) {
+ } else if (otherStruct.incompleteStruct) {
+ if (this.types.keySet().containsAll(otherStruct.types.keySet())) {
extendStruct = false;
} else {
extendStruct = true;
}
} else {
- extendStruct = !s.types.keySet().equals(this.types.keySet());
+ extendStruct = !otherStruct.types.keySet().equals(this.types.keySet());
}
- this.extensible = this.extensible || s.extensible || extendStruct;
+ this.extensible = this.extensible || otherStruct.extensible || extendStruct;
- Iterator<String> keys = s.types.keySet().iterator();
+ Iterator<String> keys = otherStruct.types.keySet().iterator();
while (keys.hasNext()) {
String fieldName = (String) keys.next();
- TLAType sType = s.types.get(fieldName);
+ TLAType sType = otherStruct.types.get(fieldName);
if (this.types.containsKey(fieldName)) {
TLAType res = this.types.get(fieldName).unify(sType);
this.types.put(fieldName, res);
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 205d09ee71b6ea0e95ee0f02ace17c8cb2871030..7395892949117faf6649ee5f3e9d04f804d5836f 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -346,7 +346,7 @@ public class Translator implements TranslationGlobals {
public static RecursiveMachineLoader parseAllMachines(final Start ast, final File f, final BParser bparser)
throws BCompoundException {
final RecursiveMachineLoader rml = new RecursiveMachineLoader(f.getParent(), bparser.getContentProvider());
- rml.loadAllMachines(f, ast, bparser.getSourcePositions(), bparser.getDefinitions());
+ rml.loadAllMachines(f, ast, bparser.getDefinitions());
return rml;
}
diff --git a/src/test/java/de/tla2b/main/MainTest.java b/src/test/java/de/tla2b/main/MainTest.java
index a8e832beb492e4db5f27b8a19d5ceaa2a39a417c..ce0d3abf8dbdc3b7d10e6208f03d1677c428df99 100644
--- a/src/test/java/de/tla2b/main/MainTest.java
+++ b/src/test/java/de/tla2b/main/MainTest.java
@@ -1,5 +1,7 @@
package de.tla2b.main;
+import java.io.File;
+
import org.junit.Test;
import de.tla2b.TLA2B;
@@ -8,8 +10,9 @@ public class MainTest {
@Test
public void testClub() throws Exception {
- String file = "src/test/resources/regression/Club/Club.tla";
- TLA2B.main(new String[] { file });
+ String dir = "src/test/resources/regression/Club/";
+ TLA2B.main(new String[] { dir + "Club.tla" });
+ new File(dir + "Club_tla.txt").deleteOnExit();
}
-
+
}
diff --git a/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java b/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java
index d120ee40d67fed3b5b8606533911699164480ca3..41ab9292ad308410ee4fbb92d9aba966cc97803d 100644
--- a/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/DefinitionsTest.java
@@ -33,4 +33,22 @@ public class DefinitionsTest {
+ "END";
compare(expected, module);
}
+
+ @Test
+ public void testGoalDefinition() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x, y \n"
+ + "Init == x = 1 /\\ y = 1 \n"
+ + "GOAL == 1=1 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS GOAL == 1 = 1;"
+ + "VARIABLES x, y\n"
+ + "INVARIANT x : INTEGER & y : INTEGER \n"
+ + "INITIALISATION x, y:(x = 1 & y = 1) \n"
+ + "END";
+ compare(expected, module);
+ }
}
diff --git a/src/test/java/de/tla2b/prettyprintb/SpecialDefinitions.java b/src/test/java/de/tla2b/prettyprintb/SpecialDefinitions.java
new file mode 100644
index 0000000000000000000000000000000000000000..4be87f509d6df5088fd4f011120aa01497747c0e
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/SpecialDefinitions.java
@@ -0,0 +1,24 @@
+package de.tla2b.prettyprintb;
+
+import static de.tla2b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+public class SpecialDefinitions {
+
+
+ @Test
+ public void testVisualisationDefinition() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CUSTOM_GRAPH_NODES == { <<a,<<\"lightgray\",b>> >> : a\\in 1..2 , b \\in 1..2} \n"
+ + "CUSTOM_GRAPH_EDGES == 1..10 \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "DEFINITIONS CUSTOM_GRAPH_NODES == UNION(a,b).(a : 1 .. 2 & b : 1 .. 2 | {(a|->(\"lightgray\"|->b))}); \n"
+ + "CUSTOM_GRAPH_EDGES == 1 .. 10;"
+ + "END";
+ compare(expected, module);
+ }
+}