diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java index 648f92ef6eae76b38df5eed0fc080ee3d5852bba..4d43d0adbb519008636bd896c10d8a2e9cb6c3cc 100644 --- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java +++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java @@ -5,7 +5,6 @@ import de.tla2b.exceptions.ConfigFileErrorException; import de.tla2b.exceptions.NotImplementedException; import de.tla2b.exceptions.SemanticErrorException; import de.tla2b.global.BBuiltInOPs; -import de.tla2b.global.TranslationGlobals; import de.tla2b.translation.BDefinitionsFinder; import de.tla2b.translation.OperationsFinder; import de.tla2b.translation.UsedDefinitionsFinder; @@ -13,15 +12,17 @@ import de.tla2b.util.DebugUtils; import de.tla2b.util.TlaUtils; import tla2sany.semantic.*; import tlc2.tool.BuiltInOPs; -import tlc2.tool.ToolGlobals; 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 init; private OpDefNode next; 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 final Map<String, SymbolNode> namingMap = new HashMap<>(); @@ -29,10 +30,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal private final ModuleNode moduleNode; 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 final List<ExprNode> inits = new ArrayList<>(); @@ -40,19 +37,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal // set of OpDefNodes which will appear in the resulting B Machine private Set<OpDefNode> usedDefinitions = new HashSet<>(); // 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 private final List<String> definitionMacros = new ArrayList<>(); private final List<OpDefNode> recursiveFunctions = new ArrayList<>(); - private final List<RecursiveDefinition> recursiveDefinitions = new ArrayList<>(); private ConfigfileEvaluator configFileEvaluator; private SpecAnalyser(ModuleNode m) { this.moduleNode = m; - this.bConstants = new ArrayList<>(); } public static SpecAnalyser createSpecAnalyser(ModuleNode m, ConfigfileEvaluator conEval) { @@ -63,7 +58,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal specAnalyser.invariants = conEval.getInvariants(); specAnalyser.bConstants = conEval.getbConstantList(); specAnalyser.configFileEvaluator = conEval; - return specAnalyser; } @@ -76,93 +70,41 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal } public static SpecAnalyser createSpecAnalyser(ModuleNode m) { + Map<String, OpDefNode> definitions = TlaUtils.getOpDefsMap(m.getOpDefs()); SpecAnalyser specAnalyser = new SpecAnalyser(m); - Map<String, OpDefNode> definitions = new HashMap<>(); - for (int i = 0; i < m.getOpDefs().length; i++) { - definitions.put(m.getOpDefs()[i].getName().toString(), m.getOpDefs()[i]); - } - - if (definitions.containsKey("Spec")) { - specAnalyser.spec = definitions.get("Spec"); - ClausefDetected("Spec", "INITIALISATION+OPERATIONS"); - } else if (definitions.containsKey("SPECIFICATION")) { - specAnalyser.spec = definitions.get("SPECIFICATION"); - ClausefDetected("SPECIFICATION", "INITIALISATION+OPERATIONS"); - } else if (definitions.containsKey("SPEC")) { - 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"); + specAnalyser.spec = detectClause(Stream.of("Spec", "SPECIFICATION", "SPEC"), + definitions, "INITIALISATION+OPERATIONS"); + specAnalyser.init = detectClause(Stream.of("Init", "INIT", "Initialisation", "INITIALISATION"), + definitions, "INITIALISATION"); + specAnalyser.next = detectClause(Stream.of("Next", "NEXT"), definitions, "OPERATIONS"); + OpDefNode invariant = detectClause(Stream.of("Inv", "INVARIANTS", "INVARIANT", "INV", "Invariant", + "Invariants", "TypeInv", "TypeOK", "IndInv"), + definitions, "INVARIANTS"); + + if (invariant != null) { + specAnalyser.invariants.add(invariant); } 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())); - return specAnalyser; } - public static void ClausefDetected(String Name, String Clause) { - DebugUtils.printMsg("Detected TLA+ Default Definition " + Name + " for Clause: " + Clause); + private static OpDefNode detectClause(Stream<String> keywords, Map<String, OpDefNode> definitions, String bClause) { + 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 { - if (spec != null) { - evalSpec(); - } else { - evalInit(); - evalNext(); - } + evalSpec(); for (OpDefNode inv : new ArrayList<>(invariants)) { try { @@ -212,26 +154,20 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal namingMap.putAll(TlaUtils.getOpDefsMap(usedDefinitions.toArray(new OpDefNode[0]))); } - private void evalInit() { - if (init != null) { - DebugUtils.printMsg("Using TLA+ Init definition to determine B INITIALISATION"); - inits.add(init.getBody()); - } - } - - private void evalNext() { - if (next != null) { - DebugUtils.printMsg("Using TLA+ Next definition to determine B OPERATIONS"); - this.nextExpr = next.getBody(); - } - } - - public void evalSpec() throws SemanticErrorException { + 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) { + DebugUtils.printMsg("Using TLA+ Init definition to determine B INITIALISATION"); + inits.add(init.getBody()); + } + if (next != null) { + DebugUtils.printMsg("Using TLA+ Next definition to determine B OPERATIONS"); + nextExpr = next.getBody(); + } } - } private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException { @@ -280,7 +216,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal } else { throw new SemanticErrorException("Can not handle specification conjunction."); } - } private void findRecursiveConstructs() throws NotImplementedException { @@ -318,8 +253,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal return bDefinitionsSet; } - public Hashtable<OpDefNode, FormalParamNode[]> getLetParams() { - return new Hashtable<>(letParams); + public Map<OpDefNode, FormalParamNode[]> getLetParams() { + return new HashMap<>(letParams); } public List<String> getDefinitionMacros() {