Add files via upload

xsk07 · Dec 7, 2021 · 1c03368 · 1c03368
1 parent 205a3b8
commit 1c03368
Show file tree

Hide file tree

Showing 20 changed files with 1,152 additions and 68 deletions.
diff --git a/sepAutSetGen.py b/sepAutSetGen.py
@@ -0,0 +1,45 @@
+import sys
+import os
+import json
+import shutil
+import pydot
+from ltlf2dfa.parser.ltlf import LTLfParser
+
+
+if __name__ == "__main__":
+    main()
+
+
+def main():
+    ''' create a directory called automata
+    if such directory already exists,
+    delete it and its content and create it again '''
+    if(os.path.exists('automata')):
+        shutil.rmtree('automata')
+    os.mkdir('automata')
+
+    ''' read the json file containing the matrix representation 
+    of the SNF of the formula and for each row of the matrix create a directory  '''
+
+    with open('matrix.json', encoding='utf-8-sig') as f: 
+        matrix = json.load(f)
+
+    for i in range(len(matrix)):
+        os.mkdir('automata/{!s}'.format(i+1))
+        save_dfa(matrix[i][0], i+1, 'past')
+        save_dfa(matrix[i][1], i+1, 'present')
+        save_dfa(matrix[i][2], i+1, 'future')
+
+
+def save_dfa(phi, row, time):
+    parser = LTLfParser()
+    formula = parser(phi)
+    dfa = formula.to_dfa()
+    graphs = pydot.graph_from_dot_data(dfa)
+    graph = graphs[0]
+    graph.write_png('automata/{!s}/{}/.png'.format(row, time))
+
+
+
+
+
diff --git a/src/converter/BackConversionRules.java b/src/converter/BackConversionRules.java
@@ -0,0 +1,131 @@
+package converter;
+
+import formula.*;
+import static formula.Operator.*;
+
+public abstract class BackConversionRules {
+
+    public static boolean patternO(BinaryFormula f) {
+        if(f.isOperator(SINCE)) {
+            Formula rc = f.getRoperand();
+            if(rc instanceof AtomicFormula ar) return ar.isTrue();
+        }
+        return false;
+    }
+
+    /** Rewriting rule: S(q, true)  =>* Oq  */
+    public static UnaryFormula backO(BinaryFormula f) {
+        if(!patternO(f)) throw new IllegalArgumentException(
+                "The formula must be of the form S(q, true)"
+        );
+        return new UnaryFormula(
+                ONCE, // O
+                f.getLoperand() // q
+        );
+    }
+
+    public static boolean patternH(BinaryFormula f) {
+        if(f.isOperator(SINCE)) {
+            Formula lc = f.getLoperand();
+            Formula rc = f.getRoperand();
+            Formula p = f.getParent();
+            boolean parentIsNot = p.isOperator(NOT);
+            boolean leftChildIsNot = lc.isOperator(NOT);
+            boolean rightChildIsTrue = rc instanceof AtomicFormula ar && ar.isTrue();
+            return parentIsNot && leftChildIsNot && rightChildIsTrue;
+        }
+        return false;
+    }
+
+    /** !S(!q, true) =>* Hq */
+    public static UnaryFormula backH(BinaryFormula f) {
+        if(!patternH(f)) throw new IllegalArgumentException(
+                "The formula must be of the form !S(!q, true)"
+        );
+        UnaryFormula lc = (UnaryFormula) f.getLoperand();
+        Formula q = lc.getOperand();
+        return new UnaryFormula(HIST, q);
+    }
+
+    public static boolean patternY(BinaryFormula f) {
+        if(f.isOperator(SINCE)) {
+            Formula rc = f.getRoperand();
+            if(rc instanceof AtomicFormula ar) return ar.isFalse();
+        }
+        return false;
+    }
+
+    /** S(q, false) =>* Yq */
+    public static UnaryFormula backY(BinaryFormula f) {
+        if(!patternY(f)) throw new IllegalArgumentException(
+                "The formula must be of the form S(q, false)"
+        );
+        return new UnaryFormula(
+                YEST, // Y
+                f.getLoperand() // q
+        );
+    }
+
+    public static boolean patternF(BinaryFormula f) {
+        if(f.isOperator(UNTIL)) {
+            Formula rc = f.getRoperand();
+            if(rc instanceof AtomicFormula ar) return ar.isTrue();
+        }
+        return false;
+    }
+
+    /** U(q, true) =>* Fq */
+    public static UnaryFormula backF(BinaryFormula f) {
+        if(!patternF(f)) throw new IllegalArgumentException(
+                "The formula must be of the form U(q, true)"
+        );
+        return new UnaryFormula(
+                FIN, // F
+                f.getLoperand() // q
+        );
+    }
+
+    public static boolean patternX(BinaryFormula f) {
+        if(f.isOperator(UNTIL)) {
+            Formula rc = f.getRoperand();
+            if(rc instanceof AtomicFormula ar) return ar.isFalse();
+        }
+        return false;
+    }
+
+    /** U(q, false) =>* Xq */
+    public static UnaryFormula backX(BinaryFormula f) {
+        if(!patternX(f)) throw new IllegalArgumentException(
+                "The formula must be of the form U(q, false)"
+        );
+        return new UnaryFormula(
+                NEXT, // X
+                f.getLoperand() // q
+        );
+    }
+
+    public static boolean patternG(BinaryFormula f) {
+        if(f.isOperator(UNTIL)) {
+            Formula lc = f.getLoperand();
+            Formula rc = f.getRoperand();
+            Formula p = f.getParent();
+            boolean parentIsNot = p.isOperator(NOT);
+            boolean leftChildIsNot = lc.isOperator(NOT);
+            boolean rightChildIsTrue = rc instanceof AtomicFormula ar && ar.isTrue();
+            return parentIsNot && leftChildIsNot && rightChildIsTrue;
+        }
+        return false;
+    }
+
+    /** !U(!q, true) =>* Gq */
+    public static UnaryFormula backG(BinaryFormula f) {
+        if(!patternG(f)) throw new IllegalArgumentException(
+                "The formula must be of the form !U(!q, true)"
+        );
+        UnaryFormula lc = (UnaryFormula) f.getLoperand();
+        Formula q = lc.getOperand();
+        return new UnaryFormula(GLOB, q);
+    }
+
+
+}
diff --git a/src/converter/FormulaConverter.java b/src/converter/FormulaConverter.java
@@ -1,11 +1,12 @@
 package converter;
 
 import formula.*;
-import java.util.LinkedList;
-import java.util.Queue;
-import java.util.Stack;
+import java.util.*;
+import static converter.BackConversionRules.*;
 import static formula.BooleanRules.*;
 import static converter.ConversionRules.*;
+import static formula.Operator.*;
+import static formula.Operator.YEST;
 
 public class FormulaConverter {
 
@@ -19,9 +20,9 @@ public void updateRoot(Formula f) {
         if(f.getParent() == null && f != root) setRoot(f);
     }
 
-    public Formula convert(Formula phi) throws IllegalArgumentException {
 
-        System.out.println("Formula conversion.");
+    /** */
+    public Formula convert(Formula phi) throws IllegalArgumentException {
 
         this.setRoot(phi);
 
@@ -52,9 +53,6 @@ else if(f instanceof BinaryFormula bf) updateRoot(
                     f.replaceFormula(applyBinaryRule(bf))
             );
         }
-
-        System.out.println("Conversion performed.");
-
         return root;
     }
 
@@ -90,4 +88,59 @@ 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) {
+
+            }
+            if(f instanceof BinaryFormula bf) {
+                if(derivedOperator(bf) != null) {
+                    switch(derivedOperator(bf)) {
+                        case FIN: {
+                            UnaryFormula nf = (UnaryFormula) f.replaceFormula(backF(bf));
+                            updateRoot(nf);
+                            break;
+                        }
+                        case GLOB: {
+                            OperatorFormula p = f.getParent();
+                            updateRoot(p.replaceFormula(backG(bf)));
+                            break;
+                        }
+                        case HIST: {
+                            OperatorFormula p = f.getParent();
+                            updateRoot(p.replaceFormula(backH(bf)));
+                            break;
+                        }
+                        case ONCE: {
+                            updateRoot(f.replaceFormula(backO(bf)));
+                            break;
+                        }
+                        case NEXT: {
+                            updateRoot(f.replaceFormula(backX(bf)));
+                            break;
+                        }
+                        case YEST: {
+                            updateRoot(f.replaceFormula(backY(bf)));
+                            break;
+                        }
+                        default: break;
+                    }
+                }
+            }
+        }
+    }
+
+    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
+        return null;
+    }
+
 }