diff --git a/.travis.yml b/.travis.yml
index c6cdb2f98e98276458315bc5f5452ad9cbe703fa..371f9b2c7916dccf7a4e9a6478e5302cd14b6e83 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -11,3 +11,6 @@ after_success: "[ $TRAVIS_BRANCH = 'master' ] && gradle uploadArchives"
env:
global:
- secure: EnIo0zaQsHATGH8S5L1W0EHtqgV2kx6bfSgxyhz7XU+xw5y2JLDn+Y3ZaX7EcMK25RkgM8nld5Se72QmpienkP7tQlb5KHdwC10KgwbHDq+IP9q+ZMD2V1MsMRdTilW/eTZ0SUohlV5g4t3KqIe8l3Hs1dzNL0YmCMtXwYHdfwk=
+notifications:
+ slack:
+ secure: VWTQE6Z6o9Xz4gZ1SOUKroz5g+exD//+FUdd6wM0tLESFhqqrfwR1dyZHIbQJpcC8KROQD5Bip6vihhACBmr+NU6nPwoNN7fJ9Dvgqt4xG4NEk3+VpVCQVfRDJF4IhHqRFx4K+9fV5I2Kr93G39U/N92lMLk/RkyoaUyju85uwM=
diff --git a/build.gradle b/build.gradle
index 7d9929a7a6cbf0fa29dc7673ecd169a68a7c0211..9cad51cb1d135ada6d255a881ff31161fae0e16f 100644
--- a/build.gradle
+++ b/build.gradle
@@ -4,7 +4,7 @@ apply plugin: 'maven'
apply plugin: 'jacoco'
apply plugin: 'findbugs'
-project.version = '1.0.2-SNAPSHOT'
+project.version = '1.0.3-SNAPSHOT'
project.group = 'de.hhu.stups'
project.sourceCompatibility = '1.7'
@@ -16,18 +16,14 @@ repositories {
name "sonatype snapshots"
url "https://oss.sonatype.org/content/repositories/snapshots"
}
- maven {
- name "cobra"
- url "http://cobra.cs.uni-duesseldorf.de/artifactory/repo"
- }
}
configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
-def parser_version = '2.5.2-SNAPSHOT'
-def tlatools_version = '1.0.2-SNAPSHOT'
+def parser_version = '2.5.1'
+def tlatools_version = '1.0.2'
dependencies {
//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
@@ -41,8 +37,8 @@ dependencies {
//compile(group: 'de.hhu.stups', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
- testCompile (group: 'junit', name: 'junit', version: '4.11')
- testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.0.8-SNAPSHOT')
+ testCompile (group: 'junit', name: 'junit', version: '4.12')
+ testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.0.8')
}
jacoco {
@@ -66,7 +62,7 @@ test {
}
-task integrationTests(type: Test){
+task regressionTests(type: Test){
doFirst{ println("Running integration tests") }
scanForTestClasses = true
//include('de/tlc4b/tlc/integration/probprivate/**')
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 1a344ff850e26fc9b1fbff3f2240732aafb767d5..9502ab7495bda11a843b5ee3840aa0e76aed7a1c 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -15,7 +15,7 @@ import de.tlc4b.analysis.ConstantsEliminator;
import de.tlc4b.analysis.ConstantsEvaluator;
import de.tlc4b.analysis.DefinitionsAnalyser;
import de.tlc4b.analysis.MachineContext;
-import de.tlc4b.analysis.NotSupportedConstructs;
+import de.tlc4b.analysis.UnsupportedConstructsFinder;
import de.tlc4b.analysis.PrecedenceCollector;
import de.tlc4b.analysis.PrimedNodesMarker;
import de.tlc4b.analysis.Renamer;
@@ -57,8 +57,7 @@ public class Translator {
// System.out.println(ast2String2.toString());
}
- public Translator(String machineString, String ltlFormula)
- throws BException {
+ public Translator(String machineString, String ltlFormula) throws BException {
this.machineString = machineString;
this.ltlFormula = ltlFormula;
BParser parser = new BParser("Testing");
@@ -68,8 +67,8 @@ public class Translator {
// System.out.println(ast2String2.toString());
}
- public Translator(String machineName, File machineFile, String ltlFormula,
- String constantSetup) throws BException, IOException {
+ public Translator(String machineName, File machineFile, String ltlFormula, String constantSetup)
+ throws BException, IOException {
this.machineName = machineName;
this.ltlFormula = ltlFormula;
@@ -82,10 +81,10 @@ public class Translator {
// Definitions of definitions files are injected in the ast of the main
// machine
- final RecursiveMachineLoader rml = new RecursiveMachineLoader(
- machineFile.getParent(), parser.getContentProvider());
+ final RecursiveMachineLoader rml = new RecursiveMachineLoader(machineFile.getParent(),
+ parser.getContentProvider());
rml.loadAllMachines(machineFile, start, parser.getSourcePositions(), parser.getDefinitions());
-
+
parsedMachines = rml.getParsedMachines();
if (constantSetup != null) {
@@ -94,13 +93,11 @@ public class Translator {
try {
start2 = con.parse("#FORMULA " + constantSetup, false);
} catch (BException e) {
- System.err
- .println("An error occured while parsing the constants setup predicate.");
+ System.err.println("An error occured while parsing the constants setup predicate.");
throw e;
}
- APredicateParseUnit parseUnit = (APredicateParseUnit) start2
- .getPParseUnit();
+ APredicateParseUnit parseUnit = (APredicateParseUnit) start2.getPParseUnit();
this.constantsSetup = parseUnit.getPredicate();
final Ast2String ast2String2 = new Ast2String();
@@ -114,75 +111,73 @@ public class Translator {
}
public void translate() {
+ UnsupportedConstructsFinder unsupportedConstructsFinder = new UnsupportedConstructsFinder(start);
+ unsupportedConstructsFinder.find();
+
// ast transformation
SeesEliminator.eliminateSeesClauses(start, parsedMachines);
- new NotSupportedConstructs(start);
DefinitionsEliminator.eliminateDefinitions(start);
- //TODO move set comprehension optimizer behind the type checker
+ // TODO move set comprehension optimizer behind the type checker
SetComprehensionOptimizer.optimizeSetComprehensions(start);
-
- MachineContext machineContext = new MachineContext(machineName, start,
- ltlFormula, constantsSetup);
+
+ MachineContext machineContext = new MachineContext(machineName, start);
+ if (ltlFormula != null) {
+ machineContext.addLTLFromula(this.ltlFormula);
+ }
+ if (this.constantsSetup != null) {
+ machineContext.setConstantSetupPredicate(constantsSetup);
+ }
+ machineContext.analyseMachine();
+
this.machineName = machineContext.getMachineName();
if (machineContext.machineContainsOperations()) {
TLC4BGlobals.setPrintCoverage(true);
}
Typechecker typechecker = new Typechecker(machineContext);
- UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
- machineContext);
-
- ConstantsEliminator constantsEliminator = new ConstantsEliminator(
- machineContext);
+ UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(machineContext);
+
+ ConstantsEliminator constantsEliminator = new ConstantsEliminator(machineContext);
constantsEliminator.start();
- ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(
- machineContext);
+ ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(machineContext);
- InvariantPreservationAnalysis invariantPreservationAnalysis = new InvariantPreservationAnalysis(
- machineContext, constantsEvaluator.getInvariantList(),
- unchangedVariablesFinder);
+ InvariantPreservationAnalysis invariantPreservationAnalysis = new InvariantPreservationAnalysis(machineContext,
+ constantsEvaluator.getInvariantList(), unchangedVariablesFinder);
- TypeRestrictor typeRestrictor = new TypeRestrictor(start,
- machineContext, typechecker, constantsEvaluator);
-
- PrecedenceCollector precedenceCollector = new PrecedenceCollector(
- start, typechecker, machineContext, typeRestrictor);
+ TypeRestrictor typeRestrictor = new TypeRestrictor(start, machineContext, typechecker, constantsEvaluator);
- DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
- machineContext);
-
-
+ PrecedenceCollector precedenceCollector = new PrecedenceCollector(start, typechecker, machineContext,
+ typeRestrictor);
+
+ DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(machineContext);
- Generator generator = new Generator(machineContext, typeRestrictor,
- constantsEvaluator, deferredSetSizeCalculator, typechecker);
+ Generator generator = new Generator(machineContext, typeRestrictor, constantsEvaluator,
+ deferredSetSizeCalculator, typechecker);
generator.generate();
- UsedStandardModules usedModules = new UsedStandardModules(start,
- typechecker, typeRestrictor, generator.getTlaModule());
+ UsedStandardModules usedModules = new UsedStandardModules(start, typechecker, typeRestrictor,
+ generator.getTlaModule());
- standardModulesToBeCreated = usedModules
- .getStandardModulesToBeCreated();
+ standardModulesToBeCreated = usedModules.getStandardModulesToBeCreated();
- PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
- .getTlaModule().getOperations(), machineContext);
+ PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator.getTlaModule().getOperations(),
+ machineContext);
primedNodesMarker.start();
Renamer renamer = new Renamer(machineContext);
- TLAPrinter printer = new TLAPrinter(machineContext, typechecker,
- unchangedVariablesFinder, precedenceCollector, usedModules,
- typeRestrictor, generator.getTlaModule(),
- generator.getConfigFile(), primedNodesMarker, renamer,
- invariantPreservationAnalysis);
+ TLAPrinter printer = new TLAPrinter(machineContext, typechecker, unchangedVariablesFinder, precedenceCollector,
+ usedModules, typeRestrictor, generator.getTlaModule(), generator.getConfigFile(), primedNodesMarker,
+ renamer, invariantPreservationAnalysis);
printer.start();
moduleString = printer.getStringbuilder().toString();
configString = printer.getConfigString().toString();
translatedLTLFormula = printer.geTranslatedLTLFormula();
- tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker,
- generator.getTlaModule(), generator.getConfigFile());
+ tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker, generator.getTlaModule(),
+ generator.getConfigFile());
}
public String getMachineString() {
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 7a8a870f55bc3cba44a5614a7b66fac8f0e1e5f8..102c2c6d1f2530841b90a39f272f783a168a4a00 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -75,30 +75,24 @@ import de.tlc4b.ltl.LTLFormulaVisitor;
public class MachineContext extends DepthFirstAdapter {
private String machineName;
- private PMachineHeader header;
private final Start start;
- private final Hashtable<String, MachineContext> machineContextsTable;
+
private final ArrayList<LTLFormulaVisitor> ltlVisitors;
- private final PPredicate constantsSetup;
+ private PPredicate constantsSetupPredicate;
+ private boolean hasConstants = false;
- private boolean constantSetupInTraceFile = false;
- // machine identifier
private final LinkedHashMap<String, Node> machineSetParameter;
private final LinkedHashMap<String, Node> machineScalarParameter;
-
private final LinkedHashMap<String, Node> deferredSets;
private final LinkedHashMap<String, Node> enumeratedSets;
private final LinkedHashMap<String, Node> enumValues;
-
- private LinkedHashMap<String, Node> constants;
- private final LinkedHashMap<String, Node> bMachineConstants;
-
private final LinkedHashMap<String, Node> variables;
+ private final LinkedHashMap<String, Node> constants;
private final LinkedHashMap<String, Node> definitions;
private final LinkedHashMap<String, Node> operations;
private final LinkedHashMap<String, AIdentifierExpression> seenMachines;
- // machine clauses
+ private PMachineHeader header;
private AAbstractMachineParseUnit abstractMachineParseUnit;
private AConstraintsMachineClause constraintMachineClause;
private ASeesMachineClause seesMachineClause;
@@ -108,27 +102,18 @@ public class MachineContext extends DepthFirstAdapter {
private AInvariantMachineClause invariantMachineClause;
private AInitialisationMachineClause initialisationMachineClause;
private AOperationsMachineClause operationMachineClause;
- private AAssertionsMachineClause assertionMachineClause;
+ private AAssertionsMachineClause assertiondMachineClause;
private ArrayList<LinkedHashMap<String, Node>> contextTable;
protected final Hashtable<Node, Node> referencesTable;
- public MachineContext(String machineName, Start start, String ltlFormula,
- PPredicate constantsSetup) {
+ public MachineContext(final String machineName, final Start start) {
this.start = start;
this.machineName = machineName;
- this.constantsSetup = constantsSetup;
this.referencesTable = new Hashtable<Node, Node>();
this.ltlVisitors = new ArrayList<LTLFormulaVisitor>();
- LTLFormulaVisitor ltlVisitor = null;
- if (null != ltlFormula) {
- ltlVisitor = new LTLFormulaVisitor("ltl", this);
- ltlVisitor.parseLTLString(ltlFormula);
- this.ltlVisitors.add(ltlVisitor);
- }
-
this.machineSetParameter = new LinkedHashMap<String, Node>();
this.machineScalarParameter = new LinkedHashMap<String, Node>();
@@ -136,28 +121,34 @@ public class MachineContext extends DepthFirstAdapter {
this.enumeratedSets = new LinkedHashMap<String, Node>();
this.enumValues = new LinkedHashMap<String, Node>();
this.constants = new LinkedHashMap<String, Node>();
- this.bMachineConstants = new LinkedHashMap<String, Node>();
this.variables = new LinkedHashMap<String, Node>();
this.definitions = new LinkedHashMap<String, Node>();
this.operations = new LinkedHashMap<String, Node>();
this.seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
+ }
- this.machineContextsTable = new Hashtable<String, MachineContext>();
- start.apply(this);
-
+ public void analyseMachine() {
+ this.start.apply(this);
+ checkConstantsSetup();
checkLTLFormulas();
+ }
- checkConstantsSetup();
+ public void addLTLFromula(final String ltlFormula) {
+ LTLFormulaVisitor ltlVisitor = new LTLFormulaVisitor("ltl", this);
+ ltlVisitor.parseLTLString(ltlFormula);
+ this.ltlVisitors.add(ltlVisitor);
+ }
+
+ public void setConstantSetupPredicate(final PPredicate constantsSetup) {
+ this.constantsSetupPredicate = constantsSetup;
}
private void checkConstantsSetup() {
- if (constantsSetup == null) {
+ if (constantsSetupPredicate == null) {
return;
}
-
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
-
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
contextTable.add(s.getDeferredSets());
@@ -166,8 +157,7 @@ public class MachineContext extends DepthFirstAdapter {
contextTable.add(s.getConstants());
contextTable.add(s.getDefinitions());
}
- constantsSetup.apply(this);
-
+ constantsSetupPredicate.apply(this);
}
private void checkLTLFormulas() {
@@ -175,18 +165,17 @@ public class MachineContext extends DepthFirstAdapter {
ltlVisitors.get(0).start();
return;
}
- ArrayList<LTLFormulaVisitor> notSupportedLTLFormulas = new ArrayList<LTLFormulaVisitor>();
+ ArrayList<LTLFormulaVisitor> formulasNotSupportedByTLC = new ArrayList<LTLFormulaVisitor>();
for (int i = 0; i < ltlVisitors.size(); i++) {
LTLFormulaVisitor visitor = ltlVisitors.get(i);
try {
visitor.start();
} catch (ScopeException e) {
- MP.println("Warning: LTL formula '" + visitor.getName()
- + "' cannot be checked by TLC.");
- notSupportedLTLFormulas.add(visitor);
+ MP.println("Warning: LTL formula '" + visitor.getName() + "' cannot be checked by TLC.");
+ formulasNotSupportedByTLC.add(visitor);
}
}
- ltlVisitors.removeAll(notSupportedLTLFormulas);
+ ltlVisitors.removeAll(formulasNotSupportedByTLC);
}
public void checkLTLBPredicate(LTLBPredicate ltlbPredicate) {
@@ -198,8 +187,7 @@ public class MachineContext extends DepthFirstAdapter {
contextTable.add(getVariables());
contextTable.add(getDefinitions());
- LinkedHashMap<String, Node> identifierHashTable = ltlbPredicate
- .getIdentifierList();
+ LinkedHashMap<String, Node> identifierHashTable = ltlbPredicate.getIdentifierList();
if (identifierHashTable.size() > 0) {
LinkedHashMap<String, Node> currentContext = new LinkedHashMap<String, Node>();
currentContext.putAll(identifierHashTable);
@@ -214,15 +202,10 @@ public class MachineContext extends DepthFirstAdapter {
}
private void identifierAlreadyExists(String name) {
- if (constants.containsKey(name) || variables.containsKey(name)
- || operations.containsKey(name)
- || deferredSets.containsKey(name)
- || enumeratedSets.containsKey(name)
- || enumValues.containsKey(name)
- || machineSetParameter.containsKey(name)
- || machineScalarParameter.containsKey(name)
- || seenMachines.containsKey(name)
- || definitions.containsKey(name)) {
+ if (constants.containsKey(name) || variables.containsKey(name) || operations.containsKey(name)
+ || deferredSets.containsKey(name) || enumeratedSets.containsKey(name) || enumValues.containsKey(name)
+ || machineSetParameter.containsKey(name) || machineScalarParameter.containsKey(name)
+ || seenMachines.containsKey(name) || definitions.containsKey(name)) {
throw new ScopeException("Duplicate identifier: '" + name + "'");
}
}
@@ -251,13 +234,11 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAMachineHeader(AMachineHeader node) {
this.header = node;
if (machineName == null) {
- List<TIdentifierLiteral> nameList = new ArrayList<TIdentifierLiteral>(
- node.getName());
+ List<TIdentifierLiteral> nameList = new ArrayList<TIdentifierLiteral>(node.getName());
this.machineName = Utils.getIdentifierAsString(nameList);
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(p.getIdentifier());
@@ -272,7 +253,6 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPredicateParseUnit(APredicateParseUnit node) {
-
node.getPredicate().apply(this);
}
@@ -300,8 +280,7 @@ public class MachineContext extends DepthFirstAdapter {
String name = def.getName().getText();
if (name.startsWith("ASSERT_LTL")) {
if (TLC4BGlobals.isCheckLTL()) {
- LTLFormulaVisitor visitor = new LTLFormulaVisitor(name,
- this);
+ LTLFormulaVisitor visitor = new LTLFormulaVisitor(name, this);
visitor.parseDefinition(def);
this.ltlVisitors.add(visitor);
}
@@ -309,24 +288,20 @@ public class MachineContext extends DepthFirstAdapter {
} else if (name.startsWith("ANIMATION_")) {
definitionsToRemove.add(def);
}
- evalDefinitionName(((AExpressionDefinitionDefinition) e)
- .getName().getText().toString(), e);
+ evalDefinitionName(((AExpressionDefinitionDefinition) e).getName().getText().toString(), e);
} else if (e instanceof APredicateDefinitionDefinition) {
- evalDefinitionName(((APredicateDefinitionDefinition) e)
- .getName().getText().toString(), e);
+ evalDefinitionName(((APredicateDefinitionDefinition) e).getName().getText().toString(), e);
} else if (e instanceof ASubstitutionDefinitionDefinition) {
- evalDefinitionName(((ASubstitutionDefinitionDefinition) e)
- .getName().getText().toString(), e);
+ evalDefinitionName(((ASubstitutionDefinitionDefinition) e).getName().getText().toString(), e);
}
}
/*
- * At this point all ASSERT_LTL formulas of the definitions are removed.
- * LTL formulas are stored in the Arraylist {@value #ltlVisitors}.
+ * At this point all LTL definitions (ASSERT_LTL) are removed. LTL
+ * formulas are stored in the Arraylist {@value #ltlVisitors}.
*/
copy.removeAll(definitionsToRemove);
-
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
contextTable.add(s.getDeferredSets());
@@ -348,64 +323,50 @@ public class MachineContext extends DepthFirstAdapter {
}
@Override
- public void caseAExpressionDefinitionDefinition(
- AExpressionDefinitionDefinition node) {
- visitBDefinition(node, node.getName().getText().toString(),
- node.getParameters(), node.getRhs());
+ public void caseAExpressionDefinitionDefinition(AExpressionDefinitionDefinition node) {
+ visitBDefinition(node, node.getName().getText().toString(), node.getParameters(), node.getRhs());
}
@Override
- public void caseAPredicateDefinitionDefinition(
- APredicateDefinitionDefinition node) {
- visitBDefinition(node, node.getName().getText().toString(),
- node.getParameters(), node.getRhs());
+ public void caseAPredicateDefinitionDefinition(APredicateDefinitionDefinition node) {
+ visitBDefinition(node, node.getName().getText().toString(), node.getParameters(), node.getRhs());
}
+ /* d == x := 1 */
@Override
- // d == x := 1
- public void caseASubstitutionDefinitionDefinition(
- ASubstitutionDefinitionDefinition node) {
- visitBDefinition(node, node.getName().getText().toString(),
- node.getParameters(), node.getRhs());
+ public void caseASubstitutionDefinitionDefinition(ASubstitutionDefinitionDefinition node) {
+ visitBDefinition(node, node.getName().getText().toString(), node.getParameters(), node.getRhs());
}
- public void visitBDefinition(Node node, String name,
- List<PExpression> copy, Node rightSide) {
+ public void visitBDefinition(Node node, String name, List<PExpression> copy, Node rightSide) {
if (!this.definitions.containsValue(node)) {
return;
}
-
contextTable.add(new LinkedHashMap<String, Node>());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
-
rightSide.apply(this);
-
contextTable.remove(contextTable.size() - 1);
}
@Override
public void caseADefinitionExpression(ADefinitionExpression node) {
- visitBDefinitionCall(node, node.getDefLiteral().getText().toString(),
- node.getParameters());
+ visitBDefinitionCall(node, node.getDefLiteral().getText().toString(), node.getParameters());
}
@Override
public void caseADefinitionPredicate(ADefinitionPredicate node) {
- visitBDefinitionCall(node, node.getDefLiteral().getText().toString(),
- node.getParameters());
+ visitBDefinitionCall(node, node.getDefLiteral().getText().toString(), node.getParameters());
}
@Override
public void caseADefinitionSubstitution(ADefinitionSubstitution node) {
- visitBDefinitionCall(node, node.getDefLiteral().getText().toString(),
- node.getParameters());
+ visitBDefinitionCall(node, node.getDefLiteral().getText().toString(), node.getParameters());
}
- private void visitBDefinitionCall(Node node, String name,
- List<PExpression> copy) {
+ private void visitBDefinitionCall(Node node, String name, List<PExpression> copy) {
for (PExpression pExpression : copy) {
pExpression.apply(this);
}
@@ -416,16 +377,13 @@ public class MachineContext extends DepthFirstAdapter {
return;
}
}
-
- throw new ScopeException("Unkown definition: '" + name
- + "' at position: " + node.getStartPos());
+ throw new ScopeException("Unkown definition: '" + name + "' at position: " + node.getStartPos());
}
@Override
public void caseASeesMachineClause(ASeesMachineClause node) {
this.seesMachineClause = node;
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getMachineNames());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getMachineNames());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(p.getIdentifier());
@@ -433,10 +391,8 @@ public class MachineContext extends DepthFirstAdapter {
try {
exist(p.getIdentifier());
} catch (ScopeException e2) {
- throw new ScopeException("Machine '" + name
- + "' is seen twice.");
+ throw new ScopeException("Machine '" + name + "' is seen twice.");
}
-
seenMachines.put(name, p);
}
}
@@ -452,8 +408,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseADeferredSetSet(ADeferredSetSet node) {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
String name = Utils.getIdentifierAsString(copy);
exist(node.getIdentifier());
deferredSets.put(name, node);
@@ -462,8 +417,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
{
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
String name = Utils.getIdentifierAsString(copy);
exist(node.getIdentifier());
enumeratedSets.put(name, node);
@@ -479,24 +433,20 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- constantSetupInTraceFile = true;
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ hasConstants = true;
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression c = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(c.getIdentifier());
exist(c.getIdentifier());
constants.put(name, c);
- bMachineConstants.put(name, c);
}
}
@Override
- public void caseAAbstractConstantsMachineClause(
- AAbstractConstantsMachineClause node) {
- constantSetupInTraceFile = true;
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) {
+ hasConstants = true;
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression c = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(c.getIdentifier());
@@ -507,8 +457,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(v.getIdentifier());
@@ -518,10 +467,8 @@ public class MachineContext extends DepthFirstAdapter {
}
@Override
- public void caseAConcreteVariablesMachineClause(
- AConcreteVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(v.getIdentifier());
@@ -530,11 +477,9 @@ public class MachineContext extends DepthFirstAdapter {
}
}
- private void putLocalVariableIntoCurrentScope(AIdentifierExpression node)
- throws ScopeException {
+ private void putLocalVariableIntoCurrentScope(AIdentifierExpression node) throws ScopeException {
String name = Utils.getIdentifierAsString(node.getIdentifier());
- LinkedHashMap<String, Node> currentScope = contextTable
- .get(contextTable.size() - 1);
+ LinkedHashMap<String, Node> currentScope = contextTable.get(contextTable.size() - 1);
if (currentScope.containsKey(name)) {
throw new ScopeException("Duplicate Identifier: " + name);
} else {
@@ -552,8 +497,7 @@ public class MachineContext extends DepthFirstAdapter {
return;
}
}
- throw new ScopeException("Unkown Identifier: '" + name
- + "' at position: " + node.getStartPos());
+ throw new ScopeException("Unkown Identifier: '" + name + "' at position: " + node.getStartPos());
}
@Override
@@ -566,20 +510,11 @@ public class MachineContext extends DepthFirstAdapter {
return;
}
}
- throw new ScopeException("Unkown Identifier: '" + name
- + "' at position: " + node.getStartPos());
+ throw new ScopeException("Unkown Identifier: '" + name + "' at position: " + node.getStartPos());
}
- private ArrayList<MachineContext> lookupExtendedMachines() {
+ private ArrayList<MachineContext> lookupReferencedMachines() {
ArrayList<MachineContext> list = new ArrayList<MachineContext>();
- for (Entry<String, AIdentifierExpression> entry : seenMachines
- .entrySet()) {
- String s = entry.getKey();
- AIdentifierExpression value = entry.getValue();
- if (value.getIdentifier().size() == 1) {
- list.add(machineContextsTable.get(s));
- }
- }
list.add(this);
return list;
}
@@ -599,14 +534,13 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
this.propertiesMachineClause = node;
- constantSetupInTraceFile = true;
+ hasConstants = true;
/**
* check identifier scope in properties clauses
*/
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
-
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
contextTable.add(s.getDeferredSets());
@@ -615,7 +549,6 @@ public class MachineContext extends DepthFirstAdapter {
contextTable.add(s.getConstants());
contextTable.add(s.getDefinitions());
}
-
if (node.getPredicates() != null) {
node.getPredicates().apply(this);
}
@@ -627,7 +560,7 @@ public class MachineContext extends DepthFirstAdapter {
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
this.contextTable.add(s.getSetParamter());
@@ -644,10 +577,10 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
- this.assertionMachineClause = node;
+ this.assertiondMachineClause = node;
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
this.contextTable.add(s.getSetParamter());
@@ -667,13 +600,12 @@ public class MachineContext extends DepthFirstAdapter {
}
@Override
- public void caseAInitialisationMachineClause(
- AInitialisationMachineClause node) {
+ public void caseAInitialisationMachineClause(AInitialisationMachineClause node) {
this.initialisationMachineClause = node;
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
@@ -695,7 +627,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAOperationsMachineClause(AOperationsMachineClause node) {
this.operationMachineClause = node;
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
- ArrayList<MachineContext> list = lookupExtendedMachines();
+ ArrayList<MachineContext> list = lookupReferencedMachines();
for (int i = 0; i < list.size(); i++) {
MachineContext s = list.get(i);
this.contextTable.add(s.getSetParamter());
@@ -714,11 +646,10 @@ public class MachineContext extends DepthFirstAdapter {
String name = Utils.getIdentifierAsString(op.getOpName());
// existString(name);
if (operations.keySet().contains(name)) {
- throw new ScopeException("Duplicate identifier: '" + name + "'");
+ throw new ScopeException(String.format("Duplicate operation: '%s'", name));
}
operations.put(name, op);
}
-
// visit all operations
for (POperation e : copy) {
e.apply(this);
@@ -729,8 +660,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAOperation(AOperation node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getReturnValues());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getReturnValues());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
exist(id.getIdentifier());
@@ -739,8 +669,7 @@ public class MachineContext extends DepthFirstAdapter {
}
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
exist(id.getIdentifier());
@@ -757,8 +686,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAAssignSubstitution(AAssignSubstitution node) {
ArrayList<LinkedHashMap<String, Node>> temp = contextTable;
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getLhsExpression());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getLhsExpression());
ArrayList<LinkedHashMap<String, Node>> varTable = new ArrayList<LinkedHashMap<String, Node>>();
varTable.add(variables);
for (PExpression e : copy) {
@@ -769,7 +697,6 @@ public class MachineContext extends DepthFirstAdapter {
// full context table
contextTable = temp;
for (Node n : ((AFunctionExpression) e).getParameters()) {
-
n.apply(this);
}
} else {
@@ -780,8 +707,7 @@ public class MachineContext extends DepthFirstAdapter {
}
{
contextTable = temp;
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getRhsExpressions());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getRhsExpressions());
for (PExpression e : copy) {
e.apply(this);
}
@@ -791,8 +717,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseALetSubstitution(ALetSubstitution node) {
contextTable.add(new LinkedHashMap<String, Node>());
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -803,8 +728,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAAnySubstitution(AAnySubstitution node) {
contextTable.add(new LinkedHashMap<String, Node>());
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -825,8 +749,7 @@ public class MachineContext extends DepthFirstAdapter {
}
}
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
e.apply(this);
}
@@ -837,8 +760,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAForallPredicate(AForallPredicate node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -853,8 +775,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAExistsPredicate(AExistsPredicate node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -869,8 +790,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseALambdaExpression(ALambdaExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -884,8 +804,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -895,12 +814,10 @@ public class MachineContext extends DepthFirstAdapter {
}
@Override
- public void caseAEventBComprehensionSetExpression(
- AEventBComprehensionSetExpression node) {
+ public void caseAEventBComprehensionSetExpression(AEventBComprehensionSetExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -915,8 +832,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -931,12 +847,10 @@ public class MachineContext extends DepthFirstAdapter {
}
@Override
- public void caseAQuantifiedIntersectionExpression(
- AQuantifiedIntersectionExpression node) {
+ public void caseAQuantifiedIntersectionExpression(AQuantifiedIntersectionExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -954,8 +868,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAGeneralProductExpression(AGeneralProductExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -973,8 +886,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAGeneralSumExpression(AGeneralSumExpression node) {
contextTable.add(new LinkedHashMap<String, Node>());
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
putLocalVariableIntoCurrentScope((AIdentifierExpression) e);
}
@@ -1006,16 +918,12 @@ public class MachineContext extends DepthFirstAdapter {
return header;
}
- public Start getTree() {
+ public Start getStartNode() {
return start;
}
public LinkedHashMap<String, Node> getSetParamter() {
- return machineSetParameter;
- }
-
- public LinkedHashMap<String, Node> getScalarParameter() {
- return machineScalarParameter;
+ return new LinkedHashMap<>(machineSetParameter);
}
public ArrayList<Node> getConstantArrayList() {
@@ -1026,36 +934,40 @@ public class MachineContext extends DepthFirstAdapter {
return list;
}
+ public LinkedHashMap<String, Node> getScalarParameter() {
+ return new LinkedHashMap<>(machineScalarParameter);
+ }
+
public LinkedHashMap<String, Node> getConstants() {
return constants;
}
public LinkedHashMap<String, Node> getDefinitions() {
- return definitions;
+ return new LinkedHashMap<>(definitions);
}
public LinkedHashMap<String, Node> getVariables() {
- return variables;
+ return new LinkedHashMap<>(variables);
}
public LinkedHashMap<String, Node> getOperations() {
- return operations;
+ return new LinkedHashMap<>(operations);
}
public LinkedHashMap<String, Node> getDeferredSets() {
- return deferredSets;
+ return new LinkedHashMap<>(deferredSets);
}
public LinkedHashMap<String, Node> getEnumeratedSets() {
- return enumeratedSets;
+ return new LinkedHashMap<>(enumeratedSets);
}
public LinkedHashMap<String, Node> getEnumValues() {
- return enumValues;
+ return new LinkedHashMap<>(enumValues);
}
public LinkedHashMap<String, AIdentifierExpression> getSeenMachines() {
- return seenMachines;
+ return new LinkedHashMap<>(seenMachines);
}
protected Hashtable<Node, Node> getReferences() {
@@ -1074,10 +986,6 @@ public class MachineContext extends DepthFirstAdapter {
return ltlVisitors;
}
- /*
- * machine clauses getter
- */
-
public AAbstractMachineParseUnit getAbstractMachineParseUnit() {
return abstractMachineParseUnit;
}
@@ -1099,11 +1007,10 @@ public class MachineContext extends DepthFirstAdapter {
}
public AAssertionsMachineClause getAssertionMachineClause() {
- return assertionMachineClause;
+ return assertiondMachineClause;
}
- public void setPropertiesMachineClaus(
- APropertiesMachineClause propertiesMachineClause) {
+ public void setPropertiesMachineClaus(APropertiesMachineClause propertiesMachineClause) {
this.propertiesMachineClause = propertiesMachineClause;
}
@@ -1127,21 +1034,16 @@ public class MachineContext extends DepthFirstAdapter {
return definitionMachineClause;
}
- public void setDefinitionsMachineClause(
- ADefinitionsMachineClause definitionMachineClause) {
+ public void setDefinitionsMachineClause(ADefinitionsMachineClause definitionMachineClause) {
this.definitionMachineClause = definitionMachineClause;
}
public PPredicate getConstantsSetup() {
- return constantsSetup;
- }
-
- public boolean constantSetupInTraceFile() {
- return constantSetupInTraceFile;
+ return constantsSetupPredicate;
}
- public LinkedHashMap<String, Node> getBMachineConstants() {
- return bMachineConstants;
+ public boolean hasConstants() {
+ return hasConstants;
}
}
diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
deleted file mode 100644
index 90fc65e1714e708fa843c1261d1d051ca28c16ae..0000000000000000000000000000000000000000
--- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
+++ /dev/null
@@ -1,90 +0,0 @@
-package de.tlc4b.analysis;
-
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.ACaseSubstitution;
-import de.be4.classicalb.core.parser.node.AExtendsMachineClause;
-import de.be4.classicalb.core.parser.node.AImportsMachineClause;
-import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
-import de.be4.classicalb.core.parser.node.APromotesMachineClause;
-import de.be4.classicalb.core.parser.node.ARefinesModelClause;
-import de.be4.classicalb.core.parser.node.ASeesMachineClause;
-import de.be4.classicalb.core.parser.node.ASeesModelClause;
-import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
-import de.be4.classicalb.core.parser.node.AUsesMachineClause;
-import de.be4.classicalb.core.parser.node.AVarSubstitution;
-import de.be4.classicalb.core.parser.node.AWhileSubstitution;
-import de.be4.classicalb.core.parser.node.Start;
-import de.tlc4b.exceptions.NotSupportedException;
-
-public class NotSupportedConstructs extends DepthFirstAdapter {
-
- public NotSupportedConstructs(Start start) {
- start.apply(this);
- }
-
- public void inARefinesModelClause(ARefinesModelClause node) {
- throw new NotSupportedException(
- "Refines clause is currently not supported.");
- }
-
- public void inASeesMachineClause(ASeesMachineClause node) {
- throw new NotSupportedException(
- "SEES clause is currently not supported.");
- }
-
- public void inAUsesMachineClause(AUsesMachineClause node) {
- throw new NotSupportedException(
- "USES clause is currently not supported.");
- }
-
- public void inAPromotesMachineClause(APromotesMachineClause node) {
- throw new NotSupportedException(
- "Promotes clause is currently not supported.");
- }
-
- public void inASeesModelClause(ASeesModelClause node) {
- throw new NotSupportedException(
- "Sees clause is currently not supported.");
- }
-
- public void inAIncludesMachineClause(AIncludesMachineClause node) {
- throw new NotSupportedException(
- "INCLUDES clause is currently not supported.");
- }
-
- public void inAExtendsMachineClause(AExtendsMachineClause node) {
- throw new NotSupportedException(
- "EXTENDS clause is currently not supported.");
- }
-
- public void inAImportsMachineClause(AImportsMachineClause node) {
- throw new NotSupportedException(
- "IMPORTS clause is currently not supported.");
- }
-
- /**
- * Substitutions
- */
-
- public void inAWhileSubstitution(AWhileSubstitution node) {
- throw new NotSupportedException(
- "While substitutions are currently not supported.");
- }
-
- public void inASequenceSubstitution(ASequenceSubstitution node) {
- throw new NotSupportedException(
- "Sequence substitutions ';' are currently not supported.");
- }
-
- public void inAVarSubstitution(AVarSubstitution node) {
- throw new NotSupportedException(
- "VAR substitutions are currently not supported.");
- }
-
- public void inACaseSubstitution(ACaseSubstitution node) {
- // TODO it is possible to support this substitution
- throw new NotSupportedException(
- "Case substitutions are currently not supported.");
- }
-
-}
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index b2c0c5d03509d888d069f2ab5e414ae3135c3e18..864e506ee3bdb55cdf626275d8d9806f6c7bcec4 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -111,7 +111,7 @@ public class Renamer extends DepthFirstAdapter {
evalDefinitions();
- machineContext.getTree().apply(this);
+ machineContext.getStartNode().apply(this);
}
private void evalEnumValues() {
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index bf7dcf73f1347eae70672c2c61aa13e403eb4800..787a25f933a5b5671eec260b5d8833df19de7d8e 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -19,7 +19,7 @@ import de.tlc4b.btypes.ITypechecker;
import de.tlc4b.btypes.IntegerOrSetOfPairType;
import de.tlc4b.btypes.IntegerOrSetType;
import de.tlc4b.btypes.IntegerType;
-import de.tlc4b.btypes.ModelValueType;
+import de.tlc4b.btypes.EnumeratedSetElement;
import de.tlc4b.btypes.PairType;
import de.tlc4b.btypes.SetType;
import de.tlc4b.btypes.StringType;
@@ -31,9 +31,8 @@ import de.tlc4b.ltl.LTLBPredicate;
import de.tlc4b.ltl.LTLFormulaVisitor;
/**
- * TODO we need a second run over ast to check if all local variables have a
+ * TODO we need a second run over the AST to check if all local variables have a
* type. This run should be performed after the normal model checking task.
- *
*/
public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@@ -41,31 +40,21 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
private final Hashtable<Node, Node> referenceTable;
private final MachineContext machineContext;
- public Typechecker(MachineContext machineContext,
- Hashtable<String, MachineContext> contextTable,
- Hashtable<String, Typechecker> typecheckerTable) {
- this.machineContext = machineContext;
- this.types = new Hashtable<Node, BType>();
- this.referenceTable = machineContext.getReferences();
- }
-
public Typechecker(MachineContext context) {
this.types = new Hashtable<Node, BType>();
this.referenceTable = context.getReferences();
this.machineContext = context;
- context.getTree().apply(this);
- checkLTLFormulas();
+ context.getStartNode().apply(this);
checkConstantsSetup();
-
+ checkLTLFormulas();
}
private void checkLTLFormulas() {
ArrayList<LTLFormulaVisitor> visitors = machineContext.getLTLFormulas();
for (int i = 0; i < visitors.size(); i++) {
LTLFormulaVisitor visitor = visitors.get(i);
- Collection<AIdentifierExpression> parameter = visitor
- .getParameter();
+ Collection<AIdentifierExpression> parameter = visitor.getParameter();
for (AIdentifierExpression param : parameter) {
setType(param, new UntypedType());
}
@@ -82,14 +71,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
if (p != null) {
setType(p, BoolType.getInstance());
p.apply(this);
- for (Entry<String, Node> entry : machineContext.getConstants()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getConstants().entrySet()) {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException(
- "Can not infer type of constant '" + c + "': "
- + getType(n));
+ throw new TypeErrorException("Can not infer type of constant '" + c + "': " + getType(n));
}
}
}
@@ -108,8 +94,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
}
- public void updateType(Node node, AbstractHasFollowers oldType,
- BType newType) {
+ public void updateType(Node node, AbstractHasFollowers oldType, BType newType) {
oldType.deleteFollower(node);
this.types.put(node, newType);
if (newType instanceof AbstractHasFollowers) {
@@ -120,8 +105,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public BType getType(Node node) {
BType res = types.get(node);
if (res == null) {
- new TypeErrorException("Node '" + node + "' has not type.\n"
- + node.getStartPos());
+ new TypeErrorException("Node '" + node + "' has no type.\n" + node.getStartPos());
}
return res;
}
@@ -135,8 +119,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getHeader().apply(this);
}
{
- List<PMachineClause> copy = new ArrayList<PMachineClause>(
- node.getMachineClauses());
+ List<PMachineClause> copy = new ArrayList<PMachineClause>(node.getMachineClauses());
for (PMachineClause e : copy) {
e.apply(this);
}
@@ -149,15 +132,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAMachineHeader(AMachineHeader node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
String name = Utils.getIdentifierAsString(p.getIdentifier());
if (Character.isUpperCase(name.charAt(0))) {
- ModelValueType m = new ModelValueType(name);
+ EnumeratedSetElement m = new EnumeratedSetElement(name);
setType(p, new SetType(m));
} else {
UntypedType u = new UntypedType();
@@ -176,11 +158,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
String setName = Utils.getIdentifierAsString(copy);
- SetType set = new SetType(new ModelValueType(setName));
+ SetType set = new SetType(new EnumeratedSetElement(setName));
setType(node, set);
List<PExpression> copy2 = new ArrayList<PExpression>(node.getElements());
for (PExpression e : copy2) {
@@ -190,16 +171,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseADeferredSetSet(ADeferredSetSet node) {
- List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
- node.getIdentifier());
+ List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
String name = Utils.getIdentifierAsString(copy);
- setType(node, new SetType(new ModelValueType(name)));
+ setType(node, new SetType(new EnumeratedSetElement(name)));
}
@Override
public void caseAConstantsMachineClause(AConstantsMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -208,10 +187,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAAbstractConstantsMachineClause(
- AAbstractConstantsMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -221,8 +198,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAVariablesMachineClause(AVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -231,10 +207,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAConcreteVariablesMachineClause(
- AConcreteVariablesMachineClause node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -248,8 +222,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseADefinitionsMachineClause(ADefinitionsMachineClause node) {
- List<PDefinition> copy = new ArrayList<PDefinition>(
- node.getDefinitions());
+ List<PDefinition> copy = new ArrayList<PDefinition>(node.getDefinitions());
for (PDefinition e : copy) {
setType(e, new UntypedType());
}
@@ -261,10 +234,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
// d(a) == 1
- public void caseAExpressionDefinitionDefinition(
- AExpressionDefinitionDefinition node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ public void caseAExpressionDefinitionDefinition(AExpressionDefinitionDefinition node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
UntypedType u = new UntypedType();
setType(e, u);
@@ -275,11 +246,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
// d(a) == 1 = 1
- public void caseAPredicateDefinitionDefinition(
- APredicateDefinitionDefinition node) {
+ public void caseAPredicateDefinitionDefinition(APredicateDefinitionDefinition node) {
setType(node, BoolType.getInstance());
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
setType(e, new UntypedType());
}
@@ -297,13 +266,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '"
- + found + "' at definition call\n");
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "' at definition call\n");
}
- LinkedList<PExpression> params = ((AExpressionDefinitionDefinition) originalDef)
- .getParameters();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ LinkedList<PExpression> params = ((AExpressionDefinitionDefinition) originalDef).getParameters();
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (int i = 0; i < params.size(); i++) {
BType type = getType(params.get(i));
setType(copy.get(i), type);
@@ -320,13 +286,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + expected + "', found '"
- + found + "' at definition call\n");
+ throw new TypeErrorException("Expected '" + expected + "', found '" + found + "' at definition call\n");
}
- LinkedList<PExpression> params = ((APredicateDefinitionDefinition) originalDef)
- .getParameters();
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ LinkedList<PExpression> params = ((APredicateDefinitionDefinition) originalDef).getParameters();
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (int i = 0; i < params.size(); i++) {
setType(copy.get(i), getType(params.get(i)));
copy.get(i).apply(this);
@@ -343,13 +306,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- for (Entry<String, Node> entry : machineContext.getScalarParameter()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getScalarParameter().entrySet()) {
String name = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException(
- "Can not infer type of parameter '" + name + "'");
+ throw new TypeErrorException("Can not infer type of parameter '" + name + "'");
}
}
}
@@ -360,13 +321,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- for (Entry<String, Node> entry : machineContext.getConstants()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getConstants().entrySet()) {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException("Can not infer type of constant '"
- + c + "': " + getType(n));
+ throw new TypeErrorException("Can not infer type of constant '" + c + "': " + getType(n));
}
}
}
@@ -375,13 +334,11 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseAInvariantMachineClause(AInvariantMachineClause node) {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
- for (Entry<String, Node> entry : machineContext.getVariables()
- .entrySet()) {
+ for (Entry<String, Node> entry : machineContext.getVariables().entrySet()) {
String c = entry.getKey();
Node n = entry.getValue();
if (getType(n).isUntyped()) {
- throw new TypeErrorException("Can not infer type of variable '"
- + c + "'");
+ throw new TypeErrorException("Can not infer type of variable '" + c + "'");
}
}
}
@@ -396,8 +353,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAInitialisationMachineClause(
- AInitialisationMachineClause node) {
+ public void caseAInitialisationMachineClause(AInitialisationMachineClause node) {
if (node.getSubstitutions() != null) {
node.getSubstitutions().apply(this);
}
@@ -406,8 +362,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAOperation(AOperation node) {
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getReturnValues());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getReturnValues());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -416,8 +371,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
{
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression id = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -435,23 +389,22 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- Node originalIdentifier = referenceTable.get(node);
+
BType expected = getType(node);
if (expected == null) {
- System.out.println("Not implemented in Typechecker:"
- + node.parent().getClass());
+ System.out.println("Not implemented in Typechecker:" + node.parent().getClass());
throw new RuntimeException(node + " Pos: " + node.getStartPos());
}
- BType found = getType(originalIdentifier);
+ Node identifierDeclarationNode = referenceTable.get(node);
+ BType found = getType(identifierDeclarationNode);
String name = Utils.getIdentifierAsString(node.getIdentifier());
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "' at identifier " + name + "\n"
- + node.getStartPos());
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + found + "' at identifier " + name
+ + "\n" + node.getStartPos());
}
}
@@ -460,8 +413,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at '=' \n" + node.getStartPos());
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at '=' \n" + node.getStartPos());
}
UntypedType x = new UntypedType();
@@ -490,8 +442,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at '=' \n" + node.getClass());
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at '=' \n" + node.getClass());
}
UntypedType x = new UntypedType();
@@ -506,12 +457,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at 'For All' \n");
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at 'For All' \n");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -526,12 +475,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Expected '" + getType(node)
- + "', found BOOL at 'Exists' \n");
+ throw new TypeErrorException("Expected '" + getType(node) + "', found BOOL at 'Exists' \n");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -565,8 +512,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getCondition(), BoolType.getInstance());
node.getCondition().apply(this);
node.getThen().apply(this);
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getWhenSubstitutions());
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(node.getWhenSubstitutions());
for (PSubstitution e : copy) {
e.apply(this);
}
@@ -587,8 +533,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getCondition(), BoolType.getInstance());
node.getCondition().apply(this);
node.getThen().apply(this);
- List<PSubstitution> copy = new ArrayList<PSubstitution>(
- node.getElsifSubstitutions());
+ List<PSubstitution> copy = new ArrayList<PSubstitution>(node.getElsifSubstitutions());
for (PSubstitution e : copy) {
e.apply(this);
}
@@ -606,10 +551,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAAssignSubstitution(AAssignSubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getLhsExpression());
- List<PExpression> copy2 = new ArrayList<PExpression>(
- node.getRhsExpressions());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getLhsExpression());
+ List<PExpression> copy2 = new ArrayList<PExpression>(node.getRhsExpressions());
for (int i = 0; i < copy.size(); i++) {
PExpression left = copy.get(i);
@@ -632,10 +575,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseABecomesElementOfSubstitution(
- ABecomesElementOfSubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseABecomesElementOfSubstitution(ABecomesElementOfSubstitution node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
SetType set = new SetType(new UntypedType());
setType(node.getSet(), set);
@@ -650,8 +591,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAAnySubstitution(AAnySubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -663,8 +603,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseALetSubstitution(ALetSubstitution node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -683,9 +622,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in '" + node.getLiteral().getText()
- + "'");
+ throw new TypeErrorException(
+ "Excepted '" + getType(node) + "' , found 'INTEGER' in '" + node.getLiteral().getText() + "'");
}
}
@@ -695,8 +633,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'INTEGER'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'INTEGER'");
}
}
@@ -706,8 +643,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NATURAL'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NATURAL'");
}
}
@@ -717,8 +653,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NATURAL1'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NATURAL1'");
}
}
@@ -728,8 +663,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'INT'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'INT'");
}
}
@@ -739,8 +673,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NAT'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NAT'");
}
}
@@ -750,8 +683,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' in 'NAT1'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(INTEGER)' in 'NAT1'");
}
}
@@ -760,8 +692,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in '-'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in '-'");
}
}
@@ -771,8 +702,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(IntegerType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(INTEGER)' at interval operator");
+ throw new TypeErrorException(
+ "Excepted '" + getType(node) + "' , found 'POW(INTEGER)' at interval operator");
}
setType(node.getLeftBorder(), IntegerType.getInstance());
@@ -796,8 +727,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' > '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' > '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -810,8 +740,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' < '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' < '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -824,8 +753,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' >= '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' >= '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -838,8 +766,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' <= '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' <= '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -852,8 +779,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' min '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' min '");
}
setType(node.getExpression(), new SetType(IntegerType.getInstance()));
node.getExpression().apply(this);
@@ -864,8 +790,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' min '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' min '");
}
setType(node.getExpression(), new SetType(IntegerType.getInstance()));
node.getExpression().apply(this);
@@ -876,8 +801,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' + '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' + '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -886,8 +810,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAMinusOrSetSubtractExpression(
- AMinusOrSetSubtractExpression node) {
+ public void caseAMinusOrSetSubtractExpression(AMinusOrSetSubtractExpression node) {
BType expected = getType(node);
BType found = new IntegerOrSetType();
@@ -903,17 +826,15 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAMultOrCartExpression(AMultOrCartExpression node) {
BType expected = getType(node);
- IntegerOrSetOfPairType found = new IntegerOrSetOfPairType(
- node.getStartPos(), node.getEndPos());
+ IntegerOrSetOfPairType found = new IntegerOrSetOfPairType(node.getStartPos(), node.getEndPos());
// setType(node.getLeft(), found.getFirst());
// setType(node.getRight(), found.getSecond());
BType result = null;
try {
result = expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "' at " + node.getClass().getSimpleName() + "\n "
- + node.getStartPos());
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "' at "
+ + node.getClass().getSimpleName() + "\n " + node.getStartPos());
}
//
// BType res2 = getType(node);
@@ -924,10 +845,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
//
if (result instanceof IntegerOrSetOfPairType) {
- setType(node.getLeft(),
- ((IntegerOrSetOfPairType) result).getFirst());
- setType(node.getRight(),
- ((IntegerOrSetOfPairType) result).getSecond());
+ setType(node.getLeft(), ((IntegerOrSetOfPairType) result).getFirst());
+ setType(node.getRight(), ((IntegerOrSetOfPairType) result).getSecond());
} else if (result instanceof IntegerType) {
setType(node.getLeft(), result);
setType(node.getRight(), result);
@@ -949,8 +868,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' / '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' / '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -963,8 +881,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' ** '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' ** '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -977,8 +894,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'INTEGER' in ' mod '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'INTEGER' in ' mod '");
}
setType(node.getLeft(), IntegerType.getInstance());
setType(node.getRight(), IntegerType.getInstance());
@@ -988,15 +904,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseASuccessorExpression(ASuccessorExpression node) {
- FunctionType found = new FunctionType(IntegerType.getInstance(),
- IntegerType.getInstance());
+ FunctionType found = new FunctionType(IntegerType.getInstance(), IntegerType.getInstance());
unify(getType(node), found, node);
}
@Override
public void caseAPredecessorExpression(APredecessorExpression node) {
- FunctionType found = new FunctionType(IntegerType.getInstance(),
- IntegerType.getInstance());
+ FunctionType found = new FunctionType(IntegerType.getInstance(), IntegerType.getInstance());
unify(getType(node), found, node);
}
@@ -1006,12 +920,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + "INTEGER" + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + "INTEGER" + "'");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1030,12 +942,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
IntegerType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + "INTEGER" + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + "INTEGER" + "'");
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1057,8 +967,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in 'TRUE'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in 'TRUE'");
}
}
@@ -1067,8 +976,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in 'FALSE'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in 'FALSE'");
}
}
@@ -1078,8 +986,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
SetType found = new SetType(BoolType.getInstance());
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'POW(BOOL)' in 'BOOL'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'POW(BOOL)' in 'BOOL'");
}
}
@@ -1088,8 +995,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in 'bool(...)'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in 'bool(...)'");
}
setType(node.getPredicate(), BoolType.getInstance());
node.getPredicate().apply(this);
@@ -1104,8 +1010,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' & '." + node.getStartPos());
+ throw new TypeErrorException(
+ "Excepted '" + getType(node) + "' , found 'BOOL' in ' & '." + node.getStartPos());
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1118,8 +1024,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' or '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' or '");
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1132,8 +1037,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' => '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' => '");
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1147,8 +1051,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
System.out.println(node.parent().getClass());
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' <=> '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' <=> '");
}
setType(node.getLeft(), BoolType.getInstance());
setType(node.getRight(), BoolType.getInstance());
@@ -1161,8 +1064,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found 'BOOL' in ' not '");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found 'BOOL' in ' not '");
}
setType(node.getPredicate(), BoolType.getInstance());
node.getPredicate().apply(this);
@@ -1191,8 +1093,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(e, u);
}
BType expected = getType(node);
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getExpressions());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getExpressions());
for (PExpression e : copy) {
e.apply(this);
}
@@ -1239,6 +1140,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
private boolean compareElementsOfList(ArrayList<Node> list) {
+ if (list.size() == 1) {
+ return true;
+ }
try {
if (list.get(0) instanceof AIntegerExpression) {
HashSet<Integer> set = new HashSet<Integer>();
@@ -1253,11 +1157,9 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
} else if (list.get(0) instanceof AIdentifierExpression) {
HashSet<Node> set = new HashSet<Node>();
for (int i = 0; i < list.size(); i++) {
- AIdentifierExpression id = (AIdentifierExpression) list
- .get(i);
+ AIdentifierExpression id = (AIdentifierExpression) list.get(i);
Node enumValue = machineContext.getReferences().get(id);
- if (!machineContext.getEnumValues()
- .containsValue(enumValue)) {
+ if (!machineContext.getEnumValues().containsValue(enumValue)) {
return false;
}
set.add(enumValue);
@@ -1274,8 +1176,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAComprehensionSetExpression(AComprehensionSetExpression node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
ArrayList<BType> typesList = new ArrayList<BType>();
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
@@ -1289,8 +1190,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found " + found + "'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found " + found + "'");
}
setType(node.getPredicates(), BoolType.getInstance());
@@ -1299,10 +1199,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAEventBComprehensionSetExpression(
- AEventBComprehensionSetExpression node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ public void caseAEventBComprehensionSetExpression(AEventBComprehensionSetExpression node) {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1340,8 +1238,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found = found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'POW(POW(_A))' in 'POW'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'POW(POW(_A))' in 'POW'");
}
setType(expr, found.getSubtype());
@@ -1375,8 +1272,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found = found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
setType(left, found);
setType(right, found);
@@ -1407,8 +1303,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
setType(node.getExpression(), new UntypedType());
@@ -1447,8 +1342,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1465,8 +1359,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1484,8 +1377,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1503,8 +1395,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
BoolType.getInstance().unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found 'BOOL'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found 'BOOL'");
}
SetType set = new SetType(new UntypedType());
@@ -1527,14 +1418,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + found + "'");
}
}
@Override
- public void caseAGeneralIntersectionExpression(
- AGeneralIntersectionExpression node) {
+ public void caseAGeneralIntersectionExpression(AGeneralIntersectionExpression node) {
SetType set = new SetType(new SetType(new UntypedType()));
setType(node.getExpression(), set);
node.getExpression().apply(this);
@@ -1544,16 +1433,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + found + "'");
}
}
@Override
public void caseAQuantifiedUnionExpression(AQuantifiedUnionExpression node) {
BType expected = getType(node);
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -1569,17 +1456,14 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@Override
- public void caseAQuantifiedIntersectionExpression(
- AQuantifiedIntersectionExpression node) {
+ public void caseAQuantifiedIntersectionExpression(AQuantifiedIntersectionExpression node) {
BType expected = getType(node);
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
UntypedType u = new UntypedType();
@@ -1595,8 +1479,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1606,8 +1489,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseALambdaExpression(ALambdaExpression node) {
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getIdentifiers());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
setType(v, new UntypedType());
@@ -1633,15 +1515,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@Override
public void caseAFunctionExpression(AFunctionExpression node) {
- FunctionType func = new FunctionType(new UntypedType(),
- new UntypedType());
+ FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
setType(node.getIdentifier(), func);
node.getIdentifier().apply(this);
@@ -1660,12 +1540,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
rangeFound.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + rangeFound + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + rangeFound + "'");
}
- ArrayList<PExpression> copy = new ArrayList<PExpression>(
- node.getParameters());
+ ArrayList<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
setType(e, new UntypedType());
e.apply(this);
@@ -1680,8 +1558,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
domainFound.unify(p, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + domainFound
- + "' , found '" + makePair(foundList) + "'");
+ throw new TypeErrorException("Excepted '" + domainFound + "' , found '" + makePair(foundList) + "'");
}
}
@@ -1703,8 +1580,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
domainFound.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + domainFound + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + domainFound + "'");
}
}
@@ -1726,8 +1602,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
rangeFound.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected
- + "' , found '" + rangeFound + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found '" + rangeFound + "'");
}
}
@@ -1783,8 +1658,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseAPartialSurjectionExpression(
- APartialSurjectionExpression node) {
+ public void caseAPartialSurjectionExpression(APartialSurjectionExpression node) {
// evalFunction(node, node.getLeft(), node.getRight());
BType dom = new UntypedType();
BType ran = new UntypedType();
@@ -1830,8 +1704,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1860,8 +1733,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1880,8 +1752,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -1902,8 +1773,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseADomainRestrictionExpression(
- ADomainRestrictionExpression node) {
+ public void caseADomainRestrictionExpression(ADomainRestrictionExpression node) {
UntypedType u = new UntypedType();
SetType setType = new SetType(u);
FunctionType f = new FunctionType(u, new UntypedType());
@@ -1918,8 +1788,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseADomainSubtractionExpression(
- ADomainSubtractionExpression node) {
+ public void caseADomainSubtractionExpression(ADomainSubtractionExpression node) {
UntypedType u = new UntypedType();
SetType setType = new SetType(u);
FunctionType f = new FunctionType(u, new UntypedType());
@@ -2020,8 +1889,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
node.getLeft().apply(this);
@@ -2038,8 +1906,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
BType right = new SetType(new PairType(v, w));
setType(node.getLeft(), left);
setType(node.getRight(), right);
- BType found = new SetType(new PairType(new PairType(t, v),
- new PairType(u, w)));
+ BType found = new SetType(new PairType(new PairType(t, v), new PairType(u, w)));
BType expected = getType(node);
unify(expected, found, node);
@@ -2149,8 +2016,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseATransRelationExpression(ATransRelationExpression node) {
UntypedType t = new UntypedType();
UntypedType u = new UntypedType();
- setType(node.getExpression(), new SetType(new PairType(t,
- new SetType(u))));
+ setType(node.getExpression(), new SetType(new PairType(t, new SetType(u))));
BType found = new SetType(new PairType(t, u));
BType expected = getType(node);
unify(expected, found, node);
@@ -2161,22 +2027,19 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "' at " + node.getClass().getSimpleName() + "\n "
- + node.getStartPos() + ":" + node.getEndPos());
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "' at "
+ + node.getClass().getSimpleName() + "\n " + node.getStartPos() + ":" + node.getEndPos());
}
}
@Override
public void caseAEmptySequenceExpression(AEmptySequenceExpression node) {
BType expected = getType(node);
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
try {
expected.unify(found, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2188,8 +2051,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseASeqExpression(ASeqExpression node) {
UntypedType t = new UntypedType();
setType(node.getExpression(), new SetType(t));
- BType found = new SetType(
- new FunctionType(IntegerType.getInstance(), t));
+ BType found = new SetType(new FunctionType(IntegerType.getInstance(), t));
BType expected = getType(node);
unify(expected, found, node);
node.getExpression().apply(this);
@@ -2197,8 +2059,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseASizeExpression(ASizeExpression node) {
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), new UntypedType()));
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), new UntypedType()));
BType found = IntegerType.getInstance();
BType expected = getType(node);
unify(expected, found, node);
@@ -2207,8 +2068,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAConcatExpression(AConcatExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getLeft(), found);
setType(node.getRight(), found);
BType expected = getType(node);
@@ -2232,8 +2092,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAFirstExpression(AFirstExpression node) {
BType found = new UntypedType();
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), found));
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), found));
BType expected = getType(node);
unify(expected, found, node);
node.getExpression().apply(this);
@@ -2241,8 +2100,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseATailExpression(ATailExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getExpression(), found);
BType expected = getType(node);
unify(expected, found, node);
@@ -2256,8 +2114,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
private void evalSetOfSequences(Node node, Node expr) {
UntypedType t = new UntypedType();
setType(expr, new SetType(t));
- BType found = new SetType(
- new FunctionType(IntegerType.getInstance(), t));
+ BType found = new SetType(new FunctionType(IntegerType.getInstance(), t));
BType expected = getType(node);
unify(expected, found, node);
expr.apply(this);
@@ -2293,8 +2150,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseALastExpression(ALastExpression node) {
BType found = new UntypedType();
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), found));
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), found));
BType expected = getType(node);
unify(expected, found, node);
node.getExpression().apply(this);
@@ -2307,8 +2163,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseARevExpression(ARevExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getExpression(), found);
BType expected = getType(node);
unify(expected, found, node);
@@ -2317,8 +2172,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAFrontExpression(AFrontExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
setType(node.getExpression(), found);
BType expected = getType(node);
unify(expected, found, node);
@@ -2328,10 +2182,8 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseAGeneralConcatExpression(AGeneralConcatExpression node) {
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
- setType(node.getExpression(),
- new FunctionType(IntegerType.getInstance(), found));
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
+ setType(node.getExpression(), new FunctionType(IntegerType.getInstance(), found));
// BType found = new SetType(new PairType(IntegerType.getInstance(),
// new UntypedType()));
@@ -2368,16 +2220,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
}
@Override
- public void caseASequenceExtensionExpression(
- ASequenceExtensionExpression node) {
+ public void caseASequenceExtensionExpression(ASequenceExtensionExpression node) {
BType expected = getType(node);
- BType found = new FunctionType(IntegerType.getInstance(),
- new UntypedType());
+ BType found = new FunctionType(IntegerType.getInstance(), new UntypedType());
try {
found = found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
BType subtype;
if (found instanceof FunctionType) {
@@ -2389,8 +2238,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
for (PExpression e : node.getExpression()) {
setType(e, subtype);
}
- List<PExpression> copy = new ArrayList<PExpression>(
- node.getExpression());
+ List<PExpression> copy = new ArrayList<PExpression>(node.getExpression());
for (PExpression e : copy) {
e.apply(this);
}
@@ -2419,8 +2267,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
unify(expected, found, node);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2434,14 +2281,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getRecord().apply(this);
- BType found = ((StructType) getType(node.getRecord()))
- .getType(fieldName);
+ BType found = ((StructType) getType(node.getRecord())).getType(fieldName);
BType expected = getType(node);
try {
unify(expected, found, node);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2468,8 +2313,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(expected, this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + expected + "' , found "
- + found + "'");
+ throw new TypeErrorException("Excepted '" + expected + "' , found " + found + "'");
}
}
@@ -2482,8 +2326,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
StringType.getInstance().unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found " + StringType.getInstance() + "'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found " + StringType.getInstance() + "'");
}
}
@@ -2493,8 +2336,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
try {
found.unify(getType(node), this);
} catch (UnificationException e) {
- throw new TypeErrorException("Excepted '" + getType(node)
- + "' , found " + found + "'");
+ throw new TypeErrorException("Excepted '" + getType(node) + "' , found " + found + "'");
}
}
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
new file mode 100644
index 0000000000000000000000000000000000000000..ca12eb32e9764b885a769745f118806c2a733e96
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -0,0 +1,96 @@
+package de.tlc4b.analysis;
+
+import java.io.StringWriter;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Set;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.ACaseSubstitution;
+import de.be4.classicalb.core.parser.node.AExtendsMachineClause;
+import de.be4.classicalb.core.parser.node.AImplementationMachineParseUnit;
+import de.be4.classicalb.core.parser.node.AImportsMachineClause;
+import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
+import de.be4.classicalb.core.parser.node.APromotesMachineClause;
+import de.be4.classicalb.core.parser.node.ARefinesModelClause;
+import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
+import de.be4.classicalb.core.parser.node.AVarSubstitution;
+import de.be4.classicalb.core.parser.node.AWhileSubstitution;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.exceptions.NotSupportedException;
+
+public class UnsupportedConstructsFinder extends DepthFirstAdapter {
+ private final Start start;
+ private static final Set<Class<? extends Node>> unsupportedClasses = new HashSet<>();
+
+ static {
+ add(ARefinesModelClause.class);
+ add(AExtendsMachineClause.class);
+ add(APromotesMachineClause.class);
+ add(AIncludesMachineClause.class);
+ add(AImportsMachineClause.class);
+
+ add(AWhileSubstitution.class);
+ add(ASequenceSubstitution.class);
+ add(AVarSubstitution.class);
+ add(ACaseSubstitution.class);
+
+ add(AImplementationMachineParseUnit.class);
+ }
+
+ private static void add(Class<? extends Node> clazz) {
+ unsupportedClasses.add(clazz);
+ }
+
+ public UnsupportedConstructsFinder(Start start) {
+ this.start = start;
+ }
+
+ public void find() {
+ start.apply(this);
+ }
+
+ private static final List<String> SUM_TYPE = new LinkedList<String>(
+ Arrays.asList("model_clause", "machine_clause", "substitution", "machine_parse_unit"));
+
+ private String formatCamel(final String input) {
+ StringWriter out = new StringWriter();
+ char[] chars = input.toCharArray();
+ for (int i = 0; i < chars.length; i++) {
+ char current = chars[i];
+ if (Character.isUpperCase(current)) {
+ out.append('_');
+ out.append(Character.toLowerCase(current));
+ } else {
+ out.append(current);
+ }
+ }
+ return out.toString();
+ }
+
+ public void defaultIn(Node node) {
+ if (unsupportedClasses.contains(node.getClass())) {
+ final String formatedName = formatCamel(node.getClass().getSimpleName());
+ final String className = node.getClass().getSimpleName();
+ for (final String suffix : SUM_TYPE) {
+ if (formatedName.endsWith(suffix)) {
+ final String shortName = formatedName.substring(3, formatedName.length() - suffix.length() - 1)
+ .toUpperCase();
+ final String[] split = suffix.split("_");
+ final String type = split[split.length - 1];
+ if (type.equals("clause") || type.equals("substitution")) {
+ throw new NotSupportedException(shortName + " " + type + " is not supported.");
+ } else {
+ throw new NotSupportedException(shortName + " is not supported.");
+ }
+
+ }
+ }
+ throw new NotSupportedException(className + " is not supported.");
+ }
+ }
+
+}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index ab416a1cf00c472861f77a8474b96fc308ae5ba1..aecdcbb166eed4af5d196ab6c0dabffc5ac65b99 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -583,7 +583,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
+ UtilMethods.getPositionAsString(e));
}
- tree = conType.createSyntaxTreeNode(typechecker);
+ tree = conType.createASTNode(typechecker);
} else {
tree = (PExpression) restrictedList.get(0);
for (int i = 1; i < restrictedList.size(); i++) {
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
index db63b09f68eafafc39d3cf1eee91341cca77392e..eb7a3a40950a4b7eeca71af60a0d64b75af8cdd1 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
@@ -49,7 +49,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
public AssignedVariablesFinder(MachineContext machineContext) {
this.assignedVariablesTable = new Hashtable<Node, HashSet<Node>>();
this.machineContext = machineContext;
- machineContext.getTree().apply(this);
+ machineContext.getStartNode().apply(this);
}
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
index 3713b6730830c3ac506fe2cdac34daa5e572b8d5..fe08cb904fe3567060755ad992bd19d0455f3860 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
@@ -87,7 +87,7 @@ public class UnchangedVariablesFinder extends DepthFirstAdapter {
this.unchangedVariablesTable = new Hashtable<Node, HashSet<Node>>();
this.unchangedVariablesNull = new Hashtable<Node, HashSet<Node>>();
- c.getTree().apply(this);
+ c.getStartNode().apply(this);
}
@Override
diff --git a/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java b/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
index 0bfd4b8466b4857c45cd0b3ead978285388b71cd..868598c0021f6e5698a63fe41249d37a10c11227 100644
--- a/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
+++ b/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
@@ -1,26 +1,29 @@
package de.tlc4b.btypes;
-
import java.util.ArrayList;
import de.be4.classicalb.core.parser.node.Node;
-public abstract class AbstractHasFollowers implements BType{
+public abstract class AbstractHasFollowers implements BType {
public abstract boolean contains(BType other);
-
- public ArrayList<Object> followers = new ArrayList<Object>();
- public void addFollower(Object obj){
- if(!followers.contains(obj))
+ private ArrayList<Object> followers = new ArrayList<Object>();
+
+ public ArrayList<Object> getFollowers() {
+ return this.followers;
+ }
+
+ public void addFollower(Object obj) {
+ if (!followers.contains(obj))
followers.add(obj);
}
-
- public String printFollower(){
+
+ public String printFollower() {
StringBuffer res = new StringBuffer();
res.append("[");
for (Object o : followers) {
- if(!(o instanceof Node)){
+ if (!(o instanceof Node)) {
res.append(o.hashCode());
res.append(o.getClass());
res.append(" ");
@@ -29,38 +32,36 @@ public abstract class AbstractHasFollowers implements BType{
res.append("]");
return res.toString();
}
-
- public void deleteFollower(Object obj){
+
+ public void deleteFollower(Object obj) {
followers.remove(obj);
}
-
-
-
- public void setFollowersTo(BType newType, ITypechecker typechecker){
- if (this == newType){
+
+ public void setFollowersTo(BType newType, ITypechecker typechecker) {
+ if (this == newType) {
return;
}
- ArrayList<Object> list = new ArrayList<Object>(followers);
- for (Object obj: list) {
- if(obj instanceof Node){
+ ArrayList<Object> list = new ArrayList<Object>(followers);
+ for (Object obj : list) {
+ if (obj instanceof Node) {
typechecker.setType((Node) obj, newType);
- }else if(obj instanceof SetType){
+ } else if (obj instanceof SetType) {
((SetType) obj).setSubtype(newType);
- }else if(obj instanceof IntegerOrSetOfPairType){
- //System.out.println("this " +this + " old " + obj + " new " + newType);
+ } else if (obj instanceof IntegerOrSetOfPairType) {
+ // System.out.println("this " +this + " old " + obj + " new " +
+ // newType);
((IntegerOrSetOfPairType) obj).update(this, newType, typechecker);
- }else if(obj instanceof PairType){
+ } else if (obj instanceof PairType) {
((PairType) obj).update(this, newType);
- }else if(obj instanceof FunctionType){
+ } else if (obj instanceof FunctionType) {
((FunctionType) obj).update(this, newType);
- }else if(obj instanceof StructType){
+ } else if (obj instanceof StructType) {
((StructType) obj).update(this, newType);
- }
- else{
- throw new RuntimeException("Missing follower type: "+ obj.getClass());
+ } else {
+ throw new RuntimeException("Missing follower type: " + obj.getClass());
}
}
this.followers.clear();
-
+
}
}
diff --git a/src/main/java/de/tlc4b/btypes/BType.java b/src/main/java/de/tlc4b/btypes/BType.java
index ed800fc80ac70ff2dd520b63200660c317d72091..b90b379def0affef19c9d9292e50f26ff792a954 100644
--- a/src/main/java/de/tlc4b/btypes/BType.java
+++ b/src/main/java/de/tlc4b/btypes/BType.java
@@ -3,11 +3,10 @@ package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tlc4b.analysis.Typechecker;
-public interface BType extends ITypeConstants{
+public interface BType {
public BType unify(BType other, ITypechecker typechecker);
public boolean isUntyped();
public boolean compare(BType other);
- public String getTlaType();
public boolean containsInfiniteType();
- public PExpression createSyntaxTreeNode(Typechecker typechecker);
+ public PExpression createASTNode(Typechecker typechecker);
}
diff --git a/src/main/java/de/tlc4b/btypes/BoolType.java b/src/main/java/de/tlc4b/btypes/BoolType.java
index ef7bb6b657758fb6e2137b8091ed07b03c0a0166..e2937dd21edcc337e4291864282c59b2f141afdd 100644
--- a/src/main/java/de/tlc4b/btypes/BoolType.java
+++ b/src/main/java/de/tlc4b/btypes/BoolType.java
@@ -43,15 +43,11 @@ public class BoolType implements BType {
return false;
}
- public String getTlaType() {
- return "BOOLEAN";
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
ABoolSetExpression node = new ABoolSetExpression();
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/ModelValueType.java b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
similarity index 73%
rename from src/main/java/de/tlc4b/btypes/ModelValueType.java
rename to src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
index 4017d4869850ae40cb3f7375dd5079c3ac28303e..41728d814aca42662b85218cc336c75ed9051ab6 100644
--- a/src/main/java/de/tlc4b/btypes/ModelValueType.java
+++ b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
@@ -8,10 +8,10 @@ import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.exceptions.UnificationException;
-public class ModelValueType implements BType {
+public class EnumeratedSetElement implements BType {
private String name;
- public ModelValueType(String name) {
+ public EnumeratedSetElement(String name) {
this.name = name;
}
@@ -23,8 +23,8 @@ public class ModelValueType implements BType {
if (!this.compare(other)) {
throw new UnificationException();
}
- if (other instanceof ModelValueType) {
- if (((ModelValueType) other).getName().equals(this.name)) {
+ if (other instanceof EnumeratedSetElement) {
+ if (((EnumeratedSetElement) other).getName().equals(this.name)) {
return this;
} else {
throw new UnificationException();
@@ -49,23 +49,19 @@ public class ModelValueType implements BType {
public boolean compare(BType other) {
if (other instanceof UntypedType)
return true;
- if (other instanceof ModelValueType) {
- if (((ModelValueType) other).getName().equals(this.name)) {
+ if (other instanceof EnumeratedSetElement) {
+ if (((EnumeratedSetElement) other).getName().equals(this.name)) {
return true;
}
}
return false;
}
- public String getTlaType() {
- return name;
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
TIdentifierLiteral literal = new TIdentifierLiteral(name);
ArrayList<TIdentifierLiteral> idList = new ArrayList<TIdentifierLiteral>();
idList.add(literal);
diff --git a/src/main/java/de/tlc4b/btypes/FunctionType.java b/src/main/java/de/tlc4b/btypes/FunctionType.java
index 64e4348a3033f8b6756cb60df2a6de4f1ca3cfbb..5687f1b866010fe55c81381951f806eab4bb014e 100644
--- a/src/main/java/de/tlc4b/btypes/FunctionType.java
+++ b/src/main/java/de/tlc4b/btypes/FunctionType.java
@@ -81,6 +81,7 @@ public class FunctionType extends AbstractHasFollowers {
setRange(newType);
}
+ @Override
public boolean compare(BType other) {
if (other instanceof UntypedType)
return true;
@@ -119,19 +120,17 @@ public class FunctionType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return "[" + domain.getTlaType() + " -> " + range.getTlaType() + "]";
- }
-
+ @Override
public boolean containsInfiniteType() {
return this.domain.containsInfiniteType()
|| this.range.containsInfiniteType();
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ @Override
+ public PExpression createASTNode(Typechecker typechecker) {
APartialFunctionExpression node = new APartialFunctionExpression(
- domain.createSyntaxTreeNode(typechecker),
- range.createSyntaxTreeNode(typechecker));
+ domain.createASTNode(typechecker),
+ range.createASTNode(typechecker));
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/ITypeConstants.java b/src/main/java/de/tlc4b/btypes/ITypeConstants.java
deleted file mode 100644
index 70822584085caea3fa9a3e3a28a7ad5d353238d2..0000000000000000000000000000000000000000
--- a/src/main/java/de/tlc4b/btypes/ITypeConstants.java
+++ /dev/null
@@ -1,6 +0,0 @@
-package de.tlc4b.btypes;
-
-public interface ITypeConstants {
-
- public final String INTEGER = "INTEGER";
-}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
index 7de577d20adc883fcf465219f3fa8f537180a064..d0d929bd7a2cac9a3785c4152a11b5171c7d8bb2 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
@@ -32,7 +32,7 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
}
public void update(BType oldType, BType newType, ITypechecker typechecker) {
- if(second.followers.contains(first)){
+ if(second.getFollowers().contains(first)){
System.out.println("integerOrsetOfPair");
throw new RuntimeException();
}
@@ -219,15 +219,11 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return null;
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
return null;
}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
index 82857bb780d299ebac98ae4592cd855a5c6fe75c..7d52dfae8b2d30cf1212699b26677083d4de14bf 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
@@ -34,7 +34,6 @@ public class IntegerOrSetType extends AbstractHasFollowers {
}
public boolean isUntyped() {
- // TODO proof
return true;
}
@@ -55,15 +54,11 @@ public class IntegerOrSetType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return null;
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
return null;
}
}
diff --git a/src/main/java/de/tlc4b/btypes/IntegerType.java b/src/main/java/de/tlc4b/btypes/IntegerType.java
index fe3d951815adfc758caae5cbe6fbfc61940dd498..9516c9f1321645bfe49208775bbd04fa24ec2fa1 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerType.java
@@ -2,7 +2,6 @@ package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
-import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.exceptions.UnificationException;
@@ -40,11 +39,6 @@ public class IntegerType implements BType {
return "INTEGER";
}
- public String getTlaType() {
- return TLC4BGlobals.getMIN_INT() + ".." + TLC4BGlobals.getMAX_INT();
- }
-
-
public boolean isUntyped() {
return false;
@@ -63,7 +57,7 @@ public class IntegerType implements BType {
return true;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
AIntegerSetExpression node = new AIntegerSetExpression();
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/PairType.java b/src/main/java/de/tlc4b/btypes/PairType.java
index 1e9057d795f94a60bc53bcfc644ab172325fbdcd..fe7e270a4b0dce4cd300a93ea6c7b9b6d5f51773 100644
--- a/src/main/java/de/tlc4b/btypes/PairType.java
+++ b/src/main/java/de/tlc4b/btypes/PairType.java
@@ -120,24 +120,15 @@ public class PairType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- String res = first.getTlaType() + " \\times ";
- if (second instanceof PairType) {
- res += "(" + second.getTlaType() + ")";
- } else
- res += second.getTlaType();
- return res;
- }
-
public boolean containsInfiniteType() {
return this.first.containsInfiniteType()
|| this.second.containsInfiniteType();
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
ACartesianProductExpression node = new ACartesianProductExpression(
- first.createSyntaxTreeNode(typechecker),
- second.createSyntaxTreeNode(typechecker));
+ first.createASTNode(typechecker),
+ second.createASTNode(typechecker));
typechecker.setType(node, new SetType(this));
return node;
}
diff --git a/src/main/java/de/tlc4b/btypes/SetType.java b/src/main/java/de/tlc4b/btypes/SetType.java
index 8137156d58a149a3e9ffdb4e8dc2abf17f865cb8..8edfe6889efbcb5bc2301932cfce8aacbee9cd31 100644
--- a/src/main/java/de/tlc4b/btypes/SetType.java
+++ b/src/main/java/de/tlc4b/btypes/SetType.java
@@ -34,8 +34,7 @@ public class SetType extends AbstractHasFollowers {
}
if (other instanceof SetType) {
((SetType) other).setFollowersTo(this, typechecker);
- this.subtype = this.subtype.unify(((SetType) other).subtype,
- typechecker);
+ this.subtype = this.subtype.unify(((SetType) other).subtype, typechecker);
return this;
}
@@ -56,12 +55,12 @@ public class SetType extends AbstractHasFollowers {
@Override
public String toString() {
- if(this.equals(subtype)){
+ if (this.equals(subtype)) {
return "POW(recursive call)";
- }else{
+ } else {
return "POW(" + subtype + ")";
}
-
+
}
public boolean isUntyped() {
@@ -75,8 +74,7 @@ public class SetType extends AbstractHasFollowers {
if (other instanceof UntypedType)
return true;
- if (other instanceof IntegerOrSetType
- || other instanceof IntegerOrSetOfPairType) {
+ if (other instanceof IntegerOrSetType || other instanceof IntegerOrSetOfPairType) {
return true;
} else if (other instanceof FunctionType) {
return other.compare(this);
@@ -86,7 +84,7 @@ public class SetType extends AbstractHasFollowers {
@Override
public boolean contains(BType other) {
- if(this.equals(subtype)){
+ if (this.equals(subtype)) {
return true;
}
if (this.subtype.equals(other)) {
@@ -98,16 +96,12 @@ public class SetType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return "SUBSET(" + subtype.getTlaType() + ")";
- }
-
public boolean containsInfiniteType() {
return this.subtype.containsInfiniteType();
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
- APowSubsetExpression node = new APowSubsetExpression(subtype.createSyntaxTreeNode(typechecker));
+ public PExpression createASTNode(Typechecker typechecker) {
+ APowSubsetExpression node = new APowSubsetExpression(subtype.createASTNode(typechecker));
typechecker.setType(node, this);
return node;
}
diff --git a/src/main/java/de/tlc4b/btypes/StringType.java b/src/main/java/de/tlc4b/btypes/StringType.java
index 4771569a3cee584c1ccc28c389332284e18e903c..b4599467f9e19f5a588c74934667dab5a8a4462a 100644
--- a/src/main/java/de/tlc4b/btypes/StringType.java
+++ b/src/main/java/de/tlc4b/btypes/StringType.java
@@ -48,15 +48,11 @@ public class StringType implements BType {
return false;
}
- public String getTlaType() {
- return "STRING";
- }
-
public boolean containsInfiniteType() {
return true;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
AStringSetExpression node = new AStringSetExpression();
typechecker.setType(node, new SetType(this));
return node;
diff --git a/src/main/java/de/tlc4b/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
index 30fc041ebadd20f5f09438086dcdd02712de9164..e2e4345bea039c43fe0714881c57d39f092f9574 100644
--- a/src/main/java/de/tlc4b/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -188,28 +188,6 @@ public class StructType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- StringBuffer res = new StringBuffer();
- res.append("[");
- Iterator<Entry<String, BType>> iterator = types.entrySet().iterator();
- if (!iterator.hasNext()) {
- res.append("...");
- } else {
- while (iterator.hasNext()) {
- Entry<String, BType> next = iterator.next();
- String fieldName = next.getKey();
- BType type = next.getValue();
- res.append(fieldName);
- res.append(":");
- res.append(type);
- if (iterator.hasNext())
- res.append(",");
- }
- }
- res.append("]");
- return res.toString();
- }
-
public boolean containsInfiniteType() {
Iterator<BType> iterator = this.types.values().iterator();
while (iterator.hasNext()) {
@@ -219,7 +197,7 @@ public class StructType extends AbstractHasFollowers {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
ArrayList<PRecEntry> list = new ArrayList<PRecEntry>();
Set<Entry<String, BType>> entrySet = this.types.entrySet();
@@ -231,7 +209,7 @@ public class StructType extends AbstractHasFollowers {
idList.add(literal);
AIdentifierExpression id = new AIdentifierExpression(idList);
ARecEntry recEntry = new ARecEntry(id,
- type.createSyntaxTreeNode(typechecker));
+ type.createASTNode(typechecker));
list.add(recEntry);
}
AStructExpression node = new AStructExpression(list);
diff --git a/src/main/java/de/tlc4b/btypes/UntypedType.java b/src/main/java/de/tlc4b/btypes/UntypedType.java
index a24e490ea03324e96f48a9cecd2d88b7c6adc80f..2d1eee0ce0f77b006f666a19e3d49a38c9ae64b3 100644
--- a/src/main/java/de/tlc4b/btypes/UntypedType.java
+++ b/src/main/java/de/tlc4b/btypes/UntypedType.java
@@ -3,7 +3,6 @@ package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tlc4b.analysis.Typechecker;
-
public class UntypedType extends AbstractHasFollowers {
public BType unify(BType other, ITypechecker typechecker) {
@@ -24,21 +23,12 @@ public class UntypedType extends AbstractHasFollowers {
return false;
}
- public String getTlaType() {
- return this.toString();
- }
-
public boolean containsInfiniteType() {
return false;
}
- public PExpression createSyntaxTreeNode(Typechecker typechecker) {
+ public PExpression createASTNode(Typechecker typechecker) {
return null;
}
-
-// @Override
-// public String toString(){
-// return "UNTYPED: Followers: "+ this.printFollower();
-// }
}
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index 51ecca716c453f1afc12c848e53195b293f76a5d..4ce9715c29df46688d92a230dd709ca04718c974 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -70,23 +70,21 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
public void parseDefinition(AExpressionDefinitionDefinition def) {
if (!(def.getRhs() instanceof AStringExpression)) {
- throw new LTLParseException(
- "Error: LTL formula is not in a string representation.");
+ throw new LTLParseException("Error: LTL formula is not in a string representation.");
}
AStringExpression stringNode = (AStringExpression) def.getRhs();
this.ltlFormula = stringNode.getContent().getText();
try {
- this.ltlFormulaStart = parse(ltlFormula);
+ this.ltlFormulaStart = parseLTLFormula(ltlFormula);
} catch (Exception e) {
- String line = "Parsing definition " + name + " (line "
- + def.getStartPos().getLine() + "):\n";
- throw new LTLParseException(line + e.getMessage());
+ String message = "Parsing definition " + name + " (line " + def.getStartPos().getLine() + "):\n";
+ throw new LTLParseException(message + e.getMessage());
}
}
- public void parseLTLString(String ltlString) {
+ public void parseLTLString(final String ltlString) {
try {
- this.ltlFormulaStart = parse(ltlString);
+ this.ltlFormulaStart = parseLTLFormula(ltlString);
} catch (Exception e) {
throw new LTLParseException(e.getMessage());
}
@@ -108,8 +106,7 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return ltlNodeToBNodeTable;
}
- public de.be4.classicalb.core.parser.node.Node getBAst(
- de.be4.ltl.core.parser.node.Node unparsedLtl) {
+ public de.be4.classicalb.core.parser.node.Node getBAst(de.be4.ltl.core.parser.node.Node unparsedLtl) {
return ltlNodeToBNodeTable.get(unparsedLtl);
}
@@ -125,14 +122,12 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
return ltlFormulaStart;
}
- public void printLTLFormula(TLAPrinter tlaPrinter,
- TypeRestrictor typeRestrictor) {
+ public void printLTLFormula(TLAPrinter tlaPrinter, TypeRestrictor typeRestrictor) {
// LTLFormulaPrinter ltlFormulaPrinter =
new LTLFormulaPrinter(tlaPrinter, this, typeRestrictor);
}
- public static Start parse(String ltlFormula) throws ParserException,
- LexerException, IOException {
+ public static Start parseLTLFormula(String ltlFormula) throws ParserException, LexerException, IOException {
StringReader reader = new StringReader(ltlFormula);
PushbackReader r = new PushbackReader(reader);
Lexer l = new LtlLexer(r);
@@ -144,13 +139,11 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
@Override
public void caseAUnparsedLtl(AUnparsedLtl node) {
- de.be4.classicalb.core.parser.node.Start start = parseBPredicate(node
- .getPredicate().getText());
+ de.be4.classicalb.core.parser.node.Start start = parseBPredicate(node.getPredicate().getText());
ltlNodeToBNodeTable.put(node, start);
- LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(),
- start);
+ LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(), start);
this.bPredicates.add(ltlBPredicate);
machineContext.checkLTLBPredicate(ltlBPredicate);
@@ -171,19 +164,17 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
@Override
public void caseAExistsLtl(AExistsLtl node) {
- handleQuantification(node, node.getExistsIdentifier().getText(), node
- .getPredicate().getText(), node.getLtl());
+ handleQuantification(node, node.getExistsIdentifier().getText(), node.getPredicate().getText(), node.getLtl());
}
@Override
public void caseAForallLtl(AForallLtl node) {
- handleQuantification(node, node.getForallIdentifier().getText(), node
- .getPredicate().getText(), node.getLtl());
+ handleQuantification(node, node.getForallIdentifier().getText(), node.getPredicate().getText(), node.getLtl());
}
- private void handleQuantification(de.be4.ltl.core.parser.node.Node node,
- String parameterName, String bPredicateString, PLtl ltl) {
+ private void handleQuantification(de.be4.ltl.core.parser.node.Node node, String parameterName,
+ String bPredicateString, PLtl ltl) {
// create an identifier (b ast node) for the parameter of the
// quantification
List<TIdentifierLiteral> list = new ArrayList<TIdentifierLiteral>();
@@ -204,8 +195,7 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
// collect all identifiers which can be used in the bPredicate and
// verify the bPredicate
- LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(),
- start);
+ LTLBPredicate ltlBPredicate = new LTLBPredicate(getUnifiedContext(), start);
this.bPredicates.add(ltlBPredicate);
machineContext.checkLTLBPredicate(ltlBPredicate);
@@ -250,68 +240,56 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
}
public void inAUntilLtl(AUntilLtl node) {
- throw new ScopeException(
- "The 'until' operator is not supported by TLC.");
+ throw new ScopeException("The 'until' operator is not supported.");
}
public void inAWeakuntilLtl(AWeakuntilLtl node) {
- throw new ScopeException(
- "The 'weak until' operator is not supported by TLC.");
+ throw new ScopeException("The 'weak until' operator is not supported.");
}
public void inAReleaseLtl(AReleaseLtl node) {
- throw new ScopeException(
- "The 'release' operator is not supported by TLC.");
+ throw new ScopeException("The 'release' operator is not supported.");
}
public void inASinceLtl(ASinceLtl node) {
- throw new ScopeException(
- "The 'since' operator is not supported by TLC.");
+ throw new ScopeException("The 'since' operator is not supported.");
}
public void inATriggerLtl(ATriggerLtl node) {
- throw new ScopeException(
- "The 'trigger' operator is not supported by TLC.");
+ throw new ScopeException("The 'trigger' operator is not supported.");
}
public void inAHistoricallyLtl(AHistoricallyLtl node) {
- throw new ScopeException(
- "The 'history' operator is not supported by TLC.");
+ throw new ScopeException("The 'history' operator is not supported.");
}
public void inAOnceLtl(AOnceLtl node) {
- throw new ScopeException("The 'once' operator is not supported by TLC.");
+ throw new ScopeException("The 'once' operator is not supported.");
}
public void inAYesterdayLtl(AYesterdayLtl node) {
- throw new ScopeException(
- "The 'yesterday' operator is not supported by TLC.");
+ throw new ScopeException("The 'yesterday' operator is not supported.");
}
@Override
public void caseAActionLtl(AActionLtl node) {
- throw new ScopeException(
- "The '[...]' operator is not supported by TLC.");
- }
-
- @Override
- public void caseAAndLtl(AAndLtl node)
- {
- inAAndLtl(node);
- if(node.getLeft() != null)
- {
- node.getLeft().apply(this);
- }
- if(node.getRight() != null)
- {
- node.getRight().apply(this);
- System.out.println(node.getRight().getClass());
- }
- outAAndLtl(node);
- }
-
- protected MachineContext getMachineContext(){
- return this.machineContext;
- }
-
+ throw new ScopeException("The '[...]' operator is not supported.");
+ }
+
+ @Override
+ public void caseAAndLtl(AAndLtl node) {
+ inAAndLtl(node);
+ if (node.getLeft() != null) {
+ node.getLeft().apply(this);
+ }
+ if (node.getRight() != null) {
+ node.getRight().apply(this);
+ }
+ outAAndLtl(node);
+ }
+
+ public MachineContext getMachineContext() {
+ return this.machineContext;
+ }
+
}
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index ca2b6c666c923f365ad4b58819f9843a31a06808..dbef5ec399014c2883028b4f6794af486217378c 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -74,7 +74,7 @@ public class Generator extends DepthFirstAdapter {
evalInvariant();
evalOperations();
evalGoal();
- machineContext.getTree().apply(this);
+ machineContext.getStartNode().apply(this);
evalSpec();
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 318f46338995903d95962fa36e3a38be947dea9f..8b9584664ec600025075019c221711ea5116260a 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -53,7 +53,7 @@ public class TLCOutputInfo {
this.constants = machineContext.getConstants().keySet();
this.hasInit = tlaModule.getInitPredicates().size() > 0;
- if (machineContext.constantSetupInTraceFile()) {
+ if (machineContext.hasConstants()) {
this.constantSetup = true;
}
diff --git a/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java b/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..030e63909a46c54e6661022ad9f6b0412c82bd9d
--- /dev/null
+++ b/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
@@ -0,0 +1,22 @@
+package de.tlc4b.analysis;
+
+import static de.tlc4b.util.TestUtil.*;
+
+import org.junit.Test;
+
+import de.tlc4b.exceptions.NotSupportedException;
+
+public class UnsupportedConstructsTest {
+
+ @Test(expected = NotSupportedException.class)
+ public void testExtends() throws Exception {
+ final String machine = "MACHINE test\n" + "EXTENDS foo\n PROMOTES bar\n" + "END";
+ tryTranslating(machine);
+ }
+
+ @Test(expected = NotSupportedException.class)
+ public void testImplementation() throws Exception {
+ final String machine = "IMPLEMENTATION test REFINES foo END";
+ tryTranslating(machine);
+ }
+}
diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
index 8aaa4172a5608f1de2e9d5dde5e365037f82dfa7..b3cfc02a8c6b2ac6f864d0b1e364a1c1370b270e 100644
--- a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
@@ -62,8 +62,8 @@ public class FunctionTest {
+ "PROPERTIES {(1|->2|->3)} = %a,b.(a = b | a+b)\n"
+ "END";
String expected = "---- MODULE test ----\n"
- + "EXTENDS Integers\n"
- + "ASSUME {<<<<1, 2>>,3>>} = {<<<<a, b>>, a + b>> : <<a, b>> \\in { <<a, b>> \\in ((Int) \\times (Int)) : a = b}}\n"
+ + "EXTENDS Integers, TLC\n"
+ + "ASSUME (<<1, 2>>:>3) = [<<a, b>> \\in {<<a, b>> \\in ((Int) \\times (Int)) : a = b} |-> a + b] \n"
+ "====";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/typechecking/FunctionTest.java b/src/test/java/de/tlc4b/typechecking/FunctionTest.java
index b9a11aa32158d0eea248e61e8e0c944574a5707c..8a815cc45214ac715e2eb1146473871e9e0f9e56 100644
--- a/src/test/java/de/tlc4b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tlc4b/typechecking/FunctionTest.java
@@ -22,6 +22,17 @@ public class FunctionTest {
assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString());
}
+ @Test
+ public void testOverride() throws BException {
+ String machine = "MACHINE test\n"
+ + "CONSTANTS k,k2,p \n"
+ + "PROPERTIES p = 1 & k = %x.(x : {1} | 1) & k2 = k <+ {1|->2}\n"
+ + "END";
+ TestTypechecker t = new TestTypechecker(machine);
+ assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k").toString());
+ assertEquals("FUNC(INTEGER,INTEGER)", t.constants.get("k2").toString());
+ }
+
@Test
public void testSetOperatorOnFunction() throws BException {
diff --git a/src/test/java/de/tlc4b/typechecking/RelationsTest.java b/src/test/java/de/tlc4b/typechecking/RelationsTest.java
index a2adbd3c363ec2c132e657ebfb785020871fbb35..8216e686eaf156cb846aad91b93477c96cd283aa 100644
--- a/src/test/java/de/tlc4b/typechecking/RelationsTest.java
+++ b/src/test/java/de/tlc4b/typechecking/RelationsTest.java
@@ -85,7 +85,7 @@ public class RelationsTest {
+ "PROPERTIES k = {1} <| {(k2, TRUE)} \n"
+ "END";
TestTypechecker t = new TestTypechecker(machine);
- assertEquals("POW(INTEGER*BOOL)", t.constants.get("k").toString());
+ assertEquals("FUNC(INTEGER,BOOL)", t.constants.get("k").toString());
assertEquals("INTEGER", t.constants.get("k2").toString());
}
diff --git a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
index 484487a14e15278f3dba4958cacaf8ec436a0929..3e3a300383f75a56996cb8e4f8913f55f41b380b 100644
--- a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
+++ b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
@@ -25,30 +25,27 @@ public class TestTypechecker {
Start start = parser.parse(machine, false);
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
- //System.out.println(ast2String2.toString());
- MachineContext c = new MachineContext(null, start, null, null);
+ // System.out.println(ast2String2.toString());
+ MachineContext c = new MachineContext(null, start);
+ c.analyseMachine();
Typechecker t = new Typechecker(c);
for (String name : c.getSetParamter().keySet()) {
- parameters.put(name,
- t.getType(c.getSetParamter().get(name)));
+ parameters.put(name, t.getType(c.getSetParamter().get(name)));
}
-
+
for (String name : c.getScalarParameter().keySet()) {
- parameters.put(name,
- t.getType(c.getScalarParameter().get(name)));
+ parameters.put(name, t.getType(c.getScalarParameter().get(name)));
}
for (String name : c.getConstants().keySet()) {
constants.put(name, t.getType(c.getConstants().get(name)));
}
-
+
for (String name : c.getVariables().keySet()) {
variables.put(name, t.getType(c.getVariables().get(name)));
}
-
}
-
-
+
}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 5c868dc78ce8f6661f1ed52d9e7c12e12ddd2a99..4dca4d68c7b4e97b5f2c97372fd0a731ad0d46c8 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -23,8 +23,7 @@ import de.tlc4b.tlc.TLCResults.TLCResult;
public class TestUtil {
- public static void compare(String expectedModule, String machineString)
- throws Exception {
+ public static void compare(final String expectedModule, final String machineString) throws Exception {
TLC4BGlobals.setForceTLCToEvalConstants(false);
ToolIO.setMode(ToolIO.TOOL);
@@ -35,11 +34,9 @@ public class TestUtil {
// TODO create standard modules BBuildins
String moduleName = b2tlaTranslator.getMachineName();
- String str1 = de.tla2bAst.Translator.translateModuleString(moduleName,
- b2tlaTranslator.getModuleString(), null);
+ String str1 = de.tla2bAst.Translator.translateModuleString(moduleName, b2tlaTranslator.getModuleString(), null);
- String str2 = de.tla2bAst.Translator.translateModuleString(moduleName,
- expectedModule, null);
+ String str2 = de.tla2bAst.Translator.translateModuleString(moduleName, expectedModule, null);
// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, b2tlaTranslator.getModuleString(), null);
// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
@@ -47,26 +44,28 @@ public class TestUtil {
if (!str1.equals(str2)) {
// assertEquals(expected, actual);
- fail("expected:\n" + expectedModule + "\nbut was:\n"
- + b2tlaTranslator.getModuleString());
+ fail("expected:\n" + expectedModule + "\nbut was:\n" + b2tlaTranslator.getModuleString());
}
// assertEquals(sb2.toString(), sb1.toString());
}
- public static String translateTLA2B(String moduleName, String tlaString)
- throws TLA2BException {
- return de.tla2bAst.Translator.translateModuleString(moduleName,
- tlaString, null);
+ public static void tryTranslating(final String machineString) throws BException {
+ TLC4BGlobals.setForceTLCToEvalConstants(false);
+ ToolIO.setMode(ToolIO.TOOL);
+ Translator b2tlaTranslator = new Translator(machineString);
+ b2tlaTranslator.translate();
}
- public static String translateTLA2B(String moduleName, String tlaString,
- String configString) throws TLA2BException {
- return de.tla2bAst.Translator.translateModuleString(moduleName,
- tlaString, configString);
+ public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
+ return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, null);
}
- public static void compareLTLFormula(String expected, String machine,
- String ltlFormula) throws Exception {
+ public static String translateTLA2B(String moduleName, String tlaString, String configString)
+ throws TLA2BException {
+ return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, configString);
+ }
+
+ public static void compareLTLFormula(String expected, String machine, String ltlFormula) throws Exception {
Translator b2tlaTranslator = new Translator(machine, ltlFormula);
b2tlaTranslator.translate();
String translatedLTLFormula = b2tlaTranslator.getTranslatedLTLFormula();
@@ -94,8 +93,8 @@ public class TestUtil {
System.out.println(ast2String2.toString());
}
- public static void compareEqualsConfig(String expectedModule,
- String expectedConfig, String machine) throws Exception {
+ public static void compareEqualsConfig(String expectedModule, String expectedConfig, String machine)
+ throws Exception {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
// print(b2tlaTranslator.getStart());
@@ -105,15 +104,14 @@ public class TestUtil {
String name = b2tlaTranslator.getMachineName();
// parse check
- translateTLA2B(name, b2tlaTranslator.getModuleString(),
- b2tlaTranslator.getConfigString());
+ translateTLA2B(name, b2tlaTranslator.getModuleString(), b2tlaTranslator.getConfigString());
assertEquals(expectedModule, b2tlaTranslator.getModuleString());
assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
}
- public static void compareModuleAndConfig(String expectedModule,
- String expectedConfig, String machine) throws Exception {
+ public static void compareModuleAndConfig(String expectedModule, String expectedConfig, String machine)
+ throws Exception {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
// print(b2tlaTranslator.getStart());
@@ -136,8 +134,7 @@ public class TestUtil {
// }
}
- public static void compareEquals(String expected, String machine)
- throws BException {
+ public static void compareEquals(String expected, String machine) throws BException {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
@@ -152,19 +149,17 @@ public class TestUtil {
}
public static TLCResult testString(String machineString) throws IOException {
- String[] args = new String[] { machineString };
String runnerClassName = TLC4BRunnerTestString.class.getCanonicalName();
-
+ String[] args = new String[] { machineString };
return runTLC(runnerClassName, args);
}
-
+
public static TLCResult test(String[] args) throws IOException {
String runnerClassName = TLC4BTester.class.getCanonicalName();
return runTLC(runnerClassName, args);
}
- private static TLCResult runTLC(String runnerClassName, String[] args)
- throws IOException {
+ private static TLCResult runTLC(String runnerClassName, String[] args) throws IOException {
System.out.println("Starting JVM...");
final Process p = startJVM("", runnerClassName, args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
@@ -192,16 +187,12 @@ public class TestUtil {
}
-
-
- private static Process startJVM(final String optionsAsString,
- final String mainClass, final String[] arguments)
+ private static Process startJVM(final String optionsAsString, final String mainClass, final String[] arguments)
throws IOException {
String separator = System.getProperty("file.separator");
- String jvm = System.getProperty("java.home") + separator + "bin"
- + separator + "java";
+ String jvm = System.getProperty("java.home") + separator + "bin" + separator + "java";
String classpath = System.getProperty("java.class.path");
List<String> command = new ArrayList<String>();
@@ -216,8 +207,7 @@ public class TestUtil {
return process;
}
- public static void testParse(String[] args, boolean deleteFiles)
- throws Exception {
+ public static void testParse(String[] args, boolean deleteFiles) throws Exception {
TLC4BGlobals.resetGlobals();
TLC4BGlobals.setDeleteOnExit(deleteFiles);
TLC4BGlobals.setCreateTraceFile(false);
@@ -231,8 +221,7 @@ public class TestUtil {
System.err.println(e.getMessage());
throw e;
}
- File module = new File(tlc4b.getBuildDir(),
- tlc4b.getMachineFileNameWithoutFileExtension() + ".tla");
+ File module = new File(tlc4b.getBuildDir(), tlc4b.getMachineFileNameWithoutFileExtension() + ".tla");
// parse result
new de.tla2bAst.Translator(module.getCanonicalPath());