diff --git a/build.gradle b/build.gradle
index f83bb03b20d7804d17ef5157b9ee09a9a524870a..cede4acc0147531d3e98d282b9c612c45d2157bc 100644
--- a/build.gradle
+++ b/build.gradle
@@ -40,7 +40,7 @@ dependencies {
test {
- exclude('de/b2tla/tlc/integration/probprivate')
+ exclude('de/tlc4b/tlc/integration/probprivate')
exclude('testing')
}
@@ -49,14 +49,14 @@ test {
task integrationtests(type: Test){
doFirst{ println("Running integration tests") }
scanForTestClasses = true
- include('de/b2tla/tlc/integration/probprivate/**')
+ include('de/tlc4b/tlc/integration/probprivate/**')
}
jar { from sourceSets.main.allJava }
jar {
from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) }
}
-manifest.mainAttributes("Main-Class" : 'de.b2tla.B2TLA')
+manifest.mainAttributes("Main-Class" : 'de.tlc4b.TLC4B')
manifest.mainAttributes("Class-Path": './tla/ tlatools.jar')
task tlc4b(dependsOn: build) << {
diff --git a/build.xml b/build.xml
index 009f6d6a92672d4f50c5b66616ce2474726018ab..47a9188af65a2cbe6f315938c584579e5c617041 100644
--- a/build.xml
+++ b/build.xml
@@ -1,5 +1,5 @@
<project default="copy">
<target name="copy">
- <copy file="build/b2tla/B2TLA.jar" tofile="../../Desktop/ProB/lib/B2TLA.jar"/>
+ <copy file="build/tlc4b/TLC4B.jar" tofile="../../Desktop/ProB/lib/TLC4B.jar"/>
</target>
</project>
\ No newline at end of file
diff --git a/src/main/java/de/b2tla/exceptions/B2TLAIOException.java b/src/main/java/de/b2tla/exceptions/B2TLAIOException.java
deleted file mode 100644
index 7c4f56a1b1b8bfc1ab9b4ddb3d8c9e4d0d8ba738..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/exceptions/B2TLAIOException.java
+++ /dev/null
@@ -1,15 +0,0 @@
-package de.b2tla.exceptions;
-
-@SuppressWarnings("serial")
-public class B2TLAIOException extends B2tlaException{
-
- public B2TLAIOException(String e) {
- super(e);
- }
-
- @Override
- public String getError() {
- return "I/O Error";
- }
-
-}
diff --git a/src/main/java/de/b2tla/exceptions/B2tlaException.java b/src/main/java/de/b2tla/exceptions/B2tlaException.java
deleted file mode 100644
index 1561c66c6f3c150888d8520c8c967bfcb45c58f5..0000000000000000000000000000000000000000
--- a/src/main/java/de/b2tla/exceptions/B2tlaException.java
+++ /dev/null
@@ -1,12 +0,0 @@
-package de.b2tla.exceptions;
-
-@SuppressWarnings("serial")
-public abstract class B2tlaException extends RuntimeException {
-
- public B2tlaException(String e) {
- super(e);
- }
-
- public abstract String getError();
-
-}
diff --git a/src/main/java/de/b2tla/B2TLA.java b/src/main/java/de/tlc4b/TLC4B.java
similarity index 83%
rename from src/main/java/de/b2tla/B2TLA.java
rename to src/main/java/de/tlc4b/TLC4B.java
index fa756bc4c634d8fc385d26e5bb37b811e465c7b4..5cf711ab59e70d5d6855b28430d25f4434055c8a 100644
--- a/src/main/java/de/b2tla/B2TLA.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -1,4 +1,4 @@
-package de.b2tla;
+package de.tlc4b;
import java.io.BufferedReader;
import java.io.File;
@@ -10,17 +10,17 @@ import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
-import de.b2tla.B2TLAGlobals;
-import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES;
-import de.b2tla.exceptions.B2TLAIOException;
-import de.b2tla.exceptions.B2tlaException;
-import de.b2tla.tlc.TLCOutputInfo;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.tlc.TLCResults;
-import de.b2tla.util.StopWatch;
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
+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 B2TLA {
+public class TLC4B {
private String mainFileName;
private String machineFileNameWithoutFileExtension;
@@ -33,7 +33,7 @@ public class B2TLA {
private String constantsSetup;
public static void main(String[] args) throws IOException {
- B2TLA b2tla = new B2TLA();
+ TLC4B b2tla = new TLC4B();
try {
b2tla.progress(args);
@@ -41,14 +41,14 @@ public class B2TLA {
System.err.println("***** Parsing Error *****");
System.err.println(e.getMessage());
return;
- } catch (B2tlaException e) {
+ } catch (TLC4BException e) {
System.err.println(e.getMessage());
System.out.println("Model checking time: 0 sec");
System.out.println("Result: " + e.getError());
return;
}
- if (B2TLAGlobals.isRunTLC()) {
+ if (TLC4BGlobals.isRunTLC()) {
try {
TLCRunner.runTLC(b2tla.machineFileNameWithoutFileExtension,
b2tla.path);
@@ -57,7 +57,7 @@ public class B2TLA {
TLCResults results = new TLCResults(b2tla.tlcOutputInfo);
results.evalResults();
- b2tla.printResults(results, B2TLAGlobals.isCreateTraceFile());
+ b2tla.printResults(results, TLC4BGlobals.isCreateTraceFile());
System.exit(0);
} catch (NoClassDefFoundError e) {
@@ -99,11 +99,11 @@ public class B2TLA {
public static void test(String[] args, boolean deleteFiles)
throws IOException {
- B2TLAGlobals.resetGlobals();
- B2TLAGlobals.setDeleteOnExit(deleteFiles);
- B2TLAGlobals.setTestingMode(true);
+ TLC4BGlobals.resetGlobals();
+ TLC4BGlobals.setDeleteOnExit(deleteFiles);
+ TLC4BGlobals.setTestingMode(true);
// B2TLAGlobals.setCleanup(true);
- B2TLA b2tla = new B2TLA();
+ TLC4B b2tla = new TLC4B();
try {
b2tla.progress(args);
} catch (Exception e) {
@@ -112,7 +112,7 @@ public class B2TLA {
return;
}
- if (B2TLAGlobals.isRunTLC()) {
+ if (TLC4BGlobals.isRunTLC()) {
TLCRunner.runTLC(b2tla.machineFileNameWithoutFileExtension,
b2tla.path);
@@ -151,58 +151,58 @@ public class B2TLA {
int index = 0;
while (index < args.length) {
if (args[index].toLowerCase().equals("-nodead")) {
- B2TLAGlobals.setDeadlockCheck(false);
+ TLC4BGlobals.setDeadlockCheck(false);
} else if (args[index].toLowerCase().equals("-notlc")) {
- B2TLAGlobals.setRunTLC(false);
+ TLC4BGlobals.setRunTLC(false);
} else if (args[index].toLowerCase().equals("-notranslation")) {
- B2TLAGlobals.setTranslate(false);
+ TLC4BGlobals.setTranslate(false);
} else if (args[index].toLowerCase().equals("-nogoal")) {
- B2TLAGlobals.setGOAL(false);
+ TLC4BGlobals.setGOAL(false);
} else if (args[index].toLowerCase().equals("-noinv")) {
- B2TLAGlobals.setInvariant(false);
+ TLC4BGlobals.setInvariant(false);
} else if (args[index].toLowerCase().equals("-wdcheck")) {
- B2TLAGlobals.setWelldefinednessCheck(true);
+ TLC4BGlobals.setWelldefinednessCheck(true);
} else if (args[index].toLowerCase().equals("-tool")) {
- B2TLAGlobals.setTool(false);
+ TLC4BGlobals.setTool(false);
} else if (args[index].toLowerCase().equals("-tmp")) {
path = System.getProperty("java.io.tmpdir");
} else if (args[index].toLowerCase().equals("-noltl")) {
- B2TLAGlobals.setCheckltl(false);
+ TLC4BGlobals.setCheckltl(false);
} else if (args[index].toLowerCase().equals("-testscript")) {
- B2TLAGlobals.setRunTestscript(true);
+ TLC4BGlobals.setRunTestscript(true);
} else if (args[index].toLowerCase().equals("-notrace")) {
} else if (args[index].toLowerCase().equals("-del")) {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
} else if (args[index].toLowerCase().equals("-workers")) {
index = index + 1;
if (index == args.length) {
- throw new B2TLAIOException(
+ throw new TLC4BIOException(
"Error: Number requiered after option '-workers'.");
}
int workers = Integer.parseInt(args[index]);
- B2TLAGlobals.setWorkers(workers);
+ TLC4BGlobals.setWorkers(workers);
} else if (args[index].toLowerCase().equals("-constantssetup")) {
- B2TLAGlobals.setProBconstantsSetup(true);
+ TLC4BGlobals.setProBconstantsSetup(true);
index = index + 1;
if (index == args.length) {
- throw new B2TLAIOException(
+ throw new TLC4BIOException(
"Error: String requiered after option '-constantssetup'.");
}
constantsSetup = args[index];
} else if (args[index].toLowerCase().equals("-ltlformula")) {
index = index + 1;
if (index == args.length) {
- throw new B2TLAIOException(
+ throw new TLC4BIOException(
"Error: LTL formula requiered after option '-ltlformula'.");
}
ltlFormula = args[index];
} else if (args[index].charAt(0) == '-') {
- throw new B2TLAIOException("Error: unrecognized option: "
+ throw new TLC4BIOException("Error: unrecognized option: "
+ args[index]);
} else {
if (mainFileName != null) {
- throw new B2TLAIOException(
+ throw new TLC4BIOException(
"Error: more than one input files: " + mainFileName
+ " and " + args[index]);
}
@@ -212,7 +212,7 @@ public class B2TLA {
index++;
}
if (mainFileName == null) {
- throw new B2TLAIOException("Main machine required!");
+ throw new TLC4BIOException("Main machine required!");
}
}
@@ -220,7 +220,7 @@ public class B2TLA {
handleParameter(args);
handleMainFileName();
- if (B2TLAGlobals.isTranslate()) {
+ if (TLC4BGlobals.isTranslate()) {
StopWatch.start("Parsing");
translator = new Translator(machineFileNameWithoutFileExtension,
getFile(), this.ltlFormula, this.constantsSetup);
@@ -260,14 +260,14 @@ public class B2TLA {
private void createFiles() {
File moduleFile = createFile(path, machineFileNameWithoutFileExtension
- + ".tla", tlaModule, B2TLAGlobals.isDeleteOnExit());
+ + ".tla", tlaModule, TLC4BGlobals.isDeleteOnExit());
if (moduleFile != null) {
System.out.println("TLA+ module '" + moduleFile.getAbsolutePath()
+ "' created.");
}
File configFile = createFile(path, machineFileNameWithoutFileExtension
- + ".cfg", config, B2TLAGlobals.isDeleteOnExit());
+ + ".cfg", config, TLC4BGlobals.isDeleteOnExit());
if (configFile != null) {
System.out.println("Configuration file '"
+ configFile.getAbsolutePath() + "' created.");
@@ -364,7 +364,7 @@ public class B2TLA {
} catch (IOException e) {
e.printStackTrace();
} finally {
- if (B2TLAGlobals.isDeleteOnExit()) {
+ if (TLC4BGlobals.isDeleteOnExit()) {
file.deleteOnExit();
}
try {
@@ -380,7 +380,7 @@ public class B2TLA {
private File getFile() {
File mainFile = new File(mainFileName);
if (!mainFile.exists()) {
- throw new B2TLAIOException("The file " + mainFileName
+ throw new TLC4BIOException("The file " + mainFileName
+ " does not exist.");
}
return mainFile;
@@ -411,7 +411,7 @@ public class B2TLA {
return file;
} catch (IOException e) {
e.printStackTrace();
- throw new B2TLAIOException(e.getMessage());
+ throw new TLC4BIOException(e.getMessage());
} finally {
if (deleteOnExit) {
file.deleteOnExit();
diff --git a/src/main/java/de/b2tla/B2TLAGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
similarity index 80%
rename from src/main/java/de/b2tla/B2TLAGlobals.java
rename to src/main/java/de/tlc4b/TLC4BGlobals.java
index a18fdb94a4e85ab53f37a86e887b5266fba54e09..362a7b9d7c23809213b946f1516d9f203d859989 100644
--- a/src/main/java/de/b2tla/B2TLAGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -1,6 +1,6 @@
-package de.b2tla;
+package de.tlc4b;
-public class B2TLAGlobals {
+public class TLC4BGlobals {
private static int DEFERRED_SET_SIZE;
private static int MAX_INT;
private static int MIN_INT;
@@ -68,7 +68,7 @@ public class B2TLAGlobals {
}
public static void setCreateTraceFile(boolean createTraceFile) {
- B2TLAGlobals.createTraceFile = createTraceFile;
+ TLC4BGlobals.createTraceFile = createTraceFile;
}
public static boolean isRunTestscript() {
@@ -76,7 +76,7 @@ public class B2TLAGlobals {
}
public static void setRunTestscript(boolean runTestscript) {
- B2TLAGlobals.runTestscript = runTestscript;
+ TLC4BGlobals.runTestscript = runTestscript;
}
public static int getDEFERRED_SET_SIZE() {
@@ -140,39 +140,39 @@ public class B2TLAGlobals {
}
public static void setDeadlockCheck(boolean deadlockCheck) {
- B2TLAGlobals.checkDeadlock = deadlockCheck;
+ TLC4BGlobals.checkDeadlock = deadlockCheck;
}
public static void setRunTLC(boolean runTLC) {
- B2TLAGlobals.runTLC = runTLC;
+ TLC4BGlobals.runTLC = runTLC;
}
public static void setTranslate(boolean translate) {
- B2TLAGlobals.translate = translate;
+ TLC4BGlobals.translate = translate;
}
public static void setInvariant(boolean invariant) {
- B2TLAGlobals.checkInvariant = invariant;
+ TLC4BGlobals.checkInvariant = invariant;
}
public static void setCheckltl(boolean checkltl) {
- B2TLAGlobals.checkLTL = checkltl;
+ TLC4BGlobals.checkLTL = checkltl;
}
public static void setTool(boolean tool) {
- B2TLAGlobals.hideTLCConsoleOutput = tool;
+ TLC4BGlobals.hideTLCConsoleOutput = tool;
}
public static void setDeleteOnExit(boolean deleteOnExit) {
- B2TLAGlobals.deleteFilesOnExit = deleteOnExit;
+ TLC4BGlobals.deleteFilesOnExit = deleteOnExit;
}
public static void setWorkers(int w){
- B2TLAGlobals.workers = w;
+ TLC4BGlobals.workers = w;
}
public static int getWorkers(){
- return B2TLAGlobals.workers;
+ return TLC4BGlobals.workers;
}
public static boolean isCleanup() {
@@ -180,7 +180,7 @@ public class B2TLAGlobals {
}
public static void setCleanup(boolean cleanup) {
- B2TLAGlobals.cleanup = cleanup;
+ TLC4BGlobals.cleanup = cleanup;
}
public static boolean isProBconstantsSetup() {
@@ -188,23 +188,23 @@ public class B2TLAGlobals {
}
public static void setProBconstantsSetup(boolean proBconstantsSetup) {
- B2TLAGlobals.proBconstantsSetup = proBconstantsSetup;
+ TLC4BGlobals.proBconstantsSetup = proBconstantsSetup;
}
public static void setTestingMode(boolean b){
- B2TLAGlobals.testingMode = b;
+ TLC4BGlobals.testingMode = b;
}
public static boolean getTestingMode(){
- return B2TLAGlobals.testingMode;
+ return TLC4BGlobals.testingMode;
}
public static void setWelldefinednessCheck(boolean b){
- B2TLAGlobals.checkWD = b;
+ TLC4BGlobals.checkWD = b;
}
public static boolean checkWelldefinedness(){
- return B2TLAGlobals.checkWD;
+ return TLC4BGlobals.checkWD;
}
}
diff --git a/src/main/java/de/b2tla/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
similarity index 92%
rename from src/main/java/de/b2tla/TLCRunner.java
rename to src/main/java/de/tlc4b/TLCRunner.java
index 7e1c6e4553aa05c70d93da3f53bf29c7fde5a76f..c8eaeddd7824614a9bd8f8248b8e97077574dce3 100644
--- a/src/main/java/de/b2tla/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -1,4 +1,4 @@
-package de.b2tla;
+package de.tlc4b;
import java.io.BufferedReader;
import java.io.File;
@@ -58,11 +58,11 @@ public class TLCRunner {
ArrayList<String> list = new ArrayList<String>();
list.add(path);
list.add(machineName);
- if (!B2TLAGlobals.isDeadlockCheck()) {
+ if (!TLC4BGlobals.isDeadlockCheck()) {
list.add("-deadlock");
}
- if(B2TLAGlobals.isCheckltl()){
+ if(TLC4BGlobals.isCheckltl()){
list.add("-cleanup");
}
// list.add("-coverage");
@@ -94,12 +94,12 @@ public class TLCRunner {
ToolIO.setMode(ToolIO.SYSTEM);
ArrayList<String> list = new ArrayList<String>();
- if (!B2TLAGlobals.isDeadlockCheck()) {
+ if (!TLC4BGlobals.isDeadlockCheck()) {
list.add("-deadlock");
}
- if(B2TLAGlobals.getWorkers() > 1){
+ if(TLC4BGlobals.getWorkers() > 1){
list.add("-workers");
- list.add(""+B2TLAGlobals.getWorkers());
+ list.add(""+TLC4BGlobals.getWorkers());
}
list.add("-config");
diff --git a/src/main/java/de/b2tla/Translator.java b/src/main/java/de/tlc4b/Translator.java
similarity index 83%
rename from src/main/java/de/b2tla/Translator.java
rename to src/main/java/de/tlc4b/Translator.java
index 6465f0889e6f6ecc620bc68e9424198e6c1f6430..14060bf896e58a856a52dbd34d1143fa1277b493 100644
--- a/src/main/java/de/b2tla/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -1,32 +1,32 @@
-package de.b2tla;
+package de.tlc4b;
import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.analysis.ConstantsEliminator;
-import de.b2tla.analysis.ConstantsEvaluator;
-import de.b2tla.analysis.DefinitionsAnalyser;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.NotSupportedConstructs;
-import de.b2tla.analysis.PrecedenceCollector;
-import de.b2tla.analysis.PrimedNodesMarker;
-import de.b2tla.analysis.Renamer;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UsedStandardModules;
-import de.b2tla.analysis.UsedStandardModules.STANDARD_MODULES;
-import de.b2tla.analysis.transformation.DefinitionsEliminator;
-import de.b2tla.analysis.typerestriction.TypeRestrictor;
-import de.b2tla.analysis.unchangedvariables.UnchangedVariablesFinder;
-import de.b2tla.prettyprint.TLAPrinter;
-import de.b2tla.tla.Generator;
-import de.b2tla.tlc.TLCOutputInfo;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.APredicateParseUnit;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.analysis.Ast2String;
+import de.tlc4b.analysis.ConstantsEliminator;
+import de.tlc4b.analysis.ConstantsEvaluator;
+import de.tlc4b.analysis.DefinitionsAnalyser;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.NotSupportedConstructs;
+import de.tlc4b.analysis.PrecedenceCollector;
+import de.tlc4b.analysis.PrimedNodesMarker;
+import de.tlc4b.analysis.Renamer;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.analysis.UsedStandardModules;
+import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
+import de.tlc4b.analysis.transformation.DefinitionsEliminator;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
+import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
+import de.tlc4b.prettyprint.TLAPrinter;
+import de.tlc4b.tla.Generator;
+import de.tlc4b.tlc.TLCOutputInfo;
public class Translator {
diff --git a/src/main/java/de/b2tla/analysis/Ast2String.java b/src/main/java/de/tlc4b/analysis/Ast2String.java
similarity index 93%
rename from src/main/java/de/b2tla/analysis/Ast2String.java
rename to src/main/java/de/tlc4b/analysis/Ast2String.java
index ac4611e55a3e540ea18b9c05a7278c1817a723ac..2802949b6d20c204e8f1b3a24611a6d7c78bcf68 100644
--- a/src/main/java/de/b2tla/analysis/Ast2String.java
+++ b/src/main/java/de/tlc4b/analysis/Ast2String.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import de.be4.classicalb.core.parser.analysis.ExtendedDFAdapter;
import de.be4.classicalb.core.parser.node.Node;
diff --git a/src/main/java/de/b2tla/analysis/ConstantsEliminator.java b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
similarity index 99%
rename from src/main/java/de/b2tla/analysis/ConstantsEliminator.java
rename to src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
index 7766ae9adbe857c9c4765e417bcb77a8e3723243..92b4edeaec52b990a9fd37ac460d1bc34871bf82 100644
--- a/src/main/java/de/b2tla/analysis/ConstantsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEliminator.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.Collection;
import java.util.HashMap;
diff --git a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
rename to src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
index c4d1c7ab13fe3a9db26d18d0979f5b45b677cc91..affde5aae4c9b149fcdf3a64558d0c3d1dc243e7 100644
--- a/src/main/java/de/b2tla/analysis/ConstantsEvaluator.java
+++ b/src/main/java/de/tlc4b/analysis/ConstantsEvaluator.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.Collection;
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java b/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
similarity index 94%
rename from src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
rename to src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
index 82b1784aac6ce664a247ed2c272685ad4a49ecaa..81ce5f7339e3eff65528b58762731975421f6401 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsAnalyser.java
+++ b/src/main/java/de/tlc4b/analysis/DefinitionsAnalyser.java
@@ -1,10 +1,9 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Set;
-import de.b2tla.B2TLAGlobals;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
@@ -14,6 +13,7 @@ import de.be4.classicalb.core.parser.node.AIntegerExpression;
import de.be4.classicalb.core.parser.node.AIntervalExpression;
import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.Node;
+import de.tlc4b.TLC4BGlobals;
/**
*
@@ -84,7 +84,7 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
AExpressionDefinitionDefinition d = (AExpressionDefinitionDefinition) node;
AIntegerExpression sizeExpr = (AIntegerExpression) d.getRhs();
int value = Integer.parseInt(sizeExpr.getLiteral().getText());
- B2TLAGlobals.setMAX_INT(value);
+ TLC4BGlobals.setMAX_INT(value);
} catch (ClassCastException e) {
}
@@ -104,7 +104,7 @@ public class DefinitionsAnalyser extends DepthFirstAdapter {
sizeExpr = (AIntegerExpression) d.getRhs();
value = Integer.parseInt(sizeExpr.getLiteral().getText());
}
- B2TLAGlobals.setMIN_INT(value);
+ TLC4BGlobals.setMIN_INT(value);
} catch (ClassCastException e) {
e.printStackTrace();
}
diff --git a/src/main/java/de/b2tla/analysis/DefinitionsOrder.java b/src/main/java/de/tlc4b/analysis/DefinitionsOrder.java
similarity index 99%
rename from src/main/java/de/b2tla/analysis/DefinitionsOrder.java
rename to src/main/java/de/tlc4b/analysis/DefinitionsOrder.java
index ffd9afb41913c524f0a0ee632704a3b69802b1de..70dd44d3f213a168e9ea0aeb566022f1d552bb61 100644
--- a/src/main/java/de/b2tla/analysis/DefinitionsOrder.java
+++ b/src/main/java/de/tlc4b/analysis/DefinitionsOrder.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.HashSet;
diff --git a/src/main/java/de/b2tla/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/MachineContext.java
rename to src/main/java/de/tlc4b/analysis/MachineContext.java
index 879c6ae55fb0dc1f2a08a55aed3d17dc0207974c..c6f4838c941c61d9efbfacd2b151e80232da468b 100644
--- a/src/main/java/de/b2tla/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.Collection;
@@ -10,9 +10,6 @@ import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
-import de.b2tla.exceptions.ScopeException;
-import de.b2tla.ltl.LTLBPredicate;
-import de.b2tla.ltl.LTLFormulaVisitor;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
@@ -68,6 +65,9 @@ import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.tlc4b.exceptions.ScopeException;
+import de.tlc4b.ltl.LTLBPredicate;
+import de.tlc4b.ltl.LTLFormulaVisitor;
public class MachineContext extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
similarity index 92%
rename from src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
rename to src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
index 3148bcf16f30021622e62a4a1d3fb26456b82e1e..c123bbe89e2018470610bd89365ed5fc9484104b 100644
--- a/src/main/java/de/b2tla/analysis/NotSupportedConstructs.java
+++ b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
@@ -1,11 +1,11 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import de.b2tla.exceptions.NotSupportedException;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.ACaseSubstitution;
import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
import de.be4.classicalb.core.parser.node.AWhileSubstitution;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.exceptions.NotSupportedException;
public class NotSupportedConstructs extends DepthFirstAdapter{
diff --git a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
similarity index 94%
rename from src/main/java/de/b2tla/analysis/PrecedenceCollector.java
rename to src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
index 5d1fae0679fbdac743e884f2b53ef951b8352d01..c3de07198c78606e306ae43e0ad7e923986d7e96 100644
--- a/src/main/java/de/b2tla/analysis/PrecedenceCollector.java
+++ b/src/main/java/de/tlc4b/analysis/PrecedenceCollector.java
@@ -1,16 +1,16 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.HashSet;
import java.util.Hashtable;
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.IntegerType;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression;
import de.be4.classicalb.core.parser.node.AMultOrCartExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.IntegerType;
public class PrecedenceCollector extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/analysis/PrimedNodesMarker.java b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
similarity index 94%
rename from src/main/java/de/b2tla/analysis/PrimedNodesMarker.java
rename to src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
index a14730da4e82e5b785fee8a97916bfb87d5a5c3e..708bf5ab9364637a3a20f2175f7f10340afc903c 100644
--- a/src/main/java/de/b2tla/analysis/PrimedNodesMarker.java
+++ b/src/main/java/de/tlc4b/analysis/PrimedNodesMarker.java
@@ -1,10 +1,9 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
-import de.b2tla.exceptions.ScopeException;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
@@ -15,6 +14,7 @@ import de.be4.classicalb.core.parser.node.APrimedIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.POperation;
+import de.tlc4b.exceptions.ScopeException;
public class PrimedNodesMarker extends DepthFirstAdapter {
private ArrayList<POperation> operations;
diff --git a/src/main/java/de/b2tla/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/Renamer.java
rename to src/main/java/de/tlc4b/analysis/Renamer.java
index 477d8f64d4da8e9390f66d1b1040f1a65cb773f4..7308851035e3c6443a93f98aed80e6e049e5f9ee 100644
--- a/src/main/java/de/b2tla/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.HashSet;
diff --git a/src/main/java/de/b2tla/analysis/StandardMadules.java b/src/main/java/de/tlc4b/analysis/StandardMadules.java
similarity index 97%
rename from src/main/java/de/b2tla/analysis/StandardMadules.java
rename to src/main/java/de/tlc4b/analysis/StandardMadules.java
index 3919f7510ff3584316ef9eac8f409184b7577f71..34d0e2277db51046e9aca1e8cc5b1db1a6681328 100644
--- a/src/main/java/de/b2tla/analysis/StandardMadules.java
+++ b/src/main/java/de/tlc4b/analysis/StandardMadules.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.HashSet;
diff --git a/src/main/java/de/b2tla/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
similarity index 95%
rename from src/main/java/de/b2tla/analysis/Typechecker.java
rename to src/main/java/de/tlc4b/analysis/Typechecker.java
index afba565867bee66997820a7dbf6fed59b67a0180..e62924005c0359b6d71dd41a7af1805d7b622cb7 100644
--- a/src/main/java/de/b2tla/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.Collection;
@@ -9,27 +9,27 @@ import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
-import de.b2tla.btypes.AbstractHasFollowers;
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.BoolType;
-import de.b2tla.btypes.FunctionType;
-import de.b2tla.btypes.ITypechecker;
-import de.b2tla.btypes.IntegerOrSetOfPairType;
-import de.b2tla.btypes.IntegerOrSetType;
-import de.b2tla.btypes.IntegerType;
-import de.b2tla.btypes.ModelValueType;
-import de.b2tla.btypes.PairType;
-import de.b2tla.btypes.SetType;
-import de.b2tla.btypes.StringType;
-import de.b2tla.btypes.StructType;
-import de.b2tla.btypes.UntypedType;
-import de.b2tla.exceptions.TypeErrorException;
-import de.b2tla.exceptions.UnificationException;
-import de.b2tla.ltl.LTLBPredicate;
-import de.b2tla.ltl.LTLFormulaVisitor;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
+import de.tlc4b.btypes.AbstractHasFollowers;
+import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.BoolType;
+import de.tlc4b.btypes.FunctionType;
+import de.tlc4b.btypes.ITypechecker;
+import de.tlc4b.btypes.IntegerOrSetOfPairType;
+import de.tlc4b.btypes.IntegerOrSetType;
+import de.tlc4b.btypes.IntegerType;
+import de.tlc4b.btypes.ModelValueType;
+import de.tlc4b.btypes.PairType;
+import de.tlc4b.btypes.SetType;
+import de.tlc4b.btypes.StringType;
+import de.tlc4b.btypes.StructType;
+import de.tlc4b.btypes.UntypedType;
+import de.tlc4b.exceptions.TypeErrorException;
+import de.tlc4b.exceptions.UnificationException;
+import de.tlc4b.ltl.LTLBPredicate;
+import de.tlc4b.ltl.LTLFormulaVisitor;
/**
* TODO we need a second run over ast to check if all local variables have a
diff --git a/src/main/java/de/b2tla/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/UsedStandardModules.java
rename to src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 143c459c54cf94700aca92e38e3d4c8f07201fb2..1dfc41bb33169638323c7f57ecc2915498aad222 100644
--- a/src/main/java/de/b2tla/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import java.util.ArrayList;
import java.util.Comparator;
@@ -7,11 +7,6 @@ import java.util.List;
import java.util.Set;
import java.util.Collections;
-import de.b2tla.analysis.typerestriction.TypeRestrictor;
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.FunctionType;
-import de.b2tla.btypes.IntegerType;
-import de.b2tla.btypes.SetType;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAddExpression;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
@@ -102,6 +97,11 @@ import de.be4.classicalb.core.parser.node.ATransRelationExpression;
import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
+import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.FunctionType;
+import de.tlc4b.btypes.IntegerType;
+import de.tlc4b.btypes.SetType;
public class UsedStandardModules extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/analysis/nodes/ElementOfNode.java b/src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java
similarity index 83%
rename from src/main/java/de/b2tla/analysis/nodes/ElementOfNode.java
rename to src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java
index 2ec06c2b6c450d0f18edf562a1cb478630726e43..176ed354403f5c61e6e21c8f82cbaac60733a853 100644
--- a/src/main/java/de/b2tla/analysis/nodes/ElementOfNode.java
+++ b/src/main/java/de/tlc4b/analysis/nodes/ElementOfNode.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis.nodes;
+package de.tlc4b.analysis.nodes;
import de.be4.classicalb.core.parser.node.PExpression;
diff --git a/src/main/java/de/b2tla/analysis/nodes/EqualsNode.java b/src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java
similarity index 83%
rename from src/main/java/de/b2tla/analysis/nodes/EqualsNode.java
rename to src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java
index 4741a35af4bbd5972e5a52c03d8b90015a237960..774252c8359e4ba44190f1707bab6dc157a78965 100644
--- a/src/main/java/de/b2tla/analysis/nodes/EqualsNode.java
+++ b/src/main/java/de/tlc4b/analysis/nodes/EqualsNode.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis.nodes;
+package de.tlc4b.analysis.nodes;
import de.be4.classicalb.core.parser.node.PExpression;
diff --git a/src/main/java/de/b2tla/analysis/nodes/NodeType.java b/src/main/java/de/tlc4b/analysis/nodes/NodeType.java
similarity index 75%
rename from src/main/java/de/b2tla/analysis/nodes/NodeType.java
rename to src/main/java/de/tlc4b/analysis/nodes/NodeType.java
index a226ab6f453b63e41968dd592b43cd4cb4888551..336eb05f9394c9e47449f1e3212e92e02ec7cc41 100644
--- a/src/main/java/de/b2tla/analysis/nodes/NodeType.java
+++ b/src/main/java/de/tlc4b/analysis/nodes/NodeType.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis.nodes;
+package de.tlc4b.analysis.nodes;
import de.be4.classicalb.core.parser.node.PExpression;
diff --git a/src/main/java/de/b2tla/analysis/nodes/SubsetNode.java b/src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java
similarity index 88%
rename from src/main/java/de/b2tla/analysis/nodes/SubsetNode.java
rename to src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java
index 77b4913bc23611f1dac23275d851c99b3b77dfa3..a83e9614dc4e037fa24682edb321c6bf4e986abf 100644
--- a/src/main/java/de/b2tla/analysis/nodes/SubsetNode.java
+++ b/src/main/java/de/tlc4b/analysis/nodes/SubsetNode.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis.nodes;
+package de.tlc4b.analysis.nodes;
import de.be4.classicalb.core.parser.node.PExpression;
diff --git a/src/main/java/de/b2tla/analysis/transformation/DefinitionCollector.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
similarity index 95%
rename from src/main/java/de/b2tla/analysis/transformation/DefinitionCollector.java
rename to src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
index 927a0694e63d6fb9d321649fad475dd3dc07094e..11287b5f6fa4fcaa7805755505c677ab2b46dbfc 100644
--- a/src/main/java/de/b2tla/analysis/transformation/DefinitionCollector.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis.transformation;
+package de.tlc4b.analysis.transformation;
import java.util.Hashtable;
diff --git a/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
similarity index 96%
rename from src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
rename to src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index 79419bffd2afbeb231aeffff6b9fc408de3eb9c5..39e8517fe77d7217ba50b4cb69ae6bbff3398ffb 100644
--- a/src/main/java/de/b2tla/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -1,4 +1,4 @@
-package de.b2tla.analysis.transformation;
+package de.tlc4b.analysis.transformation;
import java.util.ArrayList;
import java.util.Hashtable;
diff --git a/src/main/java/de/b2tla/analysis/typerestriction/IdentifierDependencies.java b/src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java
similarity index 94%
rename from src/main/java/de/b2tla/analysis/typerestriction/IdentifierDependencies.java
rename to src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java
index 67a8993f850e273d871e8a89904347e2bf1783f2..932d2dcde522c3d2f974f43464afc5f0a88e074c 100644
--- a/src/main/java/de/b2tla/analysis/typerestriction/IdentifierDependencies.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/IdentifierDependencies.java
@@ -1,12 +1,12 @@
-package de.b2tla.analysis.typerestriction;
+package de.tlc4b.analysis.typerestriction;
import java.util.HashMap;
import java.util.HashSet;
-import de.b2tla.analysis.MachineContext;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
+import de.tlc4b.analysis.MachineContext;
public class IdentifierDependencies extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
similarity index 94%
rename from src/main/java/de/b2tla/analysis/typerestriction/TypeRestrictor.java
rename to src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 2ae78ec3d90fdfe08e06e3522ef5ce10538cdbab..2a3c794dac855147464ab0f52f4f58fd96227a5b 100644
--- a/src/main/java/de/b2tla/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -1,17 +1,10 @@
-package de.b2tla.analysis.typerestriction;
+package de.tlc4b.analysis.typerestriction;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.nodes.ElementOfNode;
-import de.b2tla.analysis.nodes.EqualsNode;
-import de.b2tla.analysis.nodes.NodeType;
-import de.b2tla.analysis.nodes.SubsetNode;
-import de.b2tla.ltl.LTLFormulaVisitor;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
@@ -42,6 +35,13 @@ import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.ltl.core.parser.node.AExistsLtl;
import de.be4.ltl.core.parser.node.AForallLtl;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.analysis.nodes.ElementOfNode;
+import de.tlc4b.analysis.nodes.EqualsNode;
+import de.tlc4b.analysis.nodes.NodeType;
+import de.tlc4b.analysis.nodes.SubsetNode;
+import de.tlc4b.ltl.LTLFormulaVisitor;
public class TypeRestrictor extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/analysis/unchangedvariables/AssignedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
similarity index 95%
rename from src/main/java/de/b2tla/analysis/unchangedvariables/AssignedVariablesFinder.java
rename to src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
index a682f462fe8fb6b55c933ed4d223be16f64b1f56..a59cfb9db15a4a68feec53be6016b58765f2ccb2 100644
--- a/src/main/java/de/b2tla/analysis/unchangedvariables/AssignedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/AssignedVariablesFinder.java
@@ -1,12 +1,10 @@
-package de.b2tla.analysis.unchangedvariables;
+package de.tlc4b.analysis.unchangedvariables;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.exceptions.SubstitutionException;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
@@ -30,6 +28,8 @@ import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PSubstitution;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.exceptions.SubstitutionException;
/**
*
diff --git a/src/main/java/de/b2tla/analysis/unchangedvariables/UnchangedVariablesFinder.java b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
similarity index 95%
rename from src/main/java/de/b2tla/analysis/unchangedvariables/UnchangedVariablesFinder.java
rename to src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
index ff79eb09b1a38d9254f8e5db24959f52d93e2f17..1a51f57c409a7002b83e84f485c4630b49ea60ee 100644
--- a/src/main/java/de/b2tla/analysis/unchangedvariables/UnchangedVariablesFinder.java
+++ b/src/main/java/de/tlc4b/analysis/unchangedvariables/UnchangedVariablesFinder.java
@@ -1,12 +1,10 @@
-package de.b2tla.analysis.unchangedvariables;
+package de.tlc4b.analysis.unchangedvariables;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.List;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.exceptions.SubstitutionException;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AAssertionSubstitution;
@@ -30,6 +28,8 @@ import de.be4.classicalb.core.parser.node.ASkipSubstitution;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PSubstitution;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.exceptions.SubstitutionException;
/**
* This class is a tree walker which calculates all missing variables
diff --git a/src/main/java/de/b2tla/btypes/AbstractHasFollowers.java b/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
similarity index 94%
rename from src/main/java/de/b2tla/btypes/AbstractHasFollowers.java
rename to src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
index 2211a0687bfadbd2190fad8cf3e0dfce941f3e06..c49be299a838dfc1b494e793f3fd8aba0362f615 100644
--- a/src/main/java/de/b2tla/btypes/AbstractHasFollowers.java
+++ b/src/main/java/de/tlc4b/btypes/AbstractHasFollowers.java
@@ -1,4 +1,4 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
import java.util.ArrayList;
diff --git a/src/main/java/de/b2tla/btypes/BType.java b/src/main/java/de/tlc4b/btypes/BType.java
similarity index 82%
rename from src/main/java/de/b2tla/btypes/BType.java
rename to src/main/java/de/tlc4b/btypes/BType.java
index af611ff221e9ff17b9e0c381bb872108cc3f0595..01147cf416a0fb6590acaacf41cff6187cfcd582 100644
--- a/src/main/java/de/b2tla/btypes/BType.java
+++ b/src/main/java/de/tlc4b/btypes/BType.java
@@ -1,7 +1,7 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
public interface BType extends ITypeConstants{
public BType unify(BType other, ITypechecker typechecker);
diff --git a/src/main/java/de/b2tla/btypes/BoolType.java b/src/main/java/de/tlc4b/btypes/BoolType.java
similarity index 87%
rename from src/main/java/de/b2tla/btypes/BoolType.java
rename to src/main/java/de/tlc4b/btypes/BoolType.java
index 64cba2652f67ad68fc83a1fbbc28d7bde0bfdf3e..4206654236388d72226907ecf274ee861811bae0 100644
--- a/src/main/java/de/b2tla/btypes/BoolType.java
+++ b/src/main/java/de/tlc4b/btypes/BoolType.java
@@ -1,9 +1,9 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.ABoolSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class BoolType implements BType {
diff --git a/src/main/java/de/b2tla/btypes/FunctionType.java b/src/main/java/de/tlc4b/btypes/FunctionType.java
similarity index 93%
rename from src/main/java/de/b2tla/btypes/FunctionType.java
rename to src/main/java/de/tlc4b/btypes/FunctionType.java
index e3333fc87ee7d014e6431ec1acb1d9257f41cdbb..3653f2d1a397f9c20acfc329928ac98fbaad453b 100644
--- a/src/main/java/de/b2tla/btypes/FunctionType.java
+++ b/src/main/java/de/tlc4b/btypes/FunctionType.java
@@ -1,9 +1,9 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class FunctionType extends AbstractHasFollowers {
private BType domain;
diff --git a/src/main/java/de/b2tla/btypes/ITypeConstants.java b/src/main/java/de/tlc4b/btypes/ITypeConstants.java
similarity index 72%
rename from src/main/java/de/b2tla/btypes/ITypeConstants.java
rename to src/main/java/de/tlc4b/btypes/ITypeConstants.java
index 8ee546976e290fd998a918b1f79166b31f48fb8f..70822584085caea3fa9a3e3a28a7ad5d353238d2 100644
--- a/src/main/java/de/b2tla/btypes/ITypeConstants.java
+++ b/src/main/java/de/tlc4b/btypes/ITypeConstants.java
@@ -1,4 +1,4 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
public interface ITypeConstants {
diff --git a/src/main/java/de/b2tla/btypes/ITypechecker.java b/src/main/java/de/tlc4b/btypes/ITypechecker.java
similarity index 86%
rename from src/main/java/de/b2tla/btypes/ITypechecker.java
rename to src/main/java/de/tlc4b/btypes/ITypechecker.java
index d4c842e545df5cbcc668cc2a851bb95ef9b12d92..f620866b1ee900e0b5989a1c6f4d3c13749784d1 100644
--- a/src/main/java/de/b2tla/btypes/ITypechecker.java
+++ b/src/main/java/de/tlc4b/btypes/ITypechecker.java
@@ -1,4 +1,4 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
import de.be4.classicalb.core.parser.node.Node;
diff --git a/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
similarity index 94%
rename from src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
rename to src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
index c7a17bd8ec8bab7de0432d52f7f5b5871fc603de..f1a83cda661e3d466ac33566f05d2532bce78359 100644
--- a/src/main/java/de/b2tla/btypes/IntegerOrSetOfPairType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetOfPairType.java
@@ -1,10 +1,10 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.TypeErrorException;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.PExpression;
import de.hhu.stups.sablecc.patch.SourcePosition;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.TypeErrorException;
+import de.tlc4b.exceptions.UnificationException;
public class IntegerOrSetOfPairType extends AbstractHasFollowers {
diff --git a/src/main/java/de/b2tla/btypes/IntegerOrSetType.java b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
similarity index 89%
rename from src/main/java/de/b2tla/btypes/IntegerOrSetType.java
rename to src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
index cbc286ac6b128d851f7a3f75d6b7fc2e2b72c140..77765c9612441edba6106056348ab947340ba487 100644
--- a/src/main/java/de/b2tla/btypes/IntegerOrSetType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerOrSetType.java
@@ -1,8 +1,8 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class IntegerOrSetType extends AbstractHasFollowers {
diff --git a/src/main/java/de/b2tla/btypes/IntegerType.java b/src/main/java/de/tlc4b/btypes/IntegerType.java
similarity index 84%
rename from src/main/java/de/b2tla/btypes/IntegerType.java
rename to src/main/java/de/tlc4b/btypes/IntegerType.java
index 2d9dd4438fd52f3e75d9da57e4652250842127bc..70cbe3cfdbde080b9c7f01716089537f0a7f19b9 100644
--- a/src/main/java/de/b2tla/btypes/IntegerType.java
+++ b/src/main/java/de/tlc4b/btypes/IntegerType.java
@@ -1,10 +1,10 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.B2TLAGlobals;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class IntegerType implements BType {
@@ -41,7 +41,7 @@ public class IntegerType implements BType {
}
public String getTlaType() {
- return B2TLAGlobals.getMIN_INT() + ".." + B2TLAGlobals.getMAX_INT();
+ return TLC4BGlobals.getMIN_INT() + ".." + TLC4BGlobals.getMAX_INT();
}
diff --git a/src/main/java/de/b2tla/btypes/ModelValueType.java b/src/main/java/de/tlc4b/btypes/ModelValueType.java
similarity index 89%
rename from src/main/java/de/b2tla/btypes/ModelValueType.java
rename to src/main/java/de/tlc4b/btypes/ModelValueType.java
index c5eb10a4765e97c2221f5fb0ef2bbb986e16c0f9..0be4a04cbc8b60a68b2a52aa91b3590b7d5c1445 100644
--- a/src/main/java/de/b2tla/btypes/ModelValueType.java
+++ b/src/main/java/de/tlc4b/btypes/ModelValueType.java
@@ -1,12 +1,12 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
import java.util.ArrayList;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class ModelValueType implements BType {
private String name;
diff --git a/src/main/java/de/b2tla/btypes/PairType.java b/src/main/java/de/tlc4b/btypes/PairType.java
similarity index 92%
rename from src/main/java/de/b2tla/btypes/PairType.java
rename to src/main/java/de/tlc4b/btypes/PairType.java
index 6f0274770dac65ee0a16dbeb1f9f4eab73af146f..6e3afd0f305a7f879f01a5057608f0257e1469f0 100644
--- a/src/main/java/de/b2tla/btypes/PairType.java
+++ b/src/main/java/de/tlc4b/btypes/PairType.java
@@ -1,9 +1,9 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.ACartesianProductExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class PairType extends AbstractHasFollowers {
diff --git a/src/main/java/de/b2tla/btypes/SetType.java b/src/main/java/de/tlc4b/btypes/SetType.java
similarity index 91%
rename from src/main/java/de/b2tla/btypes/SetType.java
rename to src/main/java/de/tlc4b/btypes/SetType.java
index 04d84de70ec69b0cd30c5653f41300ece3720efd..2661434a1ecc1ecad02c24958d94fef2884a5831 100644
--- a/src/main/java/de/b2tla/btypes/SetType.java
+++ b/src/main/java/de/tlc4b/btypes/SetType.java
@@ -1,9 +1,9 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class SetType extends AbstractHasFollowers {
diff --git a/src/main/java/de/b2tla/btypes/StringType.java b/src/main/java/de/tlc4b/btypes/StringType.java
similarity index 87%
rename from src/main/java/de/b2tla/btypes/StringType.java
rename to src/main/java/de/tlc4b/btypes/StringType.java
index 74cf5dba25ec11ce66fe97b2a65e4ba9bbdd5bf0..ed5c511f0a8cfb7680769477ad4625871f799d6d 100644
--- a/src/main/java/de/b2tla/btypes/StringType.java
+++ b/src/main/java/de/tlc4b/btypes/StringType.java
@@ -1,9 +1,9 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class StringType implements BType {
diff --git a/src/main/java/de/b2tla/btypes/StructType.java b/src/main/java/de/tlc4b/btypes/StructType.java
similarity index 94%
rename from src/main/java/de/b2tla/btypes/StructType.java
rename to src/main/java/de/tlc4b/btypes/StructType.java
index d4cbdfa5c40770d877f422e581ec4ca26650b83c..79d4298dd51190b49777998eab335557d6ab0b78 100644
--- a/src/main/java/de/b2tla/btypes/StructType.java
+++ b/src/main/java/de/tlc4b/btypes/StructType.java
@@ -1,4 +1,4 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
import java.util.ArrayList;
import java.util.HashSet;
@@ -6,14 +6,14 @@ import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Set;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.exceptions.UnificationException;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ARecEntry;
import de.be4.classicalb.core.parser.node.AStructExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PRecEntry;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.exceptions.UnificationException;
public class StructType extends AbstractHasFollowers {
diff --git a/src/main/java/de/b2tla/btypes/UntypedType.java b/src/main/java/de/tlc4b/btypes/UntypedType.java
similarity index 87%
rename from src/main/java/de/b2tla/btypes/UntypedType.java
rename to src/main/java/de/tlc4b/btypes/UntypedType.java
index 808d6b5796eaa8fd5348027f3ffa3e7cc1586b74..edf9e049e4ff704134316c0b03caeb4699050f38 100644
--- a/src/main/java/de/b2tla/btypes/UntypedType.java
+++ b/src/main/java/de/tlc4b/btypes/UntypedType.java
@@ -1,7 +1,7 @@
-package de.b2tla.btypes;
+package de.tlc4b.btypes;
-import de.b2tla.analysis.Typechecker;
import de.be4.classicalb.core.parser.node.PExpression;
+import de.tlc4b.analysis.Typechecker;
public class UntypedType extends AbstractHasFollowers {
diff --git a/src/main/java/de/b2tla/exceptions/LTLParseException.java b/src/main/java/de/tlc4b/exceptions/LTLParseException.java
similarity index 64%
rename from src/main/java/de/b2tla/exceptions/LTLParseException.java
rename to src/main/java/de/tlc4b/exceptions/LTLParseException.java
index 74c017d00ae0a23895bf22ef8502af75c30e560e..c7cc54a84ed713a7c4e7bb2dfe7e1e4a02ca0675 100644
--- a/src/main/java/de/b2tla/exceptions/LTLParseException.java
+++ b/src/main/java/de/tlc4b/exceptions/LTLParseException.java
@@ -1,7 +1,7 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
-public class LTLParseException extends B2tlaException{
+public class LTLParseException extends TLC4BException{
public LTLParseException(String e) {
super(e);
diff --git a/src/main/java/de/b2tla/exceptions/NotSupportedException.java b/src/main/java/de/tlc4b/exceptions/NotSupportedException.java
similarity index 65%
rename from src/main/java/de/b2tla/exceptions/NotSupportedException.java
rename to src/main/java/de/tlc4b/exceptions/NotSupportedException.java
index 8d7abb93602c5eae37387990425d4536b20bd66f..476c3556229951f09ac90ad3d80aba2efa4a9df9 100644
--- a/src/main/java/de/b2tla/exceptions/NotSupportedException.java
+++ b/src/main/java/de/tlc4b/exceptions/NotSupportedException.java
@@ -1,7 +1,7 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
-public class NotSupportedException extends B2tlaException{
+public class NotSupportedException extends TLC4BException{
public NotSupportedException(String e){
diff --git a/src/main/java/de/b2tla/exceptions/NotSupportedLTLFormulaException.java b/src/main/java/de/tlc4b/exceptions/NotSupportedLTLFormulaException.java
similarity index 66%
rename from src/main/java/de/b2tla/exceptions/NotSupportedLTLFormulaException.java
rename to src/main/java/de/tlc4b/exceptions/NotSupportedLTLFormulaException.java
index 078dc61e07ab4181128a9faea93fbf75e5ca3121..8d36dac7f695c6e53cb074f427f6100ca81c650b 100644
--- a/src/main/java/de/b2tla/exceptions/NotSupportedLTLFormulaException.java
+++ b/src/main/java/de/tlc4b/exceptions/NotSupportedLTLFormulaException.java
@@ -1,7 +1,7 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
-public class NotSupportedLTLFormulaException extends B2tlaException{
+public class NotSupportedLTLFormulaException extends TLC4BException{
public NotSupportedLTLFormulaException(String e) {
super(e);
diff --git a/src/main/java/de/b2tla/exceptions/ScopeException.java b/src/main/java/de/tlc4b/exceptions/ScopeException.java
similarity index 61%
rename from src/main/java/de/b2tla/exceptions/ScopeException.java
rename to src/main/java/de/tlc4b/exceptions/ScopeException.java
index ee7a231941a2e5fac3b1640731956a34ae071de8..2a38f1c2016a2ce5f46f719f406cdc8b81071bc7 100644
--- a/src/main/java/de/b2tla/exceptions/ScopeException.java
+++ b/src/main/java/de/tlc4b/exceptions/ScopeException.java
@@ -1,7 +1,7 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
-public class ScopeException extends B2tlaException{
+public class ScopeException extends TLC4BException{
public ScopeException(String e){
super(e);
diff --git a/src/main/java/de/b2tla/exceptions/SubstitutionException.java b/src/main/java/de/tlc4b/exceptions/SubstitutionException.java
similarity index 61%
rename from src/main/java/de/b2tla/exceptions/SubstitutionException.java
rename to src/main/java/de/tlc4b/exceptions/SubstitutionException.java
index 12074af2bfede2fb42c10deb07229c29e0ca6dc9..0dc1d3af77064354d3f989deb18e654ed7a309c7 100644
--- a/src/main/java/de/b2tla/exceptions/SubstitutionException.java
+++ b/src/main/java/de/tlc4b/exceptions/SubstitutionException.java
@@ -1,7 +1,7 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
-public class SubstitutionException extends B2tlaException{
+public class SubstitutionException extends TLC4BException{
public SubstitutionException(String e) {
super(e);
diff --git a/src/main/java/de/tlc4b/exceptions/TLC4BException.java b/src/main/java/de/tlc4b/exceptions/TLC4BException.java
new file mode 100644
index 0000000000000000000000000000000000000000..5c4090a5698ebf1c4b1f38a5b87e30318d99eb9c
--- /dev/null
+++ b/src/main/java/de/tlc4b/exceptions/TLC4BException.java
@@ -0,0 +1,12 @@
+package de.tlc4b.exceptions;
+
+@SuppressWarnings("serial")
+public abstract class TLC4BException extends RuntimeException {
+
+ public TLC4BException(String e) {
+ super(e);
+ }
+
+ public abstract String getError();
+
+}
diff --git a/src/main/java/de/tlc4b/exceptions/TLC4BIOException.java b/src/main/java/de/tlc4b/exceptions/TLC4BIOException.java
new file mode 100644
index 0000000000000000000000000000000000000000..9d5f308b44b1416a866ab812a24ca91a724fab53
--- /dev/null
+++ b/src/main/java/de/tlc4b/exceptions/TLC4BIOException.java
@@ -0,0 +1,15 @@
+package de.tlc4b.exceptions;
+
+@SuppressWarnings("serial")
+public class TLC4BIOException extends TLC4BException{
+
+ public TLC4BIOException(String e) {
+ super(e);
+ }
+
+ @Override
+ public String getError() {
+ return "I/O Error";
+ }
+
+}
diff --git a/src/main/java/de/b2tla/exceptions/TypeErrorException.java b/src/main/java/de/tlc4b/exceptions/TypeErrorException.java
similarity index 60%
rename from src/main/java/de/b2tla/exceptions/TypeErrorException.java
rename to src/main/java/de/tlc4b/exceptions/TypeErrorException.java
index 52b29141ce0db07b316ccc8ea82be9b13b49d762..77a201ccad0ae6e7dfd920c5005fbb09d48d005e 100644
--- a/src/main/java/de/b2tla/exceptions/TypeErrorException.java
+++ b/src/main/java/de/tlc4b/exceptions/TypeErrorException.java
@@ -1,7 +1,7 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
-public class TypeErrorException extends B2tlaException {
+public class TypeErrorException extends TLC4BException {
public TypeErrorException(String e) {
super(e);
diff --git a/src/main/java/de/b2tla/exceptions/UnificationException.java b/src/main/java/de/tlc4b/exceptions/UnificationException.java
similarity index 78%
rename from src/main/java/de/b2tla/exceptions/UnificationException.java
rename to src/main/java/de/tlc4b/exceptions/UnificationException.java
index 1a08bb906cc636723c691c6fdd3ea11378382db6..676d270928b5cbd3e8ff4b633cf5f3d0c5dbacbb 100644
--- a/src/main/java/de/b2tla/exceptions/UnificationException.java
+++ b/src/main/java/de/tlc4b/exceptions/UnificationException.java
@@ -1,4 +1,4 @@
-package de.b2tla.exceptions;
+package de.tlc4b.exceptions;
@SuppressWarnings("serial")
public class UnificationException extends RuntimeException{
diff --git a/src/main/java/de/b2tla/ltl/LTLBPredicate.java b/src/main/java/de/tlc4b/ltl/LTLBPredicate.java
similarity index 97%
rename from src/main/java/de/b2tla/ltl/LTLBPredicate.java
rename to src/main/java/de/tlc4b/ltl/LTLBPredicate.java
index 15e36dbea88c0c544f5ca290664f491dbc4a81b0..59661f6b272458202ad8f8d7e5410f6a7a3e9112 100644
--- a/src/main/java/de/b2tla/ltl/LTLBPredicate.java
+++ b/src/main/java/de/tlc4b/ltl/LTLBPredicate.java
@@ -1,4 +1,4 @@
-package de.b2tla.ltl;
+package de.tlc4b.ltl;
import java.util.ArrayList;
import java.util.LinkedHashMap;
diff --git a/src/main/java/de/b2tla/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
similarity index 98%
rename from src/main/java/de/b2tla/ltl/LTLFormulaPrinter.java
rename to src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
index cf61f13f384869139eb5b0e41e9bd1adfbbdace7..e466d733cc67e6e76616a41b60e87ca4928500a5 100644
--- a/src/main/java/de/b2tla/ltl/LTLFormulaPrinter.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java
@@ -1,6 +1,5 @@
-package de.b2tla.ltl;
+package de.tlc4b.ltl;
-import de.b2tla.prettyprint.TLAPrinter;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.ltl.core.parser.analysis.DepthFirstAdapter;
@@ -19,6 +18,7 @@ import de.be4.ltl.core.parser.node.AStrongFairLtl;
import de.be4.ltl.core.parser.node.ATrueLtl;
import de.be4.ltl.core.parser.node.AUnparsedLtl;
import de.be4.ltl.core.parser.node.AWeakFairLtl;
+import de.tlc4b.prettyprint.TLAPrinter;
public class LTLFormulaPrinter extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/ltl/LTLFormulaVisitor.java b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
similarity index 97%
rename from src/main/java/de/b2tla/ltl/LTLFormulaVisitor.java
rename to src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
index b0cbf5ac981c0285dd7fbc33ccea94ef31dfc4dc..750f05a3e1635e6fcf15c9e9422d0ba9245f4813 100644
--- a/src/main/java/de/b2tla/ltl/LTLFormulaVisitor.java
+++ b/src/main/java/de/tlc4b/ltl/LTLFormulaVisitor.java
@@ -1,4 +1,4 @@
-package de.b2tla.ltl;
+package de.tlc4b.ltl;
import java.io.PushbackReader;
import java.io.StringReader;
@@ -8,10 +8,6 @@ import java.util.Hashtable;
import java.util.LinkedHashMap;
import java.util.List;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.exceptions.LTLParseException;
-import de.b2tla.exceptions.ScopeException;
-import de.b2tla.prettyprint.TLAPrinter;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -38,6 +34,10 @@ 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.MachineContext;
+import de.tlc4b.exceptions.LTLParseException;
+import de.tlc4b.exceptions.ScopeException;
+import de.tlc4b.prettyprint.TLAPrinter;
public class LTLFormulaVisitor extends DepthFirstAdapter {
diff --git a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
similarity index 94%
rename from src/main/java/de/b2tla/prettyprint/TLAPrinter.java
rename to src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index e85f28fca20e625b4b0f594f585551bd7b0adf92..1e6b7fe895c5cf13abb648c7ac4067b21ffda2de 100644
--- a/src/main/java/de/b2tla/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -1,4 +1,4 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
import java.util.ArrayList;
import java.util.HashSet;
@@ -6,34 +6,34 @@ import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
-import de.b2tla.B2TLAGlobals;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.PrecedenceCollector;
-import de.b2tla.analysis.PrimedNodesMarker;
-import de.b2tla.analysis.Renamer;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.UsedStandardModules;
-import de.b2tla.analysis.nodes.EqualsNode;
-import de.b2tla.analysis.nodes.NodeType;
-import de.b2tla.analysis.nodes.SubsetNode;
-import de.b2tla.analysis.typerestriction.TypeRestrictor;
-import de.b2tla.analysis.unchangedvariables.UnchangedVariablesFinder;
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.FunctionType;
-import de.b2tla.btypes.IntegerType;
-import de.b2tla.btypes.PairType;
-import de.b2tla.btypes.SetType;
-import de.b2tla.btypes.StructType;
-import de.b2tla.btypes.UntypedType;
-import de.b2tla.ltl.LTLFormulaVisitor;
-import de.b2tla.tla.ConfigFile;
-import de.b2tla.tla.TLADefinition;
-import de.b2tla.tla.TLAModule;
-import de.b2tla.tla.config.ConfigFileAssignment;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
-import static de.b2tla.analysis.StandardMadules.*;
+import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.PrecedenceCollector;
+import de.tlc4b.analysis.PrimedNodesMarker;
+import de.tlc4b.analysis.Renamer;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.analysis.UsedStandardModules;
+import de.tlc4b.analysis.nodes.EqualsNode;
+import de.tlc4b.analysis.nodes.NodeType;
+import de.tlc4b.analysis.nodes.SubsetNode;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
+import de.tlc4b.analysis.unchangedvariables.UnchangedVariablesFinder;
+import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.FunctionType;
+import de.tlc4b.btypes.IntegerType;
+import de.tlc4b.btypes.PairType;
+import de.tlc4b.btypes.SetType;
+import de.tlc4b.btypes.StructType;
+import de.tlc4b.btypes.UntypedType;
+import de.tlc4b.ltl.LTLFormulaVisitor;
+import de.tlc4b.tla.ConfigFile;
+import de.tlc4b.tla.TLADefinition;
+import de.tlc4b.tla.TLAModule;
+import de.tlc4b.tla.config.ConfigFileAssignment;
+import static de.tlc4b.analysis.StandardMadules.*;
public class TLAPrinter extends DepthFirstAdapter {
@@ -195,7 +195,7 @@ public class TLAPrinter extends DepthFirstAdapter {
this.configFileString.append("NEXT Next\n");
}
}
- if (B2TLAGlobals.isInvariant()) {
+ if (TLC4BGlobals.isInvariant()) {
for (int i = 0; i < configFile.getInvariantNumber(); i++) {
this.configFileString.append("INVARIANT Invariant" + (i + 1)
+ "\n");
@@ -214,7 +214,7 @@ public class TLAPrinter extends DepthFirstAdapter {
}
- if (B2TLAGlobals.isCheckltl()) {
+ if (TLC4BGlobals.isCheckltl()) {
for (int i = 0; i < machineContext.getLTLFormulas().size(); i++) {
LTLFormulaVisitor ltlVisitor = machineContext.getLTLFormulas()
.get(i);
@@ -1451,12 +1451,12 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseAMaxIntExpression(AMaxIntExpression node) {
- tlaModuleString.append(B2TLAGlobals.getMAX_INT());
+ tlaModuleString.append(TLC4BGlobals.getMAX_INT());
}
@Override
public void caseAMinIntExpression(AMinIntExpression node) {
- tlaModuleString.append(B2TLAGlobals.getMIN_INT());
+ tlaModuleString.append(TLC4BGlobals.getMIN_INT());
}
/**
@@ -1617,7 +1617,7 @@ public class TLAPrinter extends DepthFirstAdapter {
tlaModuleString.append("]");
} else {
- if(B2TLAGlobals.checkWelldefinedness()){
+ if(TLC4BGlobals.checkWelldefinedness()){
tlaModuleString.append(REL_CALL + "(");
}else{
tlaModuleString.append(REL_CALL_WITHOUT_WD_CHECK + "(");
diff --git a/src/main/java/de/b2tla/tla/ConfigFile.java b/src/main/java/de/tlc4b/tla/ConfigFile.java
similarity index 88%
rename from src/main/java/de/b2tla/tla/ConfigFile.java
rename to src/main/java/de/tlc4b/tla/ConfigFile.java
index 28eb9846ff87e977646bd0b9d40ba1369ae01ae3..5288a676f98e41f3b2cc4bc65a8f28c628653f30 100644
--- a/src/main/java/de/b2tla/tla/ConfigFile.java
+++ b/src/main/java/de/tlc4b/tla/ConfigFile.java
@@ -1,8 +1,8 @@
-package de.b2tla.tla;
+package de.tlc4b.tla;
import java.util.ArrayList;
-import de.b2tla.tla.config.ConfigFileAssignment;
+import de.tlc4b.tla.config.ConfigFileAssignment;
public class ConfigFile {
diff --git a/src/main/java/de/b2tla/tla/Generator.java b/src/main/java/de/tlc4b/tla/Generator.java
similarity index 92%
rename from src/main/java/de/b2tla/tla/Generator.java
rename to src/main/java/de/tlc4b/tla/Generator.java
index 91050277c5f55417cc7041547a8f7b54f42d3723..1e7d059980dafca98f8b690ad7a903e201307517 100644
--- a/src/main/java/de/b2tla/tla/Generator.java
+++ b/src/main/java/de/tlc4b/tla/Generator.java
@@ -1,4 +1,4 @@
-package de.b2tla.tla;
+package de.tlc4b.tla;
import java.util.ArrayList;
import java.util.Collection;
@@ -7,17 +7,6 @@ import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.List;
-import de.b2tla.B2TLAGlobals;
-import de.b2tla.analysis.ConstantsEvaluator;
-import de.b2tla.analysis.DefinitionsAnalyser;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.analysis.nodes.ElementOfNode;
-import de.b2tla.analysis.nodes.NodeType;
-import de.b2tla.analysis.typerestriction.TypeRestrictor;
-import de.b2tla.btypes.BType;
-import de.b2tla.tla.config.ModelValueAssignment;
-import de.b2tla.tla.config.SetOfModelValuesAssignment;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
@@ -37,6 +26,17 @@ import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.POperation;
import de.be4.classicalb.core.parser.node.PPredicate;
+import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.analysis.ConstantsEvaluator;
+import de.tlc4b.analysis.DefinitionsAnalyser;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.analysis.nodes.ElementOfNode;
+import de.tlc4b.analysis.nodes.NodeType;
+import de.tlc4b.analysis.typerestriction.TypeRestrictor;
+import de.tlc4b.btypes.BType;
+import de.tlc4b.tla.config.ModelValueAssignment;
+import de.tlc4b.tla.config.SetOfModelValuesAssignment;
public class Generator extends DepthFirstAdapter {
@@ -92,14 +92,14 @@ public class Generator extends DepthFirstAdapter {
private void evalSpec() {
if (this.configFile.isInit() && this.configFile.isNext()
- && B2TLAGlobals.isCheckltl()
+ && TLC4BGlobals.isCheckltl()
&& machineContext.getLTLFormulas().size() > 0) {
this.configFile.setSpec();
}
}
private void evalGoal() {
- if (B2TLAGlobals.isGOAL()) {
+ if (TLC4BGlobals.isGOAL()) {
if (machineContext.getDefinitions().keySet().contains("GOAL")) {
this.configFile.setGoal();
}
diff --git a/src/main/java/de/b2tla/tla/TLADefinition.java b/src/main/java/de/tlc4b/tla/TLADefinition.java
similarity index 90%
rename from src/main/java/de/b2tla/tla/TLADefinition.java
rename to src/main/java/de/tlc4b/tla/TLADefinition.java
index 70afc011afb7ca02bef61f32dbd2bb8b5afa6312..731193f96f39d22fe35a5f4b18585371ff9961e2 100644
--- a/src/main/java/de/b2tla/tla/TLADefinition.java
+++ b/src/main/java/de/tlc4b/tla/TLADefinition.java
@@ -1,4 +1,4 @@
-package de.b2tla.tla;
+package de.tlc4b.tla;
import de.be4.classicalb.core.parser.node.Node;
diff --git a/src/main/java/de/b2tla/tla/TLAModule.java b/src/main/java/de/tlc4b/tla/TLAModule.java
similarity index 92%
rename from src/main/java/de/b2tla/tla/TLAModule.java
rename to src/main/java/de/tlc4b/tla/TLAModule.java
index db8ca742563313fb03984a6637d874b0fc480bd9..702aad726d2d9255f6111bc9ec2d65cde19be4f0 100644
--- a/src/main/java/de/b2tla/tla/TLAModule.java
+++ b/src/main/java/de/tlc4b/tla/TLAModule.java
@@ -1,12 +1,12 @@
-package de.b2tla.tla;
+package de.tlc4b.tla;
import java.util.ArrayList;
-import de.b2tla.analysis.DefinitionsOrder;
-import de.b2tla.analysis.MachineContext;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PDefinition;
import de.be4.classicalb.core.parser.node.POperation;
+import de.tlc4b.analysis.DefinitionsOrder;
+import de.tlc4b.analysis.MachineContext;
public class TLAModule {
diff --git a/src/main/java/de/b2tla/tla/config/ConfigFileAssignment.java b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
similarity index 86%
rename from src/main/java/de/b2tla/tla/config/ConfigFileAssignment.java
rename to src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
index 74678e74155a1a8f2d3fc58f928e0a9d2b592a3d..90e880a625b11bf9b90c7e8822a061e6e2c56c50 100644
--- a/src/main/java/de/b2tla/tla/config/ConfigFileAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
@@ -1,11 +1,11 @@
-package de.b2tla.tla.config;
+package de.tlc4b.tla.config;
import java.util.ArrayList;
import java.util.List;
-import de.b2tla.analysis.Renamer;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
+import de.tlc4b.analysis.Renamer;
public abstract class ConfigFileAssignment {
diff --git a/src/main/java/de/b2tla/tla/config/ModelValueAssignment.java b/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
similarity index 85%
rename from src/main/java/de/b2tla/tla/config/ModelValueAssignment.java
rename to src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
index c7f10b2762d1866a419cda35bfe659eced690a6b..8b6ef2d13b282fac2e423181010c1e39f5f09bae 100644
--- a/src/main/java/de/b2tla/tla/config/ModelValueAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
@@ -1,8 +1,8 @@
-package de.b2tla.tla.config;
+package de.tlc4b.tla.config;
-import de.b2tla.analysis.Renamer;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
+import de.tlc4b.analysis.Renamer;
public class ModelValueAssignment extends ConfigFileAssignment{
private Node node;
diff --git a/src/main/java/de/b2tla/tla/config/SetOfModelValuesAssignment.java b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
similarity index 86%
rename from src/main/java/de/b2tla/tla/config/SetOfModelValuesAssignment.java
rename to src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
index 45ee9a6acef97543860c94250cb39060723c64d0..b08ca709fbf0d9c4f787b0b406947cc3df99a0ac 100644
--- a/src/main/java/de/b2tla/tla/config/SetOfModelValuesAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
@@ -1,13 +1,13 @@
-package de.b2tla.tla.config;
+package de.tlc4b.tla.config;
import java.util.List;
-import de.b2tla.B2TLAGlobals;
-import de.b2tla.analysis.Renamer;
import de.be4.classicalb.core.parser.node.ADeferredSetSet;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
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.
@@ -22,7 +22,7 @@ public class SetOfModelValuesAssignment extends ConfigFileAssignment{
public SetOfModelValuesAssignment(Node node, Integer size) {
this.node = node;
if(size == null){
- this.size = B2TLAGlobals.getDEFERRED_SET_SIZE();
+ this.size = TLC4BGlobals.getDEFERRED_SET_SIZE();
}else{
this.size = size;
}
diff --git a/src/main/java/de/b2tla/tlc/ModuleMatcher.java b/src/main/java/de/tlc4b/tlc/ModuleMatcher.java
similarity index 95%
rename from src/main/java/de/b2tla/tlc/ModuleMatcher.java
rename to src/main/java/de/tlc4b/tlc/ModuleMatcher.java
index ac3d8160db8170bebe6b473fee84497f19d946c3..086e32179dade827f7b479b14575b7bafe453058 100644
--- a/src/main/java/de/b2tla/tlc/ModuleMatcher.java
+++ b/src/main/java/de/tlc4b/tlc/ModuleMatcher.java
@@ -1,4 +1,4 @@
-package de.b2tla.tlc;
+package de.tlc4b.tlc;
import java.util.HashMap;
import java.util.regex.Matcher;
diff --git a/src/main/java/de/b2tla/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
similarity index 93%
rename from src/main/java/de/b2tla/tlc/TLCOutputInfo.java
rename to src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index f4f87c6f6a7c5366ad382616173e3c9097a7c8d0..2bc59563e88d84cc78c82044cc684edaf40765f1 100644
--- a/src/main/java/de/b2tla/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -1,14 +1,14 @@
-package de.b2tla.tlc;
+package de.tlc4b.tlc;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Set;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.Renamer;
-import de.b2tla.btypes.BType;
import de.be4.classicalb.core.parser.node.Node;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.Renamer;
+import de.tlc4b.btypes.BType;
public class TLCOutputInfo {
diff --git a/src/main/java/de/b2tla/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
similarity index 96%
rename from src/main/java/de/b2tla/tlc/TLCResults.java
rename to src/main/java/de/tlc4b/tlc/TLCResults.java
index ffe8195b8ee65707ed8e43fe23cf1bfabc64f798..71dabb6c67e42eccd0d04c7bf422739a741b808e 100644
--- a/src/main/java/de/b2tla/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -1,10 +1,10 @@
-package de.b2tla.tlc;
+package de.tlc4b.tlc;
import java.util.ArrayList;
import java.util.Date;
-import de.b2tla.B2TLAGlobals;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import de.tlc4b.TLC4BGlobals;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import tlc2.output.EC;
import static tlc2.output.MP.*;
import tlc2.output.Message;
@@ -59,7 +59,7 @@ public class TLCResults {
evalAllMessages();
if (hasTrace()
- || (B2TLAGlobals.getTestingMode() && OutputCollector
+ || (TLC4BGlobals.getTestingMode() && OutputCollector
.getInitialState() != null)) {
evalTrace();
}
diff --git a/src/main/java/de/b2tla/tlc/TracePrinter.java b/src/main/java/de/tlc4b/tlc/TracePrinter.java
similarity index 97%
rename from src/main/java/de/b2tla/tlc/TracePrinter.java
rename to src/main/java/de/tlc4b/tlc/TracePrinter.java
index 0a64d2d955283803ef87e84d6dde570b35d6e7e3..e79a25a0bda194b94facee0613760d78702b7807 100644
--- a/src/main/java/de/b2tla/tlc/TracePrinter.java
+++ b/src/main/java/de/tlc4b/tlc/TracePrinter.java
@@ -1,12 +1,12 @@
-package de.b2tla.tlc;
+package de.tlc4b.tlc;
import java.util.ArrayList;
-import de.b2tla.btypes.BType;
-import de.b2tla.btypes.FunctionType;
-import de.b2tla.btypes.PairType;
-import de.b2tla.btypes.SetType;
-import de.b2tla.btypes.StructType;
+import de.tlc4b.btypes.BType;
+import de.tlc4b.btypes.FunctionType;
+import de.tlc4b.btypes.PairType;
+import de.tlc4b.btypes.SetType;
+import de.tlc4b.btypes.StructType;
import tlc2.tool.TLCState;
import tlc2.tool.TLCStateInfo;
import tlc2.value.FcnLambdaValue;
diff --git a/src/main/java/de/b2tla/util/BTLCPrintStream.java b/src/main/java/de/tlc4b/util/BTLCPrintStream.java
similarity index 85%
rename from src/main/java/de/b2tla/util/BTLCPrintStream.java
rename to src/main/java/de/tlc4b/util/BTLCPrintStream.java
index 33592cd8088fa62f494f5f88caf3d3cc1e760d0f..9a6fb093c562aa800b17ac1f3fc6a71e5a4c88b7 100644
--- a/src/main/java/de/b2tla/util/BTLCPrintStream.java
+++ b/src/main/java/de/tlc4b/util/BTLCPrintStream.java
@@ -1,10 +1,10 @@
-package de.b2tla.util;
+package de.tlc4b.util;
import java.io.PipedOutputStream;
import java.io.PrintStream;
import java.util.ArrayList;
-import de.b2tla.B2TLAGlobals;
+import de.tlc4b.TLC4BGlobals;
public class BTLCPrintStream extends PrintStream {
@@ -31,7 +31,7 @@ public class BTLCPrintStream extends PrintStream {
@Override
public void println(String str){
synchronized (BTLCPrintStream.class){
- if(!B2TLAGlobals.isTool()){
+ if(!TLC4BGlobals.isTool()){
//console.println(str);
}
array.add(str);
@@ -41,7 +41,7 @@ public class BTLCPrintStream extends PrintStream {
@Override
public void print(String str){
synchronized (BTLCPrintStream.class){
- if(!B2TLAGlobals.isTool()){
+ if(!TLC4BGlobals.isTool()){
console.println(str);
}
//console.println(str);
diff --git a/src/main/java/de/b2tla/util/StopWatch.java b/src/main/java/de/tlc4b/util/StopWatch.java
similarity index 92%
rename from src/main/java/de/b2tla/util/StopWatch.java
rename to src/main/java/de/tlc4b/util/StopWatch.java
index f74b914ae9d36d4750f4e984cc9dda035add56a5..89594ba11e9b6b419f03e9a25e09733a9c09cff7 100644
--- a/src/main/java/de/b2tla/util/StopWatch.java
+++ b/src/main/java/de/tlc4b/util/StopWatch.java
@@ -1,4 +1,4 @@
-package de.b2tla.util;
+package de.tlc4b.util;
import java.util.Hashtable;
diff --git a/src/test/java/de/b2tla/analysis/ConstantsEvaluatorTest.java b/src/test/java/de/tlc4b/analysis/ConstantsEvaluatorTest.java
similarity index 87%
rename from src/test/java/de/b2tla/analysis/ConstantsEvaluatorTest.java
rename to src/test/java/de/tlc4b/analysis/ConstantsEvaluatorTest.java
index 2daf28f1c0d035edc90503610b9a2631ea28a197..7ab9fd5dcf4c6f54fb60a04676547b3a6384fa04 100644
--- a/src/test/java/de/b2tla/analysis/ConstantsEvaluatorTest.java
+++ b/src/test/java/de/tlc4b/analysis/ConstantsEvaluatorTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/ConstantsTest.java b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
similarity index 93%
rename from src/test/java/de/b2tla/analysis/ConstantsTest.java
rename to src/test/java/de/tlc4b/analysis/ConstantsTest.java
index d7bdcca8785b0f6d59cc55ab3a18b4e6d0e4757a..f74c1a9abaa5b6638059d5b3adb6756624387354 100644
--- a/src/test/java/de/b2tla/analysis/ConstantsTest.java
+++ b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
@@ -1,8 +1,9 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
+
import org.junit.Ignore;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/DeferredSetSize.java b/src/test/java/de/tlc4b/analysis/DeferredSetSize.java
similarity index 90%
rename from src/test/java/de/b2tla/analysis/DeferredSetSize.java
rename to src/test/java/de/tlc4b/analysis/DeferredSetSize.java
index 7c842f80b3a4ac15543ceb734930b41ffa48bf01..a97c0aabdd53397cad209c8974ceca5ffd633098 100644
--- a/src/test/java/de/b2tla/analysis/DeferredSetSize.java
+++ b/src/test/java/de/tlc4b/analysis/DeferredSetSize.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compareConfig;
+import static de.tlc4b.util.TestUtil.compareConfig;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java b/src/test/java/de/tlc4b/analysis/DefinitionsOrderTest.java
similarity index 96%
rename from src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java
rename to src/test/java/de/tlc4b/analysis/DefinitionsOrderTest.java
index fa87a9beaadfb58abfec28526b3926817f7dc2b8..96310fdc91b1023958802bd2a84b6d36cfe14749 100644
--- a/src/test/java/de/b2tla/analysis/DefinitionsOrderTest.java
+++ b/src/test/java/de/tlc4b/analysis/DefinitionsOrderTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/DefinitionsTest.java b/src/test/java/de/tlc4b/analysis/DefinitionsTest.java
similarity index 93%
rename from src/test/java/de/b2tla/analysis/DefinitionsTest.java
rename to src/test/java/de/tlc4b/analysis/DefinitionsTest.java
index f55a00f70f83385bebd3783e29ad391235496542..c2c1ceda0384aa1384b5d3eb4f45d6f60e2e9d58 100644
--- a/src/test/java/de/b2tla/analysis/DefinitionsTest.java
+++ b/src/test/java/de/tlc4b/analysis/DefinitionsTest.java
@@ -1,10 +1,10 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
-import de.b2tla.exceptions.ScopeException;
+import de.tlc4b.exceptions.ScopeException;
public class DefinitionsTest {
diff --git a/src/test/java/de/b2tla/analysis/ExpressionConstantTest.java b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
similarity index 91%
rename from src/test/java/de/b2tla/analysis/ExpressionConstantTest.java
rename to src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
index dfd6d8d39bfc1b42d0dbdbc31b7ad7f426476268..1efa162296f9f50cb3dc57979618f27488a89631 100644
--- a/src/test/java/de/b2tla/analysis/ExpressionConstantTest.java
+++ b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/PrecedenceTest.java b/src/test/java/de/tlc4b/analysis/PrecedenceTest.java
similarity index 92%
rename from src/test/java/de/b2tla/analysis/PrecedenceTest.java
rename to src/test/java/de/tlc4b/analysis/PrecedenceTest.java
index 1b8d55bbf423ccd997e83e243dd190176cd5aec7..57892beb9eda2cc6e7b6840163942a913f22b95f 100644
--- a/src/test/java/de/b2tla/analysis/PrecedenceTest.java
+++ b/src/test/java/de/tlc4b/analysis/PrecedenceTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/RenamerTest.java b/src/test/java/de/tlc4b/analysis/RenamerTest.java
similarity index 93%
rename from src/test/java/de/b2tla/analysis/RenamerTest.java
rename to src/test/java/de/tlc4b/analysis/RenamerTest.java
index ef8ed62da0b5416db42b984a1aa17bafb5f26db9..fbb1645886aa7588d0024dddbe5a504df2d63e88 100644
--- a/src/test/java/de/b2tla/analysis/RenamerTest.java
+++ b/src/test/java/de/tlc4b/analysis/RenamerTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.*;
+import static de.tlc4b.util.TestUtil.*;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/analysis/ScopeTest.java b/src/test/java/de/tlc4b/analysis/ScopeTest.java
similarity index 97%
rename from src/test/java/de/b2tla/analysis/ScopeTest.java
rename to src/test/java/de/tlc4b/analysis/ScopeTest.java
index 5f3840976d1c9de0661d9c28b34ac391cd2b6000..77fab2056a556745427412edae6ccc88f9e4b7ad 100644
--- a/src/test/java/de/b2tla/analysis/ScopeTest.java
+++ b/src/test/java/de/tlc4b/analysis/ScopeTest.java
@@ -1,10 +1,10 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
import org.junit.Ignore;
import org.junit.Test;
-import static de.b2tla.util.TestUtil.checkMachine;
-import de.b2tla.exceptions.ScopeException;
+import static de.tlc4b.util.TestUtil.checkMachine;
+import de.tlc4b.exceptions.ScopeException;
public class ScopeTest {
diff --git a/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
similarity index 95%
rename from src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
rename to src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
index b956efd9db9f8186634232b2c4de0f287983334b..bd5ee36d4e5cdf3aee738f27cbf8ed7d6aa4df2c 100644
--- a/src/test/java/de/b2tla/analysis/TypeRestrictionsTest.java
+++ b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.analysis;
+package de.tlc4b.analysis;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/ltl/LtlFormulaTest.java b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
similarity index 97%
rename from src/test/java/de/b2tla/ltl/LtlFormulaTest.java
rename to src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
index 1bab754ade4d9e6df218cd17c6cdd77c79a58a7e..e4915b7f96e3a6580c398afa2f43817d60264b34 100644
--- a/src/test/java/de/b2tla/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
@@ -1,14 +1,14 @@
-package de.b2tla.ltl;
+package de.tlc4b.ltl;
-import static de.b2tla.util.TestUtil.compareLTL;
-import static de.b2tla.util.TestUtil.compareEqualsConfig;
+import static de.tlc4b.util.TestUtil.compareEqualsConfig;
+import static de.tlc4b.util.TestUtil.compareLTL;
import org.junit.Ignore;
import org.junit.Test;
-import de.b2tla.exceptions.ScopeException;
-import de.b2tla.exceptions.TypeErrorException;
+import de.tlc4b.exceptions.ScopeException;
+import de.tlc4b.exceptions.TypeErrorException;
public class LtlFormulaTest {
diff --git a/src/test/java/de/b2tla/prettyprint/ClausesTest.java b/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
similarity index 85%
rename from src/test/java/de/b2tla/prettyprint/ClausesTest.java
rename to src/test/java/de/tlc4b/prettyprint/ClausesTest.java
index b4d64a26b7b133a2780c7007fbb8f8d7fabf9ade..213ae762fff335e96db2076265ca212e56007122 100644
--- a/src/test/java/de/b2tla/prettyprint/ClausesTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/ClausesTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/DataTypesTest.java b/src/test/java/de/tlc4b/prettyprint/DataTypesTest.java
similarity index 87%
rename from src/test/java/de/b2tla/prettyprint/DataTypesTest.java
rename to src/test/java/de/tlc4b/prettyprint/DataTypesTest.java
index 323c32a62789824714ae159247a5657905fb0712..482419a0ae5df436ccbccebb0cf73cf0abd16151 100644
--- a/src/test/java/de/b2tla/prettyprint/DataTypesTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/DataTypesTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java b/src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java
similarity index 83%
rename from src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java
rename to src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java
index 8e4df28d60475147c0bd12e0d45c007f44c9c89a..f57b8edd2a473bd9d6618b10d9145f12b2b1ad57 100644
--- a/src/test/java/de/b2tla/prettyprint/EnumeratedSetsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/EnumeratedSetsTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.*;
+import static de.tlc4b.util.TestUtil.*;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/FunctionTest.java b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
similarity index 94%
rename from src/test/java/de/b2tla/prettyprint/FunctionTest.java
rename to src/test/java/de/tlc4b/prettyprint/FunctionTest.java
index 1abf355493ab7b117c52b32add2bf082266f31d9..815d684ce25ca4bbb5427c79f015872fead21139 100644
--- a/src/test/java/de/b2tla/prettyprint/FunctionTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/FunctionTest.java
@@ -1,6 +1,7 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
+
+import static de.tlc4b.util.TestUtil.*;
-import static de.b2tla.util.TestUtil.*;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/LogicalPredicates.java b/src/test/java/de/tlc4b/prettyprint/LogicalPredicates.java
similarity index 89%
rename from src/test/java/de/b2tla/prettyprint/LogicalPredicates.java
rename to src/test/java/de/tlc4b/prettyprint/LogicalPredicates.java
index 2edd0b9895d74315e48cbcaddee1e67ffb651fb4..7708162c49f7de444e4872d09625dc3f6fb9a3f0 100644
--- a/src/test/java/de/b2tla/prettyprint/LogicalPredicates.java
+++ b/src/test/java/de/tlc4b/prettyprint/LogicalPredicates.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/MachineParameterTest.java b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
similarity index 92%
rename from src/test/java/de/b2tla/prettyprint/MachineParameterTest.java
rename to src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
index 658ee0d92a547102c83aae9438760d21aba188b9..feb740479ffe03d03f18bb35dee59d53670b7e2d 100644
--- a/src/test/java/de/b2tla/prettyprint/MachineParameterTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/MachineParameterTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.*;
+import static de.tlc4b.util.TestUtil.*;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/NumbersTest.java b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
similarity index 94%
rename from src/test/java/de/b2tla/prettyprint/NumbersTest.java
rename to src/test/java/de/tlc4b/prettyprint/NumbersTest.java
index 0f928f7998576cf076363e6534c5de300c84ef71..d3c079ba382ef601ca757e8bebf9eb4de2d3594e 100644
--- a/src/test/java/de/b2tla/prettyprint/NumbersTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
similarity index 95%
rename from src/test/java/de/b2tla/prettyprint/OperationsTest.java
rename to src/test/java/de/tlc4b/prettyprint/OperationsTest.java
index ef2809add54dc8895aa12ee1a8eb3e42939a39b0..b4339ec325e77515a2846de6c2310af8f1a05110 100644
--- a/src/test/java/de/b2tla/prettyprint/OperationsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
@@ -1,10 +1,10 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
-import de.b2tla.exceptions.SubstitutionException;
+import de.tlc4b.exceptions.SubstitutionException;
public class OperationsTest {
diff --git a/src/test/java/de/b2tla/prettyprint/RelationTest.java b/src/test/java/de/tlc4b/prettyprint/RelationTest.java
similarity index 89%
rename from src/test/java/de/b2tla/prettyprint/RelationTest.java
rename to src/test/java/de/tlc4b/prettyprint/RelationTest.java
index 47f160c9b36b6d0499c4e67a6908046c0fdf4cfb..1f3a08f6d8e4206a43aef8a7c6432833768024fd 100644
--- a/src/test/java/de/b2tla/prettyprint/RelationTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/RelationTest.java
@@ -1,6 +1,7 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
+
+import static de.tlc4b.util.TestUtil.*;
-import static de.b2tla.util.TestUtil.*;
import org.junit.Test;
public class RelationTest {
diff --git a/src/test/java/de/b2tla/prettyprint/SetTest.java b/src/test/java/de/tlc4b/prettyprint/SetTest.java
similarity index 95%
rename from src/test/java/de/b2tla/prettyprint/SetTest.java
rename to src/test/java/de/tlc4b/prettyprint/SetTest.java
index 85d68569c4d0b39d5e8f7411598977902963e538..e2fbe0610af2810d70e34158e46a43d2cd2232f1 100644
--- a/src/test/java/de/b2tla/prettyprint/SetTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SetTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.*;
+import static de.tlc4b.util.TestUtil.*;
import static org.junit.Assert.*;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/SetsClauseTest.java b/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
similarity index 88%
rename from src/test/java/de/b2tla/prettyprint/SetsClauseTest.java
rename to src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
index 071aa46173aad5a309cfdf9e2cb9db10ef8bd387..5a7795c686c3cbb0c9ffcbf2fbd4120ca95f3ec6 100644
--- a/src/test/java/de/b2tla/prettyprint/SetsClauseTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SetsClauseTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.*;
+import static de.tlc4b.util.TestUtil.*;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/StringTest.java b/src/test/java/de/tlc4b/prettyprint/StringTest.java
similarity index 84%
rename from src/test/java/de/b2tla/prettyprint/StringTest.java
rename to src/test/java/de/tlc4b/prettyprint/StringTest.java
index d4715c4f529412f7c45ed3f62ff8133ace6a3422..a89df695730bc9ec3cec438591c3701b26dfea89 100644
--- a/src/test/java/de/b2tla/prettyprint/StringTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/StringTest.java
@@ -1,6 +1,6 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
similarity index 96%
rename from src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
rename to src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
index 69d4ae57644c2d2c5b75dad60703bde01f97a16f..0123a5b12b75841131864d2ee67fd897ea6b2ebc 100644
--- a/src/test/java/de/b2tla/prettyprint/SubstitutionsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/SubstitutionsTest.java
@@ -1,10 +1,10 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
-import static de.b2tla.util.TestUtil.compare;
+import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
-import de.b2tla.exceptions.SubstitutionException;
+import de.tlc4b.exceptions.SubstitutionException;
public class SubstitutionsTest {
diff --git a/src/test/java/de/b2tla/prettyprint/Tester.java b/src/test/java/de/tlc4b/prettyprint/Tester.java
similarity index 92%
rename from src/test/java/de/b2tla/prettyprint/Tester.java
rename to src/test/java/de/tlc4b/prettyprint/Tester.java
index 1ed976141487312084bd046818b79ad5d53209b1..7b2fa16c8a83c126311f64ee0c998fdab9540029 100644
--- a/src/test/java/de/b2tla/prettyprint/Tester.java
+++ b/src/test/java/de/tlc4b/prettyprint/Tester.java
@@ -1,4 +1,4 @@
-package de.b2tla.prettyprint;
+package de.tlc4b.prettyprint;
import java.io.File;
import java.io.FileWriter;
diff --git a/src/test/java/de/b2tla/tlc/integration/.gitignore b/src/test/java/de/tlc4b/tlc/integration/.gitignore
similarity index 100%
rename from src/test/java/de/b2tla/tlc/integration/.gitignore
rename to src/test/java/de/tlc4b/tlc/integration/.gitignore
diff --git a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java b/src/test/java/de/tlc4b/tlc/integration/BasicsTest.java
similarity index 69%
rename from src/test/java/de/b2tla/tlc/integration/BasicsTest.java
rename to src/test/java/de/tlc4b/tlc/integration/BasicsTest.java
index 58f4a4a56ab995148f475d6105060ce23ab259d9..1c724d74c950717d968c2ebfc0f3c2b3673df1f4 100644
--- a/src/test/java/de/b2tla/tlc/integration/BasicsTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/BasicsTest.java
@@ -1,6 +1,5 @@
-package de.b2tla.tlc.integration;
+package de.tlc4b.tlc.integration;
-import static de.b2tla.tlc.TLCResults.TLCResult.NoError;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,13 +8,14 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
-import static de.b2tla.util.TestUtil.test;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
+import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
+import static de.tlc4b.util.TestUtil.test;
@RunWith(PolySuite.class)
public class BasicsTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/ErrorTest.java
similarity index 92%
rename from src/test/java/de/b2tla/tlc/integration/ErrorTest.java
rename to src/test/java/de/tlc4b/tlc/integration/ErrorTest.java
index e134f594f0c53cd35869844a3a4266430aaf5bbf..8d192c0d6d0b00903cd0de596edc690f47bddc8a 100644
--- a/src/test/java/de/b2tla/tlc/integration/ErrorTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/ErrorTest.java
@@ -1,12 +1,12 @@
-package de.b2tla.tlc.integration;
+package de.tlc4b.tlc.integration;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
import static org.junit.Assert.*;
import org.junit.Ignore;
import org.junit.Test;
-import static de.b2tla.util.TestUtil.test;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
public class ErrorTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/LTLTest.java b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
similarity index 87%
rename from src/test/java/de/b2tla/tlc/integration/LTLTest.java
rename to src/test/java/de/tlc4b/tlc/integration/LTLTest.java
index 8bfe466d7acb3b64ed315310562edabf475841d3..bf2d1d471a69785559ffb0e2b9580e1747a61964 100644
--- a/src/test/java/de/b2tla/tlc/integration/LTLTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
@@ -1,18 +1,19 @@
-package de.b2tla.tlc.integration;
+package de.tlc4b.tlc.integration;
import static org.junit.Assert.assertEquals;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+
import org.junit.BeforeClass;
import org.junit.Test;
-import de.b2tla.B2TLAGlobals;
-import static de.b2tla.util.TestUtil.test;
+import de.tlc4b.TLC4BGlobals;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
public class LTLTest {
@BeforeClass
public static void onlyOnce() {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
}
@Test
diff --git a/src/test/java/de/b2tla/tlc/integration/SpecialTest.java b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
similarity index 88%
rename from src/test/java/de/b2tla/tlc/integration/SpecialTest.java
rename to src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
index 4bcbd9b1c719c6d3addc60c5cbcf9a7aa6a9ba52..601bb9b09e6e3f542241a6c5ed62aa16016b080d 100644
--- a/src/test/java/de/b2tla/tlc/integration/SpecialTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/SpecialTest.java
@@ -1,8 +1,8 @@
-package de.b2tla.tlc.integration;
+package de.tlc4b.tlc.integration;
-import static de.b2tla.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
similarity index 68%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
index dd23fccf05495d377b846f3d1129b41bd23a3939..c694d80486f966e6981d34612e7ad6f44599968b 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/AssertionErrorTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
@@ -1,7 +1,7 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
-import static de.b2tla.util.TestUtil.test;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -10,12 +10,12 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class AssertionErrorTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
similarity index 67%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
index bb004fec57d0818cb4d1ffebb1b0fef45d0a8c0d..f49ff366ed77e548ec52d27f4b23d9f0179a49f0 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/DeadlockTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
@@ -1,7 +1,7 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
-import static de.b2tla.util.TestUtil.test;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -10,12 +10,12 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class DeadlockTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
similarity index 67%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
index 1f7298d3908008dcc33773d74ce7dfce064891e6..d41789215c177421896b2d71a05c19bbfaacee43 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/GoalTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
@@ -1,8 +1,8 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
import static org.junit.Assert.assertEquals;
-import static de.b2tla.util.TestUtil.test;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import java.io.File;
import java.util.ArrayList;
@@ -10,12 +10,12 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class GoalTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
similarity index 68%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
index f620c285edbb28784fb2a058ea4e3118a31cb2c1..8499fdb947012c36ec7f55f4b02bc7f4322891a1 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/InvariantViolationTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
@@ -1,7 +1,7 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
-import static de.b2tla.util.TestUtil.test;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -10,12 +10,12 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class InvariantViolationTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
similarity index 76%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
index 34b7fbed554ed3c1c854868b5d4a572996211b79..b0e5e3f81514e13038ca5a804379d8eae7d1988c 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/LawsTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
@@ -1,82 +1,85 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
-import static de.b2tla.util.TestUtil.test;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
+
+
+
import org.junit.Test;
-import de.b2tla.B2TLAGlobals;
+import de.tlc4b.TLC4BGlobals;
public class LawsTest {
@Test
public void BoolLaws() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws.mch"};
assertEquals(NoError, test(a));
}
@Test
public void BoolWithArithLaws() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"};
assertEquals(NoError, test(a));
}
@Test
public void FunLaws() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/FunLaws.mch"};
assertEquals(NoError, test(a));
}
@Test
public void FunLawsWithLambda() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/FunLawsWithLambda.mch"};
assertEquals(NoError, test(a));
}
@Test
public void RelLaws_TLC() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/RelLaws_TLC.mch"};
assertEquals(Goal, test(a));
}
@Test
public void BoolLaws_SetCompr() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws_SetCompr.mch"};
assertEquals(NoError, test(a));
}
@Test
public void BoolLaws_SetComprCLPFD() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"};
assertEquals(NoError, test(a));
}
@Test
public void CardinalityLaws_TLC() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
assertEquals(NoError, test(a));
}
@Test
public void EqualityLaws() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
assertEquals(NoError, test(a));
}
@Test
public void SubsetLaws() throws Exception {
- B2TLAGlobals.setDeleteOnExit(true);
+ TLC4BGlobals.setDeleteOnExit(true);
String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
assertEquals(NoError, test(a));
}
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
similarity index 67%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
index 1c2691506c4542be20f375924e2f59e6b8a67dd0..9983401381a4f237e476c1efd1c550ba0f3a1846 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/NoErrorTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
@@ -1,7 +1,7 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
-import static de.b2tla.util.TestUtil.test;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -10,12 +10,12 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class NoErrorTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
similarity index 69%
rename from src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
rename to src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
index f15d6e042f50730ab263fcc6ea83a9af21917e7c..e258315a6c9dd4fbd0796008cd6b30cf986a0320 100644
--- a/src/test/java/de/b2tla/tlc/integration/probprivate/WellDefinednessTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
@@ -1,7 +1,7 @@
-package de.b2tla.tlc.integration.probprivate;
+package de.tlc4b.tlc.integration.probprivate;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
-import static de.b2tla.util.TestUtil.test;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.test;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -10,12 +10,12 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class WellDefinednessTest extends AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java b/src/test/java/de/tlc4b/typechecking/ArithmeticOperatorTest.java
similarity index 96%
rename from src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java
rename to src/test/java/de/tlc4b/typechecking/ArithmeticOperatorTest.java
index f037047f3254e331f0bbd74e7922412744b790b9..0c1684186f2b7dd249b16406df4eaca94f45138f 100644
--- a/src/test/java/de/b2tla/typechecking/ArithmeticOperatorTest.java
+++ b/src/test/java/de/tlc4b/typechecking/ArithmeticOperatorTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class ArithmeticOperatorTest {
diff --git a/src/test/java/de/b2tla/typechecking/BooleansTest.java b/src/test/java/de/tlc4b/typechecking/BooleansTest.java
similarity index 93%
rename from src/test/java/de/b2tla/typechecking/BooleansTest.java
rename to src/test/java/de/tlc4b/typechecking/BooleansTest.java
index 8492fbd45304a43ce43c9cc8405f1f9bc2f18255..9873e9081d7b4b8a8be0cbb5a791f0c376b4aad8 100644
--- a/src/test/java/de/b2tla/typechecking/BooleansTest.java
+++ b/src/test/java/de/tlc4b/typechecking/BooleansTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class BooleansTest {
diff --git a/src/test/java/de/b2tla/typechecking/FunctionTest.java b/src/test/java/de/tlc4b/typechecking/FunctionTest.java
similarity index 95%
rename from src/test/java/de/b2tla/typechecking/FunctionTest.java
rename to src/test/java/de/tlc4b/typechecking/FunctionTest.java
index 99498e78fb5db365d4fc923e7509ade3fe1c9c46..6049057fdc267439997acc7508e82d7f022e99d5 100644
--- a/src/test/java/de/b2tla/typechecking/FunctionTest.java
+++ b/src/test/java/de/tlc4b/typechecking/FunctionTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class FunctionTest {
diff --git a/src/test/java/de/b2tla/typechecking/LogicalOperatorTest.java b/src/test/java/de/tlc4b/typechecking/LogicalOperatorTest.java
similarity index 92%
rename from src/test/java/de/b2tla/typechecking/LogicalOperatorTest.java
rename to src/test/java/de/tlc4b/typechecking/LogicalOperatorTest.java
index cacc53eb0fa7cb05c8ce21fddc24f1ab07442823..335f7d0bc889a9ddf173cd0950f611b4be379243 100644
--- a/src/test/java/de/b2tla/typechecking/LogicalOperatorTest.java
+++ b/src/test/java/de/tlc4b/typechecking/LogicalOperatorTest.java
@@ -1,4 +1,4 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import org.junit.Test;
diff --git a/src/test/java/de/b2tla/typechecking/MachineClausesTest.java b/src/test/java/de/tlc4b/typechecking/MachineClausesTest.java
similarity index 94%
rename from src/test/java/de/b2tla/typechecking/MachineClausesTest.java
rename to src/test/java/de/tlc4b/typechecking/MachineClausesTest.java
index 7ae20c623249a6f9b80395c058fd8bff1b789ef1..10f6d984c41901a6a4ca5b222a43d41f760dcdc6 100644
--- a/src/test/java/de/b2tla/typechecking/MachineClausesTest.java
+++ b/src/test/java/de/tlc4b/typechecking/MachineClausesTest.java
@@ -1,13 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.*;
-
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class MachineClausesTest {
diff --git a/src/test/java/de/b2tla/typechecking/MinusTest.java b/src/test/java/de/tlc4b/typechecking/MinusTest.java
similarity index 95%
rename from src/test/java/de/b2tla/typechecking/MinusTest.java
rename to src/test/java/de/tlc4b/typechecking/MinusTest.java
index 248431f0a5dabbfbbcda8d858bb80611748b8397..f1d93ba1e9281560ead85302e7aa5e982b52e56c 100644
--- a/src/test/java/de/b2tla/typechecking/MinusTest.java
+++ b/src/test/java/de/tlc4b/typechecking/MinusTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class MinusTest {
diff --git a/src/test/java/de/b2tla/typechecking/ModelValuesTest.java b/src/test/java/de/tlc4b/typechecking/ModelValuesTest.java
similarity index 92%
rename from src/test/java/de/b2tla/typechecking/ModelValuesTest.java
rename to src/test/java/de/tlc4b/typechecking/ModelValuesTest.java
index fdf760f13ac87a49cfc104c1c058dca700991fa9..83709a0c8b51656e1af8ce0dcbb85b5218f6c61a 100644
--- a/src/test/java/de/b2tla/typechecking/ModelValuesTest.java
+++ b/src/test/java/de/tlc4b/typechecking/ModelValuesTest.java
@@ -1,4 +1,4 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/b2tla/typechecking/MultTest.java b/src/test/java/de/tlc4b/typechecking/MultTest.java
similarity index 95%
rename from src/test/java/de/b2tla/typechecking/MultTest.java
rename to src/test/java/de/tlc4b/typechecking/MultTest.java
index a538080e6adfea82661f3b57c689fcaff5beedd4..d0797032d2e15fa4229329ec5de4f614e45240b3 100644
--- a/src/test/java/de/b2tla/typechecking/MultTest.java
+++ b/src/test/java/de/tlc4b/typechecking/MultTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class MultTest{
diff --git a/src/test/java/de/b2tla/typechecking/RecordTest.java b/src/test/java/de/tlc4b/typechecking/RecordTest.java
similarity index 94%
rename from src/test/java/de/b2tla/typechecking/RecordTest.java
rename to src/test/java/de/tlc4b/typechecking/RecordTest.java
index 0fc55519ce7f9fc07a37286291654b34ef94d038..6a90251f3059eebdd18000da7e5fbc27852c6ed2 100644
--- a/src/test/java/de/b2tla/typechecking/RecordTest.java
+++ b/src/test/java/de/tlc4b/typechecking/RecordTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class RecordTest {
diff --git a/src/test/java/de/b2tla/typechecking/RelationsTest.java b/src/test/java/de/tlc4b/typechecking/RelationsTest.java
similarity index 93%
rename from src/test/java/de/b2tla/typechecking/RelationsTest.java
rename to src/test/java/de/tlc4b/typechecking/RelationsTest.java
index b9930fb2c20c494211f08a0a3c667b303e1b633d..a2adbd3c363ec2c132e657ebfb785020871fbb35 100644
--- a/src/test/java/de/b2tla/typechecking/RelationsTest.java
+++ b/src/test/java/de/tlc4b/typechecking/RelationsTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class RelationsTest {
diff --git a/src/test/java/de/b2tla/typechecking/SequenceTest.java b/src/test/java/de/tlc4b/typechecking/SequenceTest.java
similarity index 95%
rename from src/test/java/de/b2tla/typechecking/SequenceTest.java
rename to src/test/java/de/tlc4b/typechecking/SequenceTest.java
index 30c91b1ce55c11cb6e4aab1591eb87973e91d731..231862995f9b6affb9bb80944903972fb669ed16 100644
--- a/src/test/java/de/b2tla/typechecking/SequenceTest.java
+++ b/src/test/java/de/tlc4b/typechecking/SequenceTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class SequenceTest {
diff --git a/src/test/java/de/b2tla/typechecking/SetsClauseTest.java b/src/test/java/de/tlc4b/typechecking/SetsClauseTest.java
similarity index 89%
rename from src/test/java/de/b2tla/typechecking/SetsClauseTest.java
rename to src/test/java/de/tlc4b/typechecking/SetsClauseTest.java
index 6e1eac7c33de1d089e87bd6060953d2429901437..95a7be21d89fb91f09820d4e2b34646c652f6107 100644
--- a/src/test/java/de/b2tla/typechecking/SetsClauseTest.java
+++ b/src/test/java/de/tlc4b/typechecking/SetsClauseTest.java
@@ -1,4 +1,4 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/b2tla/typechecking/SetsTest.java b/src/test/java/de/tlc4b/typechecking/SetsTest.java
similarity index 95%
rename from src/test/java/de/b2tla/typechecking/SetsTest.java
rename to src/test/java/de/tlc4b/typechecking/SetsTest.java
index 24a56a0ef2b05c07ac4f89d4add76258a2c749fd..1afcd259ae8c37a966dd552507c048c9a3f6997b 100644
--- a/src/test/java/de/b2tla/typechecking/SetsTest.java
+++ b/src/test/java/de/tlc4b/typechecking/SetsTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class SetsTest {
diff --git a/src/test/java/de/b2tla/typechecking/StringTest.java b/src/test/java/de/tlc4b/typechecking/StringTest.java
similarity index 87%
rename from src/test/java/de/b2tla/typechecking/StringTest.java
rename to src/test/java/de/tlc4b/typechecking/StringTest.java
index 2e032b078587b2f8ac977832f39015b9bce760b3..2a1cdfa6459e394205b1e02817792725d7b19952 100644
--- a/src/test/java/de/b2tla/typechecking/StringTest.java
+++ b/src/test/java/de/tlc4b/typechecking/StringTest.java
@@ -1,12 +1,13 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class StringTest {
diff --git a/src/test/java/de/b2tla/typechecking/TestTypechecker.java b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
similarity index 85%
rename from src/test/java/de/b2tla/typechecking/TestTypechecker.java
rename to src/test/java/de/tlc4b/typechecking/TestTypechecker.java
index 83c4b6ef5381f88861dda8c1a0996fe0f6c813ab..959717968006db7169f6faf3242b8e8128403be8 100644
--- a/src/test/java/de/b2tla/typechecking/TestTypechecker.java
+++ b/src/test/java/de/tlc4b/typechecking/TestTypechecker.java
@@ -1,14 +1,14 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import java.util.Hashtable;
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.analysis.MachineContext;
-import de.b2tla.analysis.Typechecker;
-import de.b2tla.btypes.BType;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.analysis.Ast2String;
+import de.tlc4b.analysis.MachineContext;
+import de.tlc4b.analysis.Typechecker;
+import de.tlc4b.btypes.BType;
public class TestTypechecker {
diff --git a/src/test/java/de/b2tla/typechecking/TypeErrosTest.java b/src/test/java/de/tlc4b/typechecking/TypeErrosTest.java
similarity index 87%
rename from src/test/java/de/b2tla/typechecking/TypeErrosTest.java
rename to src/test/java/de/tlc4b/typechecking/TypeErrosTest.java
index c7bb4e2e6df2150c428b82df28a851ccb5087f83..05efcef3b9b1be9461740003aa0582161f4d8e29 100644
--- a/src/test/java/de/b2tla/typechecking/TypeErrosTest.java
+++ b/src/test/java/de/tlc4b/typechecking/TypeErrosTest.java
@@ -1,10 +1,11 @@
-package de.b2tla.typechecking;
+package de.tlc4b.typechecking;
import org.junit.Test;
-import de.b2tla.exceptions.TypeErrorException;
+
import de.be4.classicalb.core.parser.exceptions.BException;
+import de.tlc4b.exceptions.TypeErrorException;
public class TypeErrosTest {
diff --git a/src/test/java/de/b2tla/util/AbstractParseMachineTest.java b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
similarity index 93%
rename from src/test/java/de/b2tla/util/AbstractParseMachineTest.java
rename to src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
index 692cb73d97d14ac1681ae83d41c6b872006c9f03..e8083cdc0a07829bdb242140e32c4d03aa03646d 100644
--- a/src/test/java/de/b2tla/util/AbstractParseMachineTest.java
+++ b/src/test/java/de/tlc4b/util/AbstractParseMachineTest.java
@@ -1,12 +1,12 @@
-package de.b2tla.util;
+package de.tlc4b.util;
import java.io.File;
import java.io.FilenameFilter;
import java.util.ArrayList;
import java.util.Arrays;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.PolySuite.Configuration;
public abstract class AbstractParseMachineTest {
diff --git a/src/test/java/de/b2tla/util/PolySuite.java b/src/test/java/de/tlc4b/util/PolySuite.java
similarity index 99%
rename from src/test/java/de/b2tla/util/PolySuite.java
rename to src/test/java/de/tlc4b/util/PolySuite.java
index 2d3cae1370d190f9793ee5b000b6eae79e0cdb79..0fb12b7fd1c60f8083dd5e0339b76adc1efdc621 100644
--- a/src/test/java/de/b2tla/util/PolySuite.java
+++ b/src/test/java/de/tlc4b/util/PolySuite.java
@@ -1,4 +1,4 @@
-package de.b2tla.util;
+package de.tlc4b.util;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
diff --git a/src/test/java/de/b2tla/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java
similarity index 74%
rename from src/test/java/de/b2tla/util/TLC4BTester.java
rename to src/test/java/de/tlc4b/util/TLC4BTester.java
index e8482200e2137bc9661cc00cb6167a3b18028ba0..9d77e7c995235a03126d660e6e11f5ec36b64a19 100644
--- a/src/test/java/de/b2tla/util/TLC4BTester.java
+++ b/src/test/java/de/tlc4b/util/TLC4BTester.java
@@ -1,14 +1,14 @@
-package de.b2tla.util;
+package de.tlc4b.util;
import java.io.IOException;
-import de.b2tla.B2TLA;
+import de.tlc4b.TLC4B;
public class TLC4BTester {
public static void main(String[] args) throws IOException {
System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
- B2TLA.test(args,true);
+ TLC4B.test(args,true);
}
}
diff --git a/src/test/java/de/b2tla/util/TestPair.java b/src/test/java/de/tlc4b/util/TestPair.java
similarity index 81%
rename from src/test/java/de/b2tla/util/TestPair.java
rename to src/test/java/de/tlc4b/util/TestPair.java
index 47aebd6acdea4d8a13f92847d65220831de584c9..8bdc29b34a9d39368025f3a1a5831f140c85d2e1 100644
--- a/src/test/java/de/b2tla/util/TestPair.java
+++ b/src/test/java/de/tlc4b/util/TestPair.java
@@ -1,6 +1,6 @@
-package de.b2tla.util;
+package de.tlc4b.util;
-import de.b2tla.tlc.TLCResults.TLCResult;
+import de.tlc4b.tlc.TLCResults.TLCResult;
public class TestPair {
diff --git a/src/test/java/de/b2tla/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
similarity index 95%
rename from src/test/java/de/b2tla/util/TestUtil.java
rename to src/test/java/de/tlc4b/util/TestUtil.java
index 5fafa5357905f6ce4a5ece4f9211556eef967cbc..4a4e079d018c5e8623ad5ac9fdecdb91a0a6e83f 100644
--- a/src/test/java/de/b2tla/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -1,4 +1,4 @@
-package de.b2tla.util;
+package de.tlc4b.util;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.fail;
@@ -17,11 +17,11 @@ import java.util.Arrays;
import java.util.List;
-import de.b2tla.Translator;
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.tlc.TLCResults.TLCResult;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.Translator;
+import de.tlc4b.analysis.Ast2String;
+import de.tlc4b.tlc.TLCResults.TLCResult;
public class TestUtil {
diff --git a/src/test/java/testing/CompoundScopeTest.java b/src/test/java/testing/CompoundScopeTest.java
index e47962d77e5c6e385c037f5ba9f37531a0336895..e45baa8d2022aeb2a41d80f88fa56a36f88b9c12 100644
--- a/src/test/java/testing/CompoundScopeTest.java
+++ b/src/test/java/testing/CompoundScopeTest.java
@@ -13,13 +13,14 @@ import org.junit.Test;
-import de.b2tla.analysis.Ast2String;
-import de.b2tla.analysis.MachineContext;
+
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.analysis.Ast2String;
+import de.tlc4b.analysis.MachineContext;
public class CompoundScopeTest {
diff --git a/src/test/java/testing/Testing.java b/src/test/java/testing/Testing.java
index 415a4ad47e37350d05e9dc9b9768bb9635dd6d7a..0bf941e1950772bd51b7c5e5ea299e9cc1b8dbf9 100644
--- a/src/test/java/testing/Testing.java
+++ b/src/test/java/testing/Testing.java
@@ -1,6 +1,6 @@
package testing;
-import static de.b2tla.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
import static org.junit.Assert.assertEquals;
import java.io.File;
@@ -9,13 +9,13 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.TLC4B;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
index 57230dadbb389a1c51e9919f8a8bde1b2d1cf4e7..ca5af5c6f4783c5e155e60887b224924cfe3dc4e 100644
--- a/src/test/java/testing/Testing2.java
+++ b/src/test/java/testing/Testing2.java
@@ -1,22 +1,23 @@
package testing;
-import static de.b2tla.tlc.TLCResults.TLCResult.NoError;
import static org.junit.Assert.*;
-import static de.b2tla.util.TestUtil.test;
+import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
+import static de.tlc4b.util.TestUtil.test;
+
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
-import de.b2tla.B2TLA;
-import de.b2tla.tlc.TLCResults.TLCResult;
-import de.b2tla.util.AbstractParseMachineTest;
-import de.b2tla.util.PolySuite;
-import de.b2tla.util.TestPair;
-import de.b2tla.util.PolySuite.Config;
-import de.b2tla.util.PolySuite.Configuration;
+import de.tlc4b.TLC4B;
+import de.tlc4b.tlc.TLCResults.TLCResult;
+import de.tlc4b.util.AbstractParseMachineTest;
+import de.tlc4b.util.PolySuite;
+import de.tlc4b.util.TestPair;
+import de.tlc4b.util.PolySuite.Config;
+import de.tlc4b.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class Testing2 extends AbstractParseMachineTest{
@@ -33,7 +34,7 @@ public class Testing2 extends AbstractParseMachineTest{
public void testRunTLC() throws Exception {
String[] a = new String[] {machine.getPath()};
- B2TLA.main(a);
+ TLC4B.main(a);
//B2TLA.test(a,true);
//test(a);
//assertEquals(error, B2TLA.test(a,true));