Xawirses/DTALMP
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add Handling

Browse Source
This commit is contained in:
Xawirses
2017-04-10 14:52:05 +02:00
parent b8b3cedd28
commit e5b7f09495
6 changed files with 341 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

207
src/statement/Handling.java Normal file
View File

@@ -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)