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

refactor SpecAnalyser

parent c40678aa
No related branches found
No related tags found
No related merge requests found
Pipeline #148474 passed
Stage: test
Stage: deploy
Show whitespace changes
Inline Side-by-side
src/main/java/de/tla2b/analysis/SpecAnalyser.java
+ 40
− 105
View file @ 7b6fb1ef
...@@ -5,7 +5,6 @@ import de.tla2b.exceptions.ConfigFileErrorException; ...@@ -5,7 +5,6 @@ import de.tla2b.exceptions.ConfigFileErrorException;
import de.tla2b.exceptions.NotImplementedException; import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.SemanticErrorException; import de.tla2b.exceptions.SemanticErrorException;
import de.tla2b.global.BBuiltInOPs; import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.BDefinitionsFinder; import de.tla2b.translation.BDefinitionsFinder;
import de.tla2b.translation.OperationsFinder; import de.tla2b.translation.OperationsFinder;
import de.tla2b.translation.UsedDefinitionsFinder; import de.tla2b.translation.UsedDefinitionsFinder;
...@@ -13,15 +12,17 @@ import de.tla2b.util.DebugUtils; ...@@ -13,15 +12,17 @@ import de.tla2b.util.DebugUtils;
import de.tla2b.util.TlaUtils; import de.tla2b.util.TlaUtils;
import tla2sany.semantic.*; import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs; import tlc2.tool.BuiltInOPs;
import tlc2.tool.ToolGlobals;
import java.util.*; import java.util.*;
import java.util.stream.Stream;
public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobals, TranslationGlobals { public class SpecAnalyser extends BuiltInOPs {
private OpDefNode spec; private OpDefNode spec;
private OpDefNode init; private OpDefNode init;
private OpDefNode next; private OpDefNode next;
private List<OpDefNode> invariants = new ArrayList<>(); private List<OpDefNode> invariants = new ArrayList<>();
private List<OpDeclNode> bConstants = new ArrayList<>();
// used to check if a b constant has arguments and is not overridden in the configfile
private OpDefNode expressionOpdefNode; private OpDefNode expressionOpdefNode;
private final Map<String, SymbolNode> namingMap = new HashMap<>(); private final Map<String, SymbolNode> namingMap = new HashMap<>();
...@@ -29,10 +30,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -29,10 +30,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
private final ModuleNode moduleNode; private final ModuleNode moduleNode;
private ExprNode nextExpr; private ExprNode nextExpr;
private List<OpDeclNode> bConstants;
// used to check if a b constant has arguments and is not overridden in the
// configfile
private List<BOperation> bOperations = new ArrayList<>(); private List<BOperation> bOperations = new ArrayList<>();
private final List<ExprNode> inits = new ArrayList<>(); private final List<ExprNode> inits = new ArrayList<>();
...@@ -40,19 +37,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -40,19 +37,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
// set of OpDefNodes which will appear in the resulting B Machine // set of OpDefNodes which will appear in the resulting B Machine
private Set<OpDefNode> usedDefinitions = new HashSet<>(); private Set<OpDefNode> usedDefinitions = new HashSet<>();
// definitions which are used for the type inference algorithm // definitions which are used for the type inference algorithm
private final Hashtable<OpDefNode, FormalParamNode[]> letParams = new Hashtable<>(); private final Map<OpDefNode, FormalParamNode[]> letParams = new HashMap<>();
// additional parameters of a let Operator, these parameters are from the surrounding operator // additional parameters of a let Operator, these parameters are from the surrounding operator
private final List<String> definitionMacros = new ArrayList<>(); private final List<String> definitionMacros = new ArrayList<>();
private final List<OpDefNode> recursiveFunctions = new ArrayList<>(); private final List<OpDefNode> recursiveFunctions = new ArrayList<>();
private final List<RecursiveDefinition> recursiveDefinitions = new ArrayList<>(); private final List<RecursiveDefinition> recursiveDefinitions = new ArrayList<>();
private ConfigfileEvaluator configFileEvaluator; private ConfigfileEvaluator configFileEvaluator;
private SpecAnalyser(ModuleNode m) { private SpecAnalyser(ModuleNode m) {
this.moduleNode = m; this.moduleNode = m;
this.bConstants = new ArrayList<>();
} }
public static SpecAnalyser createSpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) { public static SpecAnalyser createSpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) {
...@@ -63,7 +58,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -63,7 +58,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
specAnalyser.invariants = conEval.getInvariants(); specAnalyser.invariants = conEval.getInvariants();
specAnalyser.bConstants = conEval.getbConstantList(); specAnalyser.bConstants = conEval.getbConstantList();
specAnalyser.configFileEvaluator = conEval; specAnalyser.configFileEvaluator = conEval;
return specAnalyser; return specAnalyser;
} }
...@@ -76,93 +70,41 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -76,93 +70,41 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
} }
public static SpecAnalyser createSpecAnalyser(ModuleNode m) { public static SpecAnalyser createSpecAnalyser(ModuleNode m) {
Map<String, OpDefNode> definitions = TlaUtils.getOpDefsMap(m.getOpDefs());
SpecAnalyser specAnalyser = new SpecAnalyser(m); SpecAnalyser specAnalyser = new SpecAnalyser(m);
Map<String, OpDefNode> definitions = new HashMap<>();
for (int i = 0; i < m.getOpDefs().length; i++) { specAnalyser.spec = detectClause(Stream.of("Spec", "SPECIFICATION", "SPEC"),
definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]); definitions, "INITIALISATION+OPERATIONS");
} specAnalyser.init = detectClause(Stream.of("Init", "INIT", "Initialisation", "INITIALISATION"),
definitions, "INITIALISATION");
if (definitions.containsKey("Spec")) { specAnalyser.next = detectClause(Stream.of("Next", "NEXT"), definitions, "OPERATIONS");
specAnalyser.spec = definitions.get("Spec"); OpDefNode invariant = detectClause(Stream.of("Inv", "INVARIANTS", "INVARIANT", "INV", "Invariant",
ClausefDetected("Spec", "INITIALISATION+OPERATIONS"); "Invariants", "TypeInv", "TypeOK", "IndInv"),
} else if (definitions.containsKey("SPECIFICATION")) { definitions, "INVARIANTS");
specAnalyser.spec = definitions.get("SPECIFICATION");
ClausefDetected("SPECIFICATION", "INITIALISATION+OPERATIONS"); if (invariant != null) {
} else if (definitions.containsKey("SPEC")) { specAnalyser.invariants.add(invariant);
specAnalyser.spec = definitions.get("SPEC");
ClausefDetected("SPEC", "INITIALISATION+OPERATIONS");
}
if (definitions.containsKey("Init")) {
specAnalyser.init = definitions.get("Init");
ClausefDetected("Init", "INITIALISATION");
} else if (definitions.containsKey("INIT")) {
specAnalyser.init = definitions.get("INIT");
ClausefDetected("INIT", "INITIALISATION");
} else if (definitions.containsKey("Initialisation")) {
specAnalyser.init = definitions.get("Initialisation");
ClausefDetected("Initialisation", "INITIALISATION");
} else if (definitions.containsKey("INITIALISATION")) {
specAnalyser.init = definitions.get("INITIALISATION");
ClausefDetected("INITIALISATION", "INITIALISATION");
}
if (definitions.containsKey("Next")) {
specAnalyser.next = definitions.get("Next");
ClausefDetected("Next", "OPERATIONS");
} else if (definitions.containsKey("NEXT")) {
specAnalyser.next = definitions.get("NEXT");
ClausefDetected("NEXT", "OPERATIONS");
}
if (definitions.containsKey("Inv")) {
specAnalyser.invariants.add(definitions.get("Inv"));
ClausefDetected("Inv", "INVARIANTS");
} else if (definitions.containsKey("INVARIANTS")) {
specAnalyser.invariants.add(definitions.get("INVARIANTS"));
ClausefDetected("INVARIANTS", "INVARIANTS");
} else if (definitions.containsKey("INVARIANT")) {
specAnalyser.invariants.add(definitions.get("INVARIANT"));
ClausefDetected("INVARIANT", "INVARIANTS");
} else if (definitions.containsKey("INV")) {
specAnalyser.invariants.add(definitions.get("INV"));
ClausefDetected("INV", "INVARIANTS");
} else if (definitions.containsKey("Invariant")) {
specAnalyser.invariants.add(definitions.get("Invariant"));
ClausefDetected("Invariant", "INVARIANTS");
} else if (definitions.containsKey("Invariants")) {
specAnalyser.invariants.add(definitions.get("Invariants"));
ClausefDetected("Invariants", "INVARIANTS");
} else if (definitions.containsKey("TypeInv")) {
specAnalyser.invariants.add(definitions.get("TypeInv"));
ClausefDetected("TypeInv", "INVARIANTS");
} else if (definitions.containsKey("TypeOK")) {
specAnalyser.invariants.add(definitions.get("TypeOK"));
ClausefDetected("TypeOK", "INVARIANTS");
} else if (definitions.containsKey("IndInv")) {
specAnalyser.invariants.add(definitions.get("IndInv"));
ClausefDetected("IndInv", "INVARIANTS");
} else { } else {
System.out.println("No default Invariant detected"); DebugUtils.printMsg("No default Invariant detected");
} }
// TODO are constant in the right order
// TODO are constant in the right order
specAnalyser.bConstants.addAll(Arrays.asList(m.getConstantDecls())); specAnalyser.bConstants.addAll(Arrays.asList(m.getConstantDecls()));
return specAnalyser; return specAnalyser;
} }
public static void ClausefDetected(String Name, String Clause) { private static OpDefNode detectClause(Stream<String> keywords, Map<String, OpDefNode> definitions, String bClause) {
DebugUtils.printMsg("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause); return keywords.filter(definitions::containsKey)
.findFirst()
.map(keyword -> {
DebugUtils.printMsg("Detected TLA+ Default Definition " + keyword + " for Clause: " + bClause);
return definitions.get(keyword);
})
.orElse(null);
} }
public void start() throws SemanticErrorException, ConfigFileErrorException, NotImplementedException { public void start() throws SemanticErrorException, ConfigFileErrorException, NotImplementedException {
if (spec != null) {
evalSpec(); evalSpec();
} else {
evalInit();
evalNext();
}
for (OpDefNode inv : new ArrayList<>(invariants)) { for (OpDefNode inv : new ArrayList<>(invariants)) {
try { try {
...@@ -212,26 +154,20 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -212,26 +154,20 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
namingMap.putAll(TlaUtils.getOpDefsMap(usedDefinitions.toArray(new OpDefNode[0]))); namingMap.putAll(TlaUtils.getOpDefsMap(usedDefinitions.toArray(new OpDefNode[0])));
} }
private void evalInit() { private void evalSpec() throws SemanticErrorException {
if (spec != null) {
DebugUtils.printMsg("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS");
processConfigSpec(spec.getBody());
} else {
if (init != null) { if (init != null) {
DebugUtils.printMsg("Using TLA+ Init definition to determine B INITIALISATION"); DebugUtils.printMsg("Using TLA+ Init definition to determine B INITIALISATION");
inits.add(init.getBody()); inits.add(init.getBody());
} }
}
private void evalNext() {
if (next != null) { if (next != null) {
DebugUtils.printMsg("Using TLA+ Next definition to determine B OPERATIONS"); DebugUtils.printMsg("Using TLA+ Next definition to determine B OPERATIONS");
this.nextExpr = next.getBody(); nextExpr = next.getBody();
} }
} }
public void evalSpec() throws SemanticErrorException {
if (spec != null) {
DebugUtils.printMsg("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS");
processConfigSpec(spec.getBody());
}
} }
private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException { private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException {
...@@ -280,7 +216,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -280,7 +216,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
} else { } else {
throw new SemanticErrorException("Can not handle specification conjunction."); throw new SemanticErrorException("Can not handle specification conjunction.");
} }
} }
private void findRecursiveConstructs() throws NotImplementedException { private void findRecursiveConstructs() throws NotImplementedException {
...@@ -318,8 +253,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal ...@@ -318,8 +253,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
return bDefinitionsSet; return bDefinitionsSet;
} }
public Hashtable<OpDefNode, FormalParamNode[]> getLetParams() { public Map<OpDefNode, FormalParamNode[]> getLetParams() {
return new Hashtable<>(letParams); return new HashMap<>(letParams);
} }
public List<String> getDefinitionMacros() { public List<String> getDefinitionMacros() {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment