From c0600330bff0fafe869c7db73fdbab73317d4a3b Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Fri, 4 Feb 2022 17:22:29 +0100 Subject: [PATCH] try and fix issue with ENABLED for LTL formulas was missing quantifiers for operations with parameters Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de> --- src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java index cdf903e..012e217 100644 --- a/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java +++ b/src/main/java/de/tlc4b/ltl/LTLFormulaPrinter.java @@ -127,8 +127,13 @@ public class LTLFormulaPrinter extends DepthFirstAdapter { @Override public void caseAEnabledLtl(AEnabledLtl node) { + LinkedHashMap<String, Node> operations = ltlFormulaVisitor + .getMachineContext().getOperations(); tlaPrinter.moduleStringAppend("ENABLED("); - tlaPrinter.moduleStringAppend(node.getOperation().getText()); + //tlaPrinter.moduleStringAppend(node.getOperation().getText()); + String action1Name = node.getOperation().getText(); + Node op1 = operations.get(action1Name); + tlaPrinter.printOperationCall(op1); tlaPrinter.moduleStringAppend(")"); } -- GitLab