Update README

README.md

@@ -1,2 +1,26 @@
 # DTALMP
 Démonstrateur à tableau analytiques pour les logiques modales propositionnelles
+
+## Exécution
+```
+Entrer Expression Infixe : 
+L(a|b)>(La|Lb)
+```
+```
+W1 : !>L|ab|LaLb
+W1 : L|ab
+W1 : !|LaLb
+W1 : !La
+W1 : !Lb
+W1 -> W2
+W2 : !a
+W2 : |ab
+W1 -> W3
+W3 : !b
+W3 : |ab
+W2 : a
+W2 : b
+W3 : a
+SAT
+
+```

src/Main.java

@@ -1,5 +1,6 @@
 import expression.Expression;
 import expression.Tree;
+import statement.Handling;
 
 /**
  * Created by xawirses on 29/03/17.
@@ -8,10 +9,12 @@ public class Main {
     public static void main(String[] args) {
         Expression e = new Expression();
         e.negExpressionPrefixe();
-        System.out.println(e.getExpressionPrefixe());
+        //System.out.println(e.getExpressionPrefixe());
         System.out.println();
 
         Tree treeExpression = new Tree(e.getExpressionPrefixe());
-        treeExpression.display();
+        //treeExpression.display();
+
+        Handling handling = new Handling(treeExpression.getRoot());
     }
 }

src/expression/Expression.java

@@ -48,7 +48,7 @@ public class Expression {
         return reverse;
     }
 
-    private boolean isParenthesis(char c) {
+    private static boolean isParenthesis(char c) {
         return c == '(' || c == ')';
     }
 
@@ -60,6 +60,10 @@ public class Expression {
         return false;
     }
 
+    public static boolean isOneChildOperator(char c) {
+        return c == '!' || c == 'L' || c == 'M';
+    }
+
     private boolean isHighterOperator(char current, char stack) {
         int pCurrent = 0;
         int pStack = 0;

src/expression/Node.java

@@ -11,13 +11,17 @@ public class Node {
     private Node rigthChild;
     private int lvl;
 
-    Node(Node leftChild, Node rightChild, char name, int lvl){
+    public Node(Node leftChild, Node rightChild, char name, int lvl){
         this.node = name;
         this.leftChild = leftChild;
         this.rigthChild = rightChild;
         this.lvl = lvl;
     }
 
+    public char getNode() {
+        return node;
+    }
+
     public void display() {
         System.out.println(node);
     }
@@ -33,4 +37,38 @@ public class Node {
     public Node getRigthChild() {
         return rigthChild;
     }
+
+    public Boolean haveChild() {
+        return (leftChild != null || rigthChild != null);
+    }
+
+    public Boolean isTerminal () {
+        return (!Expression.isOperator(node) || (node == '!' && leftChild.isTerminal()));
+    }
+
+    public String show() {
+        String left = "";
+        String right = "";
+        if(leftChild != null)
+            left = leftChild.show();
+        if(rigthChild != null)
+            right = rigthChild.show();
+        return node + left + right;
+    }
+
+    public int value() {
+        if(!isTerminal())
+            return 0;
+        if(node == '!')
+            return (1+leftChild.value())%2;
+        return 1;
+    }
+
+    public char symbole() {
+        if(!isTerminal())
+            return 0;
+        if(node == '!')
+            return leftChild.symbole();
+        return node;
+    }
 }

src/expression/Tree.java

@@ -19,7 +19,7 @@ public class Tree {
         char item = exp.charAt(pos);
 
         if(Expression.isOperator(item)) {
-            if (item == '!'){
+            if (Expression.isOneChildOperator(item)){
                 Node fils = tree(pos+1);
                 Node f =  new Node(fils, null, item, 1+fils.getLvl());
                 return f;
@@ -36,6 +36,7 @@ public class Tree {
 
     public void display () {
         displayNode(root,0);
+        System.out.println();
     }
 
     private void displayNode(Node n, int lvl) {
@@ -48,4 +49,8 @@ public class Tree {
         if (n.getRigthChild() != null)
             displayNode(n.getRigthChild(),lvl+1);
     }
+
+    public Node getRoot() {
+        return root;
+    }
 }

src/statement/Handling.java

@@ -0,0 +1,207 @@
+package statement;
+
+import expression.Node;
+
+/**
+ * Created by xawirses on 07/04/17.
+ */
+public class Handling {
+    private Node expression;
+    private World first;
+    private int currentLvl = 0;
+
+    public Handling(Node expression) {
+        this.expression = expression;
+        first = new World();
+        first.addExpInWorld(this.expression, currentLvl);
+        if(handlingWorld(first))
+            System.out.println("INSAT");
+        else
+            System.out.println("SAT");
+    }
+
+    public Boolean handlingWorld(World w) {
+        currentLvl++;
+
+        if(handlingSeparating(w))
+            return true;
+
+        currentLvl++;
+
+        if(handlingBranching(w))
+            return true;
+
+        for (int i = 0; i < w.involvedSize(); i++) {
+            if(handlingWorld(w.getInvolved(i)))
+                return true;
+        }
+
+        return false;
+    }
+
+    private Boolean handlingSeparating(World w) {
+        for (int i = 0; i < w.getSize(); i++) //separated while
+            if(!w.isHandling(i))
+                if(!separatingPattern(w, i) && w.isTerminal(i) && conflictInWorld(w, i))
+                    return true;
+        return false;
+    }
+
+    private Boolean handlingBranching(World w) {
+        for (int i = 0; i < w.getSize(); i++) { //branching while
+            if(!w.isHandling(i)) {
+                if(branchingPattern(w, i)) {
+                    currentLvl++;
+                    if(handlingSeparating(w))
+                        return true;
+                    //currentLvl--;
+                }
+            }
+        }
+        return false;
+    }
+
+    private Boolean separatingPattern(World w, int i) {
+        Node expression = w.getExpression(i);
+
+        if(!expression.haveChild())
+            return false;
+        Node child = expression.getLeftChild();
+
+        switch (expression.getNode()) {
+            case '!' :
+                if(!child.haveChild())
+                    return false;
+                switch (child.getNode()) {
+                    case '!' :
+                        w.addExpInWorld(child.getLeftChild(), currentLvl);
+                        w.handling(i, currentLvl);
+                        return true;
+                    case '|' :
+                        w.addExpInWorld(new Node(child.getLeftChild(), null, '!', child.getLeftChild().getLvl()+1), currentLvl);
+                        w.addExpInWorld(new Node(child.getRigthChild(), null, '!', child.getRigthChild().getLvl()+1), currentLvl);
+                        w.handling(i, currentLvl);
+                        return true;
+                    case '>' :
+                        w.addExpInWorld(child.getLeftChild(), currentLvl);
+                        w.addExpInWorld(new Node(child.getRigthChild(), null, '!', child.getRigthChild().getLvl()+1), currentLvl);
+                        w.handling(i, currentLvl);
+                        return true;
+                    default:
+                        return false;
+                }
+            case '&' :
+                w.addExpInWorld(child, currentLvl);
+                w.addExpInWorld(expression.getRigthChild(), currentLvl);
+                w.handling(i, currentLvl);
+                return true;
+            case 'L' :
+                if(!w.haveInvolve())
+                    return false;
+                w.addExpInInvolveWorlds(child, currentLvl);
+                return true;
+            default:
+                return false;
+        }
+    }
+
+    private Boolean branchingPattern(World w, int i) {
+        Node expression = w.getExpression(i);
+        int lvl = currentLvl;
+
+        if(!expression.haveChild()) {
+            return false;
+        }
+        Node child = expression.getLeftChild();
+
+        switch (expression.getNode()) {
+            case '!' :
+                if(!child.haveChild()) {
+                    return false;
+                }
+                switch (child.getNode()) {
+                    case '&' :
+                        w.handling(i, currentLvl);
+                        w.addExpInWorld(new Node(child.getLeftChild(), null, '!', child.getLeftChild().getLvl()+1), currentLvl);
+                        if(handlingWorld(w)) {
+                            removeLvlModification(first, lvl);
+                            w.handling(i, currentLvl);
+                            w.addExpInWorld(new Node(child.getRigthChild(), null, '!', child.getRigthChild().getLvl()+1), currentLvl);
+                            if(handlingWorld(w)) {
+                                return true;
+                            }
+                        }
+
+                        return false;
+                    case 'L' :
+                        w.handling(i, currentLvl);
+                        World x = new World();
+                        w.addInvolve(x);
+                        x.addExpInWorld(new Node(child.getLeftChild(), null, '!', child.getLeftChild().getLvl()+1), currentLvl);
+                        if(handlingWorld(w)) {
+                            return true;
+                        }
+                        return false;
+                    default:
+                        return false;
+                }
+            case '|' :
+                w.handling(i, currentLvl);
+                w.addExpInWorld(child, currentLvl);
+                if(handlingWorld(w)) {
+                    removeLvlModification(w, lvl);
+                    w.handling(i, currentLvl);
+                    w.addExpInWorld(expression.getRigthChild(), currentLvl);
+                    if (handlingWorld(w)) {
+                        return true;
+                    }
+                }
+                return false;
+            case '>' :
+                w.handling(i, currentLvl);
+                w.addExpInWorld(new Node(child, null, '!', child.getLvl()+1), currentLvl);
+                if(handlingWorld(w)) {
+                    removeLvlModification(w, lvl);
+                    w.handling(i, currentLvl);
+                    w.addExpInWorld(expression.getRigthChild(), currentLvl);
+                    if (handlingWorld(w)) {
+                        return true;
+                    }
+                }
+                return false;
+            default:
+                return false;
+        }
+    }
+
+    private Boolean conflictInWorld(World w, int i) {
+        int comparator = w.getExpression(i).value();
+        int comparatorSymbole = w.getExpression(i).symbole();
+
+        for (int j = 0; j < w.getSize(); j++) {
+            Node exp = w.getExpression(j);
+            if(exp.isTerminal() && comparatorSymbole == exp.symbole() && exp.value() != comparator) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    private void removeLvlModification(World w, int lvl) {
+        currentLvl = lvl;
+
+        for (int i = w.getSize()-1; i >= 0; i--) {
+            if(w.getWhileLvl(i) >= lvl) {
+                w.removeExpression(i);
+            } else if(w.getHandling(i) >= lvl) {
+                w.handling(i,0);
+            }
+        }
+
+        for (int i = w.involvedSize()-1; i >= 0; i--) {
+            removeLvlModification(w.getInvolved(i), lvl);
+            if(w.getInvolved(i).isEmpty())
+                w.removeInvolve(i);
+        }
+    }
+} // L(a|b)>(La|Lb)

src/statement/World.java

@@ -9,11 +9,88 @@ import java.util.Collection;
  * Created by xawirses on 29/03/17.
  */
 public class World {
+    private static int worldId = 1;
     private String name;
-    private Collection<Node> expressions = new ArrayList<>();
+    private ArrayList<Node> expressions = new ArrayList<>();
-    private Collection<World> involved = new ArrayList<>();
+    private ArrayList<Integer> whileLvl = new ArrayList<>();
+    private ArrayList<Integer> handling = new ArrayList<>();
+    private ArrayList<World> involved = new ArrayList<>();
 
-    public World(String name) {
+    public World() {
-        this.name = name;
+        this.name = Integer.toString(worldId);
+        worldId +=1;
+    }
+
+    public void addExpInWorld(Node exp, int lvl) {
+        if(expressions.contains(exp))
+            return;
+        expressions.add(exp);
+        handling.add(0);
+        whileLvl.add(lvl);
+        System.out.println("W"+name+" : " + exp.show());
+    }
+
+    public Boolean isEmpty() {
+        return expressions.size() == 0;
+    }
+
+    public int getSize() {
+        return expressions.size();
+    }
+
+    public int involvedSize() {
+        return involved.size();
+    }
+
+    public Node getExpression(int i) {
+        return expressions.get(i);
+    }
+
+    public World getInvolved(int i) {
+        return involved.get(i);
+    }
+
+    public Boolean isHandling(int i) {
+        return handling.get(i) != 0;
+    }
+
+    public void handling(int i, int lvl) {
+        handling.set(i, lvl);
+    }
+
+    public Boolean haveInvolve() {
+        return !involved.isEmpty();
+    }
+
+    public void addExpInInvolveWorlds(Node exp, int lvl) {
+        for(World w : involved)
+            w.addExpInWorld(exp, lvl);
+    }
+
+    public Boolean isTerminal(int i) {
+        return expressions.get(i).isTerminal();
+    }
+
+    public void addInvolve(World w) {
+        involved.add(w);
+        System.out.println("W"+name+" -> W"+w.name);
+    }
+
+    public void removeInvolve(int i) {
+        involved.remove(i);
+    }
+
+    public int getWhileLvl(int i) {
+        return whileLvl.get(i);
+    }
+
+    public int getHandling(int i) {
+        return handling.get(i);
+    }
+
+    public void removeExpression(int i) {
+        expressions.remove(i);
+        whileLvl.remove(i);
+        handling.remove(i);
     }
 }