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

allow to use FALSE and TRUE for TLA actions

parent cf9e459c
No related branches found
No related tags found
No related merge requests found
package de.tla2b.translation; package de.tla2b.translation;
import java.util.ArrayList; import java.util.ArrayList;
import util.UniqueString;
import tla2sany.semantic.ASTConstants; import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.ExprNode; import tla2sany.semantic.ExprNode;
...@@ -14,6 +15,7 @@ import de.tla2b.analysis.AbstractASTVisitor; ...@@ -14,6 +15,7 @@ import de.tla2b.analysis.AbstractASTVisitor;
import de.tla2b.analysis.BOperation; import de.tla2b.analysis.BOperation;
import de.tla2b.analysis.SpecAnalyser; import de.tla2b.analysis.SpecAnalyser;
import de.tla2b.global.BBuiltInOPs; import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.BBuildIns;
import de.tla2b.global.TranslationGlobals; import de.tla2b.global.TranslationGlobals;
public class OperationsFinder extends AbstractASTVisitor implements public class OperationsFinder extends AbstractASTVisitor implements
...@@ -47,11 +49,11 @@ public class OperationsFinder extends AbstractASTVisitor implements ...@@ -47,11 +49,11 @@ public class OperationsFinder extends AbstractASTVisitor implements
} }
case NumeralKind: { case NumeralKind: {
throw new RuntimeException(String.format( throw new RuntimeException(String.format(
"Expected an action.%n%s", n.getLocation().toString())); "Expected an action (instead of a number).%n%s", n.getLocation().toString()));
} }
case StringKind: { case StringKind: {
throw new RuntimeException(String.format( throw new RuntimeException(String.format(
"Expected an action.%n%s", n.getLocation().toString())); "Expected an action (instead of a string).%n%s", n.getLocation().toString()));
} }
case SubstInKind: { case SubstInKind: {
throw new RuntimeException(String.format( throw new RuntimeException(String.format(
...@@ -88,9 +90,10 @@ public class OperationsFinder extends AbstractASTVisitor implements ...@@ -88,9 +90,10 @@ public class OperationsFinder extends AbstractASTVisitor implements
@Override @Override
public void visitBuiltInNode(OpApplNode n) { public void visitBuiltInNode(OpApplNode n) {
int opcode = BuiltInOPs.getOpCode(n.getOperator().getName()); UniqueString opname = n.getOperator().getName();
int opcode = BuiltInOPs.getOpCode(opname);
switch (opcode) { switch (opcode) {
case OPCODE_dl: // DisjList 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]);
...@@ -108,7 +111,7 @@ public class OperationsFinder extends AbstractASTVisitor implements ...@@ -108,7 +111,7 @@ public class OperationsFinder extends AbstractASTVisitor implements
return; return;
} }
} }
case OPCODE_lor: { case OPCODE_lor: { // logical or: split action further
String oldName = currentName; String oldName = currentName;
ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(exists); ArrayList<OpApplNode> oldExists = new ArrayList<OpApplNode>(exists);
...@@ -141,11 +144,20 @@ public class OperationsFinder extends AbstractASTVisitor implements ...@@ -141,11 +144,20 @@ public class OperationsFinder extends AbstractASTVisitor implements
case OPCODE_fa: // $FcnApply f[1] case OPCODE_fa: // $FcnApply f[1]
case OPCODE_ite: // IF THEN ELSE case OPCODE_ite: // IF THEN ELSE
case OPCODE_case: { case OPCODE_case: {
// no further decomposing: create a B operation
BOperation op = new BOperation(currentName, n, exists, specAnalyser); BOperation op = new BOperation(currentName, n, exists, specAnalyser);
bOperations.add(op); bOperations.add(op);
return; return;
} }
}
//System.out.println("OPCODE of " + opname + " = "+ opcode);
if (opname == BBuildIns.OP_false || // FALSE: always disabled
opname == BBuildIns.OP_true) { // TRUE: CHAOS
BOperation op = new BOperation(currentName, n, exists, specAnalyser);
bOperations.add(op);
return;
} }
throw new RuntimeException(String.format( throw new RuntimeException(String.format(
"Expected an action at '%s' :%n%s", n.getOperator().getName() "Expected an action at '%s' :%n%s", n.getOperator().getName()
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment