diff --git a/build.gradle b/build.gradle
index cede4acc0147531d3e98d282b9c612c45d2157bc..6ed6fc77c211fd4dbc7225884dc21a17dbff7a7a 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,6 +1,8 @@
apply plugin: 'java'
apply plugin: 'eclipse'
apply plugin: 'maven'
+apply plugin: 'jacoco'
+apply plugin: 'findbugs'
project.version = '1.0.0-SNAPSHOT'
project.group = 'de.prob'
@@ -13,7 +15,35 @@ repositories {
}
configurations { // configuration that holds jars to copy into lib
- releaseJars }
+ releaseJars
+}
+
+jacoco {
+ toolVersion = "0.6.2.201302030002"
+ reportsDir = file("$buildDir/customJacocoReportDir")
+}
+
+jacocoTestReport {
+ reports {
+ xml.enabled false
+ csv.enabled false
+ html.destination "${buildDir}/jacocoHtml"
+ }
+}
+
+tasks.withType(FindBugs) {
+ reports {
+ xml.enabled = false
+ html.enabled = true
+ }
+ }
+
+findbugs {
+ ignoreFailures = true
+}
+
+
+
def parser_version = '2.4.22-SNAPSHOT'
@@ -28,8 +58,11 @@ dependencies {
//compile(group: 'de.prob', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
- testCompile (group: 'junit', name: 'junit', version: '4.+')
+
+
+ testCompile (group: 'junit', name: 'junit', version: '4.7')
testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.4-SNAPSHOT')
+
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
releaseJars (group: 'de.prob', name: 'prologlib', version: parser_version)
@@ -42,14 +75,15 @@ dependencies {
test {
exclude('de/tlc4b/tlc/integration/probprivate')
exclude('testing')
-
+ //exclude('de/tlc4b/tlc/integration')
}
task integrationtests(type: Test){
doFirst{ println("Running integration tests") }
scanForTestClasses = true
- include('de/tlc4b/tlc/integration/probprivate/**')
+ //include('de/tlc4b/tlc/integration/probprivate/**')
+ include('de/tlc4b/**')
}
jar { from sourceSets.main.allJava }
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 0fb79e70daecf6e390facb2f6cce826551b422f2..64e46258dc826663a1a045980e305fb376eb3d6e 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -1,14 +1,14 @@
package de.tlc4b;
-import java.io.BufferedReader;
+import java.io.BufferedWriter;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
-import java.io.FileReader;
-import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
+import java.io.OutputStreamWriter;
+import java.io.UnsupportedEncodingException;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.tlc4b.TLC4BGlobals;
@@ -17,7 +17,6 @@ import de.tlc4b.exceptions.TLC4BIOException;
import de.tlc4b.exceptions.TLC4BException;
import de.tlc4b.tlc.TLCOutputInfo;
import de.tlc4b.tlc.TLCResults;
-import de.tlc4b.tlc.TLCResults.TLCResult;
import de.tlc4b.util.StopWatch;
public class TLC4B {
@@ -33,8 +32,9 @@ public class TLC4B {
private String constantsSetup;
public static void main(String[] args) throws IOException {
+ System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up
+ // windows
TLC4B tlc4b = new TLC4B();
-
try {
tlc4b.progress(args);
} catch (BException e) {
@@ -52,8 +52,6 @@ public class TLC4B {
try {
TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
tlc4b.path);
- // b2tla.evalOutput(output, B2TLAGlobals.isCreateTraceFile());
- // System.out.println("------------------------------");
TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
@@ -63,7 +61,6 @@ public class TLC4B {
} catch (NoClassDefFoundError e) {
System.err
.println("Can not find TLC. The tlatools.jar must be included in the classpath.");
- // System.out.println(e.getMessage());
}
}
@@ -98,54 +95,51 @@ public class TLC4B {
}
public static void test(String[] args, boolean deleteFiles)
- throws IOException {
+ throws Exception {
TLC4BGlobals.resetGlobals();
TLC4BGlobals.setDeleteOnExit(deleteFiles);
+ TLC4BGlobals.setCreateTraceFile(false);
TLC4BGlobals.setTestingMode(true);
// B2TLAGlobals.setCleanup(true);
- TLC4B b2tla = new TLC4B();
+ TLC4B tlc4b = new TLC4B();
try {
- b2tla.progress(args);
+ tlc4b.progress(args);
} catch (Exception e) {
e.printStackTrace();
System.err.println(e.getMessage());
- return;
+ throw e;
}
-
+ //System.out.println(tlc4b.tlaModule);
if (TLC4BGlobals.isRunTLC()) {
- TLCRunner.runTLC(b2tla.machineFileNameWithoutFileExtension,
- b2tla.path);
+ TLCRunner.runTLC(tlc4b.machineFileNameWithoutFileExtension,
+ tlc4b.path);
- TLCResults results = new TLCResults(b2tla.tlcOutputInfo);
+ TLCResults results = new TLCResults(tlc4b.tlcOutputInfo);
results.evalResults();
- @SuppressWarnings("unused")
- TLCResult result = results.getTLCResult();
- // System.out.println("Result: " + result);
+ // System.out.println("Result: " + results.getTLCResult());
+
+ tlc4b.printResults(results, false);
+ //System.out.println(results.getTrace());
- b2tla.printResults(results, false);
- System.out.println(results.getTrace());
System.exit(0);
}
- System.exit(1);
}
- @SuppressWarnings({ "unused", "null" })
- private void printTestResultsForTestscript() {
- TLCResults tlcResults = null;
- // This output is adapted to Ivo's testscript
- System.out.println("------------- Results -------------");
- System.out.println("Model Checking Time: "
- + (tlcResults.getModelCheckingTime() * 1000) + " ms");
- System.out.println("States analysed: "
- + tlcResults.getNumberOfDistinctStates());
- System.out.println("Transitions fired: "
- + tlcResults.getNumberOfTransitions());
- if (tlcResults.getTLCResult() != TLCResult.NoError) {
- System.err.println("@@");
- System.err.println("12" + tlcResults.getResultString());
- }
-
- }
+ /*
+ * private void printTestResultsForTestscript() { TLCResults tlcResults =
+ * null; // This output is adapted to Ivo's testscript
+ * System.out.println("------------- Results -------------");
+ * System.out.println("Model Checking Time: " +
+ * (tlcResults.getModelCheckingTime() * 1000) + " ms");
+ * System.out.println("States analysed: " +
+ * tlcResults.getNumberOfDistinctStates());
+ * System.out.println("Transitions fired: " +
+ * tlcResults.getNumberOfTransitions()); if (tlcResults.getTLCResult() !=
+ * TLCResult.NoError) { System.err.println("@@"); System.err.println("12" +
+ * tlcResults.getResultString()); }
+ *
+ * }
+ */
private void handleParameter(String[] args) {
int index = 0;
@@ -364,17 +358,21 @@ public class TLC4B {
System.out.println("Standard module '" + path + name
+ ".tla' created.");
} catch (IOException e) {
- e.printStackTrace();
+ throw new TLC4BIOException(e.getMessage());
} finally {
- if (TLC4BGlobals.isDeleteOnExit()) {
+ if (TLC4BGlobals.isDeleteOnExit() && file.exists()) {
file.deleteOnExit();
}
try {
- is.close();
- fos.flush();
- fos.close();
+ if (is != null) {
+ is.close();
+ }
+ if (fos != null) {
+ fos.flush();
+ fos.close();
+ }
} catch (IOException ex) {
- ex.printStackTrace();
+ throw new TLC4BIOException(ex.getMessage());
}
}
}
@@ -388,37 +386,50 @@ public class TLC4B {
return mainFile;
}
- public static String fileToString(String fileName) throws IOException {
- StringBuilder res = new StringBuilder();
- BufferedReader in = new BufferedReader(new FileReader(fileName));
- String str;
- while ((str = in.readLine()) != null) {
- res.append(str + "\n");
- }
- in.close();
- return res.toString();
- }
-
public static File createFile(String dir, String fileName, String text,
boolean deleteOnExit) {
- File d = new File(dir);
- d.mkdirs();
File file = new File(dir + File.separator + fileName);
+
+ BufferedWriter out;
try {
- file.createNewFile();
- FileWriter fw;
- fw = new FileWriter(file);
- fw.write(text);
- fw.close();
+ out = new BufferedWriter(new OutputStreamWriter(
+ new FileOutputStream(file), "UTF-8"));
+ out.write(text);
+ out.close();
return file;
+ } catch (UnsupportedEncodingException e1) {
+ throw new TLC4BIOException(e1.getMessage());
+ } catch (FileNotFoundException e1) {
+ throw new TLC4BIOException(e1.getMessage());
} catch (IOException e) {
- e.printStackTrace();
throw new TLC4BIOException(e.getMessage());
- } finally {
- if (deleteOnExit) {
+ } finally{
+ if (deleteOnExit && file.exists()) {
file.deleteOnExit();
}
}
+
+// try {
+// out = new BufferedWriter(new OutputStreamWriter(
+// new FileOutputStream(file), "UTF-8"));
+// out.write(text);
+// out.close();
+// // FileWriter fw;
+// // fw = new FileWriter(file);
+// // fw.write(text);
+// // fw.close();
+// return file;
+// } catch (IOException e) {
+// e.printStackTrace();
+// throw new TLC4BIOException(e.getMessage());
+// } finally {
+// try {
+// out.close();
+// } catch (IOException e) {
+// e.printStackTrace();
+// throw new TLC4BIOException(e.getMessage());
+// }
+// }
}
}
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index c8eaeddd7824614a9bd8f8248b8e97077574dce3..5de3b959dd1764cf41eafc281060aac7e9e43fb7 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -1,8 +1,6 @@
package de.tlc4b;
import java.io.BufferedReader;
-import java.io.File;
-import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
@@ -61,8 +59,8 @@ public class TLCRunner {
if (!TLC4BGlobals.isDeadlockCheck()) {
list.add("-deadlock");
}
-
- if(TLC4BGlobals.isCheckltl()){
+
+ if (TLC4BGlobals.isCheckltl()) {
list.add("-cleanup");
}
// list.add("-coverage");
@@ -86,22 +84,18 @@ public class TLCRunner {
public static void runTLC(String machineName, String path) {
System.out.println("--------------------------------");
-
- //BTLCPrintStream btlcStream = new BTLCPrintStream();
- //PrintStream systemOut = System.out;
- //System.setErr(btlcStream);
- //System.setOut(btlcStream);
+
ToolIO.setMode(ToolIO.SYSTEM);
-
+
ArrayList<String> list = new ArrayList<String>();
if (!TLC4BGlobals.isDeadlockCheck()) {
list.add("-deadlock");
}
- if(TLC4BGlobals.getWorkers() > 1){
+ if (TLC4BGlobals.getWorkers() > 1) {
list.add("-workers");
- list.add(""+TLC4BGlobals.getWorkers());
+ list.add("" + TLC4BGlobals.getWorkers());
}
-
+
list.add("-config");
list.add(machineName + ".cfg");
list.add(machineName);
@@ -109,23 +103,23 @@ public class TLCRunner {
String[] args = list.toArray(new String[list.size()]);
TLC tlc = new TLC();
-
+
// handle parameters
if (tlc.handleParameters(args)) {
tlc.setResolver(new SimpleFilenameToStream());
// call the actual processing method
try {
- tlc.process();
+ tlc.process();
} catch (Exception e) {
}
-
+
}
- //System.setOut(systemOut);
- //ArrayList<String> messages = btlcStream.getArrayList();
-
+ // System.setOut(systemOut);
+ // ArrayList<String> messages = btlcStream.getArrayList();
+
System.out.println("--------------------------------");
closeThreads();
- //return messages;
+ // return messages;
}
private static void closeThreads() {
@@ -141,28 +135,6 @@ public class TLCRunner {
}
// System.exit(0);
}
-
- public static void createfile(String dir, String fileName, String text) {
- File d = new File(dir);
- d.mkdirs();
- File tempFile = new File(dir + File.separator + fileName);
- try {
- tempFile.createNewFile();
- System.out
- .println("Tempfile:'" + tempFile.getName() + "' created.");
- } catch (IOException e1) {
- e1.printStackTrace();
- }
- FileWriter fw;
- try {
- fw = new FileWriter(tempFile);
- fw.write(text);
- fw.close();
- } catch (IOException e) {
- e.printStackTrace();
- }
- }
-
}
class StreamGobbler extends Thread {
@@ -180,7 +152,7 @@ class StreamGobbler extends Thread {
public void run() {
try {
- InputStreamReader isr = new InputStreamReader(is);
+ InputStreamReader isr = new InputStreamReader(is, "UTF-8");
BufferedReader br = new BufferedReader(isr);
String line = null;
while ((line = br.readLine()) != null) {
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 748a6dcb4a13a0f47593122df71bdf13867092c0..551ec40a2b0cf324584848d61bc140cfbcb7ab8d 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -93,8 +93,7 @@ public class Translator {
}
public void translate() {
- @SuppressWarnings("unused")
- DefinitionsEliminator defEliminator = new DefinitionsEliminator(start);
+ new DefinitionsEliminator(start);
new NotSupportedConstructs(start);
@@ -119,7 +118,7 @@ public class Translator {
machineContext, typechecker);
PrecedenceCollector precedenceCollector = new PrecedenceCollector(
- start, typechecker.getTypes(), machineContext, typeRestrictor);
+ start, typechecker, machineContext, typeRestrictor);
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
machineContext);
@@ -149,7 +148,7 @@ public class Translator {
configString = printer.getConfigString().toString();
tlcOutputInfo = new TLCOutputInfo(machineContext, renamer,
- typechecker.getTypes(), generator.getTlaModule());
+ typechecker, generator.getTlaModule());
}
public String getMachineString() {
diff --git a/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
index 92b4edeaec52b990a9fd37ac460d1bc34871bf82..d97d97f409c00004c820f169da14a56320026179 100644
--- a/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
@@ -7,6 +7,7 @@ import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedList;
+import java.util.Map.Entry;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACardExpression;
@@ -144,14 +145,12 @@ public class ConstantsEliminator extends DepthFirstAdapter {
constantsMachineClause.getIdentifiers().remove(id);
HashMap<String, Node> constants = machineContext.getConstants();
- String constantName = null;
- for (String key : constants.keySet()) {
- if (constants.get(key) == id) {
- constantName = key;
+ for (Entry<String, Node> entry : constants.entrySet()) {
+ if(entry.getValue() == id){
+ constants.remove(entry.getKey());
break;
}
}
- constants.remove(constantName);
}
private void removeAssignmentInPropertiesClause(Node val) {
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index c6f4838c941c61d9efbfacd2b151e80232da468b..590d9c44d9d91a50f3b97836cc6d6f72f61542da 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -1,5 +1,6 @@
package de.tlc4b.analysis;
+import java.io.Serializable;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
@@ -108,9 +109,10 @@ public class MachineContext extends DepthFirstAdapter {
private ArrayList<LinkedHashMap<String, Node>> contextTable;
- private final Hashtable<Node, Node> referencesTable;
+ protected final Hashtable<Node, Node> referencesTable;
- public MachineContext(String machineName, Start start, String ltlFormula, PPredicate constantsSetup) {
+ public MachineContext(String machineName, Start start, String ltlFormula,
+ PPredicate constantsSetup) {
this.start = start;
this.machineName = machineName;
this.constantsSetup = constantsSetup;
@@ -137,17 +139,17 @@ public class MachineContext extends DepthFirstAdapter {
this.machineContextsTable = new Hashtable<String, MachineContext>();
start.apply(this);
-
+
checkLTLFormulas();
-
+
checkConstantsSetup();
}
private void checkConstantsSetup() {
- if(constantsSetup == null){
+ if (constantsSetup == null) {
return;
}
-
+
this.contextTable = new ArrayList<LinkedHashMap<String, Node>>();
ArrayList<MachineContext> list = lookupExtendedMachines();
@@ -160,7 +162,7 @@ public class MachineContext extends DepthFirstAdapter {
contextTable.add(s.getDefinitions());
}
constantsSetup.apply(this);
-
+
}
private void checkLTLFormulas() {
@@ -174,7 +176,8 @@ public class MachineContext extends DepthFirstAdapter {
try {
visitor.start();
} catch (ScopeException e) {
- System.out.println("Warning: LTL formula '" + visitor.getName() + "' cannot be checked by TLC.");
+ System.out.println("Warning: LTL formula '" + visitor.getName()
+ + "' cannot be checked by TLC.");
notSupportedLTLFormulas.add(visitor);
}
}
@@ -242,7 +245,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAMachineHeader(AMachineHeader node) {
this.header = node;
- if(machineName == null){
+ if (machineName == null) {
List<TIdentifierLiteral> nameList = new ArrayList<TIdentifierLiteral>(
node.getName());
this.machineName = Utils.getIdentifierAsString(nameList);
@@ -300,7 +303,7 @@ public class MachineContext extends DepthFirstAdapter {
"Error: LTL formula is not in a string representation.");
}
definitionsToRemove.add(def);
- }else if (name.startsWith("ANIMATION_")){
+ } else if (name.startsWith("ANIMATION_")) {
definitionsToRemove.add(def);
}
evalDefinitionName(((AExpressionDefinitionDefinition) e)
@@ -565,7 +568,7 @@ public class MachineContext extends DepthFirstAdapter {
@Override
public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
this.propertiesMachineClause = node;
-
+
/**
* check identifier scope in properties clauses
*/
@@ -678,8 +681,8 @@ public class MachineContext extends DepthFirstAdapter {
for (POperation e : copy) {
AOperation op = (AOperation) e;
String name = Utils.getIdentifierAsString(op.getOpName());
- //existString(name);
- if (operations.keySet().contains(name)){
+ // existString(name);
+ if (operations.keySet().contains(name)) {
throw new ScopeException("Duplicate identifier: '" + name + "'");
}
operations.put(name, op);
@@ -1004,10 +1007,18 @@ public class MachineContext extends DepthFirstAdapter {
return seenMachines;
}
- public Hashtable<Node, Node> getReferences() {
+ protected Hashtable<Node, Node> getReferences() {
return referencesTable;
}
+ public Node getReferenceNode(Node node) {
+ return referencesTable.get(node);
+ }
+
+ public void addReference(Node node, Node ref) {
+ referencesTable.put(node, ref);
+ }
+
public ArrayList<LTLFormulaVisitor> getLTLFormulas() {
return ltlVisitors;
}
@@ -1073,15 +1084,17 @@ public class MachineContext extends DepthFirstAdapter {
ADefinitionsMachineClause definitionMachineClause) {
this.definitionMachineClause = definitionMachineClause;
}
-
+
public PPredicate getConstantsSetup() {
return constantsSetup;
}
}
-class PMachineClauseComparator implements Comparator<PMachineClause> {
+class PMachineClauseComparator implements Comparator<PMachineClause>,
+ Serializable {
+ private static final long serialVersionUID = 2606332412649258695L;
private static Hashtable<Object, Integer> priority = new Hashtable<Object, Integer>();
static {
// declarations clauses
diff --git a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index c03d212a8da5c4fbc13b8c5daffa7eb71c8bbddb..9a05094e989bdc3e3f206ddb2503dcac9adafb88 100644
--- a/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -5,11 +5,8 @@ import java.util.Hashtable;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
-import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression;
-import de.be4.classicalb.core.parser.node.AIntersectionExpression;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
-import de.be4.classicalb.core.parser.node.ASetSubtractionExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
@@ -30,17 +27,17 @@ public class PrecedenceCollector extends DepthFirstAdapter {
put("AExistsPredicate", 1, 1, false);
put("AForallPredicate", 1, 1, false);
put("AEquivalencePredicate", 2, 2, false);
- put("ADisjunctPredicate", 3, 3, true); //or
-
+ put("ADisjunctPredicate", 3, 3, true); // or
+
/** and **/
put("AConjunctPredicate", 3, 3, true);
put("APreconditionSubstitution", 3, 3, true);
put("AAssertionSubstitution", 3, 3, true);
put("ASelectWhenSubstitution", 3, 3, true);
- put("AParallelSubstitution", 3, 3, true);
-
- put("ASelectSubstitution", 3, 3, true); //and or or
-
+ put("AParallelSubstitution", 3, 3, true);
+
+ put("ASelectSubstitution", 3, 3, true); // and or or
+
put("AEqualPredicate", 5, 5, false);
put("ALessPredicate", 5, 5, false);
put("AGreaterPredicate", 5, 5, false);
@@ -72,26 +69,27 @@ public class PrecedenceCollector extends DepthFirstAdapter {
private final Hashtable<Node, Precedence> precedenceTable;
private final HashSet<Node> brackets;
- private final Hashtable<Node, BType> typeTable;
+ private final Typechecker typechecker;
public HashSet<Node> getBrackets() {
return brackets;
}
- public PrecedenceCollector(Start start, Hashtable<Node, BType> types, MachineContext machineContext, TypeRestrictor typeRestrictor) {
+ public PrecedenceCollector(Start start, Typechecker typeChecker,
+ MachineContext machineContext, TypeRestrictor typeRestrictor) {
precedenceTable = new Hashtable<Node, Precedence>();
brackets = new HashSet<Node>();
- typeTable = types;
+ this.typechecker = typeChecker;
start.apply(this);
-
- if(machineContext.getConstantsSetup() != null){
+
+ if (machineContext.getConstantsSetup() != null) {
machineContext.getConstantsSetup().apply(this);
}
-
+
for (Node node : typeRestrictor.getAllRestrictedNodes()) {
node.apply(this);
}
-
+
}
@Override
@@ -107,15 +105,15 @@ public class PrecedenceCollector extends DepthFirstAdapter {
Precedence p = getPrecedence(node);
if (p != null) {
precedenceTable.put(node, p);
-
- if(node.parent()!= null){
+
+ if (node.parent() != null) {
Precedence parent = precedenceTable.get(node.parent());
if (Precedence.makeBrackets(p, parent)) {
brackets.add(node);
}
}
}
- //System.out.println(node.getClass().getSimpleName() + " " + p );
+ // System.out.println(node.getClass().getSimpleName() + " " + p );
}
public void inAConvertBoolExpression(AConvertBoolExpression node) {
@@ -128,7 +126,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
@Override
public void inAMultOrCartExpression(AMultOrCartExpression node) {
- BType type = typeTable.get(node);
+ BType type = typechecker.getType(node);
Precedence p;
if (type instanceof IntegerType) {
@@ -149,7 +147,7 @@ public class PrecedenceCollector extends DepthFirstAdapter {
@Override
public void inAMinusOrSetSubtractExpression(
AMinusOrSetSubtractExpression node) {
- BType type = typeTable.get(node);
+ BType type = typechecker.getType(node);
Precedence p;
if (type instanceof IntegerType) {
// minus
diff --git a/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
index 708bf5ab9364637a3a20f2175f7f10340afc903c..b9f0d82efcc5b1851776095fe5c56c2b409a1561 100644
--- a/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
+++ b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
@@ -73,6 +73,7 @@ public class PrimedNodesMarker extends DepthFirstAdapter {
for (PExpression e : copy) {
Node ref = machineContext.getReferences().get(e);
nodesToPrime.add(ref);
+ primedNodes.add(e);
}
node.getPredicate().apply(this);
nodesToPrime = null;
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index 7308851035e3c6443a93f98aed80e6e049e5f9ee..396464f5823680470027401c0b7242ccfec7fbbf 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -3,10 +3,10 @@ package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
-import java.util.Iterator;
import java.util.LinkedHashMap;
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;
@@ -122,11 +122,11 @@ public class Renamer extends DepthFirstAdapter {
}
private void evalEnumValues() {
- LinkedHashMap<String, Node> map = machineContext.getEnumValues();
- Iterator<String> iter = map.keySet().iterator();
- while (iter.hasNext()) {
- String name = iter.next();
- Node node = map.get(name);
+
+ for (Entry<String, Node> entry : machineContext.getEnumValues()
+ .entrySet()) {
+ String name = entry.getKey();
+ Node node = entry.getValue();
if (name.indexOf('_') == 1) {
name = name.replaceFirst("_", "1_");
@@ -139,9 +139,8 @@ public class Renamer extends DepthFirstAdapter {
}
public void evalGlobalNames(LinkedHashMap<String, Node> map) {
- Iterator<String> iter = map.keySet().iterator();
- while (iter.hasNext()) {
- String name = iter.next();
+ for (Entry<String, Node> entry : map.entrySet()) {
+ String name = entry.getKey();
String newName = incName(name);
namesTable.put(map.get(name), newName);
globalNames.add(newName);
@@ -207,7 +206,7 @@ public class Renamer extends DepthFirstAdapter {
return true;
// TODO check only if the standard module is extended
- if(StandardMadules.functions.contains(name))
+ if (StandardMadules.functions.contains(name))
return true;
if (SequencesKeywords.contains(name))
return true;
diff --git a/src/main/java/de/tlc4b/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
index 34d0e2277db51046e9aca1e8cc5b1db1a6681328..a81f8f71e81754fef4c96322581a3843bed83642 100644
--- a/src/main/java/de/tlc4b/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -4,8 +4,11 @@ import java.util.ArrayList;
import java.util.HashSet;
import java.util.Set;
-public class StandardMadules {
+public final class StandardMadules {
+ private StandardMadules(){
+ }
+
// Functions
public static final String FUNC_RANGE = "Range";
public static final String FUNC_IMAGE = "Image";
@@ -19,8 +22,7 @@ public class StandardMadules {
public static final String FUNC_ASSIGN = "FuncAssign";
-
- public static ArrayList<String> functions = new ArrayList<String>();
+ public static final ArrayList<String> functions = new ArrayList<String>();
static {
functions.add(FUNC_RANGE);
functions.add(FUNC_ID);
@@ -37,11 +39,22 @@ public class StandardMadules {
public static final String TOTAL_SURJECTIVE_FUNCTION = "TotalSurFunc";
public static final String TOTAL_BIJECTIVE_FUNCTION = "TotalBijFunc";
+
+ /** Sets of Partial functions **/
public static final String PARTIAL_FUNCTION = "ParFunc";
+ public static final String PARTIAL_FUNCTION_ELEMENT_OF = "ParFuncEleOf";
+ public static final String ELEMENT_OF_PARTIAL_FUNCTION = "isEleOfParFunc";
+
+ // injective
public static final String PARTIAL_INJECTIVE_FUNCTION = "ParInjFunc";
+ public static final String PARTIAL_INJECTIVE_FUNCTION_ELEMENT_OF = "ParInjFuncEleOf";
+ // surjective
public static final String PARTIAL_SURJECTIVE_FUNCTION = "ParSurFunc";
+ public static final String PARTIAL_SURJECTIVE_FUNCTION_ELEMENT_OF = "ParSurFuncEleOf";
+ // bijective
public static final String PARITAL_BIJECTIVE_FUNCTION = "ParBijFunc";
-
+ public static final String PARITAL_BIJECTIVE_FUNCTION_ELEMENT_OF = "ParBijFuncEleOf";
+
// Relations
public static final String RELATIONS = "Relations";
public static final String REL_DOMAIN = "RelDomain";
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 728216139ed7d28420570feaca7a78133d212641..53f6f16d2767760396bea09d9f721e51b8f36366 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -5,9 +5,9 @@ import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.Hashtable;
-import java.util.LinkedHashMap;
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;
@@ -82,10 +82,6 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
node.getPredicate().apply(this);
}
- public Hashtable<Node, BType> getTypes() {
- return types;
- }
-
public MachineContext getContext() {
return machineContext;
}
@@ -304,13 +300,12 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- LinkedHashMap<String, Node> parameter = machineContext
- .getScalarParameter();
- for (String c : parameter.keySet()) {
- Node n = parameter.get(c);
+ for (Entry<String, Node> entry : machineContext.getScalarParameter().entrySet()) {
+ String name = entry.getKey();
+ Node n = entry.getValue();
if (getType(n).isUntyped()) {
throw new TypeErrorException(
- "Can not infer type of parameter '" + c + "'");
+ "Can not infer type of parameter '" + name + "'");
}
}
}
@@ -321,9 +316,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
}
- LinkedHashMap<String, Node> constants = machineContext.getConstants();
- for (String c : constants.keySet()) {
- Node n = constants.get(c);
+ for (Entry<String, Node> entry : machineContext.getConstants()
+ .entrySet()) {
+ String c = entry.getKey();
+ Node n = entry.getValue();
if (getType(n).isUntyped()) {
throw new TypeErrorException("Can not infer type of constant '"
+ c + "': " + getType(n));
@@ -335,9 +331,10 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
public void caseAInvariantMachineClause(AInvariantMachineClause node) {
setType(node.getPredicates(), BoolType.getInstance());
node.getPredicates().apply(this);
- LinkedHashMap<String, Node> variables = machineContext.getVariables();
- for (String c : variables.keySet()) {
- Node n = variables.get(c);
+ for (Entry<String, Node> entry : machineContext.getVariables()
+ .entrySet()) {
+ String c = entry.getKey();
+ Node n = entry.getValue();
if (getType(n).isUntyped()) {
throw new TypeErrorException("Can not infer type of variable '"
+ c + "'");
@@ -1324,7 +1321,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
BType expected = getType(node);
try {
- found = found.unify(expected, this);
+ found.unify(expected, this);
} catch (UnificationException e) {
throw new TypeErrorException("Excepted '" + expected + "' , found "
+ found + "'");
@@ -1657,13 +1654,21 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getLeft(), new SetType(dom));
setType(node.getRight(), new SetType(ran));
BType expected = getType(node);
- BType found = new SetType(new SetType(new PairType(dom, ran)));
+ BType found = evalFunctionTypeVsRelationType(node, dom, ran);
unify(expected, found, node);
node.getLeft().apply(this);
node.getRight().apply(this);
// evalFunction(node, node.getLeft(), node.getRight());
}
+ private BType evalFunctionTypeVsRelationType(Node node, BType dom, BType ran) {
+ String clazz = node.parent().getClass().getName();
+ if (clazz.contains("Total") || clazz.contains("Partial"))
+ return new SetType(new SetType(new PairType(dom, ran)));
+ else
+ return new SetType(new FunctionType(dom, ran));
+ }
+
@Override
public void caseATotalInjectionExpression(ATotalInjectionExpression node) {
evalFunction(node, node.getLeft(), node.getRight());
@@ -1676,7 +1681,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getLeft(), new SetType(dom));
setType(node.getRight(), new SetType(ran));
BType expected = getType(node);
- BType found = new SetType(new SetType(new PairType(dom, ran)));
+ BType found = evalFunctionTypeVsRelationType(node, dom, ran);
unify(expected, found, node);
node.getLeft().apply(this);
node.getRight().apply(this);
@@ -1697,7 +1702,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getLeft(), new SetType(dom));
setType(node.getRight(), new SetType(ran));
BType expected = getType(node);
- BType found = new SetType(new SetType(new PairType(dom, ran)));
+ BType found = evalFunctionTypeVsRelationType(node, dom, ran);
unify(expected, found, node);
node.getLeft().apply(this);
node.getRight().apply(this);
@@ -1716,7 +1721,7 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
setType(node.getLeft(), new SetType(dom));
setType(node.getRight(), new SetType(ran));
BType expected = getType(node);
- BType found = new SetType(new SetType(new PairType(dom, ran)));
+ BType found = evalFunctionTypeVsRelationType(node, dom, ran);
unify(expected, found, node);
node.getLeft().apply(this);
node.getRight().apply(this);
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 57584ed6070489669f5235c456c923b5619e711f..6ae2ca1753166ebc4dc70dc1273e7e376e850f62 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -47,7 +47,6 @@ import de.be4.classicalb.core.parser.node.ALessPredicate;
import de.be4.classicalb.core.parser.node.AMaxExpression;
import de.be4.classicalb.core.parser.node.AMinExpression;
import de.be4.classicalb.core.parser.node.AMinIntExpression;
-import de.be4.classicalb.core.parser.node.AMinusExpression;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AModuloExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
@@ -142,17 +141,8 @@ public class UsedStandardModules extends DepthFirstAdapter {
for (Node node : typeRestrictor.getAllRestrictedNodes()) {
node.apply(this);
}
-
- start.apply(this);
- }
-
- class StandardModuleComparator implements Comparator<STANDARD_MODULES> {
- public int compare(STANDARD_MODULES s1, STANDARD_MODULES s2) {
- Integer i1 = new Integer(modules.indexOf(s1));
- Integer i2 = new Integer(modules.indexOf(s2));
- return i1.compareTo(i2);
- }
+ start.apply(this);
}
public ArrayList<STANDARD_MODULES> getUsedModules() {
@@ -161,7 +151,15 @@ public class UsedStandardModules extends DepthFirstAdapter {
if (list.contains(STANDARD_MODULES.Integers)) {
list.remove(STANDARD_MODULES.Naturals);
}
- Collections.sort(list, new StandardModuleComparator());
+ Collections.sort(list, new Comparator<STANDARD_MODULES>() {
+ public int compare(STANDARD_MODULES s1, STANDARD_MODULES s2) {
+ Integer i1 = Integer.valueOf(modules.indexOf(s1));
+ Integer i2 = Integer.valueOf(modules.indexOf(s2));
+ return i1.compareTo(i2);
+ }
+ }
+
+ );
return list;
}
@@ -173,7 +171,7 @@ public class UsedStandardModules extends DepthFirstAdapter {
@Override
public void inAExpressionDefinitionDefinition(
AExpressionDefinitionDefinition node) {
- if (TLC4BGlobals.isForceTLCToEvalConstants()){
+ if (TLC4BGlobals.isForceTLCToEvalConstants()) {
usedStandardModules.add(STANDARD_MODULES.TLC);
}
}
@@ -222,11 +220,6 @@ public class UsedStandardModules extends DepthFirstAdapter {
usedStandardModules.add(STANDARD_MODULES.Naturals);
}
- public void inAMinusExpression(AMinusExpression node) {
- // TODO what is a AMinusExpression
- usedStandardModules.add(STANDARD_MODULES.Naturals);
- }
-
public void inAIntervalExpression(AIntervalExpression node) {
usedStandardModules.add(STANDARD_MODULES.Naturals);
}
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java b/src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java
index 932d2dcde522c3d2f974f43464afc5f0a88e074c..e4b9f595bc773c9f501bca2726a9e2056564159c 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java
@@ -39,7 +39,7 @@ public class IdentifierDependencies extends DepthFirstAdapter {
@Override
public void caseAIdentifierExpression(AIdentifierExpression node) {
- Node refNode = machineContext.getReferences().get(node);
+ Node refNode = machineContext.getReferenceNode(node);
if(refNode == null)
refNode = node;
HashSet<Node> set = new HashSet<Node>();
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 12a36d5f4f2c5a2a88608dd5823997a6143ce0d0..754dca4cbaa30db638d136dc0f932b8e41fe0835 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -9,6 +9,7 @@ import java.util.Set;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
+import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
@@ -98,7 +99,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
HashSet<Node> list = new HashSet<Node>();
list.add(id);
analysePredicate(bNode, list, new HashSet<Node>());
-
+
PExpression e = (PExpression) id;
HashSet<PExpression> set = new HashSet<PExpression>();
set.add(e);
@@ -109,7 +110,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
HashSet<Node> list = new HashSet<Node>();
list.add(id);
analysePredicate(bNode, list, new HashSet<Node>());
-
+
PExpression e = (PExpression) id;
HashSet<PExpression> set = new HashSet<PExpression>();
set.add(e);
@@ -151,7 +152,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
@Override
public void inAConstraintsMachineClause(AConstraintsMachineClause node) {
HashSet<Node> list = new HashSet<Node>();
- //list.addAll(machineContext.getSetParamter().values());
+ // list.addAll(machineContext.getSetParamter().values());
list.addAll(machineContext.getScalarParameter().values());
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
HashSet<PExpression> set = new HashSet<PExpression>();
@@ -186,19 +187,22 @@ public class TypeRestrictor extends DepthFirstAdapter {
private void analysePredicate(Node n, HashSet<Node> list,
HashSet<Node> ignoreList) {
- if(removedNodes.contains(n))
+ if (removedNodes.contains(n))
return;
-
+
if (n instanceof AEqualPredicate) {
PExpression left = ((AEqualPredicate) n).getLeft();
- Node r_left = machineContext.getReferences().get(left);
+ Node r_left = machineContext.getReferenceNode(left);
PExpression right = ((AEqualPredicate) n).getRight();
- Node r_right = machineContext.getReferences().get(right);
+ Node r_right = machineContext.getReferenceNode(right);
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
ArrayList<PExpression> element = new ArrayList<PExpression>();
element.add(right);
+ if (machineContext.getVariables().values().contains(r_left)) {
+ r_left = variablesHashTable.get(r_left);
+ }
putRestrictedType(r_left, new ASetExtensionExpression(element));
removedNodes.add(n);
}
@@ -206,6 +210,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
&& isAConstantExpression(right, list, ignoreList)) {
ArrayList<PExpression> element = new ArrayList<PExpression>();
element.add(right);
+ if (machineContext.getVariables().values().contains(r_right)) {
+ r_right = variablesHashTable.get(r_right);
+ }
putRestrictedType(r_right, new ASetExtensionExpression(element));
removedNodes.add(n);
}
@@ -214,10 +221,13 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (n instanceof AMemberPredicate) {
PExpression left = ((AMemberPredicate) n).getLeft();
- Node r_left = machineContext.getReferences().get(left);
+ Node r_left = machineContext.getReferenceNode(left);
PExpression right = ((AMemberPredicate) n).getRight();
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
+ if (machineContext.getVariables().values().contains(r_left)) {
+ r_left = variablesHashTable.get(r_left);
+ }
putRestrictedType(r_left, right);
removedNodes.add(n);
}
@@ -226,10 +236,13 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (n instanceof ANotMemberPredicate) {
PExpression left = ((ANotMemberPredicate) n).getLeft();
- Node r_left = machineContext.getReferences().get(left);
+ Node r_left = machineContext.getReferenceNode(left);
PExpression right = ((ANotMemberPredicate) n).getRight();
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
+ if (machineContext.getVariables().values().contains(r_left)) {
+ r_left = variablesHashTable.get(r_left);
+ }
putSubstractedType(r_left, right);
removedNodes.add(n);
}
@@ -238,11 +251,14 @@ public class TypeRestrictor extends DepthFirstAdapter {
if (n instanceof ASubsetPredicate) {
PExpression left = ((ASubsetPredicate) n).getLeft();
- Node r_left = machineContext.getReferences().get(left);
+ Node r_left = machineContext.getReferenceNode(left);
PExpression right = ((ASubsetPredicate) n).getRight();
if (list.contains(r_left)
&& isAConstantExpression(right, list, ignoreList)) {
+ if (machineContext.getVariables().values().contains(r_left)) {
+ r_left = variablesHashTable.get(r_left);
+ }
putRestrictedType(r_left, new APowSubsetExpression(right));
removedNodes.add(n);
}
@@ -250,10 +266,15 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
if (n instanceof AConjunctPredicate) {
- analysePredicate(((AConjunctPredicate) n).getLeft(), list,
+ Node left = ((AConjunctPredicate) n).getLeft();
+ Node right = ((AConjunctPredicate) n).getRight();
+ analysePredicate(left, list,
ignoreList);
- analysePredicate(((AConjunctPredicate) n).getRight(), list,
+ analysePredicate(right, list,
ignoreList);
+ if(removedNodes.contains(left) && removedNodes.contains(right)){
+ removedNodes.add(n);
+ }
return;
}
@@ -299,7 +320,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
AImplicationPredicate implication = (AImplicationPredicate) node
.getImplication();
analysePredicate(implication.getLeft(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
@Override
@@ -311,7 +333,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
@Override
@@ -323,7 +346,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
@Override
@@ -336,7 +360,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
@Override
@@ -348,7 +373,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
@Override
@@ -360,7 +386,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
public void inAGeneralSumExpression(AGeneralSumExpression node) {
@@ -371,7 +398,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
public void inAGeneralProductExpression(AGeneralProductExpression node) {
@@ -382,7 +410,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
list.add(e);
}
analysePredicate(node.getPredicates(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
private Hashtable<Node, HashSet<PExpression>> expectedIdentifieListTable = new Hashtable<Node, HashSet<PExpression>>();
@@ -441,7 +470,8 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
list.addAll(getExpectedIdentifier(node));
analysePredicate(node.getWhere(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
}
@Override
@@ -454,7 +484,28 @@ public class TypeRestrictor extends DepthFirstAdapter {
}
list.addAll(getExpectedIdentifier(node));
analysePredicate(node.getPredicate(), list, new HashSet<Node>());
- createRestrictedTypeofLocalVariables(new HashSet<PExpression>(node.getIdentifiers()));
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(
+ node.getIdentifiers()));
+ }
+
+ private Hashtable<Node, Node> variablesHashTable;
+
+ public void inABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
+ if(!(node.getPredicate() instanceof AExistsPredicate)){
+ variablesHashTable = new Hashtable<Node, Node>();
+
+ HashSet<Node> list = new HashSet<Node>();
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+ for (PExpression e : copy) {
+ Node ref = machineContext.getReferenceNode(e);
+
+ list.add(ref);
+ variablesHashTable.put(ref, e);
+ }
+ analysePredicate(node.getPredicate(), list, new HashSet<Node>());
+ createRestrictedTypeofLocalVariables(new HashSet<PExpression>(copy));
+ }
}
private void createRestrictedTypeofLocalVariables(Set<PExpression> copy) {
@@ -463,6 +514,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
ArrayList<Node> restrictedList = restrictedNodeTable.get(e);
if (restrictedList == null) {
BType conType = typechecker.getType(e);
+ if (conType == null) {
+ conType = typechecker.getType(machineContext
+ .getReferenceNode(e));
+ }
tree = conType.createSyntaxTreeNode(typechecker);
} else {
tree = (PExpression) restrictedList.get(0);
diff --git a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
index a59cfb9db15a4a68feec53be6016b58765f2ccb2..db63b09f68eafafc39d3cf1eee91341cca77392e 100644
--- a/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
@@ -43,7 +43,7 @@ import de.tlc4b.exceptions.SubstitutionException;
*/
public class AssignedVariablesFinder extends DepthFirstAdapter {
- private final Hashtable<Node, HashSet<Node>> assignedVariablesTable;
+ protected final Hashtable<Node, HashSet<Node>> assignedVariablesTable;
private final MachineContext machineContext;
public AssignedVariablesFinder(MachineContext machineContext) {
@@ -53,7 +53,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
}
- public Hashtable<Node, HashSet<Node>> getAssignedVariablesTable() {
+ protected Hashtable<Node, HashSet<Node>> getAssignedVariablesTable() {
return assignedVariablesTable;
}
@@ -124,7 +124,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
node.getIdentifiers());
HashSet<Node> list = new HashSet<Node>();
for (PExpression e : copy) {
- Node identifier = machineContext.getReferences().get(e);
+ Node identifier = machineContext.getReferenceNode(e);
list.add(identifier);
}
assignedVariablesTable.put(node, list);
@@ -137,11 +137,11 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
HashSet<Node> list = new HashSet<Node>();
for (PExpression e : copy) {
if (e instanceof AIdentifierExpression) {
- Node identifier = machineContext.getReferences().get(e);
+ Node identifier = machineContext.getReferenceNode(e);
list.add(identifier);
} else {
AFunctionExpression func = (AFunctionExpression) e;
- Node identifier = machineContext.getReferences().get(
+ Node identifier = machineContext.getReferenceNode(
func.getIdentifier());
list.add(identifier);
}
@@ -158,7 +158,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
node.getIdentifiers());
HashSet<Node> list = new HashSet<Node>();
for (PExpression e : copy) {
- Node identifier = machineContext.getReferences().get(e);
+ Node identifier = machineContext.getReferenceNode(e);
list.add(identifier);
}
assignedVariablesTable.put(node, list);
@@ -278,7 +278,7 @@ public class AssignedVariablesFinder extends DepthFirstAdapter {
@Override
public void caseADefinitionSubstitution(ADefinitionSubstitution node) {
- Node refNode = machineContext.getReferences().get(node);
+ Node refNode = machineContext.getReferenceNode(node);
HashSet<Node> assignedVariables = assignedVariablesTable.get(refNode);
assignedVariablesTable.put(node, assignedVariables);
assignedVariablesTable.put(node.parent(), assignedVariables);
diff --git a/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java b/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
index c49be299a838dfc1b494e793f3fd8aba0362f615..0bfd4b8466b4857c45cd0b3ead978285388b71cd 100644
--- a/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
+++ b/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
@@ -17,19 +17,17 @@ public abstract class AbstractHasFollowers implements BType{
}
public String printFollower(){
- String res = "[";
+ StringBuffer res = new StringBuffer();
+ res.append("[");
for (Object o : followers) {
if(!(o instanceof Node)){
- res+= o.hashCode();
- res+= o.getClass();
- //IntegerOrSetOfPairType i = (IntegerOrSetOfPairType) o;
- res += " ";
+ res.append(o.hashCode());
+ res.append(o.getClass());
+ res.append(" ");
}
-
-
}
- res+= "]";
- return res;
+ res.append("]");
+ return res.toString();
}
public void deleteFollower(Object obj){
diff --git a/src/main/java/de/tlc4b/btypes/FunctionType.java b/src/main/java/de/tlc4b/btypes/FunctionType.java
index 3653f2d1a397f9c20acfc329928ac98fbaad453b..cb16e85bdd34ee866e5f070c49b77e9a904ee0f2 100644
--- a/src/main/java/de/tlc4b/btypes/FunctionType.java
+++ b/src/main/java/de/tlc4b/btypes/FunctionType.java
@@ -1,6 +1,6 @@
package de.tlc4b.btypes;
-import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
+import de.be4.classicalb.core.parser.node.APartialFunctionExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.tlc4b.analysis.Typechecker;
import de.tlc4b.exceptions.UnificationException;
@@ -129,7 +129,7 @@ public class FunctionType extends AbstractHasFollowers {
}
public PExpression createSyntaxTreeNode(Typechecker typechecker) {
- ATotalFunctionExpression node = new ATotalFunctionExpression(
+ APartialFunctionExpression node = new APartialFunctionExpression(
domain.createSyntaxTreeNode(typechecker),
range.createSyntaxTreeNode(typechecker));
typechecker.setType(node, new SetType(this));
diff --git a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
index f1a83cda661e3d466ac33566f05d2532bce78359..a8d378e3bd85c1253a8c59e758abe5f5d5b2f1f3 100644
--- a/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
@@ -212,15 +212,11 @@ public class IntegerOrSetOfPairType extends AbstractHasFollowers {
if (this.first.equals(other) || this.second.equals(other)) {
return true;
}
- if (first instanceof AbstractHasFollowers) {
- if (((AbstractHasFollowers) first).contains(other))
- return true;
- }
- if (second instanceof AbstractHasFollowers) {
- if (((AbstractHasFollowers) second).contains(other))
- return true;
- }
- return false;
+
+ if(first.contains(other) || second.contains(other)){
+ return true;
+ }else
+ return false;
}
public String getTlaType() {
diff --git a/src/main/java/de/tlc4b/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
index 79d4298dd51190b49777998eab335557d6ab0b78..a559e315c2fb8f28619c997e420315355ed29353 100644
--- a/src/main/java/de/tlc4b/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -41,18 +41,20 @@ public class StructType extends AbstractHasFollowers {
@Override
public String toString() {
- String res = "struct(";
+ StringBuffer res = new StringBuffer();
+ res.append("struct(");
+
Iterator<String> keys = types.keySet().iterator();
if (!keys.hasNext())
- res += "...";
+ res.append("...");
while (keys.hasNext()) {
String fieldName = (String) keys.next();
- res += fieldName + ":" + types.get(fieldName);
+ res.append(fieldName + ":" + types.get(fieldName));
if (keys.hasNext())
- res += ",";
+ res.append(",");
}
- res += ")";
- return res;
+ res.append(")");
+ return res.toString();
}
public void update(BType oldType, BType newType) {
@@ -170,18 +172,19 @@ public class StructType extends AbstractHasFollowers {
}
public String getTlaType() {
- String res = "[";
+ StringBuffer res = new StringBuffer();
+ res.append("[");
Iterator<String> keys = types.keySet().iterator();
if (!keys.hasNext())
- res += "...";
+ res.append("...");
while (keys.hasNext()) {
String fieldName = (String) keys.next();
- res += fieldName + ":" + types.get(fieldName);
+ res.append(fieldName + ":" + types.get(fieldName));
if (keys.hasNext())
- res += ",";
+ res.append(",");
}
- res += "]";
- return res;
+ res.append("]");
+ return res.toString();
}
public boolean containsIntegerType() {
diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index 9f9bd433e38774396bb4bd41de7ae80009bbe815..e8befd7778f176842a1678061824aff13c539c40 100644
--- a/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -34,7 +34,6 @@ import de.be4.ltl.core.parser.node.AYesterdayLtl;
import de.be4.ltl.core.parser.node.PLtl;
import de.be4.ltl.core.parser.node.Start;
import de.be4.ltl.core.parser.parser.Parser;
-import de.tlc4b.analysis.Ast2String;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.typerestriction.TypeRestrictor;
import de.tlc4b.exceptions.LTLParseException;
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 3f62753cc6b182b9a0e3d36424b33691e22993f8..9c2a523e1b5d2b5352d6c0720a4fc91480d8ff15 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -351,7 +351,7 @@ public class TLAPrinter extends DepthFirstAdapter {
ArrayList<Node> inits = this.tlaModule.getInitPredicates();
if (inits.size() == 0)
return;
- tlaModuleString.append("Init == ");
+ tlaModuleString.append("Init ==\n\t/\\ ");
for (int i = 0; i < inits.size(); i++) {
Node init = inits.get(i);
if (init instanceof ADisjunctPredicate) {
@@ -362,9 +362,9 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append(")");
}
if (i < inits.size() - 1)
- tlaModuleString.append(" /\\ ");
+ tlaModuleString.append("\n\t/\\ ");
}
- tlaModuleString.append("\n");
+ tlaModuleString.append("\n\n");
}
private void printOperations() {
@@ -542,8 +542,31 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseABecomesSuchSubstitution(ABecomesSuchSubstitution node) {
- node.getPredicate().apply(this);
+ inABecomesSuchSubstitution(node);
+ if (node.getPredicate() instanceof AExistsPredicate) {
+ node.getPredicate().apply(this);
+ } else {
+ List<PExpression> copy = new ArrayList<PExpression>(
+ node.getIdentifiers());
+
+ for (int i = 0; i < copy.size(); i++) {
+ PExpression e = copy.get(i);
+ e.apply(this);
+ tlaModuleString.append(" \\in ");
+ typeRestrictor.getRestrictedNode(e).apply(this);
+ if (i < copy.size() - 1) {
+ tlaModuleString.append(" /\\ ");
+ }
+ }
+
+ if (!typeRestrictor.isARemovedNode(node.getPredicate())) {
+ tlaModuleString.append(" /\\ ");
+ node.getPredicate().apply(this);
+ }
+ }
+
printUnchangedVariables(node, true);
+ outABecomesSuchSubstitution(node);
}
private void printNormalAssignment(PExpression left, PExpression right) {
@@ -813,10 +836,19 @@ public class TLAPrinter extends DepthFirstAdapter {
e.apply(this);
}
if (node.getElse() != null) {
+ tlaModuleString.append(" \\/ (");
+ tlaModuleString.append("~(");
+ for (PSubstitution e : copy) {
+ ASelectWhenSubstitution w = (ASelectWhenSubstitution) e;
+ tlaModuleString.append(" \\/ ");
+ w.getCondition().apply(this);
+ }
+ tlaModuleString.append(")");
tlaModuleString.append(" /\\ ");
node.getElse().apply(this);
+ tlaModuleString.append(")");
}
-
+
if (missingVariableFinder.hasUnchangedVariables(node)
&& (copy.size() > 0 || node.getElse() != null)) {
tlaModuleString.append(")");
@@ -857,7 +889,7 @@ public class TLAPrinter extends DepthFirstAdapter {
if (!typeRestrictor.isARemovedNode(node.getWhere())) {
node.getWhere().apply(this);
- tlaModuleString.append("\n\t/\\ ");
+ tlaModuleString.append(" /\\ ");
}
node.getThen().apply(this);
@@ -885,7 +917,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
node.getPredicate().apply(this);
- tlaModuleString.append("\n\t/\\ ");
+ tlaModuleString.append(" /\\ ");
node.getSubstitution().apply(this);
printUnchangedVariables(node, true);
@@ -1006,25 +1038,19 @@ public class TLAPrinter extends DepthFirstAdapter {
public void caseAConjunctPredicate(AConjunctPredicate node) {
boolean left = typeRestrictor.isARemovedNode(node.getLeft());
boolean right = typeRestrictor.isARemovedNode(node.getRight());
- int i = left ? (right ? 1 : 2) : (right ? 3 : 4);
-
- switch (i) {
- case 1: // remove both
+
+ if(left && right){
tlaModuleString.append("TRUE");
- break;
- case 2: // remove left
+ } else if (left){
node.getRight().apply(this);
- break;
- case 3: // remove right
+ } else if (right){
node.getLeft().apply(this);
- break;
- case 4:
+ }else{
inAConjunctPredicate(node);
node.getLeft().apply(this);
tlaModuleString.append(" /\\ ");
node.getRight().apply(this);
outAConjunctPredicate(node);
- break;
}
}
@@ -1700,7 +1726,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
}
- private boolean isElementOf(Node node) {
+ private boolean isElementOfRecursive(Node node) {
Node parent = node.parent();
if (parent instanceof AMemberPredicate
&& !typeRestrictor.isARemovedNode(parent)
@@ -1710,7 +1736,7 @@ public class TLAPrinter extends DepthFirstAdapter {
} else {
String clazz = parent.getClass().getName();
if (clazz.contains("Total") || clazz.contains("Partial")) {
- return isElementOf(node.parent());
+ return isElementOfRecursive(node.parent());
} else
return false;
}
@@ -1723,7 +1749,7 @@ public class TLAPrinter extends DepthFirstAdapter {
if (subtype instanceof FunctionType) {
tlaModuleString.append(funcName);
} else {
- if (isElementOf(node)) {
+ if (isElementOfRecursive(node)) {
tlaModuleString.append(relEleOfName);
} else {
tlaModuleString.append(relName);
@@ -1760,36 +1786,53 @@ public class TLAPrinter extends DepthFirstAdapter {
node.getRight());
}
- @Override
- public void caseAPartialFunctionExpression(APartialFunctionExpression node) {
+ private void setOfPartialFuntions(Node node, String funcName,
+ String funcEleOfName, String relName, String relEleOfName,
+ Node left, Node right) {
BType type = this.typechecker.getType(node);
BType subtype = ((SetType) type).getSubtype();
if (subtype instanceof FunctionType) {
Node parent = node.parent();
if (parent instanceof AMemberPredicate
- && !typeRestrictor.isARemovedNode(parent)
- // && !this.tlaModule.getInitPredicates().contains(parent)
- ) {
- AMemberPredicate member = (AMemberPredicate) parent;
- tlaModuleString.append("isParFunc(");
- member.getLeft().apply(this);
- tlaModuleString.append(",");
- node.getLeft().apply(this);
- tlaModuleString.append(",");
- node.getRight().apply(this);
+ && !typeRestrictor.isARemovedNode(parent)) {
+ tlaModuleString.append(funcEleOfName);
+ tlaModuleString.append("(");
+ ((AMemberPredicate) parent).getLeft().apply(this);
+ tlaModuleString.append(", ");
+ left.apply(this);
+ tlaModuleString.append(", ");
+ right.apply(this);
tlaModuleString.append(")");
return;
+ }else {
+ tlaModuleString.append(funcName);
+ }
+ } else {
+ if (isElementOfRecursive(node)) {
+ tlaModuleString.append(relEleOfName);
+ } else {
+ tlaModuleString.append(relName);
}
}
+ tlaModuleString.append("(");
+ left.apply(this);
+ tlaModuleString.append(", ");
+ right.apply(this);
+ tlaModuleString.append(")");
+ }
- setOfFuntions(node, PARTIAL_FUNCTION, REL_PARTIAL_FUNCTION,
+ @Override
+ public void caseAPartialFunctionExpression(APartialFunctionExpression node) {
+ setOfPartialFuntions(node, PARTIAL_FUNCTION,
+ PARTIAL_FUNCTION_ELEMENT_OF, REL_PARTIAL_FUNCTION,
REL_PARTIAL_FUNCTION_ELEMENT_OF, node.getLeft(),
node.getRight());
}
@Override
public void caseAPartialInjectionExpression(APartialInjectionExpression node) {
- setOfFuntions(node, PARTIAL_INJECTIVE_FUNCTION,
+ setOfPartialFuntions(node, PARTIAL_INJECTIVE_FUNCTION,
+ PARTIAL_INJECTIVE_FUNCTION_ELEMENT_OF,
REL_PARTIAL_INJECTIVE_FUNCTION,
REL_PARTIAL_INJECTIVE_FUNCTION_ELEMENT_OF, node.getLeft(),
node.getRight());
@@ -1798,7 +1841,8 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAPartialSurjectionExpression(
APartialSurjectionExpression node) {
- setOfFuntions(node, PARTIAL_SURJECTIVE_FUNCTION,
+ setOfPartialFuntions(node, PARTIAL_SURJECTIVE_FUNCTION,
+ PARTIAL_SURJECTIVE_FUNCTION_ELEMENT_OF,
REL_PARTIAL_SURJECTIVE_FUNCTION,
REL_PARTIAL_SURJECTIVE_FUNCTION_ELEMENT_OF, node.getLeft(),
node.getRight());
@@ -1806,7 +1850,8 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAPartialBijectionExpression(APartialBijectionExpression node) {
- setOfFuntions(node, PARITAL_BIJECTIVE_FUNCTION,
+ setOfPartialFuntions(node, PARITAL_BIJECTIVE_FUNCTION,
+ PARITAL_BIJECTIVE_FUNCTION_ELEMENT_OF,
REL_PARTIAL_BIJECTIVE_FUNCTION,
REL_PARTIAL_BIJECTIVE_FUNCTION_ELEMENT_OF, node.getLeft(),
node.getRight());
@@ -2011,17 +2056,12 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseASubsetPredicate(ASubsetPredicate node) {
- if (node.getRight() == null) {
- tlaModuleString.append("TRUE");
- return;
- }
-
inASubsetPredicate(node);
node.getLeft().apply(this);
- //tlaModuleString.append(" \\in SUBSET(");
+ // tlaModuleString.append(" \\in SUBSET(");
tlaModuleString.append(" \\subseteq ");
node.getRight().apply(this);
- //tlaModuleString.append(")");
+ // tlaModuleString.append(")");
outASubsetPredicate(node);
}
@@ -2085,14 +2125,22 @@ public class TLAPrinter extends DepthFirstAdapter {
node.getExpression().apply(this);
tlaModuleString.append(": ");
printIdentifierList(copy);
- tlaModuleString.append(" \\in {");
- printIdentifierList(copy);
- tlaModuleString.append(" \\in ");
- printTypesOfIdentifierList(copy);
- tlaModuleString.append(": ");
- node.getPredicates().apply(this);
- tlaModuleString.append("}");
- tlaModuleString.append("})");
+ if (typeRestrictor.isARemovedNode(node.getPredicates())) {
+ tlaModuleString.append(" \\in ");
+ printTypesOfIdentifierList(copy);
+ tlaModuleString.append("})");
+ return;
+ } else {
+ tlaModuleString.append(" \\in {");
+ printIdentifierList(copy);
+ tlaModuleString.append(" \\in ");
+ printTypesOfIdentifierList(copy);
+ tlaModuleString.append(": ");
+ node.getPredicates().apply(this);
+ tlaModuleString.append("}");
+ tlaModuleString.append("})");
+ }
+
}
@Override
@@ -2105,14 +2153,21 @@ public class TLAPrinter extends DepthFirstAdapter {
node.getExpression().apply(this);
tlaModuleString.append(": ");
printIdentifierList(copy);
- tlaModuleString.append(" \\in {");
- printIdentifierList(copy);
- tlaModuleString.append(" \\in ");
- printTypesOfIdentifierList(copy);
- tlaModuleString.append(": ");
- node.getPredicates().apply(this);
- tlaModuleString.append("}");
- tlaModuleString.append("})");
+ if (typeRestrictor.isARemovedNode(node.getPredicates())) {
+ tlaModuleString.append(" \\in ");
+ printTypesOfIdentifierList(copy);
+ tlaModuleString.append("})");
+ return;
+ } else {
+ tlaModuleString.append(" \\in {");
+ printIdentifierList(copy);
+ tlaModuleString.append(" \\in ");
+ printTypesOfIdentifierList(copy);
+ tlaModuleString.append(": ");
+ node.getPredicates().apply(this);
+ tlaModuleString.append("}");
+ tlaModuleString.append("})");
+ }
}
/**
diff --git a/src/main/java/de/tlc4b/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
index a7a117d91003781f76948aca920d9c2e309a220c..61591cb733e0d0afd64f9acc833a36eeeeba7ae5 100644
--- a/src/main/java/de/tlc4b/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -6,6 +6,7 @@ import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
+import java.util.Map.Entry;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
@@ -238,16 +239,16 @@ public class Generator extends DepthFirstAdapter {
return;
LinkedHashMap<Node, Node> conValueTable = constantsEvaluator
.getValueOfIdentifierMap();
- Iterator<Node> cons = conValueTable.keySet().iterator();
- while (cons.hasNext()) {
- AIdentifierExpression con = (AIdentifierExpression) cons.next();
- Node value = conValueTable.get(con);
- // tlaModule.definitions.add(new TLADefinition(con, value));
-
+ Iterator<Entry<Node, Node>> iterator = conValueTable.entrySet().iterator();
+ while (iterator.hasNext()){
+ Entry<Node, Node> entry = iterator.next();
+ AIdentifierExpression con = (AIdentifierExpression) entry.getKey();
+ Node value = entry.getValue();
+
AExpressionDefinitionDefinition exprDef = new AExpressionDefinitionDefinition(
con.getIdentifier().get(0), new LinkedList<PExpression>(),
(PExpression) value.clone());
- machineContext.getReferences().put(exprDef, con);
+ machineContext.addReference(exprDef, con);
this.tlaModule.addToAllDefinitions(exprDef);
}
diff --git a/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
index 90e880a625b11bf9b90c7e8822a061e6e2c56c50..0bbc2d4eb0d118d691d2bb5126de82b786292d44 100644
--- a/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
@@ -12,13 +12,14 @@ public abstract class ConfigFileAssignment {
public abstract String getString(Renamer renamer);
public String getIdentifier(AIdentifierExpression node) {
- String res = "";
+ StringBuffer res = new StringBuffer();
+
List<TIdentifierLiteral> copy = new ArrayList<TIdentifierLiteral>(
node.getIdentifier());
for (TIdentifierLiteral e : copy) {
- res += e.getText();
+ res.append(e.getText());
}
- return res;
+ return res.toString();
}
}
diff --git a/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
index b08ca709fbf0d9c4f787b0b406947cc3df99a0ac..da43e2d1ed9e1ce40abcbde20d695b321e34212a 100644
--- a/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
@@ -8,29 +8,31 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.Renamer;
+
/**
*
- * This class represents an assignment in the configuration file.
- * The left side of the assignment is a constant and the right side a set of model values.
+ * This class represents an assignment in the configuration file. The left side
+ * of the assignment is a constant and the right side a set of model values.
* E.g. k = {k1, k2, k3}
*/
-public class SetOfModelValuesAssignment extends ConfigFileAssignment{
+public class SetOfModelValuesAssignment extends ConfigFileAssignment {
private Node node;
private int size;
public SetOfModelValuesAssignment(Node node, Integer size) {
this.node = node;
- if(size == null){
+ if (size == null) {
this.size = TLC4BGlobals.getDEFERRED_SET_SIZE();
- }else{
+ } else {
this.size = size;
}
-
+
}
public String getString(Renamer renamer) {
- String res = "";
+ StringBuffer res = new StringBuffer();
+
String conString;
if (node instanceof ADeferredSetSet) {
conString = "";
@@ -40,22 +42,21 @@ public class SetOfModelValuesAssignment extends ConfigFileAssignment{
conString += e.getText();
}
conString = renamer.getName(node);
- }else{
+ } else {
AIdentifierExpression id = (AIdentifierExpression) node;
conString = getIdentifier(id);
}
-
- res += conString + " = {";
+
+ res.append(conString).append(" = {");
for (int j = 1; j < size + 1; j++) {
- res += conString + j;
+ res.append(conString + j);
if (j < size) {
- res += ", ";
+ res.append(",");
}
}
- res += "}\n";
-
- return res;
+ res.append("}\n");
+
+ return res.toString();
}
-
-
+
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index 25b95a4654d1956f733495a96b362c388786e526..912acc2edf9b98507edd4702787b40551fd16f65 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -1,77 +1,75 @@
package de.tlc4b.tlc;
import java.util.Hashtable;
-import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Set;
+import java.util.Map.Entry;
import de.be4.classicalb.core.parser.node.Node;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.Renamer;
+import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType;
import de.tlc4b.tla.TLAModule;
public class TLCOutputInfo {
-
+
Hashtable<String, String> namesMapping;
Hashtable<String, BType> typesTable;
Set<String> constants;
- boolean constantSetup= false;
- private boolean init= false;
-
- public boolean hasInitialisation(){
- return init;
+ boolean constantSetup = false;
+ private boolean hasInit = false;
+
+ public boolean hasInitialisation() {
+ return hasInit;
}
-
- public String getBName(String tlaName){
+
+ public String getBName(String tlaName) {
return namesMapping.get(tlaName);
}
-
- public BType getBType(String tlaName){
+
+ public BType getBType(String tlaName) {
return typesTable.get(tlaName);
}
-
- public Hashtable<String, BType> getTypes(){
- return typesTable;
- }
-
- public void setConstantSetup(){
+
+ public void setConstantSetup() {
this.constantSetup = true;
}
-
- public boolean isAConstant(String tlaName){
+
+ public boolean isAConstant(String tlaName) {
return constants.contains(getBName(tlaName));
}
-
- public boolean hasConstants(){
- return constants.size()>0 || constantSetup;
+
+ public boolean hasConstants() {
+ return constants.size() > 0 || constantSetup;
}
-
+
public TLCOutputInfo(MachineContext machineContext, Renamer renamer,
- Hashtable<Node, BType> types, TLAModule tlaModule) {
-
- namesMapping = new Hashtable<String, String>();
- typesTable = new Hashtable<String, BType>();
- constants = machineContext.getConstants().keySet();
- init = tlaModule.getInitPredicates().size()>0;
-
- if(machineContext.getConstantsMachineClause() != null){
+ Typechecker typechecker, TLAModule tlaModule) {
+
+ this.namesMapping = new Hashtable<String, String>();
+ this.typesTable = new Hashtable<String, BType>();
+ this.constants = machineContext.getConstants().keySet();
+ this.hasInit = tlaModule.getInitPredicates().size() > 0;
+
+ if (machineContext.getConstantsMachineClause() != null) {
this.constantSetup = true;
}
-
+
LinkedHashMap<String, Node> identifiers = new LinkedHashMap<String, Node>();
identifiers.putAll(machineContext.getConstants());
identifiers.putAll(machineContext.getVariables());
identifiers.putAll(machineContext.getEnumValues());
+
- for (Iterator<String> iter = identifiers.keySet().iterator(); iter.hasNext();) {
- String name = iter.next();
- Node node = identifiers.get(name);
+ for (Entry<String, Node> entry : identifiers.entrySet()) {
+ String name = entry.getKey();
+ Node node = entry.getValue();
String newName = renamer.getNameOfRef(node);
namesMapping.put(newName, name);
- typesTable.put(newName, types.get(node));
+ typesTable.put(newName, typechecker.getType(node));
}
-
+
}
}
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 924e15be10562545da2ba4cac5744cff3fea4e51..d96e9a698b69661e96851c4637821fd428d14317 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -64,11 +64,12 @@ public class TLCResults {
evalTrace();
}
- if(tlcResult == NoError & tlcOutputInfo.hasInitialisation() & numberOfDistinctStates == 0){
+ if (tlcResult == NoError && tlcOutputInfo.hasInitialisation()
+ && numberOfDistinctStates == 0) {
// Can not setup constants
tlcResult = InitialStateError;
}
-
+
}
private void evalTrace() {
@@ -80,14 +81,16 @@ public class TLCResults {
printer = new TracePrinter(OutputCollector.getInitialState(),
tlcOutputInfo);
}
- traceString = printer.getTrace().toString();
+ if (printer != null) {
+ traceString = printer.getTrace().toString();
+ }
}
private void evalAllMessages() {
ArrayList<Message> messages = OutputCollector.getAllMessages();
for (Message m : messages) {
-
+
switch (m.getMessageClass()) {
case ERROR:
evalErrorMessage(m);
@@ -102,7 +105,8 @@ public class TLCResults {
case NONE:
evalStatusMessage(m);
break;
-
+ default:
+ break;
}
}
@@ -113,7 +117,7 @@ public class TLCResults {
}
private void evalStatusMessage(Message m) {
-
+
switch (m.getMessageCode()) {
case EC.TLC_STARTING:
@@ -135,12 +139,19 @@ public class TLCResults {
case EC.TLC_SUCCESS:
tlcResult = TLCResult.NoError;
break;
+
+ default:
+ break;
}
}
private void evalErrorMessage(Message m) {
- //System.out.println(m.getMessageCode() + " "+ m.getParameters().length);
+ // System.out.print(m.getMessageCode() + " "+ m.getParameters().length);
+ // for (int i = 0; i < m.getParameters().length; i++) {
+ // System.out.print(" "+m.getParameters()[i]);
+ // }
+ // System.out.println();
switch (m.getMessageCode()) {
case EC.TLC_INVARIANT_VIOLATED_INITIAL:
case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR:
@@ -192,6 +203,8 @@ public class TLCResults {
tlcResult = evaluatingParameter(m.getParameters());
break;
+ default:
+ break;
}
}
@@ -208,6 +221,10 @@ public class TLCResults {
return WellDefinednessError;
} else if (s.contains("tlc2.module.TLC.Assert")) {
return tlcResult = WellDefinednessError;
+ } else if (s
+ .contains("CHOOSE x \\in S: P, but no element of S satisfied P")
+ && s.contains("module FunctionsAsRelations")) {
+ return tlcResult = WellDefinednessError;
}
}
diff --git a/src/main/java/de/tlc4b/util/BTLCPrintStream.java b/src/main/java/de/tlc4b/util/BTLCPrintStream.java
deleted file mode 100644
index 9a6fb093c562aa800b17ac1f3fc6a71e5a4c88b7..0000000000000000000000000000000000000000
--- a/src/main/java/de/tlc4b/util/BTLCPrintStream.java
+++ /dev/null
@@ -1,61 +0,0 @@
-package de.tlc4b.util;
-
-import java.io.PipedOutputStream;
-import java.io.PrintStream;
-import java.util.ArrayList;
-
-import de.tlc4b.TLC4BGlobals;
-
-
-public class BTLCPrintStream extends PrintStream {
- private final PrintStream console;
- private final ArrayList<String> array;
- public BTLCPrintStream() {
- super(new PipedOutputStream());
- this.console = System.out;
- this.array = new ArrayList<String>();
- }
-
- public void resetSystemOut(){
- System.setOut(console);
- }
-
- public String[] getArray(){
- return array.toArray(new String[array.size()]);
- }
-
- public ArrayList<String> getArrayList(){
- return array;
- }
-
- @Override
- public void println(String str){
- synchronized (BTLCPrintStream.class){
- if(!TLC4BGlobals.isTool()){
- //console.println(str);
- }
- array.add(str);
- }
- }
-
- @Override
- public void print(String str){
- synchronized (BTLCPrintStream.class){
- if(!TLC4BGlobals.isTool()){
- console.println(str);
- }
- //console.println(str);
- array.add(str);
- }
- }
-
- @Override
- public void print(Object obj){
- synchronized (BTLCPrintStream.class){
- //console.println(obj.toString());
- array.add(obj.toString());
- }
- }
-
-
-}
diff --git a/src/main/java/de/tlc4b/util/StopWatch.java b/src/main/java/de/tlc4b/util/StopWatch.java
index 89594ba11e9b6b419f03e9a25e09733a9c09cff7..a0a719b3940cb5130f416bc5bdc02531ce3a788f 100644
--- a/src/main/java/de/tlc4b/util/StopWatch.java
+++ b/src/main/java/de/tlc4b/util/StopWatch.java
@@ -7,12 +7,12 @@ public class StopWatch {
private static final Hashtable<String, Long> runTime = new Hashtable<String, Long>();
public static void start(String id) {
- startTime.put(id, new Long(System.currentTimeMillis()));
+ startTime.put(id, System.currentTimeMillis());
}
public static long stop(String id) {
long stopTime = System.currentTimeMillis()
- - ((Long) startTime.remove(id)).longValue();
+ - startTime.remove(id);
runTime.put(id, stopTime);
return stopTime;
}
diff --git a/src/main/resources/standardModules/Functions.tla b/src/main/resources/standardModules/Functions.tla
index 7a689799e88c33bfe2fb99d1f9a8d37c1a284f21..21da3eaab84a5642e0699d01a3f104cdf4dd2956 100644
--- a/src/main/resources/standardModules/Functions.tla
+++ b/src/main/resources/standardModules/Functions.tla
@@ -47,6 +47,9 @@ TotalBijFunc(S, T) == {f \in [S -> T]: T = Range(f) /\
ParFunc(S, T) == UNION{[x -> T] :x \in SUBSET S}
\* The set of all partial functions
+
+ParFuncEleOf(f, S, T) == {x \in {f} : DOMAIN f \subseteq S /\ Range(f) \subseteq T}
+ \* The set containing f if f is a partial function
isEleOfParFunc(f, S, T) == DOMAIN f \subseteq S /\ Range(f) \subseteq T
\* Test if the function f is a partial function
@@ -55,10 +58,30 @@ ParInjFunc(S, T)== {f \in ParFunc(S, T):
Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set of all partial injective functions
+ParInjFuncEleOf(f, S, T)== {x \in {f}:
+ /\ DOMAIN f \subseteq S
+ /\ Range(f) \subseteq T
+ /\ Cardinality(DOMAIN f) = Cardinality(Range(f))}
+\* The set containing f if f is a partial injective function
+
ParSurFunc(S, T)== {f \in ParFunc(S, T): T = Range(f)}
\* The set of all partial surjective function
-ParBijFunc(S, T) == {f \in ParFunc(S, T): T = Range(f) /\
- Cardinality(DOMAIN f) = Cardinality(Range(f))}
+ParSurFuncEleOf(f, S, T)== {x \in {f}:
+ /\ DOMAIN f \subseteq S
+ /\ Range(f) \subseteq T
+ /\ T = Range(f)}
+\* The set containing f if f is a partial surjective function
+
+ParBijFunc(S, T) == {f \in ParFunc(S, T):
+ /\ Range(f) = T
+ /\ Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set of all partial bijective functions
+
+ParBijFuncEleOf(f, S, T) == {x \in {f}:
+ /\ DOMAIN f \subseteq S
+ /\ Range(f) \subseteq T
+ /\ Cardinality(DOMAIN f) = Cardinality(Range(f))
+ /\ T = Range(f)}
+\* The set containing f if f is a partial bijective function
=============================================================================
diff --git a/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java b/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..a9f58d1ed3b170ad8f8c91a924ac10cc5ddc1148
--- /dev/null
+++ b/src/test/java/de/tlc4b/coverage/IntegrationCoverageTest.java
@@ -0,0 +1,47 @@
+package de.tlc4b.coverage;
+
+
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.tlc4b.TLC4B;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class IntegrationCoverageTest extends AbstractParseMachineTest{
+
+
+ private final File machine;
+
+ public IntegrationCoverageTest(File machine, TLCResult result) {
+ this.machine = machine;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] {machine.getPath(), "-notlc"};
+ TLC4B.test(a,true);
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<String> list = new ArrayList<String>();
+ final ArrayList<String> ignoreList = new ArrayList<String>();
+ list.add("../prob_examples/public_examples/TLC/");
+
+ list.add("./src/test/resources/");
+ ignoreList.add("./src/test/resources/compound/");
+ ignoreList.add("./src/test/resources/other/");
+ ignoreList.add("./src/test/resources/test/");
+ ignoreList.add("./src/test/resources/testing/");
+ return getConfiguration2(list, ignoreList);
+ }
+
+}
diff --git a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
index e4587e0b5c629da32d127fad31ad717dcdff2401..8aaa4172a5608f1de2e9d5dde5e365037f82dfa7 100644
--- a/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
@@ -106,8 +106,8 @@ public class FunctionTest {
String machine = "MACHINE test\n"
+ "PROPERTIES {} = {1,2} +-> {1,2}\n" + "END";
String expected = "---- MODULE test ----\n"
- + "EXTENDS FunctionsAsRelations\n"
- + "ASSUME {} = RelParFunc({1, 2}, {1, 2})\n"
+ + "EXTENDS Functions\n"
+ + "ASSUME {} = ParFunc({1, 2}, {1, 2})\n"
+ "====";
compareEquals(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
index de03a6eb274c563e1b4ebee278158d4b8cf15c3d..9c5dcc8d3c803d90eb6f7ae187f9e753bc0ce0a4 100644
--- a/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
@@ -42,7 +42,6 @@ public class MachineParameterTest {
String expected = "---- MODULE test----\n"
+ "a == 1\n"
+ "b == 2 \n"
- + "ASSUME TRUE\n"
+ "======";
compare(expected, machine);
}
diff --git a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
index 53eec85b71462737aef046c7d14485e9d43409fd..da79ba87d9efb2009cc1b8de453846e59d3842a1 100644
--- a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
@@ -85,7 +85,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
- + "Init == x = 1 /\\ y = 1 \n"
+ + "Init == x \\in {1} /\\ y \\in {1} \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x, y>>\n"
+ "====";
compare(expected, machine);
@@ -104,8 +104,8 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
- + "Init == x = 1 /\\ y = 1 \n"
- + "foo == x' = 1 /\\ y' = 1\n"
+ + "Init == x \\in {1} /\\ y \\in {1}\n"
+ + "foo == x' \\in {1} /\\ y' \\in {1}\n"
+ "Next == foo\n"
+ "====";
compare(expected, machine);
@@ -125,8 +125,8 @@ public class OperationsTest {
+ "EXTENDS Naturals\n"
+ "VARIABLES x, y \n"
+ "Invariant == x = 1 /\\ y = 1\n"
- + "Init == x = 1 /\\ y = 1 \n"
- + "foo == x' = x + 1 /\\ UNCHANGED <<y>>\n"
+ + "Init == x \\in {1} /\\ y \\in {1} \n"
+ + "foo == x' \\in {x + 1} /\\ UNCHANGED <<y>>\n"
+ "Next == foo\n"
+ "====";
compare(expected, machine);
@@ -187,7 +187,7 @@ public class OperationsTest {
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
+ "Init == x = 1 \n"
- + "foo(p) == \\E p2 \\in {1} : TRUE /\\ x' = p + p2\n"
+ + "foo(p) == \\E p2 \\in {1} : x' = p + p2\n"
+ "Next == \\E p \\in {1} : foo(p)\n"
+ "====";
compare(expected, machine);
diff --git a/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
index 0123a5b12b75841131864d2ee67fd897ea6b2ebc..773a8674122c39c7d1223fc93b69c61dbe7adb85 100644
--- a/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
@@ -55,7 +55,7 @@ public class SubstitutionsTest {
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
+ "Invariant == x = 1\n"
- + "Init == \\E a \\in {1}, b \\in {2} : TRUE /\\ x = a + b \n"
+ + "Init == \\E a \\in {1}, b \\in {2} : x = a + b \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
compare(expected, machine);
@@ -70,10 +70,9 @@ public class SubstitutionsTest {
+ "END";
String expected = "---- MODULE test ----\n"
- + "EXTENDS Naturals \n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
- + "Init == 1 = 1 /\\ x = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Init == \n/\\ 1 = 1 \n/\\ x = 1\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
compare(expected, machine);
@@ -90,8 +89,8 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
- + "Invariant == x = 1\n"
- + "Init == 1 = 1 /\\ x = 1\n"
+ + "Invariant1 == x = 1\n"
+ + "Init == \n/\\1 = 1 \n/\\ x = 1\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
compare(expected, machine);
diff --git a/src/test/java/de/tlc4b/typechecking/FunctionTest.java b/src/test/java/de/tlc4b/typechecking/FunctionTest.java
index 6049057fdc267439997acc7508e82d7f022e99d5..b9a11aa32158d0eea248e61e8e0c944574a5707c 100644
--- a/src/test/java/de/tlc4b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tlc4b/typechecking/FunctionTest.java
@@ -189,7 +189,7 @@ public class FunctionTest {
+ "PROPERTIES k = INT +-> INT \n"
+ "END";
TestTypechecker t = new TestTypechecker(machine);
- assertEquals("POW(POW(INTEGER*INTEGER))", t.constants.get("k").toString());
+ assertEquals("POW(FUNC(INTEGER,INTEGER))", t.constants.get("k").toString());
}
diff --git a/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
index e8083cdc0a07829bdb242140e32c4d03aa03646d..47bfb0fc2b08d6c13aa138b967e14fc9e63957e9 100644
--- a/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
+++ b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
@@ -2,6 +2,7 @@ package de.tlc4b.util;
import java.io.File;
import java.io.FilenameFilter;
+import java.io.IOException;
import java.util.ArrayList;
import java.util.Arrays;
@@ -28,9 +29,80 @@ public abstract class AbstractParseMachineTest {
return dir.listFiles(new MachineFilenameFilter());
}
+ protected static File[] getMachinesRecursive(String path, ArrayList<String> ignoreList) {
+ File[] files = walk(path, ignoreList).toArray(new File[0]);
+ return files;
+ }
+
+ private static ArrayList<File> walk(String path, ArrayList<String> ignoreList) {
+ File root = new File(path);
+ File[] list = root.listFiles();
+
+ ArrayList<File> files = new ArrayList<File>();
+ if (list == null)
+ return files;
+
+ for (File f : list) {
+ if (f.isDirectory()) {
+ boolean visitDir = true;
+ for (String string : ignoreList) {
+ File ignore = new File(string);
+ try {
+ if(f.getCanonicalPath().equals(ignore.getCanonicalPath())){
+ visitDir = false;
+ }
+ } catch (IOException e) {
+ visitDir = false;
+ }
+ }
+ if(visitDir){
+ files.addAll(walk(f.getAbsolutePath(),ignoreList));
+ }
+
+ } else {
+ String name =f.getName();
+ if (name.endsWith(".mch")) {
+ files.add(f);
+ }
+ }
+ }
+ return files;
+ }
+
+ protected static Configuration getConfiguration2(ArrayList<String> list, ArrayList<String> ignoreList) {
+ final ArrayList<File> allMachines = new ArrayList<File>();
+
+ final ArrayList<TLCResult> expectedValues = new ArrayList<TLCResult>();
+ for (String path : list) {
+ File[] machines = getMachinesRecursive(path, ignoreList);
+ allMachines.addAll(Arrays.asList(machines));
+ for (int i = 0; i < machines.length; i++) {
+ expectedValues.add(TLCResult.NoError);
+ }
+ }
+
+ return new Configuration() {
+ public int size() {
+ return allMachines.size();
+ }
+
+ public File getTestValue(int index) {
+ return allMachines.get(index);
+ }
+
+ public String getTestName(int index) {
+ return allMachines.get(index).getName();
+ }
+
+ public TLCResult getExpectedValue(int index) {
+ return expectedValues.get(index);
+ }
+ };
+ }
+
protected static Configuration getConfiguration(ArrayList<TestPair> list) {
final ArrayList<File> allMachines = new ArrayList<File>();
-
+
final ArrayList<TLCResult> expectedValues = new ArrayList<TLCResult>();
for (TestPair testPair : list) {
File[] machines = getMachines(testPair.getPath());
@@ -39,7 +111,7 @@ public abstract class AbstractParseMachineTest {
expectedValues.add(testPair.getResult());
}
}
-
+
return new Configuration() {
public int size() {
return allMachines.size();
diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java
index 9d77e7c995235a03126d660e6e11f5ec36b64a19..438b8c00fb31fc1c39cc14434fa57270b86b0dc7 100644
--- a/src/test/java/de/tlc4b/util/TLC4BTester.java
+++ b/src/test/java/de/tlc4b/util/TLC4BTester.java
@@ -1,12 +1,11 @@
package de.tlc4b.util;
-import java.io.IOException;
import de.tlc4b.TLC4B;
public class TLC4BTester {
- public static void main(String[] args) throws IOException {
+ public static void main(String[] args) throws Exception {
System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
TLC4B.test(args,true);
}
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index ca5af5c6f4783c5e155e60887b224924cfe3dc4e..a121924d2f39706f40059f4c902a2e8da9b0ff26 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -1,9 +1,7 @@
package testing;
-import static org.junit.Assert.*;
import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
-import static de.tlc4b.util.TestUtil.test;
import java.io.File;
import java.util.ArrayList;
@@ -23,22 +21,16 @@ import de.tlc4b.util.PolySuite.Configuration;
public class Testing2 extends AbstractParseMachineTest{
private final File machine;
- private final TLCResult error;
public Testing2(File machine, TLCResult result) {
this.machine = machine;
- this.error = result;
}
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] {machine.getPath()};
-
- TLC4B.main(a);
- //B2TLA.test(a,true);
- //test(a);
- //assertEquals(error, B2TLA.test(a,true));
- //assertEquals(1,2);
+ //TLC4B.main(a);
+ TLC4B.test(a,false);
}
@Config
@@ -48,15 +40,4 @@ public class Testing2 extends AbstractParseMachineTest{
return getConfiguration(list);
}
-// @Test
-// public void testInvariantError() throws Exception {
-// String[] a = new String[] { "./src/test/resources/laws/RelationsTest.mch", "-tmp" };
-// B2TLA.main(a);
-// }
-
-// @Test
-// public void testInvariantError() throws Exception {
-// String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch" };
-// assertEquals(InvariantViolation, B2TLA.test(a,false));
-// }
}
diff --git a/src/test/resources/basics/Arithmetic.mch b/src/test/resources/basics/Arithmetic.mch
deleted file mode 100644
index aee8c08c64a552e5cfb35cc873133207cec4f8d7..0000000000000000000000000000000000000000
--- a/src/test/resources/basics/Arithmetic.mch
+++ /dev/null
@@ -1,5 +0,0 @@
-MACHINE Arithmetic
-PROPERTIES
-SIGMA(z).(z: 1..3 & z < 3 | 1) = 2
-& PI(z).(z: 1..3 & z < 3 | 2) = 4
-END
\ No newline at end of file
diff --git a/src/test/resources/basics/FunctionsAsRelationsTest.mch b/src/test/resources/basics/FunctionsAsRelationsTest.mch
index 83f0a0ba17b05899be7583ba27fccae110fdc0c4..25780f17bc7d876725c26c12296e5f342d0c8ff9 100644
--- a/src/test/resources/basics/FunctionsAsRelationsTest.mch
+++ b/src/test/resources/basics/FunctionsAsRelationsTest.mch
@@ -4,8 +4,8 @@ PROPERTIES
/* The following functions are translated as relations */
/* total function */
-{{(1,3),(2,3)}} = {1,2} --> {3}
-& {(1,1)} : {1} --> NATURAL
+{{(1,3),(1+1,3)}} = {1,2} --> {3}
+& {(1+1,1)} : {2} --> NATURAL
/* total injectiv function */
& {{(1,3), (2,4)}, {(1,4),(2,3)}} = {1,2} >-> {3,4}
diff --git a/src/test/resources/basics/NumbersTest.mch b/src/test/resources/basics/NumbersTest.mch
index 886f1fd41ae9cfe67131a427e3b7cfbf2d39f85a..87c066a502bd458cea3a122286e10eda5cb55ae9 100644
--- a/src/test/resources/basics/NumbersTest.mch
+++ b/src/test/resources/basics/NumbersTest.mch
@@ -1,5 +1,13 @@
MACHINE NumbersTest
PROPERTIES
-SIGMA(x).( x :{ 1, 2, 3 } | x + 1 ) = 9
-& SIGMA(x).( x :{ 1, 2, 3 } | 1 ) = 3
+SIGMA(z).(z: 1..3 & z < 3 | 1) = 2
+& PI(z).(z: 1..3 & z < 3 | 2) = 4
+& 0 : NAT
+& 0 : NATURAL
+& 1 : NAT1
+& 1 : NATURAL1
+& -1 : INT
+& -1 : INTEGER
+& 2 / 2 = 1
+& 3 mod 2 = 1
END
\ No newline at end of file
diff --git a/src/test/resources/basics/RecordTest.mch b/src/test/resources/basics/RecordTest.mch
new file mode 100644
index 0000000000000000000000000000000000000000..e067e2a7fad7db61f39df9c83277dbcca380f23d
--- /dev/null
+++ b/src/test/resources/basics/RecordTest.mch
@@ -0,0 +1,4 @@
+MACHINE RecordTest
+PROPERTIES
+rec(a:1)'a = 1
+END
\ No newline at end of file
diff --git a/src/test/resources/basics/SetsTest.mch b/src/test/resources/basics/SetsTest.mch
index 615e48764973278f15f68257b3e9c6d97129e7e3..c787eca82181b0a8e4ac18c99ea77261df939a5e 100644
--- a/src/test/resources/basics/SetsTest.mch
+++ b/src/test/resources/basics/SetsTest.mch
@@ -5,4 +5,7 @@ PROPERTIES
& UNION(x).(x :{2,4} | {y | y : 0..x}) = {0, 1, 2, 3, 4}
& (1,TRUE,2) : {a,b,c | a : {1} & b : {TRUE} & c : {2}}
& UNION(z).(z: {1,2} & 1 = 1| {z}) = {1,2}
+& INTER(x).(x: {1,2} & 1 = 1| {x+x, x}) = {2}
+& INTER(x).(x: {1,2} & 1 = 1| {x+x, x}) = {2}
+& {1} : {x| x <: 1..3}
END
\ No newline at end of file
diff --git a/src/test/resources/basics/StringTest.mch b/src/test/resources/basics/StringTest.mch
new file mode 100644
index 0000000000000000000000000000000000000000..2d267eb71916792e8d6505f0c923c962a65ca998
--- /dev/null
+++ b/src/test/resources/basics/StringTest.mch
@@ -0,0 +1,4 @@
+MACHINE StringTest
+PROPERTIES
+"abc" : STRING
+END
\ No newline at end of file
diff --git a/src/test/resources/basics/SubstitutionsTest.mch b/src/test/resources/basics/SubstitutionsTest.mch
new file mode 100644
index 0000000000000000000000000000000000000000..17c44c404d79cd73dad86e3e2435f880b17a6052
--- /dev/null
+++ b/src/test/resources/basics/SubstitutionsTest.mch
@@ -0,0 +1,10 @@
+MACHINE FunctionsTest
+VARIABLES x
+INVARIANT x : 1..5
+INITIALISATION x := 1
+OPERATIONS
+op1 = PRE 1 = 1 THEN x := 2 END;
+op2 = LET a, b, c BE a = 1 & b : {1} & c = 2 IN x := 2 END;
+op3 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 ELSE x:= 3 END;
+op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END
+END
\ No newline at end of file
diff --git a/src/test/resources/laws/FunctionsTest.mch b/src/test/resources/laws/FunctionsTest.mch
index ad6119d1cce4977e4ed111bf37ab0b405640cff2..f05d0f82678eff0aacccc1fef067f85f2ba2da7c 100644
--- a/src/test/resources/laws/FunctionsTest.mch
+++ b/src/test/resources/laws/FunctionsTest.mch
@@ -1,4 +1,6 @@
MACHINE FunctionsTest
+DEFINITIONS
+f == %x.(x : 1..10 | x+1)
VARIABLES x
INVARIANT x : 1..3
INITIALISATION x := 1
@@ -12,9 +14,23 @@ ASSERTIONS
%x.(x:{1,2}|x) : {1,2} >-> {1,2,3};
%x.(x:{1,2,3}|1) : {1,2,3} -->> {1};
%x.(x:{1,2}|x) : {1,2} >->> {1,2};
-
+ %x,y.(x : 1..3 & y : 1..3| x+ y)(1,2) = 3;
+ %x.(x : 1..2| x ) : 1..3 +-> 1..3;
%x.(x:{1,2}|1) : {1,2,3} +-> {1};
+ %x.(x:{1,2} & 1=1|1) : {1,2,3} +-> {1};
%x.(x:{1}|1) : {1,2,3} >+> {1};
%x.(x:{1,2}|1) : {1,2,3} +->> {1};
- %x.(x:{1,2}|x) : {1,2,3} >+>> {1,2}
+ %x.(x:{1,2}|x) : {1,2,3} >+>> {1,2};
+
+ dom(f) = 1..10;
+ ran(f) = 2..11;
+ id(1..3) = %x.(x : 1..3 | x);
+ 1..3 <| f = %x.(x : 1..3 | x + 1);
+ 1..3 <<| f = %x.(x : 4..10 | x + 1);
+ f |> 1..3 = %x.(x : 1..2 | x + 1);
+ f |>> 1..3 = %x.(x : 3..10 | x + 1);
+ f~= %x.(x : 2..11 | x-1);
+ f[1..3] = 2..4;
+ f <+ %x.(x : 10..11 | x+1) = %x.(x : 1..11 | x + 1);
+ f <+ %x.(x : 1..11 | x-1) = %x.(x : 1..11 | x - 1)
END
\ No newline at end of file
diff --git a/src/test/resources/laws/FunctionsTest2.mch b/src/test/resources/laws/FunctionsTest2.mch
deleted file mode 100644
index 9a5f63017f8b2f669076494377114a89feaf0e6e..0000000000000000000000000000000000000000
--- a/src/test/resources/laws/FunctionsTest2.mch
+++ /dev/null
@@ -1,16 +0,0 @@
-MACHINE FunctionsTest2
-DEFINITIONS
-f == %x.(x : 1..10 | x+1)
-PROPERTIES
- dom(f) = 1..10
-& ran(f) = 2..11
-& id(1..3) = %x.(x : 1..3 | x)
-& 1..3 <| f = %x.(x : 1..3 | x + 1)
-& 1..3 <<| f = %x.(x : 4..10 | x + 1)
-& f |> 1..3 = %x.(x : 1..2 | x + 1)
-& f |>> 1..3 = %x.(x : 3..10 | x + 1)
-& f~= %x.(x : 2..11 | x-1)
-& f[1..3] = 2..4
-& f <+ %x.(x : 10..11 | x+1) = %x.(x : 1..11 | x + 1)
-& f <+ %x.(x : 1..11 | x-1) = %x.(x : 1..11 | x - 1)
-END
\ No newline at end of file
diff --git a/src/test/resources/laws/SequencesAsRelationsTest.mch b/src/test/resources/laws/SequencesAsRelationsTest.mch
index 73bb9261827b90488d70979e96fba0fc0fe72e02..4d4b924ee4a2131575c2dae0142a83807dab4824 100644
--- a/src/test/resources/laws/SequencesAsRelationsTest.mch
+++ b/src/test/resources/laws/SequencesAsRelationsTest.mch
@@ -1,69 +1,69 @@
MACHINE SequencesAsRelationsTest
PROPERTIES
{} = []
-& {(1,1)} = [1]
+& {(1+0,1)} = [1]
/* Set of sequences */
-& {(1,1)} : seq({1})
-& {(1,2)} /: seq({1})
-& not({(1,1)} /: seq({1}))
-& {} : seq({1})
+& {(1+0,1)} : seq({1})
+& {(1+0,2)} /: seq({1})
+& not({(1+0,1)} /: seq({1}))
+& {} : seq({1+0})
& {} : seq({})
/* Set of sequences */
-& {(1,1)} : seq1({1})
+& {(1+0,1)} : seq1({1})
& {} /: seq1({})
-& {(1,2)} /: seq1({1})
-& not({} : seq1({1}))
+& {(1+0,2)} /: seq1({1})
+& not({} : seq1({1+0}))
& not({} : seq1({}))
/* Set of injective sequences */
& iseq({}) = {{}}
-& iseq({1}) = {{},{(1,1)}}
+& iseq({1}) = {{},{(1+0,1)}}
/* Set of non empty injective sequences */
& iseq1({}) = {}
-& iseq1({1}) = {{(1,1)}}
+& iseq1({1}) = {{(1+0,1)}}
/* Size */
& size({}) = 0
-& size({(1,1),(2,2)}) = 2
+& size({(1+0,1),(2,2)}) = 2
/* Concatenation */
-& {(1,1),(2,2)}^{(1,3)} = {(1,1),(2,2),(3,3)}
-& {(1,1),(2,2)}^{} = {(1,1),(2,2)}
-& {}^{(1,1),(2,2)} = {(1,1),(2,2)}
+& {(1+0,1),(2,2)}^{(1,3)} = {(1,1),(2,2),(3,3)}
+& {(1+0,1),(2,2)}^{} = {(1,1),(2,2)}
+& {}^{(1+0,1),(2,2)} = {(1,1),(2,2)}
& {}^{} = {}
/* Prepand */
-& 1 -> {(1,2),(2,3)} = {(1,1),(2,2),(3,3)}
-& 1 -> {} = {(1,1)}
+& 1 -> {(1+0,2),(2,3)} = {(1,1),(2,2),(3,3)}
+& 1 -> {} = {(1+0,1)}
/* Append */
-& {(1,1),(2,2)} <- 3 = {(1,1),(2,2),(3,3)}
-& {} <- 1 = {(1,1)}
+& {(1+0,1),(2,2)} <- 3 = {(1,1),(2,2),(3,3)}
+& {} <- 1 = {(1+0,1)}
/* Front */
-& front({(1,1)}) = {}
-& front({(1,1),(2,2),(3,3)}) = {(1,1),(2,2)}
+& front({(1+0,1)}) = {}
+& front({(1+0,1),(2,2),(3,3)}) = {(1,1),(2,2)}
/* First */
-& first({(1,1)}) = 1
-& first({(1,1),(2,2)}) = 1
+& first({(1+0,1)}) = 1
+& first({(1+0,1),(2,2)}) = 1
/* Tail */
-& tail({(1,1)}) = {}
-& tail({(1,1),(2,2),(3,3)}) = {(1,2),(2,3)}
+& tail({(1+0,1)}) = {}
+& tail({(1+0,1),(2,2),(3,3)}) = {(1,2),(2,3)}
/* Last */
-& last({(1,1)}) = 1
-& last({(1,1),(2,2)}) = 2
+& last({(1+0,1)}) = 1
+& last({(1+0,1),(2,2)}) = 2
/* Reverse */
& rev({}) = {}
-& rev({(1,1)}) = {(1,1)}
-& rev({(1,1),(2,2),(3,3)}) = {(1,3),(2,2),(3,1)}
+& rev({(1+0,1)}) = {(1,1)}
+& rev({(1+0,1),(2,2),(3,3)}) = {(1,3),(2,2),(3,1)}
/* Generalized Concatenation */
& conc({(1,{(1,1),(2,2)}),(2,{(1,3)})}) = {(1,1),(2,2),(3,3)}
@@ -77,13 +77,13 @@ PROPERTIES
& perm({}) = {{}}
/* Take first elements */
-& {(1,1),(2,2)} /|\ 1 = {(1,1)}
-& {(1,1),(2,2)} /|\ 2 = {(1,1),(2,2)}
-& {(1,1)} /|\ 0 = {}
+& {(1+0,1),(2,2)} /|\ 1 = {(1,1)}
+& {(1+0,1),(2,2)} /|\ 2 = {(1,1),(2,2)}
+& {(1+0,1)} /|\ 0 = {}
& {} /|\ 0 = {}
-& {(1,1),(2,2)} \|/ 1 = {(1,2)}
-& {(1,1),(2,2)} \|/ 0 = {(1,1),(2,2)}
-& {(1,1)} \|/ 1 = {}
+& {(1+0,1),(2,2)} \|/ 1 = {(1,2)}
+& {(1+0,1),(2,2)} \|/ 0 = {(1,1),(2,2)}
+& {(1+0,1)} \|/ 1 = {}
& {} \|/ 0 = {}
END
\ No newline at end of file
diff --git a/src/test/resources/ltl/FairnessCounter.mch b/src/test/resources/ltl/FairnessCounter.mch
index b904c71c31d7de8d56ef7e1d9586c8502af08e8d..1ad80ef546d9d30d9f6127a04d536656219bdb33 100644
--- a/src/test/resources/ltl/FairnessCounter.mch
+++ b/src/test/resources/ltl/FairnessCounter.mch
@@ -1,6 +1,6 @@
MACHINE FairnessCounter
DEFINITIONS
-ASSERT_LTL_1 == "WF(Reset) & WF(Inc) => F {x = 0}"
+ASSERT_LTL_1 == "WF(Reset) & SF(Inc) => F {x = 0}"
VARIABLES x
INVARIANT
x : 0..20