Skip to content
Snippets Groups Projects
Commit 4ca233ba authored by Jan Gruteser's avatar Jan Gruteser
Browse files

apply IntelliJ reformat code to fix many indents

parent f495b228
No related branches found
No related tags found
No related merge requests found
Pipeline #134774 passed
Showing
with 1629 additions and 1679 deletions
......@@ -5,13 +5,7 @@ import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2bAst.Translator;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.DefaultParser;
import org.apache.commons.cli.HelpFormatter;
import org.apache.commons.cli.Option;
import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException;
import org.apache.commons.cli.*;
public class TLA2B implements TranslationGlobals {
public final static String VERSION = "version";
......
package de.tla2b.analysis;
import java.util.*;
import java.util.Map.Entry;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABlockSubstitution;
import de.be4.classicalb.core.parser.node.AMemberPredicate;
import de.be4.classicalb.core.parser.node.AOperation;
import de.be4.classicalb.core.parser.node.ASelectSubstitution;
import de.be4.classicalb.core.parser.node.ASkipSubstitution;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.*;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.TLAType;
import de.tla2bAst.BAstCreator;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.SubstInNode;
import tla2sany.semantic.SymbolNode;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
import java.util.*;
import java.util.Map.Entry;
public class BOperation extends BuiltInOPs implements ASTConstants,
ToolGlobals, TranslationGlobals {
private final String name;
......@@ -264,9 +246,9 @@ public class BOperation extends BuiltInOPs implements ASTConstants,
for (OpApplNode n : existQuans) {
FormalParamNode[][] params = n.getBdedQuantSymbolLists();
for (FormalParamNode[] param : params) {
for (int j = 0; j < param.length; j++) {
formalParams.add(param[j]);
opParams.add(param[j].getName().toString());
for (FormalParamNode formalParamNode : param) {
formalParams.add(formalParamNode);
opParams.add(formalParamNode.getName().toString());
}
}
}
......
package de.tla2b.analysis;
import java.util.Hashtable;
import de.tla2b.global.BBuiltInOPs;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import util.UniqueString;
import java.util.Hashtable;
public class InstanceTransformation extends BuiltInOPs implements ASTConstants {
final OpDefNode[] defs;
......
package de.tla2b.analysis;
import de.tla2b.exceptions.NotImplementedException;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tlc2.tool.BuiltInOPs;
import de.tla2b.exceptions.NotImplementedException;
public class RecursiveDefinition extends BuiltInOPs {
......
package de.tla2b.analysis;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Set;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.FrontEndException;
......@@ -16,19 +10,12 @@ import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.BDefinitionsFinder;
import de.tla2b.translation.OperationsFinder;
import de.tla2b.translation.UsedDefinitionsFinder;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.SymbolNode;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
import java.util.*;
public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals {
private OpDefNode spec;
private OpDefNode init;
......@@ -97,47 +84,65 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
if (definitions.containsKey("Spec")) {
specAnalyser.spec = definitions.get("Spec"); ClausefDetected("Spec","INITIALISATION+OPERATIONS");
specAnalyser.spec = definitions.get("Spec");
ClausefDetected("Spec", "INITIALISATION+OPERATIONS");
} else if (definitions.containsKey("SPECIFICATION")) {
specAnalyser.spec = definitions.get("SPECIFICATION"); ClausefDetected("SPECIFICATION","INITIALISATION+OPERATIONS");
specAnalyser.spec = definitions.get("SPECIFICATION");
ClausefDetected("SPECIFICATION", "INITIALISATION+OPERATIONS");
} else if (definitions.containsKey("SPEC")) {
specAnalyser.spec = definitions.get("SPEC"); ClausefDetected("SPEC","INITIALISATION+OPERATIONS");
specAnalyser.spec = definitions.get("SPEC");
ClausefDetected("SPEC", "INITIALISATION+OPERATIONS");
}
if (definitions.containsKey("Init")) {
specAnalyser.init = definitions.get("Init"); ClausefDetected("Init","INITIALISATION");
specAnalyser.init = definitions.get("Init");
ClausefDetected("Init", "INITIALISATION");
} else if (definitions.containsKey("INIT")) {
specAnalyser.init = definitions.get("INIT"); ClausefDetected("INIT","INITIALISATION");
specAnalyser.init = definitions.get("INIT");
ClausefDetected("INIT", "INITIALISATION");
} else if (definitions.containsKey("Initialisation")) {
specAnalyser.init = definitions.get("Initialisation"); ClausefDetected("Initialisation","INITIALISATION");
specAnalyser.init = definitions.get("Initialisation");
ClausefDetected("Initialisation", "INITIALISATION");
} else if (definitions.containsKey("INITIALISATION")) {
specAnalyser.init = definitions.get("INITIALISATION"); ClausefDetected("INITIALISATION","INITIALISATION");
specAnalyser.init = definitions.get("INITIALISATION");
ClausefDetected("INITIALISATION", "INITIALISATION");
}
if (definitions.containsKey("Next")) {
specAnalyser.next = definitions.get("Next"); ClausefDetected("Next","OPERATIONS");
specAnalyser.next = definitions.get("Next");
ClausefDetected("Next", "OPERATIONS");
} else if (definitions.containsKey("NEXT")) {
specAnalyser.next = definitions.get("NEXT"); ClausefDetected("NEXT","OPERATIONS");
specAnalyser.next = definitions.get("NEXT");
ClausefDetected("NEXT", "OPERATIONS");
}
if (definitions.containsKey("Inv")) {
specAnalyser.invariants.add(definitions.get("Inv")); ClausefDetected("Inv","INVARIANTS");
specAnalyser.invariants.add(definitions.get("Inv"));
ClausefDetected("Inv", "INVARIANTS");
} else if (definitions.containsKey("INVARIANTS")) {
specAnalyser.invariants.add(definitions.get("INVARIANTS")); ClausefDetected("INVARIANTS","INVARIANTS");
specAnalyser.invariants.add(definitions.get("INVARIANTS"));
ClausefDetected("INVARIANTS", "INVARIANTS");
} else if (definitions.containsKey("INVARIANT")) {
specAnalyser.invariants.add(definitions.get("INVARIANT")); ClausefDetected("INVARIANT","INVARIANTS");
specAnalyser.invariants.add(definitions.get("INVARIANT"));
ClausefDetected("INVARIANT", "INVARIANTS");
} else if (definitions.containsKey("INV")) {
specAnalyser.invariants.add(definitions.get("INV")); ClausefDetected("INV","INVARIANTS");
specAnalyser.invariants.add(definitions.get("INV"));
ClausefDetected("INV", "INVARIANTS");
} else if (definitions.containsKey("Invariant")) {
specAnalyser.invariants.add(definitions.get("Invariant")); ClausefDetected("Invariant","INVARIANTS");
specAnalyser.invariants.add(definitions.get("Invariant"));
ClausefDetected("Invariant", "INVARIANTS");
} else if (definitions.containsKey("Invariants")) {
specAnalyser.invariants.add(definitions.get("Invariants")); ClausefDetected("Invariants","INVARIANTS");
specAnalyser.invariants.add(definitions.get("Invariants"));
ClausefDetected("Invariants", "INVARIANTS");
} else if (definitions.containsKey("TypeInv")) {
specAnalyser.invariants.add(definitions.get("TypeInv")); ClausefDetected("TypeInv","INVARIANTS");
specAnalyser.invariants.add(definitions.get("TypeInv"));
ClausefDetected("TypeInv", "INVARIANTS");
} else if (definitions.containsKey("TypeOK")) {
specAnalyser.invariants.add(definitions.get("TypeOK")); ClausefDetected("TypeOK","INVARIANTS");
specAnalyser.invariants.add(definitions.get("TypeOK"));
ClausefDetected("TypeOK", "INVARIANTS");
} else if (definitions.containsKey("IndInv")) {
specAnalyser.invariants.add(definitions.get("IndInv")); ClausefDetected("IndInv","INVARIANTS");
specAnalyser.invariants.add(definitions.get("IndInv"));
ClausefDetected("IndInv", "INVARIANTS");
}
// TODO are constant in the right order
......@@ -150,6 +155,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
// TODO: use -verbose OPTION from command line
System.out.println("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause);
}
public static void DebugMsg(String Msg) {
// TODO: use -verbose OPTION from command line
System.out.println(Msg);
......
package de.tla2b.analysis;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Set;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SemanticNode;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Set;
public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
ASTConstants {
private final static Set<String> KEYWORDS = new HashSet<>();
static {
KEYWORDS.add("seq");
KEYWORDS.add("left");
......@@ -76,6 +69,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
}
private final static Hashtable<String, String> INFIX_OPERATOR = new Hashtable<>();
static {
INFIX_OPERATOR.put("!!", "exclamationmark2");
INFIX_OPERATOR.put("??", "questionmark2");
......@@ -98,6 +92,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
}
private final static Hashtable<String, String> BBUILTIN_OPERATOR = new Hashtable<>();
static {
BBUILTIN_OPERATOR.put("+", "plus");
BBUILTIN_OPERATOR.put("-", "minus");
......@@ -270,8 +265,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
FormalParamNode[][] params = opApplNode.getBdedQuantSymbolLists();
Set<String> newUsedNames = new HashSet<>(usedNames);
for (FormalParamNode[] formalParamNodes : params) {
for (int j = 0; j < formalParamNodes.length; j++) {
FormalParamNode param = formalParamNodes[j];
for (FormalParamNode param : formalParamNodes) {
String paramName = param.getName().toString();
String newName = incName(paramName, usedNames);
param.setToolObject(NEW_NAME, newName);
......
package de.tla2b.analysis;
import java.util.Arrays;
import java.util.Comparator;
import java.util.Hashtable;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import java.util.Arrays;
import java.util.Comparator;
import java.util.Hashtable;
public class SymbolSorter {
private final ModuleNode moduleNode;
......
package de.tla2b.analysis;
import java.util.*;
import java.util.Map.Entry;
import de.tla2b.config.ConfigfileEvaluator;
import de.tla2b.config.TLCValueNode;
import de.tla2b.config.ValueObj;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.exceptions.TypeErrorException;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.exceptions.*;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
......@@ -18,6 +11,9 @@ import de.tla2b.types.*;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import java.util.*;
import java.util.Map.Entry;
public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns, TranslationGlobals {
private static final int TEMP_TYPE_ID = 6;
......
package de.tla2b.analysis;
import java.util.HashSet;
import java.util.Set;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.*;
import java.util.HashSet;
import java.util.Set;
public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns {
......
package de.tla2b.config;
import java.util.ArrayList;
import java.util.Enumeration;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.LinkedHashMap;
import java.util.Map;
import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.UnificationException;
import de.tla2b.types.*;
import tla2sany.semantic.InstanceNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.OpDefOrDeclNode;
import tla2sany.semantic.*;
import tlc2.tool.ModelConfig;
import tlc2.util.Vect;
import tlc2.value.IntValue;
......@@ -22,6 +11,8 @@ import tlc2.value.ModelValue;
import tlc2.value.SetEnumValue;
import tlc2.value.Value;
import java.util.*;
/**
* This class evaluates the configfile and collects all necessary information of
* the configfile. All used identifier in the configfile are checked to be valid
......
package de.tla2b.config;
import java.util.Hashtable;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AbortException;
import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDeclNode;
import tla2sany.semantic.OpDefNode;
import tla2sany.semantic.SymbolNode;
import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs;
import java.util.Hashtable;
public class ModuleOverrider extends BuiltInOPs implements ASTConstants {
private final ModuleNode moduleNode;
......
......@@ -6,6 +6,7 @@ import tla2sany.modanalyzer.SpecObj;
public class FrontEndException extends TLA2BException {
public SpecObj spec;
public FrontEndException(String e) {
super(e);
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment