Skip to content
Snippets Groups Projects
Commit dc122b68 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add debugging feedback 


Signed-off-by: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent 24a15cb6
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/main/java/de/tla2b/analysis/SpecAnalyser.java
+ 38
− 17
View file @ dc122b68
......@@ -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
......@@ -142,6 +146,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();
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment