From 0435989f1a6a296fa2ffbb8a6d84a069e582bded Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Wed, 23 Apr 2014 12:21:51 +0200
Subject: [PATCH] Collecting all B definitions to make the recursive machine
loader happy
---
src/main/java/de/tla2bAst/BAstCreator.java | 36 ++++++++++++++-------
src/main/java/de/tla2bAst/Translator.java | 1 -
src/test/java/de/tla2b/examples/MCTest.java | 1 +
3 files changed, 26 insertions(+), 12 deletions(-)
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 5197cbb..0486e12 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -105,6 +105,7 @@ import de.be4.classicalb.core.parser.node.AStringExpression;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
import de.be4.classicalb.core.parser.node.AStructExpression;
import de.be4.classicalb.core.parser.node.ASubsetPredicate;
+import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.ATailExpression;
import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
@@ -271,16 +272,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
}
}
- Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
- .getUsedExternalFunctions();
- if (bDefs.size() == 0 && set.size() == 0) {
- return;
- }
-
- ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
List<PDefinition> defs = new ArrayList<PDefinition>();
+ Set<EXTERNAL_FUNCTIONS> set = usedExternalFunctions
+ .getUsedExternalFunctions();
defs.addAll(createDefinitionsForExternalFunctions(set));
for (OpDefNode opDefNode : bDefs) {
@@ -299,7 +295,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
d.setParameters(list);
d.setRhs(visitExprNodePredicate(opDefNode.getBody()));
defs.add(d);
- bDefinitions.addDefinition(d, Definitions.Type.Expression);
} else {
AExpressionDefinitionDefinition d = new AExpressionDefinitionDefinition();
d.setName(new TIdentifierLiteral(opDefNode.getName().toString()));
@@ -307,12 +302,31 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
d.setParameters(list);
d.setRhs(visitExprNodeExpression(opDefNode.getBody()));
defs.add(d);
- bDefinitions.addDefinition(d, Definitions.Type.Expression);
}
}
- defClause.setDefinitions(defs);
- machineClauseList.add(defClause);
+
+ if (defs.size() > 0) {
+ ADefinitionsMachineClause defClause = new ADefinitionsMachineClause();
+ defClause.setDefinitions(defs);
+ machineClauseList.add(defClause);
+ for (PDefinition def : defs) {
+ if (def instanceof AExpressionDefinitionDefinition) {
+ bDefinitions.addDefinition(
+ (AExpressionDefinitionDefinition) def,
+ Definitions.Type.Expression);
+ } else if (def instanceof APredicateDefinitionDefinition) {
+ bDefinitions.addDefinition(
+ (APredicateDefinitionDefinition) def,
+ Definitions.Type.Predicate);
+ } else {
+ bDefinitions.addDefinition(
+ (ASubstitutionDefinitionDefinition) def,
+ Definitions.Type.Substitution);
+ }
+ }
+ }
+
}
private ArrayList<PDefinition> createDefinitionsForExternalFunctions(
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index c16b574..6546b27 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -210,7 +210,6 @@ public class Translator {
specAnalyser, usedExternalFunctions, predicateVsExpression);
this.bDefinitions = bAstCreator.getBDefinitions();
-
return bAstCreator.getStartNode();
}
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index 19d068f..f8bad91 100644
--- a/src/test/java/de/tla2b/examples/MCTest.java
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -55,6 +55,7 @@ public class MCTest {
runModule(file);
}
+
@Test
public void testChannel() throws Exception {
String file = "src/test/resources/examples/Channel/Channel.tla";
--
GitLab