From 46ed6d32fc478b071d2386b989eb18fbf92f85b4 Mon Sep 17 00:00:00 2001 From: Jan Gruteser <jan.gruteser@hhu.de> Date: Sat, 27 Jul 2024 09:11:16 +0200 Subject: [PATCH] support description pragma for operations --- .../de/tlc4b/analysis/MachineContext.java | 3 ++- src/main/java/de/tlc4b/util/UtilMethods.java | 19 +++++++++++------ .../de/tlc4b/prettyprint/OperationsTest.java | 21 +++++++++++++++++++ 3 files changed, 36 insertions(+), 7 deletions(-) diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java index b80100d..e9d31d1 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 fedd597..2e824b3 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 ceafde9..1741ed1 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); + } } -- GitLab