diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index 31562e5c4869590e431857b300f90a45d4a199aa..7848c355aa43c75cd1cbfe836a1fd9342ee2fe80 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b;
import org.apache.commons.cli.CommandLine;
diff --git a/src/main/java/de/tla2b/analysis/BOperation.java b/src/main/java/de/tla2b/analysis/BOperation.java
index 447ab988534106ef146129b491fe1d3735c2bcf8..91dd132214b63279b5a6770c6a8b61e26b11704c 100644
--- a/src/main/java/de/tla2b/analysis/BOperation.java
+++ b/src/main/java/de/tla2b/analysis/BOperation.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.ArrayList;
@@ -321,9 +317,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
findUnchangedVaribalesInSemanticNode(node);
}
- /**
- * @param node2
- */
private void findUnchangedVaribalesInSemanticNode(SemanticNode node) {
switch (node.getKind()) {
case OpApplKind: {
@@ -344,9 +337,6 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
}
}
- /**
- * @param node2
- */
private void findUnchangedVariablesInOpApplNode(OpApplNode n) {
int kind = n.getOperator().getKind();
diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
index e8ab4c5b0da06d2937ac603bf05313184814bb4c..2d0b92bd694949a17c79a546d9dd7dd6404dec08 100644
--- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java
+++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.Hashtable;
@@ -34,9 +30,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
private int substitutionId = 11;
- /**
- * @param moduleNode
- */
public InstanceTransformation(ModuleNode moduleNode) {
defs = moduleNode.getOpDefs();
defsHash = new Hashtable<String, OpDefNode>();
@@ -70,12 +63,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param exprOrOpArgNode
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprOrOpArgNode generateNewExprOrOpArgNode(ExprOrOpArgNode n,
String prefix) throws AbortException {
if (n instanceof ExprNode) {
@@ -85,12 +72,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param body
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprNode generateNewExprNode(ExprNode n, String prefix)
throws AbortException {
switch (n.getKind()) {
@@ -158,12 +139,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
throw new RuntimeException();
}
- /**
- * @param n
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprNode generateNewOpApplNode(OpApplNode n, String prefix)
throws AbortException {
switch (n.getOperator().getKind()) {
@@ -232,12 +207,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
throw new RuntimeException("OpApplkind not implemented jet");
}
- /**
- * @param n
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprNode generateNewBuiltInNode(OpApplNode n, String prefix)
throws AbortException {
switch (getOpCode(n.getOperator().getName())) {
@@ -324,12 +293,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param args
- * @param prefix
- * @return
- * @throws AbortException
- */
private ExprOrOpArgNode[] generateNewArgs(ExprOrOpArgNode[] args,
String prefix) throws AbortException {
ExprOrOpArgNode[] res = new ExprOrOpArgNode[args.length];
@@ -339,10 +302,6 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
return res;
}
- /**
- * @param oldParams
- * @return
- */
private FormalParamNode[] generateNewParams(FormalParamNode[] oldParams) {
FormalParamNode[] newParams = new FormalParamNode[oldParams.length];
for (int i = 0; i < oldParams.length; i++) {
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index 54ccc5434db2eb625063a34b02de5b8fc0159ca5..97c9bfc95f4d44ef3f031a3e58c2eff0db5c042f 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import de.tla2b.exceptions.NotImplementedException;
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 6d0450448756c82abbae15f8e4d56fe652ba8986..2bb80655c96c2d87aa6f626da56b07ce0e278a18 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.ArrayList;
diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
index 0471c862499adaabe7887f9a8574c761c5981af9..50267aa6e0c5125291b3c4c2cb1097a7bc76c5d6 100644
--- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java
+++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
@@ -123,10 +119,6 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
private Set<String> globalNames = new HashSet<String>();
private Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<OpDefNode, Set<String>>();
- /**
- * @param moduleNode
- * @param specAnalyser
- */
public SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.usedDefinitions = specAnalyser.getUsedDefinitions();
diff --git a/src/main/java/de/tla2b/analysis/SymbolSorter.java b/src/main/java/de/tla2b/analysis/SymbolSorter.java
index 514837f1c390fee44d28a134fe04d0746b926da9..f32ed64169ad57a4b4413ed8c67ce8a44ab52cbb 100644
--- a/src/main/java/de/tla2b/analysis/SymbolSorter.java
+++ b/src/main/java/de/tla2b/analysis/SymbolSorter.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.Arrays;
@@ -80,4 +76,4 @@ class OpDefNodeComparator implements Comparator<OpDefNode> {
return 1;
return 0;
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/analysis/TypeChecker.java b/src/main/java/de/tla2b/analysis/TypeChecker.java
index 70120d2d409ef18a4269837ff5c1b2468e44b802..5e92c5338ea1c0c271a55f37874d25aaa74e7908 100644
--- a/src/main/java/de/tla2b/analysis/TypeChecker.java
+++ b/src/main/java/de/tla2b/analysis/TypeChecker.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.analysis;
import java.util.ArrayList;
@@ -63,11 +59,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
private ConfigfileEvaluator conEval;
- /**
- * @param moduleNode
- * @param conEval
- * @param specAnalyser
- */
public TypeChecker(ModuleNode moduleNode, ConfigfileEvaluator conEval, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
this.specAnalyser = specAnalyser;
@@ -221,10 +212,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /**
- * @param def
- * @throws TLA2BException
- */
public void visitOpDefNode(OpDefNode def) throws TLA2BException {
FormalParamNode[] params = def.getParams();
for (int i = 0; i < params.length; i++) {
@@ -254,12 +241,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- /**
- * @param exprOrOpArgNode
- * @param instance
- * @throws TypeErrorException
- * @throws NotImplementedException
- */
private TLAType visitExprOrOpArgNode(ExprOrOpArgNode n, TLAType expected) throws TLA2BException {
if (n instanceof ExprNode) {
return visitExprNode((ExprNode) n, expected);
@@ -351,12 +332,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return (TLAType) n.getToolObject(TYPE_ID);
}
- /**
- * @param n
- * @param expected
- * @return {@link TLAType}
- * @throws TLA2BException
- */
private TLAType visitOpApplNode(OpApplNode n, TLAType expected) throws TLA2BException {
switch (n.getOperator().getKind()) {
@@ -497,19 +472,13 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /**
- * @param exprNode
- * @param expected
- * @return {@link TLAType}
- * @throws TLA2BException
- */
private TLAType evalBuiltInKind(OpApplNode n, TLAType expected) throws TLA2BException {
switch (getOpCode(n.getOperator().getName())) {
- /**********************************************************************
+ /*
* equality and disequality: =, #, /=
- **********************************************************************/
+ */
case OPCODE_eq: // =
case OPCODE_noteq: // /=, #
{
@@ -524,9 +493,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- **********************************************************************/
+ */
case OPCODE_neg: // Negation
case OPCODE_lnot: // Negation
case OPCODE_cl: // $ConjList
@@ -548,9 +517,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Quantification: \A x \in S : P or \E x \in S : P
- **********************************************************************/
+ */
case OPCODE_be: // \E x \in S : P
case OPCODE_bf: // \A x \in S : P
{
@@ -565,9 +534,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Set Operators
- **********************************************************************/
+ */
case OPCODE_se: // SetEnumeration {..}
{
SetType found = new SetType(new UntypedType());
@@ -626,9 +595,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance();
}
- /**********************************************************************
+ /*
* Set Constructor
- **********************************************************************/
+ */
case OPCODE_sso: // $SubsetOf Represents {x \in S : P}
{
@@ -684,9 +653,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return setOfSet.getSubType();
}
- /**********************************************************************
+ /*
* Prime
- **********************************************************************/
+ */
case OPCODE_prime: // prime
{
try {
@@ -702,9 +671,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- /***********************************************************************
+ /*
* Tuple: Tuple as Function 1..n to Set (Sequence)
- ***********************************************************************/
+ */
case OPCODE_tup: { // $Tuple
ArrayList<TLAType> list = new ArrayList<TLAType>();
for (int i = 0; i < n.getArgs().length; i++) {
@@ -733,9 +702,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* Function constructors
- ***********************************************************************/
+ */
case OPCODE_rfs: // recursive function ( f[x\in Nat] == IF x = 0 THEN 1
// ELSE f[n-1]
{
@@ -782,9 +751,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* Function call
- ***********************************************************************/
+ */
case OPCODE_fa: // $FcnApply f[1]
{
TLAType domType;
@@ -840,9 +809,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /***********************************************************************
+ /*
* Domain of Function
- ***********************************************************************/
+ */
case OPCODE_domain: {
FunctionType func = new FunctionType(new UntypedType(), new UntypedType());
@@ -856,9 +825,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
return res;
}
- /***********************************************************************
+ /*
* Set of Function
- ***********************************************************************/
+ */
case OPCODE_sof: // [ A -> B]
{
SetType A = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
@@ -874,17 +843,17 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /**********************************************************************
+ /*
* Except
- **********************************************************************/
+ */
case OPCODE_exc: // $Except
{
return evalExcept(n, expected);
}
- /***********************************************************************
+ /*
* Cartesian Product: A \X B
- ***********************************************************************/
+ */
case OPCODE_cp: // $CartesianProd A \X B \X C as $CartesianProd(A, B, C)
{
ArrayList<TLAType> list = new ArrayList<TLAType>();
@@ -903,9 +872,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* Records
- ***********************************************************************/
+ */
case OPCODE_sor: // $SetOfRcds [L1 : e1, L2 : e2]
{
StructType struct = new StructType();
@@ -969,9 +938,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return r.getType(fieldName);
}
- /***********************************************************************
+ /*
* miscellaneous constructs
- ***********************************************************************/
+ */
case OPCODE_ite: // IF THEN ELSE
{
visitExprOrOpArgNode(n.getArgs()[0], BoolType.getInstance());
@@ -985,12 +954,12 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
case OPCODE_case: {
- /**
+ /*
* CASE p1 -> e1 [] p2 -> e2 represented as $Case( $Pair(p1,
* e1),$Pair(p2, e2) ) and CASE p1 -> e1 [] p2 -> e2 [] OTHER -> e3
* represented as $Case( $Pair(p1, e1), $Pair(p2, e2), $Pair(null,
* e3))
- **/
+ */
TLAType found = expected;
for (int i = 0; i < n.getArgs().length; i++) {
OpApplNode pair = (OpApplNode) n.getArgs()[i];
@@ -1046,9 +1015,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return BoolType.getInstance().unify(expected);
}
- /***********************************************************************
+ /*
* no TLA+ Built-ins
- ***********************************************************************/
+ */
case 0: {
return evalBBuiltIns(n, expected);
}
@@ -1126,12 +1095,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return domType;
}
- /**
- * @param n
- * @param expected
- * @return
- * @throws TLA2BException
- */
private TLAType evalExcept(OpApplNode n, TLAType expected) throws TLA2BException {
TLAType t = visitExprOrOpArgNode(n.getArgs()[0], expected);
n.setToolObject(TYPE_ID, t);
@@ -1199,12 +1162,6 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
- /**
- * @param list
- * @param valueType
- * @return
- * @throws TLA2BException
- */
private TLAType evalType(LinkedList<ExprOrOpArgNode> list, TLAType valueType) throws TLA2BException {
if (list.size() == 0) {
return valueType;
@@ -1225,9 +1182,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
switch (BBuiltInOPs.getOpcode(n.getOperator().getName())) {
// B Builtins
- /**********************************************************************
+ /*
* Standard Module Naturals
- **********************************************************************/
+ */
case B_OPCODE_gt: // >
case B_OPCODE_lt: // <
case B_OPCODE_leq: // <=
@@ -1290,9 +1247,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
}
}
- /**********************************************************************
+ /*
* Standard Module Integers
- **********************************************************************/
+ */
case B_OPCODE_int: // Int
{
try {
@@ -1317,9 +1274,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return IntType.getInstance();
}
- /**********************************************************************
+ /*
* Standard Module FiniteSets
- **********************************************************************/
+ */
case B_OPCODE_finite: // IsFiniteSet
{
try {
@@ -1344,9 +1301,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return IntType.getInstance();
}
- /**********************************************************************
+ /*
* Standard Module Sequences
- **********************************************************************/
+ */
case B_OPCODE_seq: { // Seq(S) - set of sequences, S must be a set
SetType S = (SetType) visitExprOrOpArgNode(n.getArgs()[0], new SetType(new UntypedType()));
@@ -1441,9 +1398,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
// TODO add BSeq to tla standard modules
- /**********************************************************************
+ /*
* Standard Module TLA2B
- **********************************************************************/
+ */
case B_OPCODE_min: // MinOfSet(S)
case B_OPCODE_max: // MaxOfSet(S)
@@ -1472,9 +1429,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /**********************************************************************
+ /*
* Standard Module TLA2B
- **********************************************************************/
+ */
case B_OPCODE_pow1: // POW1
{
@@ -1490,9 +1447,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /**********************************************************************
+ /*
* Standard Module Relations
- **********************************************************************/
+ */
case B_OPCODE_rel_inverse: // POW1
{
SetType set = new SetType(new TupleType(2));
@@ -1511,9 +1468,9 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
return found;
}
- /***********************************************************************
+ /*
* TLA+ Built-Ins, but not in tlc.tool.BuiltInOPs
- ***********************************************************************/
+ */
case B_OPCODE_bool: // BOOLEAN
try {
SetType found = new SetType(BoolType.getInstance());
diff --git a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
index 9c2c6f57814e4081b1912c6dae25060dedc86965..70707605201af2c943ca8528c56a172c76d964fa 100644
--- a/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
+++ b/src/main/java/de/tla2b/config/ConfigfileEvaluator.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import java.util.ArrayList;
@@ -75,11 +71,6 @@ public class ConfigfileEvaluator {
// configuration file. All constants with arguments have to be overridden in
// the configuration file.
-
- /**
- * @param configAst
- * @param moduleNode
- */
public ConfigfileEvaluator(ModelConfig configAst, ModuleNode moduleNode) {
this.configAst = configAst;
this.moduleNode = moduleNode;
@@ -116,10 +107,6 @@ public class ConfigfileEvaluator {
this.enumeratedTypes = new LinkedHashMap<String, EnumType>();
}
- /**
- * @throws ConfigFileErrorException
- *
- */
public void start() throws ConfigFileErrorException {
evalNext(); // check if NEXT declaration is a valid definition
evalInit(); // check if INIT declaration is a valid definition
@@ -214,9 +201,7 @@ public class ConfigfileEvaluator {
}
/**
- * Represents a override statement in the configuration file: k <- def
- *
- * @throws ConfigFileErrorException
+ * Represents a override statement in the configuration file: k <- def
*/
@SuppressWarnings("unchecked")
private void evalConstantOrDefOverrides() throws ConfigFileErrorException {
diff --git a/src/main/java/de/tla2b/config/ModuleOverrider.java b/src/main/java/de/tla2b/config/ModuleOverrider.java
index 40b92b254de36eaa91b40aeba64230fac193c673..1b6108c29593ba802c2ce3fcf2b6be8d009ccb5c 100644
--- a/src/main/java/de/tla2b/config/ModuleOverrider.java
+++ b/src/main/java/de/tla2b/config/ModuleOverrider.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import java.util.Hashtable;
@@ -26,10 +22,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private Hashtable<OpDefNode, OpDefNode> operatorOverrideTable;
private Hashtable<OpDefNode, ValueObj> operatorAssignments;
- /**
- * @param constantOverrideTable
- * @param operatorOverrideTable
- */
public ModuleOverrider(ModuleNode moduleNode,
Hashtable<OpDeclNode, OpDefNode> constantOverrideTable,
Hashtable<OpDefNode, OpDefNode> operatorOverrideTable,
@@ -40,10 +32,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
this.operatorAssignments = operatorAssignments;
}
- /**
- * @param moduleNode
- * @param conEval
- */
public ModuleOverrider(ModuleNode moduleNode, ConfigfileEvaluator conEval) {
this.moduleNode = moduleNode;
this.constantOverrideTable = conEval.getConstantOverrideTable();
@@ -109,9 +97,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
}
}
- /**
- * @param body
- */
private OpApplNode visitExprNode(ExprNode n) {
switch (n.getKind()) {
@@ -140,9 +125,6 @@ public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
return null;
}
- /**
- * @param n
- */
private OpApplNode visitOpApplNode(OpApplNode n) {
SymbolNode s = n.getOperator();
switch (s.getKind()) {
diff --git a/src/main/java/de/tla2b/config/TLCValueNode.java b/src/main/java/de/tla2b/config/TLCValueNode.java
index f8d9d0e9b0295e520073a9de1c2aaee4c515cbe4..5878606e2ceb855749d9e9279934897c142394b9 100644
--- a/src/main/java/de/tla2b/config/TLCValueNode.java
+++ b/src/main/java/de/tla2b/config/TLCValueNode.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import de.tla2b.global.TranslationGlobals;
@@ -16,11 +12,6 @@ public class TLCValueNode extends NumeralNode implements TranslationGlobals {
private Value value;
private TLAType type;
- /**
- * @param valObj
- * @param stn
- * @throws AbortException
- */
public TLCValueNode(ValueObj valObj, TreeNode stn) throws AbortException {
super("1337", stn);
this.value = valObj.getValue();
diff --git a/src/main/java/de/tla2b/config/ValueObj.java b/src/main/java/de/tla2b/config/ValueObj.java
index 668add56ef239c479dbda0aa241520f8daa04e27..85b95f99dcb565ff3610d57e1f586fa0b45521a0 100644
--- a/src/main/java/de/tla2b/config/ValueObj.java
+++ b/src/main/java/de/tla2b/config/ValueObj.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.config;
import de.tla2b.types.TLAType;
diff --git a/src/main/java/de/tla2b/exceptions/SemanticErrorException.java b/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
index 6af42f002872b1d925d7710e362819ba0bc9be7c..7708c8b8897ca27ab429cb3a8373e639b3d6a926 100644
--- a/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
+++ b/src/main/java/de/tla2b/exceptions/SemanticErrorException.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.exceptions;
@SuppressWarnings("serial")
diff --git a/src/main/java/de/tla2b/exceptions/UnificationException.java b/src/main/java/de/tla2b/exceptions/UnificationException.java
index 710fbc9a332bc6bda869c639cf395e7bbccacf7e..8ca36d7eb1669c4539af5b730e03be08a7540248 100644
--- a/src/main/java/de/tla2b/exceptions/UnificationException.java
+++ b/src/main/java/de/tla2b/exceptions/UnificationException.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.exceptions;
@SuppressWarnings("serial")
public class UnificationException extends TLA2BException{
diff --git a/src/main/java/de/tla2b/global/TranslationGlobals.java b/src/main/java/de/tla2b/global/TranslationGlobals.java
index 938cfc33de83757570e7072e68c30fa73fbd7444..cc159dfb118af2742823d822c3bcd5350e296ef9 100644
--- a/src/main/java/de/tla2b/global/TranslationGlobals.java
+++ b/src/main/java/de/tla2b/global/TranslationGlobals.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.global;
import java.util.ArrayList;
diff --git a/src/main/java/de/tla2b/types/EnumType.java b/src/main/java/de/tla2b/types/EnumType.java
index c0ce831aee6d9c107fc9a520d2378c9817add320..a78c0fe3b49e8b7fb6a83d1e2517f36829103e3a 100644
--- a/src/main/java/de/tla2b/types/EnumType.java
+++ b/src/main/java/de/tla2b/types/EnumType.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.types;
import java.util.ArrayList;
@@ -12,8 +8,6 @@ import de.tla2b.exceptions.UnificationException;
import de.tla2b.output.TypeVisitorInterface;
import de.tla2bAst.BAstCreator;
-
-
public class EnumType extends AbstractHasFollowers {
public LinkedHashSet<String> modelvalues;
public int id;
@@ -90,4 +84,4 @@ public class EnumType extends AbstractHasFollowers {
}
-}
\ No newline at end of file
+}
diff --git a/src/main/java/de/tla2b/types/StringType.java b/src/main/java/de/tla2b/types/StringType.java
index 13b5623ed26f9382ec1a2c849838cfdbaabc3f19..8e507fd5c6bae0523259afbce656be49e836d69e 100644
--- a/src/main/java/de/tla2b/types/StringType.java
+++ b/src/main/java/de/tla2b/types/StringType.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.types;
import de.be4.classicalb.core.parser.node.AStringSetExpression;
diff --git a/src/main/java/de/tla2b/types/StructOrFunctionType.java b/src/main/java/de/tla2b/types/StructOrFunctionType.java
index fc4aea18059a0c65577465890ee993eb8bbba115..0243e925e129b35975a4541e832db4142ab3e953 100644
--- a/src/main/java/de/tla2b/types/StructOrFunctionType.java
+++ b/src/main/java/de/tla2b/types/StructOrFunctionType.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.types;
import java.util.Iterator;
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 46c2d552b483ce4959de758458820bd64bb211a4..df56ca78ed9a5a59304c8fd8a1a9eda9660311ee 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -87,9 +87,6 @@ public class BAstCreator extends BuiltInOPs
/**
* Creates a B AST node for a TLA expression
- *
- * @param moduleNode
- * @param specAnalyser
*/
public BAstCreator(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
this.moduleNode = moduleNode;
@@ -996,9 +993,9 @@ public class BAstCreator extends BuiltInOPs
returnNode = new ABooleanFalseExpression();
break;
- /**********************************************************************
+ /*
* Standard Module Naturals
- **********************************************************************/
+ */
case B_OPCODE_nat: // Nat
returnNode = new ANaturalSetExpression();
break;
@@ -1098,9 +1095,9 @@ public class BAstCreator extends BuiltInOPs
case B_OPCODE_string: // STRING
returnNode = new AStringSetExpression();
break;
- /**********************************************************************
+ /*
* Standard Module Sequences
- **********************************************************************/
+ */
case B_OPCODE_seq: // Seq(S) - set of sequences
returnNode = new ASeqExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
@@ -1295,9 +1292,9 @@ public class BAstCreator extends BuiltInOPs
return new AConvertBoolExpression(notEqual);
}
- /**********************************************************************
+ /*
* Set Operators
- **********************************************************************/
+ */
case OPCODE_se: // SetEnumeration {..}
{
diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java
index ea33cfb29a8e96cacadd7e9a5386b157d2cf74fc..7fd7ee86c6e666186638bbb8ebf2f158dd07bb51 100644
--- a/src/main/java/de/tla2bAst/ExpressionTranslator.java
+++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java
@@ -185,10 +185,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return n;
}
- /**
- * @param moduleFileName
- * @throws de.tla2b.exceptions.FrontEndException
- */
private SpecObj parseModuleWithoutSemanticAnalyse(String moduleFileName,
String module) {
SpecObj spec = new SpecObj(moduleFileName, null);
@@ -211,10 +207,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
return spec;
}
- /**
- * @param spec
- * @return
- */
private void evalVariables(SpecObj spec, String moduleName) {
ParseUnit p = (ParseUnit) spec.parseUnitContext.get(moduleName);
TreeNode n_module = p.getParseTree();
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 7395892949117faf6649ee5f3e9d04f804d5836f..ad5ce0c860f18ecc879d0553f0c6bfe1fb2252c2 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -94,12 +94,6 @@ public class Translator implements TranslationGlobals {
/**
* External interface
- *
- * @param moduleName
- * @param moduleString
- * @param configString
- * @return
- * @throws TLA2BException
*/
public static String translateModuleString(String moduleName, String moduleString, String configString)
throws TLA2BException {
diff --git a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
index c1722d8c3542ed254119a517f773fd25b3721eda..69bfaa6282803984c8e4cb56f2f0a48d02001ca6 100644
--- a/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/ComplexExpressionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
index 97e570cccc3c7f1cdad9a1cb3ebdb1935b7ed44c..01f1577c56a05f7398bc67b15ce3b741fcd97f60 100644
--- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
+++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/expression/TestError.java b/src/test/java/de/tla2b/expression/TestError.java
index 104ff1b69f85845fe761399e9bb0f953a54d830d..63f113bce03dfc290d7a9549f9bea95e46839801 100644
--- a/src/test/java/de/tla2b/expression/TestError.java
+++ b/src/test/java/de/tla2b/expression/TestError.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExpr;
diff --git a/src/test/java/de/tla2b/expression/TestKeywords.java b/src/test/java/de/tla2b/expression/TestKeywords.java
index ef4ecec88e4e24cc4e4f0c2e01a457188a49354f..7516daeb1c26d4265479417b9ed4d367dde6749f 100644
--- a/src/test/java/de/tla2b/expression/TestKeywords.java
+++ b/src/test/java/de/tla2b/expression/TestKeywords.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/expression/TestSequences.java b/src/test/java/de/tla2b/expression/TestSequences.java
index 9fabeecf4b077d798ee1cdc20ade27c2ec2eb0d5..123e10a74d22cb675db7c0c0fb25131776e2ce57 100644
--- a/src/test/java/de/tla2b/expression/TestSequences.java
+++ b/src/test/java/de/tla2b/expression/TestSequences.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExpr;
diff --git a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
index 6570544fcfa7d43fe7e756b1ea4538d322cf58e6..98b5c659f8ad96e5bc303df75617193f0a8369fc 100644
--- a/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/BBuiltInsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index e2a58e5492d31e22cc09f420f32829d06e7f2e4a..351f4f1d03a1e8f01cf403ad922280b6a2e9203a 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
@@ -98,9 +94,9 @@ public class FunctionTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* recursive Function
- **********************************************************************/
+ */
@Ignore
@Test
@@ -122,9 +118,9 @@ public class FunctionTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Function call
- **********************************************************************/
+ */
@Test
public void testFunctionCall() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index 5293734658343d92cbf619b11374dba3eba83119..6cf231b2857f751ae0a2833146254af2f5a79ba1 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import org.junit.Test;
@@ -43,9 +39,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
- * Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- **********************************************************************/
+ /*
+ * Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
+ */
@Test
public void testAnd() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -71,9 +67,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Negation: ~, \neg, \lnot
- **********************************************************************/
+ */
@Test
public void testNegation() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -84,9 +80,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Implication and Equivalence: =>, \equiv
- **********************************************************************/
+ */
@Test
public void testImplication() throws Exception {
@@ -112,9 +108,9 @@ public class LogicOperatorsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Quantification: \A x \in S : P or \E x \in S : P
- **********************************************************************/
+ */
@Test
public void testUniversalQuantifier() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java b/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
index fa457c914fd29cd9b5259939209bc55612f8d226..bb851df8b3e810640ba686c85d8113c49b7c53e3 100644
--- a/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/PrecedenceTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/RecordTest.java b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
index c956984edb449197afe511bd9b18718d8e9c2b00..c837c85133974086ba250dd490aaf7c336c41b33 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecordTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecordTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
@@ -16,9 +12,9 @@ public class RecordTest {
ToolIO.setMode(ToolIO.TOOL);
}
- /**********************************************************************
+ /*
* Set of Records: [L1 : e1, L2 : e2]
- **********************************************************************/
+ */
@Test
public void testStruct() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -34,9 +30,9 @@ public class RecordTest {
}
- /**********************************************************************
+ /*
* Record: [L1 |-> e1, L2 |-> e2]
- **********************************************************************/
+ */
@Test
public void testRecord() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -65,9 +61,9 @@ public class RecordTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Record Select: r.c
- **********************************************************************/
+ */
@Test
public void testRecordSelect() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -94,9 +90,9 @@ public class RecordTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Record Except
- **********************************************************************/
+ */
@Test
public void testRecordExcept() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -110,9 +106,9 @@ public class RecordTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Record Except @
- **********************************************************************/
+ */
@Test
public void testRecordExceptAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsTest.java b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
index e9739e28b049f3e8e41ab61852a9ee35d245d40d..cbc5b000b837284dcd905066a64484510b9305ad 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
@@ -34,9 +30,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Element of: \in, \notin
- **********************************************************************/
+ */
@Test
public void testMemberOf() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -68,9 +64,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* set operators like difference, union, intersection: \setdiff, \cup, \cap
- **********************************************************************/
+ */
@Test
public void testSetDifference() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -104,9 +100,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Subseteq: subset or equal
- **********************************************************************/
+ */
@Test
public void testSubsteq() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -118,9 +114,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* SUBSET: conforms POW in B
- **********************************************************************/
+ */
@Test
public void testSubset() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -132,9 +128,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* UNION
- **********************************************************************/
+ */
@Test
public void testUnion() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -146,9 +142,9 @@ public class SetsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Set Constructor
- **********************************************************************/
+ */
@Test
public void testConstructor1() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/TupleTest.java b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
index 8001764bd315d8f1253fa51ede7986892d0aa557..8528ef4f0ecd7460c330f35f825fbf1f76fa63b7 100644
--- a/src/test/java/de/tla2b/prettyprintb/TupleTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/TupleTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/VariablesTest.java b/src/test/java/de/tla2b/prettyprintb/VariablesTest.java
index 386aa9198e480ff1e38ad7a41ada7ebaa47dc7c2..1188100abd2d06c0b1c6f96b01e58236c8521551 100644
--- a/src/test/java/de/tla2b/prettyprintb/VariablesTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/VariablesTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
index 7daa5a4aa834d12f96d61b6bbf4540a5ef6d4e35..8c64d97626eb5ea3af1c88bed35d16db6ef50721 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleFiniteSetsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
index 47c88dcf92d27ab2ce6348d384bd903d78249c6d..58cc1c4ad7d97def206990c1dfe90bc416a64a72 100644
--- a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleNaturalsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.prettyprintb.standardmodules;
import static de.tla2b.util.TestUtil.compare;
@@ -13,9 +9,9 @@ import org.junit.Test;
public class ModuleNaturalsTest {
- /**********************************************************************
+ /*
* >, <, <=, >=
- **********************************************************************/
+ */
@Test
public void testCompareOperators() throws Exception {
@@ -41,9 +37,9 @@ public class ModuleNaturalsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Arithmetic operator: +, -, *, %, ^ (\div operator is not tested)
- **********************************************************************/
+ */
@Test
public void testArithmeticOperators() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -56,9 +52,9 @@ public class ModuleNaturalsTest {
compare(expected, module);
}
- /**********************************************************************
+ /*
* Interval operator: x .. y
- **********************************************************************/
+ */
@Test
public void testDotDot() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
index a79f3b65f25528091feb3163d01273fa01d20757..5a9954b5b3e7ac06d56e250f8f94fbfb270c6420 100644
--- a/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
+++ b/src/test/java/de/tla2b/typechecking/BBuiltInsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -18,9 +14,9 @@ import de.tla2b.util.TestUtil;
public class BBuiltInsTest {
- /**********************************************************************
+ /*
* BOOLEAN
- **********************************************************************/
+ */
@Test
public void testBoolean() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -42,9 +38,9 @@ public class BBuiltInsTest {
}
- /**********************************************************************
+ /*
* String
- **********************************************************************/
+ */
@Test
public void testString() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -64,9 +60,9 @@ public class BBuiltInsTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Bool value: TRUE, FALSE
- **********************************************************************/
+ */
@Test
public void testBoolValue() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/ConfigTest.java b/src/test/java/de/tla2b/typechecking/ConfigTest.java
index ff938d0deb2b08a1810e709968b3a45a6edb8ca8..2968bcef481f2ce892155b671794e09c86fe807e 100644
--- a/src/test/java/de/tla2b/typechecking/ConfigTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConfigTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
index f3c7471b068f64a3b257c02bbd740deb9ef89309..998607a9fda4254c8d92ae4abb29bbe423bb643a 100644
--- a/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
+++ b/src/test/java/de/tla2b/typechecking/ConstantTypesTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
diff --git a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
index 954fe821e0418b9b5e1436e88bad89b0e5f525ad..e1a65ae29e3ab0f3cec2a7e5e3eacff8c0ec399f 100644
--- a/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
+++ b/src/test/java/de/tla2b/typechecking/DefinitionsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -16,9 +12,9 @@ import de.tla2b.util.TestUtil;
public class DefinitionsTest {
- /**********************************************************************
+ /*
* Definition: foo(a,b) == e
- **********************************************************************/
+ */
@Test
public void testDefinition() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -72,9 +68,9 @@ public class DefinitionsTest {
assertEquals("BOOL", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Definition Call
- **********************************************************************/
+ */
@Test
public void testDefinitionCall() throws FrontEndException, TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/ExceptTest.java b/src/test/java/de/tla2b/typechecking/ExceptTest.java
index 82d4cc18787154a905a01807280971467fd5b200..5531720aa94eb350870325da0578e67f82104335 100644
--- a/src/test/java/de/tla2b/typechecking/ExceptTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExceptTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/ExtendsTest.java b/src/test/java/de/tla2b/typechecking/ExtendsTest.java
index 95e7cedf057e1b2d67bb885121f57dd26f1e13c3..a62dca20ca6e5c81155d00460ce01ffec11a0ffe 100644
--- a/src/test/java/de/tla2b/typechecking/ExtendsTest.java
+++ b/src/test/java/de/tla2b/typechecking/ExtendsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/FunctionTest.java b/src/test/java/de/tla2b/typechecking/FunctionTest.java
index a73ea0b2705b961e764dd5d2e902f2aee69534fb..e12fda6a5e5b71dbc1f18e8d63a4502e0526fe0d 100644
--- a/src/test/java/de/tla2b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tla2b/typechecking/FunctionTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class FunctionTest {
- /**********************************************************************
+ /*
* Function constructor
- **********************************************************************/
+ */
@Test
public void testSimpleFunctionConstructor() throws FrontEndException,
@@ -165,9 +161,9 @@ public class FunctionTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* recursive Function
- **********************************************************************/
+ */
@Test
public void testRecursiveFunction() throws FrontEndException,
TLA2BException {
@@ -183,9 +179,9 @@ public class FunctionTest {
assertEquals("INTEGER", t.getConstantType("k3"));
}
- /**********************************************************************
+ /*
* Function call
- **********************************************************************/
+ */
@Test
public void testFunctionCall() throws FrontEndException, TLA2BException {
@@ -244,9 +240,9 @@ public class FunctionTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Domain
- **********************************************************************/
+ */
@Test
public void testDomain() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -273,9 +269,9 @@ public class FunctionTest {
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Set of Function
- **********************************************************************/
+ */
@Test
public void testSetOfFunction() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -310,9 +306,9 @@ public class FunctionTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Except
- **********************************************************************/
+ */
@Test
public void testFunctionExcept() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -412,9 +408,9 @@ public class FunctionTest {
assertEquals("POW(INTEGER*INTEGER*INTEGER)", t.getConstantType("k"));
}
- /**********************************************************************
+ /*
* Except @
- **********************************************************************/
+ */
@Test
public void testAt2() throws FrontEndException, TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index 329a772f0855ba85b5c7e53c40172c9ce00f25bb..6ac9c7d201cb9dab69bde3bfa7ae12b15561ce84 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
index f4585bf4dc0ae16d6592ca53c4820478a8c8c153..c46e2f7b8543ea3814e77adef342b9db4b4f9785 100644
--- a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class LogicOperatorsTest {
- /**********************************************************************
+ /*
* equality and disequality: =, #,
- **********************************************************************/
+ */
@Test
public void testEquality() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -48,9 +44,9 @@ public class LogicOperatorsTest {
- /**********************************************************************
+ /*
* Logic Operators: \neg, \lnot, \land, \cl, \lor, \dl, \equiv, =>
- **********************************************************************/
+ */
@Test
public void testLogicOperators() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -73,9 +69,9 @@ public class LogicOperatorsTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Quantification: \A x \in S : P or \E x \in S : P.
- **********************************************************************/
+ */
@Test
diff --git a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
index e49d769afedfc53d0c910852f4ffaaa7d53bcf03..6ed199bc9d04ab258aeac58672f3e6fefa1c9ace 100644
--- a/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
+++ b/src/test/java/de/tla2b/typechecking/MiscellaneousConstructsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -16,9 +12,9 @@ import de.tla2b.util.TestUtil;
public class MiscellaneousConstructsTest {
- /**********************************************************************
+ /*
* IF THEN ELSE
- **********************************************************************/
+ */
@Test
public void testIfThenElse() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -33,9 +29,9 @@ public class MiscellaneousConstructsTest {
}
- /**********************************************************************
+ /*
* IF THEN ELSE
- **********************************************************************/
+ */
@Test
public void testCase() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -65,9 +61,9 @@ public class MiscellaneousConstructsTest {
assertEquals("INTEGER",t.getConstantType("e3"));
}
- /**********************************************************************
+ /*
* LET d == exp IN e
- **********************************************************************/
+ */
@Test
public void testLetIn() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/OpArgTest.java b/src/test/java/de/tla2b/typechecking/OpArgTest.java
index a000e9be0c60e2caa9bed3ff6e07fabf3395258a..0c96a265dbf4a29f782ac2f803032198b2eafe9a 100644
--- a/src/test/java/de/tla2b/typechecking/OpArgTest.java
+++ b/src/test/java/de/tla2b/typechecking/OpArgTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
diff --git a/src/test/java/de/tla2b/typechecking/SetTest.java b/src/test/java/de/tla2b/typechecking/SetTest.java
index 4fad92a6033832457a2ce1ce105c9abc73de906d..3d5c323521209a7cb1d179e7818c89fcf3a092d9 100644
--- a/src/test/java/de/tla2b/typechecking/SetTest.java
+++ b/src/test/java/de/tla2b/typechecking/SetTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.*;
@@ -14,15 +10,11 @@ import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.util.TestTypeChecker;
import de.tla2b.util.TestUtil;
-import tla2sany.semantic.AbortException;
-
public class SetTest {
- /**********************************************************************
+ /*
* Set Enumeration: {1,2,3}
- *
- * @throws AbortException
- **********************************************************************/
+ */
@Test
public void testSetEnumeration() throws FrontEndException, TLA2BException {
@@ -97,9 +89,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Element of: \in, \notin
- **********************************************************************/
+ */
@Test
public void testElementOfSet() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -150,9 +142,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* set operators like difference, union, intersection
- **********************************************************************/
+ */
@Test
public void testSetOperators() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -196,9 +188,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* set constructor: {x \in S : p}.
- **********************************************************************/
+ */
@Test
public void testSubsetOf() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -310,9 +302,9 @@ public class SetTest {
assertEquals("POW(INTEGER*BOOL)", t.getConstantType("S"));
}
- /**********************************************************************
+ /*
* set constructor: {e : x \in S}
- **********************************************************************/
+ */
@Test
public void testSetOfAll() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -391,9 +383,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* SUBSET: conforms POW in B
- **********************************************************************/
+ */
@Test
public void testSubset() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -425,9 +417,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* UNION
- **********************************************************************/
+ */
@Test
public void testUnion() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -468,9 +460,9 @@ public class SetTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Subseteq: subset or equal
- **********************************************************************/
+ */
@Test
public void testSubseteq() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/StringTest.java b/src/test/java/de/tla2b/typechecking/StringTest.java
index 4ae59cec51d86e3730fe22c3883fc06681b98cd4..e606c6b9d6c87973384bc282dfa91eb87d695ab6 100644
--- a/src/test/java/de/tla2b/typechecking/StringTest.java
+++ b/src/test/java/de/tla2b/typechecking/StringTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class StringTest {
- /**********************************************************************
+ /*
* a String: "abc"
- **********************************************************************/
+ */
@Test
public void testAString() throws FrontEndException, TLA2BException {
@@ -67,9 +63,9 @@ public class StringTest {
}
- /**********************************************************************
+ /*
* STRING
- **********************************************************************/
+ */
@Test
public void testString() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/StructTest.java b/src/test/java/de/tla2b/typechecking/StructTest.java
index e9ef27613053e7aa38d4797092f30d681f2de88e..3b577f56ed0e6943f58553568389dcec420e1eed 100644
--- a/src/test/java/de/tla2b/typechecking/StructTest.java
+++ b/src/test/java/de/tla2b/typechecking/StructTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import static org.junit.Assert.assertEquals;
@@ -20,9 +16,9 @@ public class StructTest {
ToolIO.setMode(ToolIO.TOOL);
}
- /**********************************************************************
+ /*
* Set of Records: [L1 : e1, L2 : e2]
- **********************************************************************/
+ */
@Test
public void testStruct() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -84,9 +80,9 @@ public class StructTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Record: [L1 |-> e1, L2 |-> e2]
- **********************************************************************/
+ */
@Test
public void testRecord() throws FrontEndException, TLA2BException {
@@ -128,9 +124,9 @@ public class StructTest {
assertEquals("BOOL", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Record Select: r.c
- **********************************************************************/
+ */
@Test
public void testRecordSelect() throws FrontEndException, TLA2BException {
@@ -220,9 +216,9 @@ public class StructTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Record Except
- **********************************************************************/
+ */
@Test
public void testRecordExcept() throws FrontEndException, TLA2BException {
@@ -248,9 +244,9 @@ public class StructTest {
assertEquals("struct(a:INTEGER,b:BOOL)", t.getConstantType("k2"));
}
- /**********************************************************************
+ /*
* Record Except @
- **********************************************************************/
+ */
@Test
public void testRecordExceptAt() throws FrontEndException, TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/TupleTest.java b/src/test/java/de/tla2b/typechecking/TupleTest.java
index 48b0fb9225adb602eaf6b7a4f4eaf186c0a5dfb7..2581f924fb871393a9c58503f1e5480f88d25830 100644
--- a/src/test/java/de/tla2b/typechecking/TupleTest.java
+++ b/src/test/java/de/tla2b/typechecking/TupleTest.java
@@ -157,9 +157,9 @@ public class TupleTest {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Cartesian Product
- **********************************************************************/
+ */
@Test
public void testCartesianProduct2() throws FrontEndException,
TLA2BException {
diff --git a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
index 413014fb12af5b6c178cc805c131a55ebf7f1675..9dd382d560d13e874fb3ba3dc41054db92c2c88b 100644
--- a/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
+++ b/src/test/java/de/tla2b/typechecking/TypeConflictsTest.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking;
import org.junit.Test;
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
index fa93e1d0fc72c34dfb059497b22d5a21a0e4f639..44c102b1f759c4a690b19893db1294a614356edc 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleFiniteSets.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleFiniteSets {
- /**********************************************************************
+ /*
* IsFiniteSet
- **********************************************************************/
+ */
@Test
public void unifyIsFiniteSet() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -73,9 +69,9 @@ public class TestModuleFiniteSets {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Cardinality
- **********************************************************************/
+ */
@Test
public void unifyCardinality() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
index b658435a201b03a406568fd6e7dcbcb6265650b8..66941f424a1c4e3194edf9b407e71406b0976d23 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleIntegers.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleIntegers {
- /**********************************************************************
+ /*
* Int
- **********************************************************************/
+ */
@Test
public void unifyInt() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -40,9 +36,9 @@ public class TestModuleIntegers {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* unary minus: -x
- **********************************************************************/
+ */
@Test
public void unifyUnaryMinus() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
index 3fa055da24b9cc519bc546bd8f7bcc7b36833c24..5d6501c06b0cbfd9d9f3a138f623e6ec4acfdae3 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleNaturals.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.assertEquals;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleNaturals {
- /**********************************************************************
+ /*
* Relational operators: >, <, <=, >=
- **********************************************************************/
+ */
@Test
public void testRelationalOperators() throws FrontEndException,
TLA2BException {
@@ -44,9 +40,9 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Arithmetic operator: +, -, *, /, mod, exp
- **********************************************************************/
+ */
@Test
public void testArithmeticOperators() throws FrontEndException,
TLA2BException {
@@ -72,9 +68,9 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Interval operator: x .. y
- **********************************************************************/
+ */
@Test
public void testDotDot() throws FrontEndException, TLA2BException {
@@ -99,9 +95,9 @@ public class TestModuleNaturals {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Nat
- **********************************************************************/
+ */
@Test
public void testNat() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
index 0ae160faef029bcd572d77ab1cada3a7c3685481..7eccb44a531bce6005dc992aa54ae9fb794452ef 100644
--- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
+++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleSequences.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.typechecking.standardmodules;
import static org.junit.Assert.*;
@@ -17,9 +13,9 @@ import de.tla2b.util.TestUtil;
public class TestModuleSequences {
- /**********************************************************************
+ /*
* Seq(S): The set of all sequences of elements in S.
- **********************************************************************/
+ */
@Test
public void testSeq() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -64,9 +60,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* Len(S)
- **********************************************************************/
+ */
@Test
public void testLen() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -109,9 +105,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* s \o s2 - concatenation of s and s2
- **********************************************************************/
+ */
@Test
public void testUnifyConcatenation() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -180,9 +176,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* Append(s, e)
- **********************************************************************/
+ */
@Test
public void testUnifyAppend() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -237,9 +233,9 @@ public class TestModuleSequences {
}
- /**********************************************************************
+ /*
* Head(s): the first element of the seq
- **********************************************************************/
+ */
@Test
public void testUnifyHead() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -274,9 +270,9 @@ public class TestModuleSequences {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* Tail(s): the sequence without the first element
- **********************************************************************/
+ */
@Test
public void testUnifyTail() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
@@ -312,9 +308,9 @@ public class TestModuleSequences {
TestUtil.typeCheckString(module);
}
- /**********************************************************************
+ /*
* SubSeq(s,m,n): The sequence <<s[m], s[m+1], ... , s[n]>>
- **********************************************************************/
+ */
@Test
public void testUnifySubSeq() throws FrontEndException, TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index 2dd2c112007892d403b2dd46aa6cf4a06a2f76e6..5e7af8bbaeb0be14e78e02ff381cbe440ef12f96 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.util;
import java.util.Hashtable;
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 0781ae22a33464782b2dc24ab8e3fc3484d425a5..d0d9cf7c7eb4b05f435ce6f446f5967c2d70859e 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -1,7 +1,3 @@
-/**
- * @author Dominik Hansen <Dominik.Hansen at hhu.de>
- **/
-
package de.tla2b.util;
import static org.junit.Assert.*;