Add back conversion functionality classes

xsk07 · Dec 15, 2021 · 5307c27 · 5307c27
1 parent 783b322
commit 5307c27
Show file tree

Hide file tree

Showing 7 changed files with 124 additions and 28 deletions.
diff --git a/src/converter/BackConversionRules.java b/src/converter/BackConversionRules.java
@@ -127,5 +127,51 @@ public static UnaryFormula backG(BinaryFormula f) {
         return new UnaryFormula(GLOB, q);
     }
 
+    public static boolean patternW(BinaryFormula f) {
+        if(f.isOperator(OR)) {
+            Formula lc = f.getLoperand();
+            Formula rc = f.getRoperand();
+            BinaryFormula u;
+            UnaryFormula g;
+            boolean lcG_and_rcU = lc.isOperator(GLOB) && rc.isOperator(UNTIL);
+            boolean lcU_and_rcG = lc.isOperator(UNTIL) && rc.isOperator(GLOB);
+            if(lcU_and_rcG || lcG_and_rcU) {
+                // U(p,q) | Gq
+                if(lc.isOperator(UNTIL) && rc.isOperator(GLOB)) {
+                    u = (BinaryFormula) lc;
+                    g = (UnaryFormula) rc;
+                }
+                // Gq | U(p,q)
+                // lc.isOperator(GLOB) && rc.isOperator(UNTIL)
+                else {
+                    g = (UnaryFormula) lc;
+                    u = (BinaryFormula) rc;
+                }
+                Formula gChild = g.getOperand();
+                Formula q = u.getRoperand();
+                return gChild.equalTo(q);
+            }
+        }
+        return false;
+    }
+
+    /** (U(p,q) | Gq) =>* W(p,q) */
+    public static BinaryFormula backW(BinaryFormula f) {
+
+        if(!patternW(f)) throw new IllegalArgumentException(
+                "The formula must be of the form U(p,q) | Gq"
+        );
+
+        Formula lc = f.getLoperand();
+        Formula rc = f.getRoperand();
+        BinaryFormula u;
+        // U(p,q) | Gq
+        boolean lcU_and_rcG = lc.isOperator(UNTIL) && rc.isOperator(GLOB);
+        if(lcU_and_rcG) u = (BinaryFormula) lc;
+        // Gq | U(p,q)
+        // if(lc.isOperator(GLOB) && rc.isOperator(UNTIL))
+        else u = (BinaryFormula) rc;
+        return new BinaryFormula(UNLESS, u.getRoperand(), u.getLoperand());
+    }
 
 }
diff --git a/src/converter/FormulaConverter.java b/src/converter/FormulaConverter.java
@@ -7,6 +7,7 @@
 import static converter.ConversionRules.*;
 import static formula.Operator.*;
 import static formula.Operator.YEST;
+import static separator.FormulaSimplifier.simplify;
 
 public class FormulaConverter {
 
@@ -21,12 +22,11 @@ public void updateRoot(Formula f) {
     }
 
 
-    /** */
     public Formula convert(Formula phi) throws IllegalArgumentException {
 
         this.setRoot(phi);
 
-        /* the stack and the queue will contain by construction only OperatorFormulas */
+        /* the stack and the queue will contain by construction only OperatorFormula's */
         Stack<Formula> stack = new Stack<>();
         Queue<Formula> queue = new LinkedList<>();
         /* if phi is an OperatorFormula then initialize the queue with it */
@@ -88,15 +88,45 @@ private BinaryFormula applyBinaryRule(BinaryFormula f) {
         };
     }
 
-    public void backConversion(Formula phi) {
-        Queue<Formula> q = new LinkedList<>();
-        q.add(phi);
-        while (!q.isEmpty()) {
-            Formula f = q.remove();
-            if(f instanceof UnaryFormula uf) {
+    public Formula backConversion(Formula phi) {
+        this.setRoot(phi);
+
+        /* the stack and the queue will contain by construction only OperatorFormulae */
+        Stack<Formula> stack = new Stack<>();
+        Queue<Formula> queue = new LinkedList<>();
+        /* if phi is an OperatorFormula then initialize the queue with it */
+        if(phi instanceof OperatorFormula) queue.add(phi);
 
+        while(!queue.isEmpty()) {
+            OperatorFormula f = (OperatorFormula) queue.remove();
+            stack.push(f);
+            if(f instanceof UnaryFormula uf) {
+                if(uf.getOperand() instanceof OperatorFormula) queue.add(uf.getOperand());
             }
             if(f instanceof BinaryFormula bf) {
+                if(bf.getLoperand() instanceof OperatorFormula) queue.add(bf.getLoperand());
+                if(bf.getRoperand() instanceof OperatorFormula) queue.add(bf.getRoperand());
+            }
+        }
+
+        while (!stack.isEmpty()) {
+            Formula f = stack.pop();
+
+            if(f instanceof UnaryFormula uf) {
+                if(uf.isOperator(NOT)) {
+                    if(needTruthValueNegation(uf)){
+                        Formula nf = truthValueNegation(uf);
+                        uf.replaceFormula(nf);
+                        updateRoot(nf);
+                    }
+                    if(needsInvolution(uf)){
+                        Formula nf = involution(uf);
+                        uf.replaceFormula(nf);
+                        updateRoot(nf);
+                    }
+                }
+            }
+            else if(f instanceof BinaryFormula bf) {
                 if(derivedOperator(bf) != null) {
                     switch(derivedOperator(bf)) {
                         case FIN: {
@@ -126,20 +156,32 @@ public void backConversion(Formula phi) {
                             updateRoot(f.replaceFormula(backY(bf)));
                             break;
                         }
+                        case UNLESS: {
+                            updateRoot(f.replaceFormula(backW(bf)));
+                            break;
+                        }
                         default: break;
                     }
                 }
+                // perform some simplifications of the formula based on rules of the boolean logic
+                else {
+                    Formula nf = simplify(bf);
+                    bf.replaceFormula(nf);
+                    updateRoot(nf);
+                }
             }
         }
+        return getRoot();
     }
 
     private static Operator derivedOperator(BinaryFormula f) {
-        if(patternG(f)) return GLOB; // !U(!q, true) =>* Gq
-        if(patternF(f)) return FIN;  // U(q, true) =>* Fq
-        if(patternX(f)) return NEXT; // U(q, false) =>* Xq
-        if(patternH(f)) return HIST; // !S(!q, true) =>* Hq
-        if(patternO(f)) return ONCE; // S(q, true)  =>* Oq
-        if(patternY(f)) return YEST; // S(q, false) =>* Yq
+        if(patternG(f)) return GLOB; // !U(!q, true)
+        if(patternF(f)) return FIN;  // U(q, true)
+        if(patternX(f)) return NEXT; // U(q, false)
+        if(patternH(f)) return HIST; // !S(!q, true)
+        if(patternO(f)) return ONCE; // S(q, true)
+        if(patternY(f)) return YEST; // S(q, false)
+        if(patternW(f)) return UNLESS; // U(p,q) | Gq
         return null;
     }
 

diff --git a/src/formula/AtomConstant.java b/src/formula/AtomConstant.java
@@ -6,10 +6,18 @@ public enum AtomConstant {
     FALSE ("false");
 
     private final String image;
+    private AtomConstant complement;
+
+    static {
+        TRUE.complement = FALSE;
+        FALSE.complement = TRUE;
+    }
 
     AtomConstant(String img) { image = img; }
 
     /** @return Returns the image of the atom constant */
     public String getImage() { return image; }
 
+    public AtomConstant getComplement() {return complement; }
+
 }
diff --git a/src/formula/BooleanRules.java b/src/formula/BooleanRules.java
@@ -243,13 +243,4 @@ private static BinaryFormula rightDistributiveLaw(BinaryFormula f){
         );
     }
 
-
-
-
-
-
-
-
-
-
 }
diff --git a/src/main/Main.java b/src/main/Main.java
@@ -24,7 +24,7 @@ public class Main {
     private static final int DEFAULT_PROMPT_WIDTH = 160;
     private static final String DEFAULT_ENCODING = "png";
     private static final InputStream DEFAULT_INPUT_SOURCE = System.in;
-    private static final String DEFAULT_OUTPUT_FILENAME = "output/out.";
+    private static final String DEFAULT_OUTPUT_FILENAME = "out.";
     private static final Parser parser = new Parser(DEFAULT_INPUT_SOURCE);
     private static final FormulaConverter converter = new FormulaConverter();
     private static final FormulaSeparator separator = new FormulaSeparator();
@@ -33,7 +33,7 @@ public class Main {
     public static void main(String[] args) throws ParseException, IllegalArgumentException {
 
         String header = "Separates an LTLp formula into a combination of pure formulae and generates the corresponding separated automata set \n\n";
-        String footer = "\nPlease report issues at: "; //https://github.com/xsk07/LTLpSeparator
+        String footer = "\nPlease report issues at:  https://github.com/xsk07/LTLpSeparator";
 
         HelpFormatter formatter = new HelpFormatter();
         formatter.setOptionComparator(null);
@@ -74,6 +74,7 @@ public static void main(String[] args) throws ParseException, IllegalArgumentExc
                                 parseFormula(inputSource)
                         )
                 );
+                //result = converter.backConversion(result);
                 outputTask(result, outFile, outputEncoding);
             }
             if(cmd.hasOption("a")) {
@@ -86,7 +87,7 @@ public static void main(String[] args) throws ParseException, IllegalArgumentExc
                 );
                 PureFormulaeMatrix m = normalizer.getPureFormulaeMatrix(result);
                 matrixToJsonFile(m);
-                System.out.println(m.getDegree());
+                //result = converter.backConversion(result);
                 outputTask(result, outFile, outputEncoding);
             }
         } catch (org.apache.commons.cli.ParseException | IOException | InterruptedException | ExecutionException e) {

diff --git a/src/test/BackConversionTest.java b/src/test/BackConversionTest.java
@@ -0,0 +1,10 @@
+package test;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+class BackConversionTest {
+
+
+
+
+}
diff --git a/src/test/DegreeTest.java b/src/test/DegreeTest.java
@@ -9,8 +9,6 @@
 import parser.SimpleNode;
 import java.io.ByteArrayInputStream;
 import java.util.ArrayList;
-
-
 import static formula.Formula.parseTreeToFormula;
 import static separator.FormulaSeparator.maxKofDegreeM;
Original file line number	Diff line number	Diff line change
Expand Up		@@ -243,13 +243,4 @@ private static BinaryFormula rightDistributiveLaw(BinaryFormula f){
		);
		}










		}