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

minor cleanup in OperationsFinder

parent 8b165835
No related branches found
No related tags found
No related merge requests found
Pipeline #148575 passed
...@@ -5,11 +5,13 @@ import de.tla2b.analysis.BOperation; ...@@ -5,11 +5,13 @@ import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser; import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuildIns; import de.tla2b.global.BBuildIns;
import de.tla2b.global.BBuiltInOPs; import de.tla2b.global.BBuiltInOPs;
import de.tla2b.util.DebugUtils;
import tla2sany.semantic.*; import tla2sany.semantic.*;
import tlc2.tool.BuiltInOPs; import tlc2.tool.BuiltInOPs;
import util.UniqueString; import util.UniqueString;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.List;
import static de.tla2b.global.TranslationGlobals.SUBSTITUTE_PARAM; import static de.tla2b.global.TranslationGlobals.SUBSTITUTE_PARAM;
...@@ -17,9 +19,9 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -17,9 +19,9 @@ public class OperationsFinder extends AbstractASTVisitor {
private final SpecAnalyser specAnalyser; private final SpecAnalyser specAnalyser;
private String currentName; private String currentName;
private ArrayList<OpApplNode> exists; private List<OpApplNode> exists;
// a list containing all existential quantifier which will be parameters in the resulting B Machine // a list containing all existential quantifier which will be parameters in the resulting B Machine
private final ArrayList<BOperation> bOperations; private final List<BOperation> bOperations;
public OperationsFinder(SpecAnalyser specAnalyser) { public OperationsFinder(SpecAnalyser specAnalyser) {
this.specAnalyser = specAnalyser; this.specAnalyser = specAnalyser;
...@@ -31,7 +33,6 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -31,7 +33,6 @@ public class OperationsFinder extends AbstractASTVisitor {
} }
} }
public void visitExprNode(ExprNode n) { public void visitExprNode(ExprNode n) {
switch (n.getKind()) { switch (n.getKind()) {
case OpApplKind: { case OpApplKind: {
...@@ -39,28 +40,17 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -39,28 +40,17 @@ public class OperationsFinder extends AbstractASTVisitor {
return; return;
} }
case NumeralKind: case NumeralKind:
case DecimalKind: { case DecimalKind:
throw new RuntimeException(String.format( throw new RuntimeException(String.format("Expected an action (instead of a number).%n%s", n.getLocation().toString()));
"Expected an action (instead of a number).%n%s", n.getLocation().toString())); case StringKind:
} throw new RuntimeException(String.format("Expected an action (instead of a string).%n%s", n.getLocation().toString()));
case StringKind: { case SubstInKind:
throw new RuntimeException(String.format( case AtNodeKind: // @
"Expected an action (instead of a string).%n%s", n.getLocation().toString())); throw new RuntimeException(String.format("Expected an action.%n%s", n.getLocation().toString()));
} case LetInKind: // we do not visit the local definitions
case SubstInKind: {
throw new RuntimeException(String.format(
"Expected an action.%n%s", n.getLocation().toString()));
}
case AtNodeKind: { // @
throw new RuntimeException(String.format(
"Expected an action.%n%s", n.getLocation().toString()));
}
case LetInKind: {
// we do not visit the local definitions
visitExprNode(((LetInNode) n).getBody()); visitExprNode(((LetInNode) n).getBody());
} }
} }
}
public void visitUserDefinedNode(OpApplNode n) { public void visitUserDefinedNode(OpApplNode n) {
OpDefNode def = (OpDefNode) n.getOperator(); OpDefNode def = (OpDefNode) n.getOperator();
...@@ -70,9 +60,9 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -70,9 +60,9 @@ public class OperationsFinder extends AbstractASTVisitor {
} }
for (int i = 0; i < def.getParams().length; i++) { for (int i = 0; i < def.getParams().length; i++) {
FormalParamNode param = def.getParams()[i]; def.getParams()[i].setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
param.setToolObject(SUBSTITUTE_PARAM, n.getArgs()[i]);
} }
// TODO: remember params to omit unneeded in B operation
currentName = def.getName().toString(); currentName = def.getName().toString();
visitExprNode(def.getBody()); visitExprNode(def.getBody());
} }
...@@ -81,14 +71,14 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -81,14 +71,14 @@ public class OperationsFinder extends AbstractASTVisitor {
public void visitBuiltInNode(OpApplNode n) { public void visitBuiltInNode(OpApplNode n) {
UniqueString opname = n.getOperator().getName(); UniqueString opname = n.getOperator().getName();
int opcode = BuiltInOPs.getOpCode(opname); int opcode = BuiltInOPs.getOpCode(opname);
DebugUtils.printDebugMsg("OPCODE of " + opname + " = "+ opcode);
switch (opcode) { switch (opcode) {
case OPCODE_dl: // DisjList: split action further case OPCODE_dl: { // DisjList: split action further
{
if (n.getArgs().length == 1) { if (n.getArgs().length == 1) {
visitExprOrOpArgNode(n.getArgs()[0]); visitExprOrOpArgNode(n.getArgs()[0]);
} else { } else {
String oldName = currentName; String oldName = currentName;
ArrayList<OpApplNode> oldExists = new ArrayList<>(exists); List<OpApplNode> oldExists = new ArrayList<>(exists);
for (int i = 0; i < n.getArgs().length; i++) { for (int i = 0; i < n.getArgs().length; i++) {
exists = new ArrayList<>(oldExists); exists = new ArrayList<>(oldExists);
...@@ -100,7 +90,7 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -100,7 +90,7 @@ public class OperationsFinder extends AbstractASTVisitor {
} }
case OPCODE_lor: { // logical or: split action further case OPCODE_lor: { // logical or: split action further
String oldName = currentName; String oldName = currentName;
ArrayList<OpApplNode> oldExists = new ArrayList<>(exists); List<OpApplNode> oldExists = new ArrayList<>(exists);
for (int i = 0; i < n.getArgs().length; i++) { for (int i = 0; i < n.getArgs().length; i++) {
exists = new ArrayList<>(oldExists); exists = new ArrayList<>(oldExists);
...@@ -115,7 +105,8 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -115,7 +105,8 @@ public class OperationsFinder extends AbstractASTVisitor {
return; return;
} }
case OPCODE_unchanged: // all other action predicates:
case OPCODE_unchanged: // UNCHANGED
case OPCODE_eq: // = case OPCODE_eq: // =
case OPCODE_noteq: // /=, # case OPCODE_noteq: // /=, #
case OPCODE_neg: // Negation case OPCODE_neg: // Negation
...@@ -135,20 +126,18 @@ public class OperationsFinder extends AbstractASTVisitor { ...@@ -135,20 +126,18 @@ public class OperationsFinder extends AbstractASTVisitor {
bOperations.add(new BOperation(currentName, n, exists, specAnalyser)); bOperations.add(new BOperation(currentName, n, exists, specAnalyser));
return; return;
} }
} }
//System.out.println("OPCODE of " + opname + " = "+ opcode); //System.out.println("OPCODE of " + opname + " = "+ opcode);
if (opname == BBuildIns.OP_false || // FALSE: always disabled if (opname == BBuildIns.OP_false || opname == BBuildIns.OP_true) {
opname == BBuildIns.OP_true) { // TRUE: CHAOS // FALSE: always disabled; TRUE: CHAOS
bOperations.add(new BOperation(currentName, n, exists, specAnalyser)); bOperations.add(new BOperation(currentName, n, exists, specAnalyser));
return; return;
} }
throw new RuntimeException(String.format( throw new RuntimeException(String.format("Expected an action at '%s':%n%s", opname, n.getLocation()));
"Expected an action at '%s' :%n%s", n.getOperator().getName(), n.getLocation().toString()));
} }
public ArrayList<BOperation> getBOperations() { public List<BOperation> getBOperations() {
return bOperations; return bOperations;
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment