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

support description pragma for operations

parent 9c8f234e
No related branches found
No related tags found
No related merge requests found
Pipeline #139998 passed
......@@ -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)) {
......
......@@ -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();
......
......@@ -406,4 +406,25 @@ 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);
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment