diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java index b80100df54fb6b0e31bdbd3341485afe07eb0335..e9d31d10b58a4177f2c465b84d10a3fa08a113a0 100644 --- a/src/main/java/de/tlc4b/analysis/MachineContext.java +++ b/src/main/java/de/tlc4b/analysis/MachineContext.java @@ -15,6 +15,7 @@ import de.tlc4b.ltl.LTLBPredicate; import de.tlc4b.ltl.LTLFormulaVisitor; import static de.tlc4b.util.UtilMethods.getIdentifierExpression; +import static de.tlc4b.util.UtilMethods.getOperation; public class MachineContext extends DepthFirstAdapter { @@ -554,7 +555,7 @@ public class MachineContext extends DepthFirstAdapter { List<POperation> copy = new ArrayList<>(node.getOperations()); // first collect all operations for (POperation e : copy) { - AOperation op = (AOperation) e; + AOperation op = getOperation(e); String name = Utils.getTIdentifierListAsString(op.getOpName()); // existString(name); if (operations.containsKey(name)) { diff --git a/src/main/java/de/tlc4b/util/UtilMethods.java b/src/main/java/de/tlc4b/util/UtilMethods.java index fedd59716bea35c1dd8f89ac9db588a69b7bde71..2e824b3dfc82c032a7c063d09142440a9e3d82c2 100644 --- a/src/main/java/de/tlc4b/util/UtilMethods.java +++ b/src/main/java/de/tlc4b/util/UtilMethods.java @@ -17,12 +17,7 @@ public class UtilMethods { public static AIdentifierExpression getIdentifierExpression(PExpression e) { AIdentifierExpression identifier; if (e instanceof ADescriptionExpression) { - PExpression desc = ((ADescriptionExpression) e).getExpression(); - if (desc instanceof AIdentifierExpression) { - identifier = (AIdentifierExpression) desc; - } else { - throw new IllegalStateException("Unexpected expression type: " + e); - } + identifier = getIdentifierExpression(((ADescriptionExpression) e).getExpression()); } else if (e instanceof AIdentifierExpression) { identifier = (AIdentifierExpression) e; } else { @@ -31,6 +26,18 @@ public class UtilMethods { return identifier; } + public static AOperation getOperation(POperation e) { + AOperation op; + if (e instanceof ADescriptionOperation) { + op = getOperation(((ADescriptionOperation) e).getOperation()); + } else if (e instanceof AOperation) { + op = (AOperation) e; + } else { + throw new IllegalStateException("Unexpected operation type: " + e); + } + return op; + } + public static String getPositionAsString(Node node) { StringBuilder sb = new StringBuilder(); SourcePosition startPos = node.getStartPos(); diff --git a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java index ceafde9351a7f4a24630ca1797772793a840af86..1741ed12ab89d41915f1e5f45f3c31da107b9f36 100644 --- a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java +++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java @@ -405,5 +405,26 @@ public class OperationsTest { + "===="; compare(expected, machine); } + + @Test + public void testOperationWithDescPragma() throws Exception { + String machine = "MACHINE test\n" + + "VARIABLES x\n" + + "INVARIANT x = 1\n" + + "INITIALISATION x := 1\n" + + "OPERATIONS\n" + + "inc = x := x + 1 /*@desc increment x*/\n" + + "END"; + + String expected = "---- MODULE test ----\n" + + "EXTENDS Naturals\n" + + "VARIABLES x \n" + + "Invariant1 == x = 1\n" + + "Init == x = 1 \n" + + "inc == x' = x + 1\n" + + "Next == \\/ inc \n" + + "===="; + compare(expected, machine); + } }