diff --git a/build.gradle b/build.gradle
index 2cae3e19114134948d7350013fdbcf128102e6e4..5dde9842c5760062dea1fa0f95d40de6b83b1c67 100644
--- a/build.gradle
+++ b/build.gradle
@@ -18,10 +18,6 @@ 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 {
@@ -29,17 +25,20 @@ configurations.all {
}
def parser_version = '2.5.0-SNAPSHOT'
+def prob_version = '2.0.0-SNAPSHOT'
def tlatools_version = '1.0.2-SNAPSHOT'
dependencies {
+
+ compile 'commons-cli:commons-cli:1.2'
compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
compile (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
compile (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
- //compile(group: 'de.prob', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
+ testCompile (group: 'de.hhu.stups', name: 'de.prob2.kernel', version: prob_version)
testCompile (group: 'junit', name: 'junit', version: '4.+')
}
diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index f411cf0caafa3ffa6c5457f6a07d75c9e8635e29..0529bdfa91a2c957627d453491d099cba6233a05 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -4,6 +4,13 @@
package de.tla2b;
+import org.apache.commons.cli.CommandLine;
+import org.apache.commons.cli.HelpFormatter;
+import org.apache.commons.cli.Option;
+import org.apache.commons.cli.OptionBuilder;
+import org.apache.commons.cli.Options;
+import org.apache.commons.cli.ParseException;
+import org.apache.commons.cli.PosixParser;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.NotImplementedException;
@@ -11,7 +18,11 @@ import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2bAst.Translator;
+
+
public class TLA2B implements TranslationGlobals {
+ public final static String VERSION = "version";
+
private String mainFile;
private static boolean error = false;
@@ -21,27 +32,33 @@ public class TLA2B implements TranslationGlobals {
}
public void handleParameter(String[] args) {
- int i;
- for (i = 0; (i < args.length) && (args[i].charAt(0) == '-'); i++) {
- if (args[i].equals("-version")) {
- System.out.println("TLA2B version " + VERSION);
+ PosixParser parser = new PosixParser();
+ Options options = getCommandlineOptions();
+ try {
+ CommandLine line = parser.parse(options, args);
+ String[] remainingArgs = line.getArgs();
+ if (remainingArgs.length != 1) {
+ System.err.println("Error: expected a module file.");
System.exit(-1);
} else {
- System.err.println("Illegal switch: " + args[i]);
- System.exit(-1);
+ mainFile = remainingArgs[0];
}
- }
-
- if (i == args.length) {
- System.err.println("Error: expected a module file.");
+ if (line.hasOption(VERSION)) {
+ System.out.println("TLA2B version: " + VERSION_NUMBER);
+ }
+ } catch (ParseException e) {
+ System.out.println(e.getMessage());
+ HelpFormatter formatter = new HelpFormatter();
+ formatter.printHelp("java -jar TLA2B.jar [file]", options);
System.exit(-1);
}
- mainFile = args[i];
+
}
public static void main(String[] args) {
// To indicate an error we use the exit code -1
TLA2B tla2b = new TLA2B();
+
tla2b.handleParameter(args);
Translator translator = null;
@@ -60,11 +77,25 @@ public class TLA2B implements TranslationGlobals {
} catch (TLA2BException e) {
System.err.print("**** Translation Error ****\n");
System.err.println(e.getMessage());
+ //e.printStackTrace();
System.exit(-1);
}
translator.createMachineFile();
translator.createProbFile();
}
-
+ @SuppressWarnings("static-access")
+ private static Options getCommandlineOptions() {
+ Options options = new Options();
+ options.addOption(VERSION, false, "prints the current version of TLA2B");
+
+ Option config = OptionBuilder
+ .withArgName("file")
+ .hasArg()
+ .withDescription(
+ "config file")
+ .create("config");
+ options.addOption(config);
+ return options;
+ }
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 7e1a3ab923cfb961b38cc5d5969c86adf895ac33..9412c11c26c1772461b7e0dc34466b0285928d9a 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -258,7 +258,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
for (OpDefNode def : set) {
if (def.getInRecursive()) {
throw new NotImplementedException(
- "Recursive definitions are currently not supported.");
+ "Recursive definitions are currently not supported: " + def.getName() + "\n" + def.getLocation() );
// bDefinitionsSet.remove(def);
// RecursiveDefinition rd = new RecursiveDefinition(def);
// recursiveDefinitions.add(rd);
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index fed156c6418ec9a4e50fdfe34bbc8ac97c12b228..af5d946f4998a5efa975fe3b9014bfac8c274a0e 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -11,7 +11,6 @@ import java.util.Set;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
-
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.FormalParamNode;
@@ -238,8 +237,12 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
if (BBuiltInOPs.contains(def.getName())) {
break;
}
-
- usedNamesTable.get(def).addAll(usedNames);
+ Set<String> set = usedNamesTable.get(def);
+ if (set!=null){
+ usedNamesTable.get(def).addAll(usedNames);
+ }
+
+
for (int i = 0; i < n.getChildren().length; i++) {
visitNode(opApplNode.getArgs()[i], usedNames);
}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 0132e66c6cd2a9cfe732f3a4c4333cf84d46d078..c742b5f730e33c0075587e9f0cb101cbf7b0ccf8 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -436,7 +436,8 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
if (t == null) {
- throw new RuntimeException();
+ t = new UntypedType(); // TODO is this correct?
+ //throw new RuntimeException();
}
try {
TLAType result = expected.unify(t);
@@ -473,6 +474,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
try {
found = found.unify(expected);
} catch (UnificationException e) {
+ e.printStackTrace();
throw new TypeErrorException(String.format(
"Expected %s, found %s at definition '%s',%n%s",
expected, found, def.getName(), n.getLocation()));
@@ -796,7 +798,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
try {
- found = found.unify(expected);
+ found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException("Expected '" + expected
+ "', found '" + found + "'.\n" + n.getLocation());
@@ -805,7 +807,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
TLAType t = null;
try {
t = (TLAType) recFunc.getToolObject(TYPE_ID);
- found = found.unify(t);
+ found = (FunctionType) found.unify(t);
} catch (UnificationException e) {
throw new TypeErrorException("Expected '" + expected
+ "', found '" + t + "'.\n" + n.getLocation());
@@ -822,7 +824,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
visitExprOrOpArgNode(n.getArgs()[0], found.getRange());
try {
- found = found.unify(expected);
+ found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException("Expected '" + expected
+ "', found '" + found + "'.\n" + n.getLocation());
@@ -884,6 +886,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
} catch (UnificationException e) {
throw new TypeErrorException("Expected '" + expected
+ "', found '" + found + "'.\n"
+ + n.getArgs()[0].toString(2) + "\n"
+ n.getLocation());
}
return found;
@@ -1148,7 +1151,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
FunctionType expected = new FunctionType(
IntType.getInstance(), new UntypedType());
try {
- expected = expected.unify(subType);
+ expected = (FunctionType) expected.unify(subType);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
"Expected %s, found %s at parameter %s,%n%s",
@@ -1475,10 +1478,10 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
case B_OPCODE_conc: { // s \o s2 - concatenation of s and s2
- FunctionType found = new FunctionType(IntType.getInstance(),
+ TLAType found = new FunctionType(IntType.getInstance(),
new UntypedType());
- found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
- found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[1], found);
+ found = visitExprOrOpArgNode(n.getArgs()[0], found);
+ found = visitExprOrOpArgNode(n.getArgs()[1], found);
try {
found = found.unify(expected);
} catch (UnificationException e) {
@@ -1496,7 +1499,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
visitExprOrOpArgNode(n.getArgs()[1], found.getRange());
try {
- found = found.unify(expected);
+ found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
"Expected %s, found %s at 'Append',%n%s", expected,
@@ -1526,7 +1529,7 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
new UntypedType());
found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
try {
- found = found.unify(expected);
+ found = (FunctionType) found.unify(expected);
} catch (UnificationException e) {
throw new TypeErrorException(String.format(
"Expected %s, found %s at 'Tail',%n%s", expected,
@@ -1536,9 +1539,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
case B_OPCODE_subseq: { // SubSeq(s,m,n)
- FunctionType found = new FunctionType(IntType.getInstance(),
+ TLAType found = new FunctionType(IntType.getInstance(),
new UntypedType());
- found = (FunctionType) visitExprOrOpArgNode(n.getArgs()[0], found);
+ found = visitExprOrOpArgNode(n.getArgs()[0], found);
visitExprOrOpArgNode(n.getArgs()[1], IntType.getInstance());
visitExprOrOpArgNode(n.getArgs()[2], IntType.getInstance());
try {
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index d0af064ae1466a0ef2668130d4de6f28d18e96b9..6fa75ccdccf48dae3b5669b37d1aa501274dcd95 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -10,7 +10,7 @@ import java.util.Arrays;
import tla2sany.semantic.FrontEnd;
public interface TranslationGlobals {
- final String VERSION = "1.0.7";
+ final String VERSION_NUMBER = "1.0.7";
final int TLCValueKind = 100;
diff --git a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
index 1358de3c48c979b14b628cf803756bfd9094d7f5..5a1af43594584608ad23769f8a5e8d10b6ec7c18 100644
--- a/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
+++ b/src/main/java/de/tla2b/output/ASTPrettyPrinter.java
@@ -8,7 +8,6 @@ import java.util.List;
import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
-import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.ADefinitionExpression;
diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
index 1010fa8370632d3f117c7a80ddc703ec307c5cf7..9a2d280175c06ed72cc82aea6da074d4f4cb5afd 100644
--- a/src/main/java/de/tla2b/output/PrologPrinter.java
+++ b/src/main/java/de/tla2b/output/PrologPrinter.java
@@ -4,7 +4,6 @@ import java.io.File;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.ArrayList;
-import java.util.HashMap;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
@@ -16,7 +15,6 @@ import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.hhu.stups.sablecc.patch.PositionedNode;
-import de.hhu.stups.sablecc.patch.SourcePositions;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.PrologTermOutput;
import de.tla2b.types.TLAType;
diff --git a/src/main/java/de/tla2b/output/TlaTypePrinter.java b/src/main/java/de/tla2b/output/TlaTypePrinter.java
index 97bd0c2bb47563fa4f16b560256542d8ff406d83..ac60b6a052c9f0ac1d687e6358b8e458de619d70 100644
--- a/src/main/java/de/tla2b/output/TlaTypePrinter.java
+++ b/src/main/java/de/tla2b/output/TlaTypePrinter.java
@@ -8,7 +8,6 @@ import de.be4.classicalb.core.parser.analysis.prolog.NodeIdAssignment;
import de.be4.classicalb.core.parser.analysis.prolog.PositionPrinter;
import de.be4.classicalb.core.parser.node.Node;
import de.hhu.stups.sablecc.patch.PositionedNode;
-import de.hhu.stups.sablecc.patch.SourcePositions;
import de.prob.prolog.output.IPrologTermOutput;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.types.BoolType;
diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index c5ef8a780193fd08e13862b9ccc71225103a3dfb..933423dac2e62da9bfc13bc32e13e3f8a775fae7 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -37,7 +37,7 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements
}
visitAssumptions(specAnalyser.getModuleNode().getAssumptions());
-
+
if (specAnalyser.getNext() != null) {
visitExprNode(specAnalyser.getNext());
}
diff --git a/src/main/java/de/tla2b/types/FunctionType.java b/src/main/java/de/tla2b/types/FunctionType.java
index bd2656b35f873e15428052bd3f0058c2ec6afa69..e283d1f362284f61e3cb14c4190aa0a60dff4152 100644
--- a/src/main/java/de/tla2b/types/FunctionType.java
+++ b/src/main/java/de/tla2b/types/FunctionType.java
@@ -21,6 +21,9 @@ public class FunctionType extends AbstractHasFollowers {
this.setRange(new UntypedType());
}
+ public FunctionType(int string) {
+ super(string);
+ }
public void update(TLAType oldType, TLAType newType) {
if (domain == oldType)
@@ -30,22 +33,26 @@ public class FunctionType extends AbstractHasFollowers {
}
@Override
- public boolean compare(TLAType o) {
- if (this.contains(o))
+ public boolean compare(TLAType other) {
+ if (this.contains(other))
return false;
- if (o.getKind() == UNTYPED)
+ if (other.getKind() == UNTYPED)
+ return true;
+ if (other instanceof StringType
+ && domain.compare(IntType.getInstance())
+ && range instanceof UntypedType) {
return true;
- if (o instanceof FunctionType) {
- FunctionType f = (FunctionType) o;
+ }
+ if (other instanceof FunctionType) {
+ FunctionType f = (FunctionType) other;
return domain.compare(f.domain) && range.compare(f.range);
}
- if(o instanceof TupleType){
- return o.compare(this);
+ if (other instanceof TupleType) {
+ return other.compare(this);
}
- if(o instanceof TupleOrFunction){
- return o.compare(this);
+ if (other instanceof TupleOrFunction) {
+ return other.compare(this);
}
-
return false;
}
@@ -66,24 +73,32 @@ public class FunctionType extends AbstractHasFollowers {
}
@Override
- public FunctionType unify(TLAType o) throws UnificationException {
- if (!this.compare(o))
+ public TLAType unify(TLAType other) throws UnificationException {
+ if (other == null || !this.compare(other)) {
throw new UnificationException();
- if (o instanceof UntypedType) {
- ((UntypedType) o).setFollowersTo(this);
+ }
+
+ if (other instanceof StringType) {
+ this.setFollowersTo(other);
+ return StringType.getInstance();
+ }
+
+ if (other instanceof UntypedType) {
+ ((UntypedType) other).setFollowersTo(this);
return this;
}
- if (o instanceof FunctionType) {
- domain = domain.unify(((FunctionType) o).domain);
- range = range.unify(((FunctionType) o).range);
+ if (other instanceof FunctionType) {
+ domain = domain.unify(((FunctionType) other).domain);
+ range = range.unify(((FunctionType) other).range);
return this;
}
- if (o instanceof TupleType){
- return (FunctionType) o.unify(this);
+ if (other instanceof TupleType) {
+ return (FunctionType) other.unify(this);
}
- if(o instanceof TupleOrFunction){
- return (FunctionType) o.unify(this);
+ if (other instanceof TupleOrFunction) {
+ return (FunctionType) other.unify(this);
}
+
throw new RuntimeException();
}
@@ -108,13 +123,13 @@ public class FunctionType extends AbstractHasFollowers {
((AbstractHasFollowers) range).addFollower(this);
}
}
-
+
@Override
public String toString() {
String res = "POW(" + domain + "*";
if (range instanceof TupleType) {
res += "(" + range + ")";
- } else{
+ } else {
res += range;
}
res += ")";
@@ -123,7 +138,8 @@ public class FunctionType extends AbstractHasFollowers {
@Override
public PExpression getBNode() {
- return new APartialFunctionExpression(domain.getBNode(), range.getBNode());
+ return new APartialFunctionExpression(domain.getBNode(),
+ range.getBNode());
}
public void apply(TypeVisitorInterface vistor) {
diff --git a/src/main/java/de/tla2b/types/SetType.java b/src/main/java/de/tla2b/types/SetType.java
index 4f5780bcc641b43874adce99886f70554baab87d..4179d0cce48a1b1c0d91aefe65ae99cf6d0d86a2 100644
--- a/src/main/java/de/tla2b/types/SetType.java
+++ b/src/main/java/de/tla2b/types/SetType.java
@@ -37,7 +37,6 @@ public class SetType extends AbstractHasFollowers {
}
public SetType unify(TLAType o) throws UnificationException {
-
if (!this.compare(o)|| this.contains(o)) {
throw new UnificationException();
}
diff --git a/src/main/java/de/tla2b/types/StringType.java b/src/main/java/de/tla2b/types/StringType.java
index b32ab64ce7e7a927a26b2989a5858cff17c42874..13b5623ed26f9382ec1a2c849838cfdbaabc3f19 100644
--- a/src/main/java/de/tla2b/types/StringType.java
+++ b/src/main/java/de/tla2b/types/StringType.java
@@ -11,27 +11,25 @@ import de.tla2b.output.TypeVisitorInterface;
public class StringType extends TLAType {
- private static StringType instance = new StringType();
-
- private StringType() {
+ public StringType() {
super(STRING);
}
-
- public static StringType getInstance(){
- return instance;
- }
- @Override
- public String toString() {
- return "STRING";
+ private static StringType instance = new StringType();
+
+ public static StringType getInstance() {
+ return instance;
}
@Override
public boolean compare(TLAType o) {
if (o.getKind() == UNTYPED || o.getKind() == STRING)
return true;
- else
+ else if (o instanceof FunctionType) {
+ return o.compare(this);
+ } else
return false;
+
}
@Override
@@ -41,21 +39,32 @@ public class StringType extends TLAType {
@Override
public StringType unify(TLAType o) throws UnificationException {
+ if (!this.compare(o)) {
+ throw new UnificationException();
+ }
if (o.getKind() == STRING) {
return this;
} else if (o instanceof UntypedType) {
((UntypedType) o).setFollowersTo(this);
((UntypedType) o).deleteFollowers();
return this;
- } else
+ } else if (o instanceof FunctionType) {
+ // function
+ if (o instanceof AbstractHasFollowers) {
+ ((AbstractHasFollowers) o).setFollowersTo(this);
+ ((AbstractHasFollowers) o).deleteFollowers();
+ }
+ return this;
+ } else {
throw new UnificationException();
+ }
}
@Override
public StringType cloneTLAType() {
return this;
}
-
+
@Override
public boolean contains(TLAType o) {
return false;
@@ -69,5 +78,10 @@ public class StringType extends TLAType {
public void apply(TypeVisitorInterface visitor) {
visitor.caseStringType(this);
}
-
+
+ @Override
+ public String toString() {
+ return "STRING";
+ }
+
}
diff --git a/src/main/java/de/tla2b/types/TupleOrFunction.java b/src/main/java/de/tla2b/types/TupleOrFunction.java
index f120eb7fb867b2ed2e4f47c5bfcb8cca72bd4f05..a9f006ef10fd4f554dd060d5fbdf74d0387096ae 100644
--- a/src/main/java/de/tla2b/types/TupleOrFunction.java
+++ b/src/main/java/de/tla2b/types/TupleOrFunction.java
@@ -70,7 +70,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
func.setRange(new UntypedType());
FunctionType res;
try {
- res = func.unify(this);
+ res = (FunctionType) func.unify(this);
return res.getBNode();
} catch (UnificationException e) {
// tuple
@@ -330,7 +330,7 @@ public class TupleOrFunction extends AbstractHasFollowers {
FunctionType func = new FunctionType(IntType.getInstance(),
new UntypedType());
try {
- func = func.unify(this);
+ func = (FunctionType) func.unify(this);
this.setFollowersTo(func);
return func;
} catch (UnificationException e) {
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 4355d6ce5facd9df5ae86e2d282ad1b62fec6678..67bfccab441b827c7b1a4736ef34ae350d0c7d66 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -11,11 +11,7 @@ import java.io.OutputStreamWriter;
import java.io.PrintWriter;
import java.io.UnsupportedEncodingException;
import java.util.Date;
-import java.util.HashMap;
import java.util.Hashtable;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.Definitions;
@@ -23,10 +19,6 @@ import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
-import de.hhu.stups.sablecc.patch.IToken;
-import de.hhu.stups.sablecc.patch.PositionedNode;
-import de.hhu.stups.sablecc.patch.SourcePositions;
-import de.hhu.stups.sablecc.patch.SourcecodeRange;
import de.tla2b.analysis.InstanceTransformation;
import de.tla2b.analysis.PredicateVsExpression;
import de.tla2b.analysis.SpecAnalyser;
@@ -247,7 +239,6 @@ public class Translator implements TranslationGlobals {
SymbolSorter symbolSorter = new SymbolSorter(moduleNode);
symbolSorter.sort();
-
PredicateVsExpression predicateVsExpression = new PredicateVsExpression(
moduleNode);
@@ -266,7 +257,6 @@ public class Translator implements TranslationGlobals {
specAnalyser.start();
typechecker = new TypeChecker(moduleNode, conEval, specAnalyser);
typechecker.start();
-
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
@@ -365,7 +355,7 @@ public class Translator implements TranslationGlobals {
ASTPrettyPrinter aP = new ASTPrettyPrinter(BAst, renamer);
BAst.apply(aP);
StringBuilder result = aP.getResultAsStringbuilder();
- result.insert(0, "/*@ generated by TLA2B " + VERSION + " " + new Date()
+ result.insert(0, "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date()
+ " */\n");
try {
diff --git a/src/test/java/de/tla2b/examples/RegressionTests.java b/src/test/java/de/tla2b/examples/RegressionTests.java
index d5b0220bb5f0e3bd9472530497dd07b3ca842a8b..1b92c2f3314e81081a5f73ec7860effd1ae28e46 100644
--- a/src/test/java/de/tla2b/examples/RegressionTests.java
+++ b/src/test/java/de/tla2b/examples/RegressionTests.java
@@ -1,6 +1,6 @@
package de.tla2b.examples;
-import static de.tla2b.util.TestUtil.runModule;
+import static de.tla2b.util.TestUtil.load_TLA_File;
import java.io.File;
import java.util.ArrayList;
@@ -23,16 +23,13 @@ public class RegressionTests extends AbstractParseModuleTest{
@Test
public void testRunTLC() throws Exception {
- //String[] a = new String[] { moduleFile.getPath() };
- System.out.println(moduleFile.getPath());
- runModule(moduleFile.getPath());
+ load_TLA_File(moduleFile.getPath());
}
@Config
public static Configuration getConfig() {
final ArrayList<String> list = new ArrayList<String>();
final ArrayList<String> ignoreList = new ArrayList<String>();
-
list.add("./src/test/resources/regression");
return getConfiguration2(list, ignoreList);
}
diff --git a/src/test/java/de/tla2b/typechecking/StringTest.java b/src/test/java/de/tla2b/typechecking/StringTest.java
index 6944edec529ba2bce7e200085971b57440934ef6..4ae59cec51d86e3730fe22c3883fc06681b98cd4 100644
--- a/src/test/java/de/tla2b/typechecking/StringTest.java
+++ b/src/test/java/de/tla2b/typechecking/StringTest.java
@@ -39,6 +39,33 @@ public class StringTest {
TestUtil.typeCheckString(module);
}
+ @Test
+ public void testStringAsSequence() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME \"a\" \\o \"bc\" = \"abc\" \n"
+ + "=================================";
+ TestUtil.typeCheckString(module);
+ }
+
+ @Test
+ public void testStringAsSequence2() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME SubSeq(\"abc\",1,1) = \"a\" \n"
+ + "=================================";
+ TestUtil.typeCheckString(module);
+ }
+
+ @Test
+ public void testStringAsSequence3() throws FrontEndException, TLA2BException {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Sequences \n"
+ + "ASSUME Len(\"abc\") = 3 \n"
+ + "=================================";
+ TestUtil.typeCheckString(module);
+ }
+
/**********************************************************************
* STRING
@@ -61,4 +88,7 @@ public class StringTest {
TestUtil.typeCheckString(module);
}
+
+
+
}
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 319ea77bb8513b9143738e80b1e52413f89853d1..280953886818616a20bd788c26bf076738e504bb 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -4,13 +4,19 @@
package de.tla2b.util;
-import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.*;
+
+import java.util.Set;
import util.FileUtil;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.prob.scripting.Api;
+import de.prob.statespace.StateSpace;
+import de.prob.statespace.Trace;
+import de.prob.statespace.Transition;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.output.ASTPrettyPrinter;
@@ -193,5 +199,22 @@ public class TestUtil {
final String string = ast2String.toString();
return string;
}
+
+ public static void load_TLA_File(String tlaFile) throws Exception{
+ Api api = de.prob.Main.getInjector().getInstance(Api.class);
+ //TODO translate here and then pass the AST to api
+ // Currently B definitions are not recognized by the api load command
+// Translator t = new Translator(tlaFile);
+// Start start = t.translate();
+// ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
+// start.apply(aP);
+// System.out.println(aP.getResultString());
+
+ //StateSpace stateSpace = api.b_load(start);
+ StateSpace stateSpace = api.tla_load(tlaFile);
+ Trace trace= new Trace(stateSpace);
+ Set<Transition> nextTransitions = trace.getNextTransitions();
+ assertTrue(nextTransitions.size() > 0);
+ }
}
diff --git a/src/test/resources/regression/DefCapture/DefCapture.mch b/src/test/resources/regression/DefCapture/DefCapture.mch
deleted file mode 100644
index 643c7fff3b40fe6be59a0be8c867eb6c7666f23d..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/DefCapture/DefCapture.mch
+++ /dev/null
@@ -1,10 +0,0 @@
-MACHINE DefCapture
-PROPERTIES
- Double(2)
- & NotDouble(3)
- & {x|x : {2, 3} & NotDouble(x)} = {3}
-DEFINITIONS
- Double(y) == #x_1.(x_1 : 1 .. 10 & x_1 + x_1 = y);
-
- NotDouble(y) == not(Double(y))
-END
diff --git a/src/test/resources/regression/DefCapture/DefCapture.tla b/src/test/resources/regression/DefCapture/DefCapture.tla
deleted file mode 100644
index 7aa53cc4b90354d9c2be1b201caa5df3b9ae503d..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/DefCapture/DefCapture.tla
+++ /dev/null
@@ -1,15 +0,0 @@
--------------------------------- MODULE DefCapture --------------------------------
-EXTENDS Naturals
-
-Double(y) == \E x \in 1..10 :(x+x=y)
-
-NotDouble(y) == \neg Double(y)
-
-ASSUME Double(2)
-
-ASSUME NotDouble(3)
-
-ASSUME {x \in {2,3} : NotDouble(x)} = {3}
-
-=======================
-
diff --git a/src/test/resources/regression/SumAndProduct/SumAndProductConstraint.tla b/src/test/resources/regression/SumAndProduct/SumAndProductConstraint.tla
deleted file mode 100644
index 2472c5b259793e95aa32994682b4938c7ea1da66..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/SumAndProduct/SumAndProductConstraint.tla
+++ /dev/null
@@ -1,56 +0,0 @@
-------------------------- MODULE SumAndProductConstraint -------------------------
-(****************************************************************************)
-(* This module formalizes the "sum and product" puzzle, due to Freudenthal *)
-(* (1969), and which goes as follows: *)
-(* J says to S and P: I have chosen two integers x and y such that *)
-(* 1 < x <= y < 100. In a moment, I will inform S only of the sum x+y *)
-(* and P only of the product x*y. These announcements remain private. *)
-(* You are required to determine the pair (x,y). He acts as said. *)
-(* The following conversation now takes place: *)
-(* 1. P says: "I don't know it." *)
-(* 2. S says: "I knew you didn't." *)
-(* 3. P says: "Now I know it." *)
-(* 4. S says: "I now also know it." *)
-(* Determine the pair (x,y). *)
-(* In fact, the first announcement is implied by the second one, so we will *)
-(* not take it into account in the following formal. *)
-(****************************************************************************)
-
-EXTENDS Naturals, FiniteSets, TLC
-
-Pairs == { <<i,j>> \in (2 .. 99) \X (2 .. 99) : i <= j }
-
-(* S and P can only observe the sum and product of a pair of numbers *)
-obsS(i,j) == i+j
-obsP(i,j) == i*j
-
-equivS(i,j,k,l) == obsS(i,j) = obsS(k,l)
-equivP(i,j,k,l) == obsP(i,j) = obsP(k,l)
-
-(* Assertions are formalized as sets of pairs, and a "world" is a pair.
- S and P know an assertion A in world <<i,j>> \in W if all worlds in W
- equivalent to (i,j) satisfy A. *)
-knowsS(W,i,j,A) == \A <<k,l>> \in W : equivS(i,j,k,l) => <<k,l>> \in A
-knowsP(W,i,j,A) == \A <<k,l>> \in W : equivP(i,j,k,l) => <<k,l>> \in A
-
-(* S and P know that A is false in world <<i,j>> if no world equivalent to
- (i,j) satisfies A. *)
-knowsS_neg(W,i,j,A) == \A <<k,l>> \in W : equivS(i,j,k,l) => <<k,l>> \notin A
-knowsP_neg(W,i,j,A) == \A <<k,l>> \in W : equivP(i,j,k,l) => <<k,l>> \notin A
-
-(* worlds in which P can identify the pair uniquely *)
-knowP_pair == { <<i,j>> \in Pairs : knowsP(Pairs, i,j, {<<i,j>>}) }
-(* worlds in which S knows that P cannot know the pair *)
-Step2 == { <<i,j>> \in Pairs : knowsS_neg(Pairs, i,j, knowP_pair) }
-(* filter out worlds in Step2 for which P now knows the pair uniquely *)
-Step3 == { <<i,j>> \in Step2 : knowsP(Step2, i,j, {<<i,j>>}) }
-(* now restrict to worlds in Step3 for which also S knows the pair uniquely *)
-Step4 == { <<i,j>> \in Step3 : knowsS(Step3, i,j, {<<i,j>>}) }
-
-CONSTANTS k
-ASSUME k = Step4
-
-==================================================================================
-\* Modification History
-\* Last modified Mon Apr 22 11:02:28 CEST 2013 by merz
-\* Created Sun Apr 21 19:19:53 CEST 2013 by merz
diff --git a/src/test/resources/regression/SumAndProduct/SumAndProductTransition.tla b/src/test/resources/regression/SumAndProduct/SumAndProductTransition.tla
deleted file mode 100644
index 94feee1746e078d07522b4f368ef216e61fd5c39..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/SumAndProduct/SumAndProductTransition.tla
+++ /dev/null
@@ -1,96 +0,0 @@
-------------------------- MODULE SumAndProductTransition ---------------------
-(****************************************************************************)
-(* This module formalizes the "sum and product" puzzle, due to Freudenthal *)
-(* (1969), and which goes as follows: *)
-(* J says to S and P: I have chosen two integers x and y such that *)
-(* 1 < x <= y < 100. In a moment, I will inform S only of the sum x+y *)
-(* and P only of the product x*y. These announcements remain private. *)
-(* You are required to determine the pair (x,y). He acts as said. *)
-(* The following conversation now takes place: *)
-(* 1. P says: "I don't know it." *)
-(* 2. S says: "I knew you didn't." *)
-(* 3. P says: "Now I know it." *)
-(* 4. S says: "I now also know it." *)
-(* Determine the pair (x,y). *)
-(* *)
-(* The following TLA+ module represents the puzzle as a transition system *)
-(* where the two values are picked arbitrarily, then the feasibility of the *)
-(* above dialogue is verified, with S and P adapting their beliefs at each *)
-(* step. *)
-(* In fact, the first announcement is implied by the second one, so we do *)
-(* not have to represent it explicitly. *)
-(****************************************************************************)
-
-EXTENDS Naturals, FiniteSets
-
-VARIABLES x, y, \* the numbers chosen by J
- beliefP, beliefS, \* the pairs considered possible by P and S
- step \* next announcement in the conversation
-
-Pairs == { <<i,j>> \in (2 .. 99) \X (2 .. 99) : i <= j }
-
-(* Set of pairs that are equivalent from the point of view of P or S with a pair (i,j).
- In particular, possibleP(x,y) denotes the set of pairs that P considers possible
- given her initial knowledge. *)
-possibleP(i,j) == { <<u,v>> \in Pairs : u*v = i*j }
-possibleS(i,j) == { <<u,v>> \in Pairs : u+v = i+j }
-
-(* Given a set B of beliefs (pairs of numbers), an agent knows the pair if B
- is a singleton. For example, P knows the pair if knows(beliefP) holds. *)
-knows(B) == Cardinality(B) = 1
-
-(* Given a set B of beliefs, one knows that P knows the pair, if for every
- belief b in B, P knows the result based on what it considers compatible
- with b. For example, S knows that P knows if knows_knowsP(beliefS) holds. *)
-knows_knowsP(B) == \A <<i,j>> \in B : knows(possibleP(i,j))
-
-(* Similarly, given B, one knows that P doesn't know if there is no pair in B
- for which P knows. *)
-knows_not_knowsP(B) == \A <<i,j>> \in B : ~ knows(possibleP(i,j))
-
-Init ==
- /\ x \in 2 .. 99 /\ y \in 2 .. 99 /\ x <= y
-(* uncomment the following conjunct to check uniqueness of solution *)
-\* /\ ~ (x=4 /\ y=13)
- /\ beliefP = possibleP(x,y)
- /\ beliefS = possibleS(x,y)
- /\ step = 2
-
-(* The following actions correspond to the different steps in the conversation. *)
-Step2 ==
- /\ step = 2
- /\ ~ knows(beliefP) \* logically redundant, but speeds up verification
- /\ knows_not_knowsP(beliefS)
- /\ beliefP' = beliefP \ { <<i,j>> \in beliefP : ~ knows_not_knowsP(possibleS(i,j)) }
- /\ step' = 3
- /\ UNCHANGED <<x,y,beliefS>>
-
-Step3 ==
- /\ step = 3
- /\ knows(beliefP)
- /\ beliefS' = beliefS \ { <<i,j>> \in beliefS :
- LET P == possibleP(i,j)
- IN ~ knows(P \ {<<u,v>> \in P : ~ knows_not_knowsP(possibleS(u,v))}) }
- /\ step' = 4
- /\ UNCHANGED <<x,y,beliefP>>
-
-Step4 ==
- /\ step = 4
- /\ knows(beliefS)
- /\ step' = 5
- /\ UNCHANGED <<x,y,beliefP,beliefS>>
-
-Next == Step2 \/ Step3 \/ Step4
-
-vars == <<x,y,beliefP,beliefS>>
-
-SumProduct == Init /\ [][Next]_vars
-
-(* The following assertion says that the protocol cannot finish. Try to verify it
- in order to find the solution of the puzzle (disable deadlock checking). *)
-Impossible == step # 5
-
-=============================================================================
-\* Modification History
-\* Last modified Mon Apr 22 12:17:12 CEST 2013 by merz
-\* Created Fri Apr 19 18:30:06 CEST 2013 by merz