From dc122b6877ca6affd779e0c7ceb8af081f6e4979 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 3 Feb 2022 14:39:26 +0100
Subject: [PATCH] add debugging feedback
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../java/de/tla2b/analysis/SpecAnalyser.java | 55 +++++++++++++------
1 file changed, 38 insertions(+), 17 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 027d745..cd3b7a1 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -97,43 +97,47 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
}
if (definitions.containsKey("Spec")) {
- specAnalyser.spec = definitions.get("Spec");
+ specAnalyser.spec = definitions.get("Spec"); ClausefDetected("Spec","INITIALISATION+OPERATIONS");
} else if (definitions.containsKey("SPECIFICATION")) {
- specAnalyser.spec = definitions.get("SPECIFICATION");
+ specAnalyser.spec = definitions.get("SPECIFICATION"); ClausefDetected("SPECIFICATION","INITIALISATION+OPERATIONS");
} else if (definitions.containsKey("SPEC")) {
- specAnalyser.spec = definitions.get("SPEC");
+ specAnalyser.spec = definitions.get("SPEC"); ClausefDetected("SPEC","INITIALISATION+OPERATIONS");
}
if (definitions.containsKey("Init")) {
- specAnalyser.init = definitions.get("Init");
+ specAnalyser.init = definitions.get("Init"); ClausefDetected("Init","INITIALISATION");
} else if (definitions.containsKey("INIT")) {
- specAnalyser.init = definitions.get("INIT");
+ specAnalyser.init = definitions.get("INIT"); ClausefDetected("INIT","INITIALISATION");
} else if (definitions.containsKey("Initialisation")) {
- specAnalyser.init = definitions.get("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");
+ specAnalyser.next = definitions.get("Next"); ClausefDetected("Next","OPERATIONS");
} else if (definitions.containsKey("NEXT")) {
- specAnalyser.next = definitions.get("NEXT");
+ specAnalyser.next = definitions.get("NEXT"); ClausefDetected("NEXT","OPERATIONS");
}
if (definitions.containsKey("Inv")) {
- specAnalyser.invariants.add(definitions.get("Inv"));
+ specAnalyser.invariants.add(definitions.get("Inv")); ClausefDetected("Inv","INVARIANTS");
} else if (definitions.containsKey("INVARIANTS")) {
- specAnalyser.invariants.add(definitions.get("INVARIANTS"));
+ specAnalyser.invariants.add(definitions.get("INVARIANTS")); ClausefDetected("INVARIANTS","INVARIANTS");
} else if (definitions.containsKey("INVARIANT")) {
- specAnalyser.invariants.add(definitions.get("INVARIANT"));
+ specAnalyser.invariants.add(definitions.get("INVARIANT")); ClausefDetected("INVARIANT","INVARIANTS");
} else if (definitions.containsKey("INV")) {
- specAnalyser.invariants.add(definitions.get("INV"));
+ specAnalyser.invariants.add(definitions.get("INV")); ClausefDetected("INV","INVARIANTS");
} else if (definitions.containsKey("Invariant")) {
- specAnalyser.invariants.add(definitions.get("Invariant"));
+ specAnalyser.invariants.add(definitions.get("Invariant")); ClausefDetected("Invariant","INVARIANTS");
} else if (definitions.containsKey("Invariants")) {
- specAnalyser.invariants.add(definitions.get("Invariants"));
+ specAnalyser.invariants.add(definitions.get("Invariants")); ClausefDetected("Invariants","INVARIANTS");
} else if (definitions.containsKey("TypeInv")) {
- specAnalyser.invariants.add(definitions.get("TypeInv"));
+ specAnalyser.invariants.add(definitions.get("TypeInv")); ClausefDetected("TypeInv","INVARIANTS");
} else if (definitions.containsKey("TypeOK")) {
- specAnalyser.invariants.add(definitions.get("TypeOK"));
+ specAnalyser.invariants.add(definitions.get("TypeOK")); ClausefDetected("TypeOK","INVARIANTS");
+ }else if (definitions.containsKey("IndInv")) {
+ specAnalyser.invariants.add(definitions.get("IndInv")); ClausefDetected("IndInv","INVARIANTS");
}
// TODO are constant in the right order
@@ -141,6 +145,15 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
return specAnalyser;
}
+
+ public static void ClausefDetected(String Name, String Clause) {
+ // 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);
+ }
public void start()
throws SemanticErrorException, FrontEndException, ConfigFileErrorException, NotImplementedException {
@@ -161,14 +174,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
if (opDefNode.getKind() == UserDefinedOpKind && !BBuiltInOPs.contains(opDefNode.getName())) {
int i = invariants.indexOf(inv);
invariants.set(i, opDefNode);
+ DebugMsg("Adding invariant "+i);
}
} catch (ClassCastException e) {
}
}
+ DebugMsg("Detecting OPERATIONS from disjunctions");
OperationsFinder operationsFinder = new OperationsFinder(this);
bOperations = operationsFinder.getBOperations();
+ DebugMsg("Finding used definitions");
UsedDefinitionsFinder definitionFinder = new UsedDefinitionsFinder(this);
this.usedDefinitions = definitionFinder.getUsedDefinitions();
@@ -176,6 +192,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
this.bDefinitionsSet = bDefinitionFinder.getBDefinitionsSet();
// usedDefinitions.addAll(bDefinitionsSet);
+ DebugMsg("Computing variable declarations");
// test whether there is a init predicate if there is a variable
if (moduleNode.getVariableDecls().length > 0 && inits == null) {
throw new SemanticErrorException("No initial predicate is defined.");
@@ -194,9 +211,11 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
for (OpDeclNode var : moduleNode.getVariableDecls()) {
namingHashTable.put(var.getName().toString(), var);
}
+ DebugMsg("Number of variables detected: " + moduleNode.getVariableDecls().length);
for (OpDeclNode con : moduleNode.getConstantDecls()) {
namingHashTable.put(con.getName().toString(), con);
}
+ DebugMsg("Number of constants detected: " + moduleNode.getConstantDecls().length);
for (OpDefNode def : usedDefinitions) {
namingHashTable.put(def.getName().toString(), def);
}
@@ -205,25 +224,27 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants, ToolGlobal
private void evalInit() {
if (init != null) {
+ System.out.println("Using TLA+ Init definition to determine B INITIALISATION");
inits.add(init.getBody());
}
}
private void evalNext() throws FrontEndException {
if (next != null) {
+ System.out.println("Using TLA+ Next definition to determine B OPERATIONS");
this.nextExpr = next.getBody();
}
}
public void evalSpec() throws SemanticErrorException, FrontEndException {
if (spec != null) {
+ System.out.println("Using TLA+ Spec to determine B INITIALISATION and OPERATIONS");
processConfigSpec(spec.getBody());
}
}
private void processConfigSpec(ExprNode exprNode) throws SemanticErrorException, FrontEndException {
-
if (exprNode instanceof OpApplNode) {
OpApplNode opApp = (OpApplNode) exprNode;
ExprOrOpArgNode[] args = opApp.getArgs();
--
GitLab