From 7d4afe99f7efb9be4baa41b897f8b19408fa8241 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 13 Mar 2014 11:53:26 +0100
Subject: [PATCH] Renaming
---
build.gradle | 6 +-
build.xml | 2 +-
.../de/b2tla/exceptions/B2TLAIOException.java | 15 ----
.../de/b2tla/exceptions/B2tlaException.java | 12 ---
.../de/{b2tla/B2TLA.java => tlc4b/TLC4B.java} | 86 +++++++++----------
.../TLC4BGlobals.java} | 38 ++++----
.../java/de/{b2tla => tlc4b}/TLCRunner.java | 12 +--
.../java/de/{b2tla => tlc4b}/Translator.java | 38 ++++----
.../{b2tla => tlc4b}/analysis/Ast2String.java | 2 +-
.../analysis/ConstantsEliminator.java | 2 +-
.../analysis/ConstantsEvaluator.java | 2 +-
.../analysis/DefinitionsAnalyser.java | 8 +-
.../analysis/DefinitionsOrder.java | 2 +-
.../analysis/MachineContext.java | 8 +-
.../analysis/NotSupportedConstructs.java | 4 +-
.../analysis/PrecedenceCollector.java | 6 +-
.../analysis/PrimedNodesMarker.java | 4 +-
.../de/{b2tla => tlc4b}/analysis/Renamer.java | 2 +-
.../analysis/StandardMadules.java | 2 +-
.../analysis/Typechecker.java | 38 ++++----
.../analysis/UsedStandardModules.java | 12 +--
.../analysis/nodes/ElementOfNode.java | 2 +-
.../analysis/nodes/EqualsNode.java | 2 +-
.../analysis/nodes/NodeType.java | 2 +-
.../analysis/nodes/SubsetNode.java | 2 +-
.../transformation/DefinitionCollector.java | 2 +-
.../transformation/DefinitionsEliminator.java | 2 +-
.../IdentifierDependencies.java | 4 +-
.../typerestriction/TypeRestrictor.java | 16 ++--
.../AssignedVariablesFinder.java | 6 +-
.../UnchangedVariablesFinder.java | 6 +-
.../btypes/AbstractHasFollowers.java | 2 +-
.../de/{b2tla => tlc4b}/btypes/BType.java | 4 +-
.../de/{b2tla => tlc4b}/btypes/BoolType.java | 6 +-
.../{b2tla => tlc4b}/btypes/FunctionType.java | 6 +-
.../btypes/ITypeConstants.java | 2 +-
.../{b2tla => tlc4b}/btypes/ITypechecker.java | 2 +-
.../btypes/IntegerOrSetOfPairType.java | 8 +-
.../btypes/IntegerOrSetType.java | 6 +-
.../{b2tla => tlc4b}/btypes/IntegerType.java | 10 +--
.../btypes/ModelValueType.java | 6 +-
.../de/{b2tla => tlc4b}/btypes/PairType.java | 6 +-
.../de/{b2tla => tlc4b}/btypes/SetType.java | 6 +-
.../{b2tla => tlc4b}/btypes/StringType.java | 6 +-
.../{b2tla => tlc4b}/btypes/StructType.java | 6 +-
.../{b2tla => tlc4b}/btypes/UntypedType.java | 4 +-
.../exceptions/LTLParseException.java | 4 +-
.../exceptions/NotSupportedException.java | 4 +-
.../NotSupportedLTLFormulaException.java | 4 +-
.../exceptions/ScopeException.java | 4 +-
.../exceptions/SubstitutionException.java | 4 +-
.../de/tlc4b/exceptions/TLC4BException.java | 12 +++
.../de/tlc4b/exceptions/TLC4BIOException.java | 15 ++++
.../exceptions/TypeErrorException.java | 4 +-
.../exceptions/UnificationException.java | 2 +-
.../{b2tla => tlc4b}/ltl/LTLBPredicate.java | 2 +-
.../ltl/LTLFormulaPrinter.java | 4 +-
.../ltl/LTLFormulaVisitor.java | 10 +--
.../prettyprint/TLAPrinter.java | 62 ++++++-------
.../de/{b2tla => tlc4b}/tla/ConfigFile.java | 4 +-
.../de/{b2tla => tlc4b}/tla/Generator.java | 28 +++---
.../{b2tla => tlc4b}/tla/TLADefinition.java | 2 +-
.../de/{b2tla => tlc4b}/tla/TLAModule.java | 6 +-
.../tla/config/ConfigFileAssignment.java | 4 +-
.../tla/config/ModelValueAssignment.java | 4 +-
.../config/SetOfModelValuesAssignment.java | 8 +-
.../{b2tla => tlc4b}/tlc/ModuleMatcher.java | 2 +-
.../{b2tla => tlc4b}/tlc/TLCOutputInfo.java | 8 +-
.../de/{b2tla => tlc4b}/tlc/TLCResults.java | 8 +-
.../de/{b2tla => tlc4b}/tlc/TracePrinter.java | 12 +--
.../util/BTLCPrintStream.java | 8 +-
.../de/{b2tla => tlc4b}/util/StopWatch.java | 2 +-
.../analysis/ConstantsEvaluatorTest.java | 4 +-
.../analysis/ConstantsTest.java | 5 +-
.../analysis/DeferredSetSize.java | 4 +-
.../analysis/DefinitionsOrderTest.java | 4 +-
.../analysis/DefinitionsTest.java | 6 +-
.../analysis/ExpressionConstantTest.java | 4 +-
.../analysis/PrecedenceTest.java | 4 +-
.../analysis/RenamerTest.java | 4 +-
.../{b2tla => tlc4b}/analysis/ScopeTest.java | 6 +-
.../analysis/TypeRestrictionsTest.java | 4 +-
.../{b2tla => tlc4b}/ltl/LtlFormulaTest.java | 10 +--
.../prettyprint/ClausesTest.java | 4 +-
.../prettyprint/DataTypesTest.java | 4 +-
.../prettyprint/EnumeratedSetsTest.java | 4 +-
.../prettyprint/FunctionTest.java | 5 +-
.../prettyprint/LogicalPredicates.java | 4 +-
.../prettyprint/MachineParameterTest.java | 4 +-
.../prettyprint/NumbersTest.java | 4 +-
.../prettyprint/OperationsTest.java | 6 +-
.../prettyprint/RelationTest.java | 5 +-
.../{b2tla => tlc4b}/prettyprint/SetTest.java | 4 +-
.../prettyprint/SetsClauseTest.java | 4 +-
.../prettyprint/StringTest.java | 4 +-
.../prettyprint/SubstitutionsTest.java | 6 +-
.../{b2tla => tlc4b}/prettyprint/Tester.java | 2 +-
.../tlc/integration/.gitignore | 0
.../tlc/integration/BasicsTest.java | 18 ++--
.../tlc/integration/ErrorTest.java | 6 +-
.../tlc/integration/LTLTest.java | 11 +--
.../tlc/integration/SpecialTest.java | 6 +-
.../probprivate/AssertionErrorTest.java | 18 ++--
.../integration/probprivate/DeadlockTest.java | 18 ++--
.../tlc/integration/probprivate/GoalTest.java | 18 ++--
.../probprivate/InvariantViolationTest.java | 18 ++--
.../tlc/integration/probprivate/LawsTest.java | 31 ++++---
.../integration/probprivate/NoErrorTest.java | 18 ++--
.../probprivate/WellDefinednessTest.java | 18 ++--
.../typechecking/ArithmeticOperatorTest.java | 5 +-
.../typechecking/BooleansTest.java | 5 +-
.../typechecking/FunctionTest.java | 5 +-
.../typechecking/LogicalOperatorTest.java | 2 +-
.../typechecking/MachineClausesTest.java | 6 +-
.../typechecking/MinusTest.java | 5 +-
.../typechecking/ModelValuesTest.java | 2 +-
.../typechecking/MultTest.java | 5 +-
.../typechecking/RecordTest.java | 5 +-
.../typechecking/RelationsTest.java | 5 +-
.../typechecking/SequenceTest.java | 5 +-
.../typechecking/SetsClauseTest.java | 2 +-
.../typechecking/SetsTest.java | 5 +-
.../typechecking/StringTest.java | 5 +-
.../typechecking/TestTypechecker.java | 10 +--
.../typechecking/TypeErrosTest.java | 5 +-
.../util/AbstractParseMachineTest.java | 6 +-
.../de/{b2tla => tlc4b}/util/PolySuite.java | 2 +-
.../de/{b2tla => tlc4b}/util/TLC4BTester.java | 6 +-
.../de/{b2tla => tlc4b}/util/TestPair.java | 4 +-
.../de/{b2tla => tlc4b}/util/TestUtil.java | 8 +-
src/test/java/testing/CompoundScopeTest.java | 5 +-
src/test/java/testing/Testing.java | 16 ++--
src/test/java/testing/Testing2.java | 21 ++---
133 files changed, 556 insertions(+), 536 deletions(-)
delete mode 100644 src/main/java/de/b2tla/exceptions/B2TLAIOException.java
delete mode 100644 src/main/java/de/b2tla/exceptions/B2tlaException.java
rename src/main/java/de/{b2tla/B2TLA.java => tlc4b/TLC4B.java} (83%)
rename src/main/java/de/{b2tla/B2TLAGlobals.java => tlc4b/TLC4BGlobals.java} (80%)
rename src/main/java/de/{b2tla => tlc4b}/TLCRunner.java (92%)
rename src/main/java/de/{b2tla => tlc4b}/Translator.java (83%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/Ast2String.java (93%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/ConstantsEliminator.java (99%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/ConstantsEvaluator.java (96%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/DefinitionsAnalyser.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/DefinitionsOrder.java (99%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/MachineContext.java (96%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/NotSupportedConstructs.java (92%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/PrecedenceCollector.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/PrimedNodesMarker.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/Renamer.java (96%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/StandardMadules.java (97%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/Typechecker.java (95%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/UsedStandardModules.java (96%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/nodes/ElementOfNode.java (83%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/nodes/EqualsNode.java (83%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/nodes/NodeType.java (75%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/nodes/SubsetNode.java (88%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/transformation/DefinitionCollector.java (95%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/transformation/DefinitionsEliminator.java (96%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/typerestriction/IdentifierDependencies.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/typerestriction/TypeRestrictor.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/unchangedvariables/AssignedVariablesFinder.java (95%)
rename src/main/java/de/{b2tla => tlc4b}/analysis/unchangedvariables/UnchangedVariablesFinder.java (95%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/AbstractHasFollowers.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/BType.java (82%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/BoolType.java (87%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/FunctionType.java (93%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/ITypeConstants.java (72%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/ITypechecker.java (86%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/IntegerOrSetOfPairType.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/IntegerOrSetType.java (89%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/IntegerType.java (84%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/ModelValueType.java (89%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/PairType.java (92%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/SetType.java (91%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/StringType.java (87%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/StructType.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/btypes/UntypedType.java (87%)
rename src/main/java/de/{b2tla => tlc4b}/exceptions/LTLParseException.java (64%)
rename src/main/java/de/{b2tla => tlc4b}/exceptions/NotSupportedException.java (65%)
rename src/main/java/de/{b2tla => tlc4b}/exceptions/NotSupportedLTLFormulaException.java (66%)
rename src/main/java/de/{b2tla => tlc4b}/exceptions/ScopeException.java (61%)
rename src/main/java/de/{b2tla => tlc4b}/exceptions/SubstitutionException.java (61%)
create mode 100644 src/main/java/de/tlc4b/exceptions/TLC4BException.java
create mode 100644 src/main/java/de/tlc4b/exceptions/TLC4BIOException.java
rename src/main/java/de/{b2tla => tlc4b}/exceptions/TypeErrorException.java (60%)
rename src/main/java/de/{b2tla => tlc4b}/exceptions/UnificationException.java (78%)
rename src/main/java/de/{b2tla => tlc4b}/ltl/LTLBPredicate.java (97%)
rename src/main/java/de/{b2tla => tlc4b}/ltl/LTLFormulaPrinter.java (98%)
rename src/main/java/de/{b2tla => tlc4b}/ltl/LTLFormulaVisitor.java (97%)
rename src/main/java/de/{b2tla => tlc4b}/prettyprint/TLAPrinter.java (94%)
rename src/main/java/de/{b2tla => tlc4b}/tla/ConfigFile.java (88%)
rename src/main/java/de/{b2tla => tlc4b}/tla/Generator.java (92%)
rename src/main/java/de/{b2tla => tlc4b}/tla/TLADefinition.java (90%)
rename src/main/java/de/{b2tla => tlc4b}/tla/TLAModule.java (92%)
rename src/main/java/de/{b2tla => tlc4b}/tla/config/ConfigFileAssignment.java (86%)
rename src/main/java/de/{b2tla => tlc4b}/tla/config/ModelValueAssignment.java (85%)
rename src/main/java/de/{b2tla => tlc4b}/tla/config/SetOfModelValuesAssignment.java (86%)
rename src/main/java/de/{b2tla => tlc4b}/tlc/ModuleMatcher.java (95%)
rename src/main/java/de/{b2tla => tlc4b}/tlc/TLCOutputInfo.java (93%)
rename src/main/java/de/{b2tla => tlc4b}/tlc/TLCResults.java (96%)
rename src/main/java/de/{b2tla => tlc4b}/tlc/TracePrinter.java (97%)
rename src/main/java/de/{b2tla => tlc4b}/util/BTLCPrintStream.java (85%)
rename src/main/java/de/{b2tla => tlc4b}/util/StopWatch.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/ConstantsEvaluatorTest.java (87%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/ConstantsTest.java (93%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/DeferredSetSize.java (90%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/DefinitionsOrderTest.java (96%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/DefinitionsTest.java (93%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/ExpressionConstantTest.java (91%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/PrecedenceTest.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/RenamerTest.java (93%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/ScopeTest.java (97%)
rename src/test/java/de/{b2tla => tlc4b}/analysis/TypeRestrictionsTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/ltl/LtlFormulaTest.java (97%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/ClausesTest.java (85%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/DataTypesTest.java (87%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/EnumeratedSetsTest.java (83%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/FunctionTest.java (94%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/LogicalPredicates.java (89%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/MachineParameterTest.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/NumbersTest.java (94%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/OperationsTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/RelationTest.java (89%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/SetTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/SetsClauseTest.java (88%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/StringTest.java (84%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/SubstitutionsTest.java (96%)
rename src/test/java/de/{b2tla => tlc4b}/prettyprint/Tester.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/.gitignore (100%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/BasicsTest.java (69%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/ErrorTest.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/LTLTest.java (87%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/SpecialTest.java (88%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/AssertionErrorTest.java (68%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/DeadlockTest.java (67%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/GoalTest.java (67%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/InvariantViolationTest.java (68%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/LawsTest.java (76%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/NoErrorTest.java (67%)
rename src/test/java/de/{b2tla => tlc4b}/tlc/integration/probprivate/WellDefinednessTest.java (69%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/ArithmeticOperatorTest.java (96%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/BooleansTest.java (93%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/FunctionTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/LogicalOperatorTest.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/MachineClausesTest.java (94%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/MinusTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/ModelValuesTest.java (92%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/MultTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/RecordTest.java (94%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/RelationsTest.java (93%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/SequenceTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/SetsClauseTest.java (89%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/SetsTest.java (95%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/StringTest.java (87%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/TestTypechecker.java (85%)
rename src/test/java/de/{b2tla => tlc4b}/typechecking/TypeErrosTest.java (87%)
rename src/test/java/de/{b2tla => tlc4b}/util/AbstractParseMachineTest.java (93%)
rename src/test/java/de/{b2tla => tlc4b}/util/PolySuite.java (99%)
rename src/test/java/de/{b2tla => tlc4b}/util/TLC4BTester.java (74%)
rename src/test/java/de/{b2tla => tlc4b}/util/TestPair.java (81%)
rename src/test/java/de/{b2tla => tlc4b}/util/TestUtil.java (95%)
diff --git a/build.gradle b/build.gradle
index f83bb03..cede4ac 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 009f6d6..47a9188 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 7c4f56a..0000000
--- 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 1561c66..0000000
--- 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 fa756bc..5cf711a 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 a18fdb9..362a7b9 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 7e1c6e4..c8eaedd 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 6465f08..14060bf 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 ac4611e..2802949 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 7766ae9..92b4ede 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 c4d1c7a..affde5a 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 82b1784..81ce5f7 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 ffd9afb..70dd44d 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 879c6ae..c6f4838 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 3148bcf..c123bbe 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 5d1fae0..c3de071 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 a14730d..708bf5a 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 477d8f6..7308851 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 3919f75..34d0e22 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 afba565..e629240 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 143c459..1dfc41b 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 2ec06c2..176ed35 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 4741a35..774252c 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 a226ab6..336eb05 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 77b4913..a83e961 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 927a069..11287b5 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 79419bf..39e8517 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 67a8993..932d2dc 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 2ae78ec..2a3c794 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 a682f46..a59cfb9 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 ff79eb0..1a51f57 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 2211a06..c49be29 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 af611ff..01147cf 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 64cba26..4206654 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 e3333fc..3653f2d 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 8ee5469..7082258 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 d4c842e..f620866 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 c7a17bd..f1a83cd 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 cbc286a..77765c9 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 2d9dd44..70cbe3c 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 c5eb10a..0be4a04 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 6f02747..6e3afd0 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 04d84de..2661434 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 74cf5db..ed5c511 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 d4cbdfa..79d4298 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 808d6b5..edf9e04 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 74c017d..c7cc54a 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 8d7abb9..476c355 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 078dc61..8d36dac 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 ee7a231..2a38f1c 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 12074af..0dc1d3a 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 0000000..5c4090a
--- /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 0000000..9d5f308
--- /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 52b2914..77a201c 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 1a08bb9..676d270 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 15e36db..59661f6 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 cf61f13..e466d73 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 b0cbf5a..750f05a 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 e85f28f..1e6b7fe 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 28eb984..5288a67 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 9105027..1e7d059 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 70afc01..731193f 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 db8ca74..702aad7 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 74678e7..90e880a 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 c7f10b2..8b6ef2d 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 45ee9a6..b08ca70 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 ac3d816..086e321 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 f4f87c6..2bc5956 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 ffe8195..71dabb6 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 0a64d2d..e79a25a 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 33592cd..9a6fb09 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 f74b914..89594ba 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 2daf28f..7ab9fd5 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 d7bdcca..f74c1a9 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 7c842f8..a97c0aa 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 fa87a9b..96310fd 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 f55a00f..c2c1ced 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 dfd6d8d..1efa162 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 1b8d55b..57892be 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 ef8ed62..fbb1645 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 5f38409..77fab20 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 b956efd..bd5ee36 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 1bab754..e4915b7 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 b4d64a2..213ae76 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 323c32a..482419a 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 8e4df28..f57b8ed 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 1abf355..815d684 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 2edd0b9..7708162 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 658ee0d..feb7404 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 0f928f7..d3c079b 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 ef2809a..b4339ec 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 47f160c..1f3a08f 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 85d6856..e2fbe06 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 071aa46..5a7795c 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 d4715c4..a89df69 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 69d4ae5..0123a5b 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 1ed9761..7b2fa16 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 58f4a4a..1c724d7 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 e134f59..8d192c0 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 8bfe466..bf2d1d4 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 4bcbd9b..601bb9b 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 dd23fcc..c694d80 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 bb004fe..f49ff36 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 1f7298d..d417892 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 f620c28..8499fdb 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 34b7fbe..b0e5e3f 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 1c26915..9983401 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 f15d6e0..e258315 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 f037047..0c16841 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 8492fbd..9873e90 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 99498e7..6049057 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 cacc53e..335f7d0 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 7ae20c6..10f6d98 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 248431f..f1d93ba 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 fdf760f..83709a0 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 a538080..d079703 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 0fc5551..6a90251 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 b9930fb..a2adbd3 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 30c91b1..2318629 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 6e1eac7..95a7be2 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 24a56a0..1afcd25 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 2e032b0..2a1cdfa 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 83c4b6e..9597179 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 c7bb4e2..05efcef 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 692cb73..e8083cd 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 2d3cae1..0fb12b7 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 e848220..9d77e7c 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 47aebd6..8bdc29b 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 5fafa53..4a4e079 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 e47962d..e45baa8 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 415a4ad..0bf941e 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 57230da..ca5af5c 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));
--
GitLab