diff --git a/.travis.yml b/.travis.yml
index 371f9b2c7916dccf7a4e9a6478e5302cd14b6e83..abe843baddbc5952e76f80cf52d2386c1248bb8d 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 9cad51cb1d135ada6d255a881ff31161fae0e16f..d6daa92230e728a347a790fa50e8b62bb03992b7 100644
--- a/build.gradle
+++ b/build.gradle
@@ -4,25 +4,25 @@ apply plugin: 'maven'
apply plugin: 'jacoco'
apply plugin: 'findbugs'
-project.version = '1.0.3-SNAPSHOT'
+project.version = '1.0.3'
project.group = 'de.hhu.stups'
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 c00d21c0c4c83fd82c817716f76c191009bc3a4f..81125adf95b5bd5e35fab7b4c696b14fe2d56a59 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 9502ab7495bda11a843b5ee3840aa0e76aed7a1c..da8bd947a67919c6f315c29376d46ba93abea9c4 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 102c2c6d1f2530841b90a39f272f783a168a4a00..14ccb839f370d24244113cb31df39615783d8b6e 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 b9f0d82efcc5b1851776095fe5c56c2b409a1561..c09d4a2e31046baf26fa15d0d60d18f838b807bd 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 864e506ee3bdb55cdf626275d8d9806f6c7bcec4..63676ea98bfb86e74f1d208854cd81a9c67e45f1 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 d9919c7acc51fa75bc77012532e28f61783a9e91..9c487ec517380257988a91fe54f865809f350eb7 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) {
@@ -423,6 +423,20 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getRight().apply(this);
}
+ @Override
+ public void caseAIfThenElseExpression(AIfThenElseExpression node) {
+ setType(node.getCondition(), BoolType.getInstance());
+ node.getCondition().apply(this);
+
+ UntypedType x = new UntypedType();
+ setType(node.getThen(), x);
+ setType(node.getElse(), x);
+ node.getThen().apply(this);
+ node.getElse().apply(this);
+ BType found = getType(node.getThen());
+ unify(getType(node), found, node);
+ }
+
@Override
public void caseANotEqualPredicate(ANotEqualPredicate node) {
try {
@@ -2246,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);
@@ -2261,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);
@@ -2289,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 38fb4969b12ec1767b1a9f59770cddde2821aefb..3456f2e9dd0a80896419b07d5f3ac65db0a2b1c4 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 c90ba2108061750fc300fe64a73ca63a47401cb4..fb46a533605db50d523fd85450eef4f3553e5df3 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 7424d4605840cfa845982e802a31adf47266278d..5dd60e094f33b63e4f87e58a462eb0dfb28981a4 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 aecdcbb166eed4af5d196ab6c0dabffc5ac65b99..80a65e7fbf35f130b9457c41e6ac02ddfeb3bf09 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 4ce9715c29df46688d92a230dd709ca04718c974..56108205d108030724fdf4a2627ea2fe2f43913e 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 8791cb0f10074e827712512142cc03fe8457a661..9504f362b72e2e4dd502e204e15721b1dafeb9e3 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);
}
@@ -1196,6 +1196,17 @@ public class TLAPrinter extends DepthFirstAdapter {
node.getRight().apply(this);
outANotEqualPredicate(node);
}
+
+ @Override
+ public void caseAIfThenElseExpression(AIfThenElseExpression node) {
+ moduleStringAppend("(IF ");
+ node.getCondition().apply(this);
+ moduleStringAppend(" THEN ");
+ node.getThen().apply(this);
+ moduleStringAppend(" ELSE ");
+ node.getElse().apply(this);
+ moduleStringAppend(")");
+ }
@Override
public void caseAConjunctPredicate(AConjunctPredicate node) {
@@ -1867,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/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index 80bbdddcafb5edc70bee8fb374e65a0380b4d3f7..dbef5ec399014c2883028b4f6794af486217378c 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -70,7 +70,7 @@ public class Generator extends DepthFirstAdapter {
evalMachineSets();
evalDefinitions();
evalConstants();
-
+
evalInvariant();
evalOperations();
evalGoal();
@@ -143,13 +143,12 @@ public class Generator extends DepthFirstAdapter {
Node value = idValueTable.get(param);
if (value != null) {
- tlaModule.tlaDefinitions.add(new TLADefinition(param, value));
+ tlaModule.addTLADefinition(new TLADefinition(param, value));
continue;
}
Integer intValue = constantsEvaluator.getIntValue(param);
if (intValue != null) {
- tlaModule.tlaDefinitions
- .add(new TLADefinition(param, intValue));
+ tlaModule.addTLADefinition(new TLADefinition(param, intValue));
continue;
}
@@ -205,7 +204,7 @@ public class Generator extends DepthFirstAdapter {
Node n = itr2.next();
AEnumeratedSetSet e = (AEnumeratedSetSet) n;
TLADefinition def = new TLADefinition(e, e);
- this.tlaModule.tlaDefinitions.add(def);
+ this.tlaModule.addTLADefinition(def);
List<PExpression> copy = new ArrayList<PExpression>(e.getElements());
for (PExpression element : copy) {
this.tlaModule.constants.add(element);
diff --git a/src/main/java/de/tlc4b/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
index d373d37c99b9e9a37afb1e0b5cdb3ca9f4d5ee46..2135d0cabf3a506bac5888539a90c40cf2fdedd0 100644
--- a/src/main/java/de/tlc4b/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -9,14 +9,14 @@ public class TLAModule {
protected String moduleName;
- protected final ArrayList<TLADefinition> tlaDefinitions;
+ private final ArrayList<TLADefinition> tlaDefinitions;
protected final ArrayList<Node> constants;
protected final ArrayList<Node> assumes;
protected final ArrayList<Node> variables;
protected final ArrayList<Node> invariants;
private final ArrayList<Node> initPredicates;
protected final ArrayList<POperation> operations;
- private ArrayList<PDefinition> bDefinitions;
+ private ArrayList<PDefinition> bDefinitions;
private final ArrayList<Node> assertions;
protected ArrayList<PDefinition> allDefinitions;
@@ -110,4 +110,7 @@ public class TLAModule {
return this.initPredicates.size() > 0;
}
+ public void addTLADefinition(TLADefinition defintion) {
+ this.tlaDefinitions.add(defintion);
+ }
}
diff --git a/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java b/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..399fb6ecc37af9207a0c52eaab751fccf1cb5666
--- /dev/null
+++ b/src/test/java/de/tlc4b/prettyprint/SyntaxExtensionsTest.java
@@ -0,0 +1,20 @@
+package de.tlc4b.prettyprint;
+
+import static de.tlc4b.util.TestUtil.compare;
+
+import org.junit.Test;
+
+
+public class SyntaxExtensionsTest {
+
+ @Test
+ public void testIfThenElseg() throws Exception {
+ String machine = "MACHINE test\n"
+ + "PROPERTIES 1 = (IF 1=1 THEN 1 ELSE 2 END) \n" + "END";
+
+ String expected = "---- MODULE test----\n"
+ + "ASSUME 1 = (IF 1 = 1 THEN 1 ELSE 2) \n"
+ + "======";
+ compare(expected, machine);
+ }
+}
diff --git a/src/test/java/de/tlc4b/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
index 3e3a300383f75a56996cb8e4f8913f55f41b380b..d26e7ccd1d03a9eef76ab2e64a75f593ec583f29 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 4dca4d68c7b4e97b5f2c97372fd0a731ad0d46c8..7fc8d56af27894e54968f8a95cf2f088495f0e45 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 {