From 746e3efb6f4c6cf70cc5b67f9c8f2ea3657328ec Mon Sep 17 00:00:00 2001
From: Alexander Steen <a.steen@fu-berlin.de>
Date: Tue, 19 Jan 2021 19:13:50 +0100
Subject: [PATCH] corrected negation embedding with more parentheses

---
 .../src/main/java/transformation/ModalTransformator.java   | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/lib_embedding/src/main/java/transformation/ModalTransformator.java b/lib_embedding/src/main/java/transformation/ModalTransformator.java
index 654f5fe..cf87b40 100644
--- a/lib_embedding/src/main/java/transformation/ModalTransformator.java
+++ b/lib_embedding/src/main/java/transformation/ModalTransformator.java
@@ -365,7 +365,12 @@ private void replaceNullaryAndUnaryOperators(Node leaf) throws AnalysisException
                 usedConnectives.add("mfalse");
                 break;
             case "~":
-                leaf.setLabel("mnot @");
+                Node operatorTree = leaf.getNextTopBranchingNode(); // should be thf_unary_formula
+                if (!operatorTree.getRule().equals("thf_unary_formula")) throw new ImplementationError("~ ... is not a thf_unary_formula.");
+                operatorTree.replaceChildAt(0, new Node("t_mnot", "mnot @"));
+                operatorTree.addChildAt(new Node("t_left_paren", "("), 0);
+                operatorTree.addChild(new Node("t_right_paren", ")"));
+//                leaf.setLabel("mnot @");
                 usedConnectives.add("mnot");
                 break;
             // embed simple modality