From ed6f7312982e79b33339c9e986fe590d157187c0 Mon Sep 17 00:00:00 2001
From: dohan <dohan001@hhu.de>
Date: Fri, 31 Aug 2018 15:25:13 +0200
Subject: [PATCH] adapt to new parser version
---
.travis.yml | 1 +
build.gradle | 14 ++++----
src/main/java/de/tlc4b/TLC4B.java | 6 ++--
src/main/java/de/tlc4b/Translator.java | 12 +++----
.../de/tlc4b/analysis/MachineContext.java | 34 +++++++++---------
.../de/tlc4b/analysis/PrimedNodesMarker.java | 4 +--
src/main/java/de/tlc4b/analysis/Renamer.java | 4 +--
.../java/de/tlc4b/analysis/Typechecker.java | 16 ++++-----
.../transformation/DefinitionsEliminator.java | 10 +++---
.../transformation/SeesEliminator.java | 4 +--
.../SetComprehensionOptimizer.java | 12 +++----
.../typerestriction/TypeRestrictor.java | 4 +--
.../java/de/tlc4b/ltl/LTLFormulaVisitor.java | 4 +--
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 10 +++---
.../tlc4b/typechecking/TestTypechecker.java | 8 ++++-
src/test/java/de/tlc4b/util/TestUtil.java | 36 +++++++++++++------
16 files changed, 101 insertions(+), 78 deletions(-)
diff --git a/.travis.yml b/.travis.yml
index 371f9b2..abe843b 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,4 +1,5 @@
language: java
+sudo: true
script: gradle build
before_install:
- openssl aes-256-cbc -pass pass:$ENCRYPTION_PASSWORD -in secring.gpg.enc -out secring.gpg
diff --git a/build.gradle b/build.gradle
index 9cad51c..8740a40 100644
--- a/build.gradle
+++ b/build.gradle
@@ -11,18 +11,18 @@ project.sourceCompatibility = '1.7'
project.targetCompatibility = '1.7'
repositories {
- mavenCentral()
- maven {
- name "sonatype snapshots"
- url "https://oss.sonatype.org/content/repositories/snapshots"
- }
+ mavenCentral()
+ maven {
+ name "sonatype snapshots"
+ url "https://oss.sonatype.org/content/repositories/snapshots"
+ }
}
configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
-def parser_version = '2.5.1'
+def parser_version = '2.9.12'
def tlatools_version = '1.0.2'
dependencies {
@@ -38,7 +38,7 @@ 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.12')
- testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.0.8')
+ testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.1.0')
}
jacoco {
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index c00d21c..81125ad 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -13,7 +13,7 @@ import java.io.UnsupportedEncodingException;
import java.util.LinkedHashMap;
import java.util.Map.Entry;
-import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
import de.tlc4b.exceptions.TLC4BIOException;
@@ -49,7 +49,7 @@ public class TLC4B {
TLC4B tlc4b = new TLC4B();
try {
tlc4b.process(args);
- } catch (BException e) {
+ } catch (BCompoundException e) {
printlnErr("***** Parsing Error *****");
printlnErr(e.getMessage());
return;
@@ -337,7 +337,7 @@ public class TLC4B {
}
}
- public void process(String[] args) throws IOException, BException {
+ public void process(String[] args) throws IOException, BCompoundException {
MP.print("Arguments: ");
for (int i = 0; i < args.length; i++) {
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 9502ab7..da8bd94 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -7,7 +7,7 @@ import java.util.Map;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
-import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
@@ -48,7 +48,7 @@ public class Translator {
private TLCOutputInfo tlcOutputInfo;
private String translatedLTLFormula;
- public Translator(String machineString) throws BException {
+ public Translator(String machineString) throws BCompoundException {
this.machineString = machineString;
BParser parser = new BParser("Testing");
start = parser.parse(machineString, false);
@@ -57,7 +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 BCompoundException {
this.machineString = machineString;
this.ltlFormula = ltlFormula;
BParser parser = new BParser("Testing");
@@ -68,7 +68,7 @@ public class Translator {
}
public Translator(String machineName, File machineFile, String ltlFormula, String constantSetup)
- throws BException, IOException {
+ throws BCompoundException, IOException {
this.machineName = machineName;
this.ltlFormula = ltlFormula;
@@ -83,7 +83,7 @@ public class Translator {
// machine
final RecursiveMachineLoader rml = new RecursiveMachineLoader(machineFile.getParent(),
parser.getContentProvider());
- rml.loadAllMachines(machineFile, start, parser.getSourcePositions(), parser.getDefinitions());
+ rml.loadAllMachines(machineFile, start, parser.getDefinitions());
parsedMachines = rml.getParsedMachines();
@@ -92,7 +92,7 @@ public class Translator {
Start start2 = null;
try {
start2 = con.parse("#FORMULA " + constantSetup, false);
- } catch (BException e) {
+ } catch (BCompoundException e) {
System.err.println("An error occured while parsing the constants setup predicate.");
throw e;
}
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 102c2c6..14ccb83 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -9,7 +9,6 @@ import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
@@ -64,6 +63,7 @@ import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.be4.classicalb.core.parser.util.Utils;
import de.tlc4b.MP;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.transformation.DefinitionsSorter;
@@ -197,7 +197,7 @@ public class MachineContext extends DepthFirstAdapter {
}
private void exist(LinkedList<TIdentifierLiteral> list) {
- String name = Utils.getIdentifierAsString(list);
+ String name = Utils.getTIdentifierListAsString(list);
identifierAlreadyExists(name);
}
@@ -235,13 +235,13 @@ public class MachineContext extends DepthFirstAdapter {
this.header = node;
if (machineName == null) {
List<TIdentifierLiteral> nameList = new ArrayList<TIdentifierLiteral>(node.getName());
- this.machineName = Utils.getIdentifierAsString(nameList);
+ this.machineName = Utils.getTIdentifierListAsString(nameList);
}
List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(p.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(p.getIdentifier());
exist(p.getIdentifier());
if (Character.isUpperCase(name.charAt(0))) {
this.machineSetParameter.put(name, p);
@@ -386,7 +386,7 @@ public class MachineContext extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<PExpression>(node.getMachineNames());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(p.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(p.getIdentifier());
try {
exist(p.getIdentifier());
@@ -409,7 +409,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseADeferredSetSet(ADeferredSetSet node) {
List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
- String name = Utils.getIdentifierAsString(copy);
+ String name = Utils.getTIdentifierListAsString(copy);
exist(node.getIdentifier());
deferredSets.put(name, node);
}
@@ -418,14 +418,14 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
{
List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
- String name = Utils.getIdentifierAsString(copy);
+ String name = Utils.getTIdentifierListAsString(copy);
exist(node.getIdentifier());
enumeratedSets.put(name, node);
}
List<PExpression> copy = new ArrayList<PExpression>(node.getElements());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(v.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(v.getIdentifier());
exist(v.getIdentifier());
enumValues.put(name, v);
}
@@ -437,7 +437,7 @@ public class MachineContext extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression c = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(c.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(c.getIdentifier());
exist(c.getIdentifier());
constants.put(name, c);
}
@@ -449,7 +449,7 @@ public class MachineContext extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression c = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(c.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(c.getIdentifier());
exist(c.getIdentifier());
constants.put(name, c);
}
@@ -460,7 +460,7 @@ public class MachineContext extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(v.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(v.getIdentifier());
exist(v.getIdentifier());
variables.put(name, v);
}
@@ -471,14 +471,14 @@ public class MachineContext extends DepthFirstAdapter {
List<PExpression> copy = new ArrayList<PExpression>(node.getIdentifiers());
for (PExpression e : copy) {
AIdentifierExpression v = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(v.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(v.getIdentifier());
exist(v.getIdentifier());
variables.put(name, v);
}
}
private void putLocalVariableIntoCurrentScope(AIdentifierExpression node) throws ScopeException {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
LinkedHashMap<String, Node> currentScope = contextTable.get(contextTable.size() - 1);
if (currentScope.containsKey(name)) {
throw new ScopeException("Duplicate Identifier: " + name);
@@ -489,7 +489,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
for (int i = contextTable.size() - 1; i >= 0; i--) {
LinkedHashMap<String, Node> currentScope = contextTable.get(i);
if (currentScope.containsKey(name)) {
@@ -502,7 +502,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPrimedIdentifierExpression(APrimedIdentifierExpression node) {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
for (int i = contextTable.size() - 1; i >= 0; i--) {
LinkedHashMap<String, Node> currentScope = contextTable.get(i);
if (currentScope.containsKey(name)) {
@@ -643,7 +643,7 @@ public class MachineContext extends DepthFirstAdapter {
// first collect all operations
for (POperation e : copy) {
AOperation op = (AOperation) e;
- String name = Utils.getIdentifierAsString(op.getOpName());
+ String name = Utils.getTIdentifierListAsString(op.getOpName());
// existString(name);
if (operations.keySet().contains(name)) {
throw new ScopeException(String.format("Duplicate operation: '%s'", name));
@@ -740,7 +740,7 @@ public class MachineContext extends DepthFirstAdapter {
public void caseAOpSubstitution(AOpSubstitution node) {
if (node.getName() != null) {
AIdentifierExpression op = (AIdentifierExpression) node.getName();
- String name = Utils.getIdentifierAsString(op.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(op.getIdentifier());
Node o = operations.get(name);
if (o != null) {
this.referencesTable.put(op, o);
diff --git a/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
index b9f0d82..c09d4a2 100644
--- a/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
+++ b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
@@ -14,6 +13,7 @@ import de.be4.classicalb.core.parser.node.APrimedIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.POperation;
+import de.be4.classicalb.core.parser.util.Utils;
import de.tlc4b.exceptions.ScopeException;
public class PrimedNodesMarker extends DepthFirstAdapter {
@@ -97,7 +97,7 @@ public class PrimedNodesMarker extends DepthFirstAdapter {
return;
}
}
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
throw new ScopeException("Unkown identifier: '"+name+"$0'");
}
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index 864e506..63676ea 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -8,7 +8,6 @@ import java.util.List;
import java.util.Set;
import java.util.Map.Entry;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
@@ -30,6 +29,7 @@ import de.be4.classicalb.core.parser.node.AVarSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.util.Utils;
public class Renamer extends DepthFirstAdapter {
private final MachineContext machineContext;
@@ -216,7 +216,7 @@ public class Renamer extends DepthFirstAdapter {
private String renameIdentifier(Node node) {
AIdentifierExpression id = (AIdentifierExpression) node;
- String name = Utils.getIdentifierAsString(id.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(id.getIdentifier());
String newName = incName(name);
namesTable.put(id, newName);
return newName;
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 787a25f..9c487ec 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -8,9 +8,9 @@ import java.util.LinkedList;
import java.util.List;
import java.util.Map.Entry;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
+import de.be4.classicalb.core.parser.util.Utils;
import de.tlc4b.btypes.AbstractHasFollowers;
import de.tlc4b.btypes.BType;
import de.tlc4b.btypes.BoolType;
@@ -135,7 +135,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
List<PExpression> copy = new ArrayList<PExpression>(node.getParameters());
for (PExpression e : copy) {
AIdentifierExpression p = (AIdentifierExpression) e;
- String name = Utils.getIdentifierAsString(p.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(p.getIdentifier());
if (Character.isUpperCase(name.charAt(0))) {
@@ -160,7 +160,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseAEnumeratedSetSet(AEnumeratedSetSet node) {
List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
- String setName = Utils.getIdentifierAsString(copy);
+ String setName = Utils.getTIdentifierListAsString(copy);
SetType set = new SetType(new EnumeratedSetElement(setName));
setType(node, set);
List<PExpression> copy2 = new ArrayList<PExpression>(node.getElements());
@@ -172,7 +172,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
@Override
public void caseADeferredSetSet(ADeferredSetSet node) {
List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(node.getIdentifier());
- String name = Utils.getIdentifierAsString(copy);
+ String name = Utils.getTIdentifierListAsString(copy);
setType(node, new SetType(new EnumeratedSetElement(name)));
}
@@ -399,7 +399,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
Node identifierDeclarationNode = referenceTable.get(node);
BType found = getType(identifierDeclarationNode);
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
try {
expected.unify(found, this);
} catch (UnificationException e) {
@@ -2260,7 +2260,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
e.getValue().apply(this);
AIdentifierExpression i = (AIdentifierExpression) e.getIdentifier();
- String name = Utils.getIdentifierAsString(i.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(i.getIdentifier());
found.add(name, getType(e.getValue()));
}
BType expected = getType(node);
@@ -2275,7 +2275,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseARecordFieldExpression(ARecordFieldExpression node) {
StructType s = new StructType();
AIdentifierExpression i = (AIdentifierExpression) node.getIdentifier();
- String fieldName = Utils.getIdentifierAsString(i.getIdentifier());
+ String fieldName = Utils.getTIdentifierListAsString(i.getIdentifier());
s.add(fieldName, new UntypedType());
setType(node.getRecord(), s);
@@ -2303,7 +2303,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
e.getValue().apply(this);
AIdentifierExpression i = (AIdentifierExpression) e.getIdentifier();
- String name = Utils.getIdentifierAsString(i.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(i.getIdentifier());
BType t = ((SetType) getType(e.getValue())).getSubtype();
s.add(name, t);
}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index 38fb496..3456f2e 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -4,7 +4,6 @@ import java.util.ArrayList;
import java.util.Hashtable;
import java.util.List;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
@@ -20,6 +19,7 @@ import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PMachineClause;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.Utils;
import de.tlc4b.analysis.StandardMadules;
/**
@@ -136,7 +136,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
for (int i = 0; i < clone.getParameters().size(); i++) {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
- String paramName = Utils.getIdentifierAsString(p.getIdentifier());
+ String paramName = Utils.getTIdentifierListAsString(p.getIdentifier());
Node arg = arguments.get(i);
arg.apply(this);
@@ -168,7 +168,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
for (int i = 0; i < clone.getParameters().size(); i++) {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
- String paramName = Utils.getIdentifierAsString(p.getIdentifier());
+ String paramName = Utils.getTIdentifierListAsString(p.getIdentifier());
Node arg = arguments.get(i);
arg.apply(this);
context.put(paramName, node.getParameters().get(i));
@@ -200,7 +200,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
for (int i = 0; i < clone.getParameters().size(); i++) {
AIdentifierExpression p = (AIdentifierExpression) clone
.getParameters().get(i);
- String paramName = Utils.getIdentifierAsString(p.getIdentifier());
+ String paramName = Utils.getTIdentifierListAsString(p.getIdentifier());
Node arg = arguments.get(i);
arg.apply(this);
@@ -218,7 +218,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
public void caseAIdentifierExpression(AIdentifierExpression node) {
if (contextStack.size() == 0)
return;
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
for (int i = contextStack.size() - 1; i >= 0; i--) {
Hashtable<String, PExpression> context = contextStack.get(i);
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
index c90ba21..fb46a53 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
@@ -6,7 +6,6 @@ import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.Map;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractConstantsMachineClause;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
@@ -23,6 +22,7 @@ import de.be4.classicalb.core.parser.node.PMachineClause;
import de.be4.classicalb.core.parser.node.PParseUnit;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.Utils;
import de.tlc4b.TLC4BGlobals;
public class SeesEliminator extends DepthFirstAdapter {
@@ -56,7 +56,7 @@ public class SeesEliminator extends DepthFirstAdapter {
for (PExpression pExpression : machineNames) {
AIdentifierExpression id = (AIdentifierExpression) pExpression;
String machineName = Utils
- .getIdentifierAsString(id.getIdentifier());
+ .getTIdentifierListAsString(id.getIdentifier());
if (!resolvedMachines.contains(machineName)) {
resolvedMachines.add(machineName);
Start start = parsedMachines.get(machineName);
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
index 7424d46..5dd60e0 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SetComprehensionOptimizer.java
@@ -6,7 +6,6 @@ import java.util.Hashtable;
import java.util.LinkedList;
import java.util.Set;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
@@ -20,6 +19,7 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.Utils;
/*
* This class performs an AST transformation on set comprehension nodes. For
@@ -49,7 +49,7 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
for (int i = 0; i < identifiers.size(); i++) {
AIdentifierExpression id = (AIdentifierExpression) identifiers
.get(i);
- String name = Utils.getIdentifierAsString(id.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(id.getIdentifier());
list.add(name);
identifierTable.put(name, id);
}
@@ -189,7 +189,7 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
if (equal.getLeft() instanceof AIdentifierExpression) {
AIdentifierExpression id = (AIdentifierExpression) equal
.getLeft();
- String name = Utils.getIdentifierAsString(id.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(id.getIdentifier());
Set<String> names = new HashSet<String>(values.keySet());
names.add(name);
if (list.contains(name)
@@ -202,7 +202,7 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
&& equal.getRight() instanceof AIdentifierExpression) {
AIdentifierExpression id = (AIdentifierExpression) equal
.getRight();
- String name = Utils.getIdentifierAsString(id.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(id.getIdentifier());
Set<String> names = new HashSet<String>(values.keySet());
names.add(name);
if (list.contains(name)
@@ -227,7 +227,7 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
if (names.contains(name)) {
hasDependency = true;
}
@@ -288,7 +288,7 @@ public class SetComprehensionOptimizer extends DepthFirstAdapter {
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- String name = Utils.getIdentifierAsString(node.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(node.getIdentifier());
// todo the name is not a unique of the node
PExpression value = values.get(name);
if (value != null) {
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index aecdcbb..80a65e7 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -7,7 +7,6 @@ import java.util.Hashtable;
import java.util.List;
import java.util.Set;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
@@ -44,6 +43,7 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
+import de.be4.classicalb.core.parser.util.Utils;
import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AForallLtl;
import de.tlc4b.TLC4BGlobals;
@@ -572,7 +572,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
&& !(e.parent() instanceof ALambdaExpression)
&& !(e.parent() instanceof AComprehensionSetExpression)) {
AIdentifierExpression id = (AIdentifierExpression) e;
- String localVariableName = Utils.getIdentifierAsString(id
+ String localVariableName = Utils.getTIdentifierListAsString(id
.getIdentifier());
throw new NotSupportedException(
"Unable to restrict the type '"
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index 4ce9715..5610820 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -10,7 +10,7 @@ import java.util.LinkedHashMap;
import java.util.List;
import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AStringExpression;
@@ -155,7 +155,7 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
de.be4.classicalb.core.parser.node.Start start = null;
try {
start = parser.parse(bPredicate, false);
- } catch (BException e) {
+ } catch (BCompoundException e) {
throw new LTLParseException(e.getMessage());
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 55687a6..9504f36 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -7,9 +7,9 @@ import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
-import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
+import de.be4.classicalb.core.parser.util.Utils;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.PrecedenceCollector;
@@ -717,7 +717,7 @@ public class TLAPrinter extends DepthFirstAdapter {
private void printNormalAssignment(PExpression left, PExpression right) {
AIdentifierExpression id = (AIdentifierExpression) left;
- String name = Utils.getIdentifierAsString(id.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(id.getIdentifier());
if (!machineContext.getVariables().containsKey(name)) {
moduleStringAppend("TRUE");
} else {
@@ -1138,7 +1138,7 @@ public class TLAPrinter extends DepthFirstAdapter {
inAIdentifierExpression(node);
String name = renamer.getNameOfRef(node);
if (name == null) {
- name = Utils.getIdentifierAsString(node.getIdentifier());
+ name = Utils.getTIdentifierListAsString(node.getIdentifier());
}
if (StandardMadules.isAbstractConstant(name)) {
// in order to pass the member check
@@ -1156,7 +1156,7 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAPrimedIdentifierExpression(APrimedIdentifierExpression node) {
String name = renamer.getNameOfRef(node);
if (name == null) {
- name = Utils.getIdentifierAsString(node.getIdentifier());
+ name = Utils.getTIdentifierListAsString(node.getIdentifier());
}
moduleStringAppend(name);
}
@@ -1878,7 +1878,7 @@ public class TLAPrinter extends DepthFirstAdapter {
if (node.getIdentifier() instanceof AIdentifierExpression) {
AIdentifierExpression id = (AIdentifierExpression) node
.getIdentifier();
- String name = Utils.getIdentifierAsString(id.getIdentifier());
+ String name = Utils.getTIdentifierListAsString(id.getIdentifier());
if (StandardMadules.isAbstractConstant(name)) {
moduleStringAppend(name);
diff --git a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
index 3e3a300..d26e7cc 100644
--- a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
+++ b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
@@ -3,6 +3,7 @@ package de.tlc4b.typechecking;
import java.util.Hashtable;
import de.be4.classicalb.core.parser.BParser;
+import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
import de.tlc4b.analysis.MachineContext;
@@ -22,7 +23,12 @@ public class TestTypechecker {
variables = new Hashtable<String, BType>();
BParser parser = new BParser("Test");
- Start start = parser.parse(machine, false);
+ Start start;
+ try {
+ start = parser.parse(machine, false);
+ } catch (BCompoundException e) {
+ throw e.getFirstException();
+ }
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
// System.out.println(ast2String2.toString());
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 4dca4d6..7fc8d56 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -13,6 +13,7 @@ import java.util.Arrays;
import java.util.List;
import util.ToolIO;
+import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.exceptions.TLA2BException;
@@ -52,8 +53,14 @@ public class TestUtil {
public static void tryTranslating(final String machineString) throws BException {
TLC4BGlobals.setForceTLCToEvalConstants(false);
ToolIO.setMode(ToolIO.TOOL);
- Translator b2tlaTranslator = new Translator(machineString);
- b2tlaTranslator.translate();
+ Translator b2tlaTranslator;
+ try {
+ b2tlaTranslator = new Translator(machineString);
+ b2tlaTranslator.translate();
+ } catch (BCompoundException e) {
+ throw e.getFirstException();
+ }
+
}
public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
@@ -135,17 +142,26 @@ public class TestUtil {
}
public static void compareEquals(String expected, String machine) throws BException {
- Translator b2tlaTranslator = new Translator(machine);
- b2tlaTranslator.translate();
- System.out.println(b2tlaTranslator.getModuleString());
- assertEquals(expected, b2tlaTranslator.getModuleString());
+ try {
+ Translator b2tlaTranslator = new Translator(machine);
+ b2tlaTranslator.translate();
+ System.out.println(b2tlaTranslator.getModuleString());
+ assertEquals(expected, b2tlaTranslator.getModuleString());
+ } catch (BCompoundException e) {
+ throw e.getFirstException();
+ }
+
}
public static String translate(String machine) throws BException {
- Translator translator = new Translator(machine);
- translator.translate();
- System.out.println(translator.getModuleString());
- return translator.getModuleString();
+ try {
+ Translator translator = new Translator(machine);
+ translator.translate();
+ System.out.println(translator.getModuleString());
+ return translator.getModuleString();
+ } catch (BCompoundException e) {
+ throw e.getFirstException();
+ }
}
public static TLCResult testString(String machineString) throws IOException {
--
GitLab