| /** |
| * <copyright> |
| * OCL2AC is developed by Nebras Nassar based on an initial version developed by Thorsten Arendt and Jan Steffen Becker. |
| * </copyright> |
| */ |
| package laxcondition.util.extensions; |
| |
| import java.util.ArrayList; |
| import java.util.List; |
| |
| import org.eclipse.emf.common.util.BasicEList; |
| import org.eclipse.emf.common.util.EList; |
| import org.eclipse.emf.common.util.TreeIterator; |
| import org.eclipse.emf.ecore.EClass; |
| import org.eclipse.emf.ecore.EObject; |
| import org.eclipse.emf.ecore.EPackage; |
| import org.eclipse.emf.ecore.util.EcoreUtil; |
| |
| import graph.Edge; |
| import graph.Graph; |
| import graph.Node; |
| import laxcondition.Condition; |
| import laxcondition.Formula; |
| import laxcondition.LaxCondition; |
| import laxcondition.LaxconditionFactory; |
| import laxcondition.Operator; |
| import laxcondition.QuantifiedLaxCondition; |
| import laxcondition.Quantifier; |
| import laxcondition.True; |
| |
| public class LaxConditionSimplifier { |
| |
| private Condition condition; |
| private LaxconditionFactory factory; |
| |
| public LaxConditionSimplifier(Condition condition) { |
| this.condition = condition; |
| this.factory = LaxconditionFactory.eINSTANCE; |
| } |
| |
| public boolean simplify() { |
| if (simplifyNames()) { |
| return simplify(); |
| } |
| if (simplifyTrueOrFalseInFormula()) { |
| return simplify(); |
| } |
| if (simplifyNotNot()) { |
| return simplify(); |
| } |
| |
| if (simplifyExists()) { |
| return simplify(); |
| } |
| return true; |
| } |
| |
| private boolean insert(EObject container, LaxCondition oldContent, LaxCondition newContent) { |
| if (container instanceof Condition) { |
| Condition constraint = (Condition) container; |
| constraint.setLaxCondition(newContent); |
| return true; |
| } |
| if (container instanceof QuantifiedLaxCondition) { |
| QuantifiedLaxCondition qlc = (QuantifiedLaxCondition) container; |
| qlc.setCondition(newContent); |
| return true; |
| } |
| if (container instanceof Formula) { |
| Formula f = (Formula) container; |
| int index = f.getArguments().indexOf(oldContent); |
| f.getArguments().set(index, newContent); |
| return true; |
| } |
| return false; |
| } |
| |
| private boolean simplifyNames() { |
| TreeIterator<EObject> iter1 = condition.eAllContents(); |
| while (iter1.hasNext()) { |
| EObject eObject1 = iter1.next(); |
| if (eObject1 instanceof Node) { |
| Node node1 = (Node) eObject1; |
| if (node1.getNames().size() > 1) { |
| for (String name : node1.getNames()) { |
| boolean onlyOnce = true; |
| TreeIterator<EObject> iter2 = condition.eAllContents(); |
| while (iter2.hasNext()) { |
| EObject eObject2 = iter2.next(); |
| if (eObject2 instanceof Node) { |
| Node node2 = (Node) eObject2; |
| if (node1 != node2 && node2.getNames().contains(name)) { |
| onlyOnce = false; |
| break; |
| } |
| } |
| } |
| if (onlyOnce) { |
| node1.removeName(name); |
| System.out.println("Removing name: " + name); |
| return true; |
| } |
| } |
| } |
| } |
| } |
| return false; |
| } |
| |
| private boolean simplifyExists() { |
| TreeIterator<EObject> iter = condition.eAllContents(); |
| while (iter.hasNext()) { |
| EObject eObject = iter.next(); |
| if (isExistsCondition(eObject)) { |
| QuantifiedLaxCondition outerCondition = (QuantifiedLaxCondition) eObject; |
| LaxCondition cond = outerCondition.getCondition(); |
| if (isExistsCondition(cond)) { |
| QuantifiedLaxCondition innerCondition = (QuantifiedLaxCondition) cond; |
| if (isTrue(innerCondition.getCondition())) { |
| Graph outerGraph = outerCondition.getGraph(); |
| Graph innerGraph = innerCondition.getGraph(); |
| if (isSubGraph(outerGraph, innerGraph)) { |
| outerCondition.setGraph(innerGraph); |
| outerCondition.setCondition(factory.createTrue()); |
| System.out.println("Equivalence E1.c"); |
| return true; |
| } |
| if (isSubGraph(innerGraph, outerGraph)) { |
| outerCondition.setCondition(factory.createTrue()); |
| System.out.println("Equivalence E1.c"); |
| return true; |
| } |
| if (areClanDisjoint(innerGraph, outerGraph)) { |
| EList<Node> innerNodes = innerGraph.getNodes(); |
| innerGraph.getNodes().clear(); |
| outerGraph.getNodes().addAll(innerNodes); |
| EList<Edge> innerEdges = innerGraph.getEdges(); |
| innerGraph.getEdges().clear(); |
| outerGraph.getEdges().addAll(innerEdges); |
| outerCondition.setCondition(factory.createTrue()); |
| System.out.println("Equivalence E1.b"); |
| return true; |
| } |
| if (haveIntersection(innerGraph, outerGraph)) { |
| EList<Intersection> intersections = getIntersections(outerGraph, innerGraph); |
| EObject container = outerCondition.eContainer(); |
| if (intersections.size() == 1) { |
| QuantifiedLaxCondition condition = factory.createQuantifiedLaxCondition(); |
| condition.setQuantifier(Quantifier.EXISTS); |
| condition.setGraph(glue(outerGraph, intersections.get(0), innerGraph)); |
| condition.setCondition(factory.createTrue()); |
| insert(container, outerCondition, condition); |
| System.out.println("Equivalence E1.a"); |
| return true; |
| } |
| Formula formula = factory.createFormula(); |
| formula.setOp(Operator.OR); |
| for (Intersection intersection : intersections) { |
| QuantifiedLaxCondition condition = factory.createQuantifiedLaxCondition(); |
| condition.setQuantifier(Quantifier.EXISTS); |
| condition.setGraph( |
| glue(outerCondition.getGraph(), intersection, innerCondition.getGraph())); |
| condition.setCondition(factory.createTrue()); |
| formula.getArguments().add(condition); |
| } |
| insert(container, outerCondition, formula); |
| System.out.println("Equivalence E1.a"); |
| return true; |
| } |
| if (hasOnlyOneNode(innerGraph)) { |
| Node innerNode = innerGraph.getNodes().get(0); |
| if (hasTwoNames(innerNode)) { |
| String name1 = innerNode.getNames().get(0); |
| String name2 = innerNode.getNames().get(1); |
| if (containsExactlyOne(outerGraph, name1, name2)) { |
| rename(outerGraph, name1, name2); |
| outerCondition.setCondition(factory.createTrue()); |
| System.out.println("Equivalence E3'"); |
| return true; |
| } |
| } |
| } |
| } |
| } |
| if (isAndFormula(cond)) { |
| Formula andFormula = (Formula) cond; |
| if (andFormula.getArguments().size() == 2) { |
| if (isExistsCondition(andFormula.getArguments().get(0)) |
| && isExistsCondition(andFormula.getArguments().get(1))) { |
| QuantifiedLaxCondition cond1 = (QuantifiedLaxCondition) andFormula.getArguments().get(0); |
| QuantifiedLaxCondition cond2 = (QuantifiedLaxCondition) andFormula.getArguments().get(1); |
| if (cond1.getCondition() instanceof True && cond2.getCondition() instanceof True) { |
| Graph gr = outerCondition.getGraph(); |
| Graph gr1 = cond1.getGraph(); |
| Graph gr2 = cond2.getGraph(); |
| if (hasOnlyOneNode(gr) && hasOnlyOneNode(gr2)) { |
| Node node = gr.getNodes().get(0); |
| Node node2 = gr2.getNodes().get(0); |
| if (haveSameTypes(node, node2) && hasOneName(node) && hasTwoNames(node2)) { |
| String name = node.getName(); |
| String name1 = node2.getName().split("=")[0]; |
| String name2 = node2.getName().split("=")[1]; |
| if (name.equals(name1) || name.equals(name2)) { |
| if (containsExactlyOne(gr1, name1, name2)) { |
| rename(gr1, name1, name2); |
| outerCondition.setCondition(cond1); |
| System.out.println("Equivalence E3"); |
| return true; |
| } |
| } |
| } |
| } |
| if (hasOnlyOneNode(gr) && hasOnlyOneNode(gr1)) { |
| Node node = gr.getNodes().get(0); |
| Node node1 = gr1.getNodes().get(0); |
| if (haveSameTypes(node, node1) && hasOneName(node) && hasTwoNames(node1)) { |
| String name = node.getName(); |
| String name1 = node1.getName().split("=")[0]; |
| String name2 = node1.getName().split("=")[1]; |
| if (name.equals(name1) || name.equals(name2)) { |
| if (containsExactlyOne(gr2, name1, name2)) { |
| rename(gr2, name1, name2); |
| outerCondition.setCondition(cond2); |
| System.out.println("Equivalence E3"); |
| return true; |
| } |
| } |
| } |
| } |
| System.out.println("=> haveRecurringNodes: " + haveRecurringNodes(gr1, gr2)); |
| System.out.println( |
| "=> containsEachRecurringNode: " + containsEachRecurringNode(gr, gr1, gr2)); |
| if (haveRecurringNodes(gr1, gr2)) { |
| if (containsEachRecurringNode(gr, gr1, gr2) |
| || containsNoRecurringNodeType(gr, gr1, gr2)) { |
| if (haveIntersection(gr1, gr2)) { |
| EList<Intersection> intersections = getIntersections(gr1, gr2); |
| if (intersections.size() == 1) { |
| QuantifiedLaxCondition condition = factory |
| .createQuantifiedLaxCondition(); |
| condition.setQuantifier(Quantifier.EXISTS); |
| condition.setGraph(glue(gr1, intersections.get(0), gr2)); |
| condition.setCondition(factory.createTrue()); |
| outerCondition.setCondition(condition); |
| System.out.println("Equivalence E2.a"); |
| return true; |
| } |
| Formula formula = factory.createFormula(); |
| formula.setOp(Operator.OR); |
| for (Intersection intersection : intersections) { |
| QuantifiedLaxCondition condition = factory |
| .createQuantifiedLaxCondition(); |
| condition.setQuantifier(Quantifier.EXISTS); |
| condition.setGraph(glue(gr1, intersection, gr2)); |
| condition.setCondition(factory.createTrue()); |
| formula.getArguments().add(condition); |
| } |
| outerCondition.setCondition(formula); |
| System.out.println("Equivalence E2.a"); |
| return true; |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| } |
| if (isAndFormula(eObject)) { |
| Formula andFormula = (Formula) eObject; |
| if (andFormula.getArguments().size() == 2) { |
| if (isExistsCondition(andFormula.getArguments().get(0)) |
| && isExistsCondition(andFormula.getArguments().get(1))) { |
| QuantifiedLaxCondition cond1 = (QuantifiedLaxCondition) andFormula.getArguments().get(0); |
| QuantifiedLaxCondition cond2 = (QuantifiedLaxCondition) andFormula.getArguments().get(1); |
| if (cond1.getCondition() instanceof True && cond2.getCondition() instanceof True) { |
| Graph gr1 = cond1.getGraph(); |
| Graph gr2 = cond2.getGraph(); |
| if (areClanDisjoint(gr1, gr2) && areNodeNameDisjoint(gr1, gr2)) { |
| EList<Node> nodes = gr2.getNodes(); |
| gr2.getNodes().clear(); |
| gr1.getNodes().addAll(nodes); |
| EList<Edge> edges = gr2.getEdges(); |
| gr2.getEdges().clear(); |
| gr1.getEdges().addAll(edges); |
| EObject container = andFormula.eContainer(); |
| insert(container, andFormula, cond1); |
| System.out.println("Equivalence E2.b"); |
| return true; |
| } |
| } |
| } |
| } |
| |
| } |
| } |
| return false; |
| } |
| |
| private boolean haveRecurringNodes(Graph gr1, Graph gr2) { |
| EList<Node> recurringNodes = collectRecurringNodes(gr1, gr2); |
| return (!recurringNodes.isEmpty()); |
| } |
| |
| private boolean containsEachRecurringNode(Graph gr, Graph gr1, Graph gr2) { |
| EList<Node> recurringNodes = collectRecurringNodes(gr1, gr2); |
| for (Node recurringNode : recurringNodes) { |
| boolean occurs = false; |
| String nodeName = recurringNode.getName(); |
| EClass type = recurringNode.getType(); |
| for (Node node : gr.getNodes()) { |
| if (node.getName().equals(nodeName) && node.getType() == type) { |
| occurs = true; |
| break; |
| } |
| } |
| if (!occurs) { |
| return false; |
| } |
| } |
| return true; |
| } |
| |
| private boolean containsNoRecurringNodeType(Graph gr, Graph gr1, Graph gr2) { |
| EList<Node> recurringNodes = collectRecurringNodes(gr1, gr2); |
| boolean occurs = false; |
| for (Node recurringNode : recurringNodes) { |
| EClass type = recurringNode.getType(); |
| for (Node node : gr.getNodes()) { |
| if (node.getType() == type) { |
| occurs = true; |
| break; |
| } |
| } |
| } |
| return !occurs; |
| } |
| |
| private EList<Node> collectRecurringNodes(Graph gr1, Graph gr2) { |
| EList<Node> recurringNodes = new BasicEList<Node>(); |
| for (Node node1 : gr1.getNodes()) { |
| String nodeName = node1.getName(); |
| EClass type = node1.getType(); |
| for (Node node2 : gr2.getNodes()) { |
| if (node2.getName().equals(nodeName) && node2.getType() == type) { |
| recurringNodes.add(node1); |
| break; |
| } |
| } |
| } |
| return recurringNodes; |
| } |
| |
| private void rename(Graph graph, String name1, String name2) { |
| String newName = name1 + "=" + name2; |
| for (Node node : graph.getNodes()) { |
| if (node.getName().equals(name1) || node.getName().equals(name2)) { |
| node.setName(newName); |
| } |
| } |
| } |
| |
| private boolean containsExactlyOne(Graph graph, String name1, String name2) { |
| boolean exists1 = false; |
| boolean exists2 = false; |
| for (Node node : graph.getNodes()) { |
| if (node.getName().equals(name1)) |
| exists1 = true; |
| if (node.getName().equals(name2)) |
| exists2 = true; |
| } |
| return ((exists1 && !exists2) || (!exists1 && exists2)); |
| } |
| |
| private boolean hasTwoNames(Node node) { |
| return (node.getName().split("=").length == 2); |
| } |
| |
| private boolean hasOneName(Node node) { |
| return (node.getName().split("=").length == 1); |
| } |
| |
| private boolean haveSameTypes(Node node1, Node node2) { |
| return (node1.getType() == node2.getType()); |
| } |
| |
| private boolean hasOnlyOneNode(Graph graph) { |
| return (graph.getNodes().size() == 1 && graph.getEdges().isEmpty()); |
| } |
| |
| private Graph glue(Graph gr1, Intersection intersection, Graph gr2) { |
| Graph graph = intersection.getSourceGraph(); |
| |
| for (Node node : gr1.getNodes()) { |
| if (!intersection.containsSource(node)) { |
| Node nodeCopy = EcoreUtil.copy(node); |
| intersection.addNodeMapping(new NodeMapping(nodeCopy, node)); |
| graph.getNodes().add(nodeCopy); |
| } |
| } |
| for (Node node : gr2.getNodes()) { |
| if (!intersection.containsTarget(node)) { |
| Node nodeCopy = EcoreUtil.copy(node); |
| intersection.addNodeMapping(new NodeMapping(nodeCopy, node)); |
| graph.getNodes().add(nodeCopy); |
| } |
| } |
| |
| for (Edge edge : gr1.getEdges()) { |
| if (!intersection.containsTarget(edge)) { |
| Edge edgeCopy = EcoreUtil.copy(edge); |
| edgeCopy.setSource(intersection.getSourceNode1(edge.getSource())); |
| edgeCopy.setTarget(intersection.getSourceNode1(edge.getTarget())); |
| graph.getEdges().add(edgeCopy); |
| } |
| } |
| for (Edge edge : gr2.getEdges()) { |
| if (!intersection.containsTarget(edge)) { |
| Edge edgeCopy = EcoreUtil.copy(edge); |
| edgeCopy.setSource(intersection.getSourceNode(edge.getSource())); |
| edgeCopy.setTarget(intersection.getSourceNode(edge.getTarget())); |
| graph.getEdges().add(edgeCopy); |
| } |
| } |
| graph.setTypegraph(gr1.getTypegraph()); |
| return graph; |
| } |
| |
| private EList<Intersection> getIntersections(Graph gr1, Graph gr2) { |
| EList<Intersection> intersections = new BasicEList<Intersection>(); |
| EList<Graph> subGraphs = new BasicEList<Graph>(); |
| fillSubGraphs(subGraphs, gr1); |
| for (Graph graph : subGraphs) { |
| if (isSubGraph(graph, gr2)) { |
| intersections.add(getIntersection(graph, gr2)); |
| } |
| } |
| return intersections; |
| } |
| |
| private Intersection getIntersection(Graph subGraph, Graph graph) { |
| Intersection intersection = new Intersection(); |
| for (Node n1 : subGraph.getNodes()) { |
| for (Node n2 : graph.getNodes()) { |
| if (n1.getType() == n2.getType() && n1.getName().equals(n2.getName())) { |
| intersection.addNodeMapping(new NodeMapping(n1, n2)); |
| } |
| } |
| } |
| for (Edge e1 : subGraph.getEdges()) { |
| Node src1 = e1.getSource(); |
| NodeMapping srcMapping = getMapping(intersection.getNodeMappings(), src1); |
| Node tgt1 = e1.getTarget(); |
| NodeMapping tgtMapping = getMapping(intersection.getNodeMappings(), tgt1); |
| for (Edge e2 : graph.getEdges()) { |
| Node src2 = e2.getSource(); |
| Node tgt2 = e2.getTarget(); |
| if (e1.getType() == e2.getType() && srcMapping.getTargetNode() == src2 |
| && tgtMapping.getTargetNode() == tgt2) { |
| intersection.addEdgeMapping(new EdgeMapping(e1, e2)); |
| break; |
| } |
| } |
| } |
| return intersection; |
| } |
| |
| private void fillSubGraphs(EList<Graph> subGraphs, Graph graph) { |
| EList<Edge> edges = cloneEdges(graph); |
| for (Edge edge : edges) { |
| graph.getEdges().remove(edge); |
| Graph gr = EcoreUtil.copy(graph); |
| graph.getEdges().add(edge); |
| testAndFill(subGraphs, gr); |
| } |
| EList<Node> nodes = cloneNodes(graph); |
| for (Node node : nodes) { |
| if (!isConnected(node, graph)) { |
| graph.getNodes().remove(node); |
| Graph gr = EcoreUtil.copy(graph); |
| graph.getNodes().add(node); |
| if (!isEmptyGraph(gr)) { |
| testAndFill(subGraphs, gr); |
| } |
| } |
| } |
| } |
| |
| private boolean isEmptyGraph(Graph graph) { |
| return (graph.getNodes().isEmpty() && graph.getEdges().isEmpty()); |
| } |
| |
| private boolean isConnected(Node node, Graph graph) { |
| for (Edge edge : graph.getEdges()) { |
| if (edge.getSource() == node) |
| return true; |
| if (edge.getTarget() == node) |
| return true; |
| } |
| return false; |
| } |
| |
| private void testAndFill(EList<Graph> graphs, Graph graph) { |
| if (!contains(graphs, graph)) { |
| graphs.add(graph); |
| fillSubGraphs(graphs, graph); |
| } |
| } |
| |
| private boolean contains(EList<Graph> graphs, Graph graph) { |
| for (Graph gr : graphs) { |
| if (isSameGraph(gr, graph)) { |
| return true; |
| } |
| } |
| return false; |
| } |
| |
| private boolean isSameGraph(Graph gr1, Graph gr2) { |
| return (isSubGraph(gr1, gr2) && isSubGraph(gr2, gr1)); |
| } |
| |
| private EList<Node> cloneNodes(Graph graph) { |
| EList<Node> nodes = new BasicEList<Node>(); |
| for (Node node : graph.getNodes()) { |
| nodes.add(node); |
| } |
| return nodes; |
| } |
| |
| private EList<Edge> cloneEdges(Graph graph) { |
| EList<Edge> edges = new BasicEList<Edge>(); |
| for (Edge edge : graph.getEdges()) { |
| edges.add(edge); |
| } |
| return edges; |
| } |
| |
| private boolean areNodeNameDisjoint(Graph gr1, Graph gr2) { |
| List<String> names1 = getNodeNames(gr1); |
| List<String> names2 = getNodeNames(gr2); |
| for (String str1 : names1) { |
| for (String str2 : names2) { |
| if (str1.equals(str2)) { |
| return false; |
| } |
| } |
| } |
| return true; |
| } |
| |
| private List<String> getNodeNames(Graph graph) { |
| List<String> names = new ArrayList<String>(); |
| for (Node node : graph.getNodes()) { |
| names.addAll(node.getNames()); |
| } |
| return names; |
| } |
| |
| private boolean haveIntersection(Graph gr1, Graph gr2) { |
| EList<Intersection> intersections = getIntersections(gr1, gr2); |
| return !intersections.isEmpty(); |
| } |
| |
| private boolean areClanDisjoint(Graph gr1, Graph gr2) { |
| for (Node n1 : gr1.getNodes()) { |
| EList<EClass> clan1 = getClan(n1.getType()); |
| for (Node n2 : gr2.getNodes()) { |
| if (clan1.contains(n2.getType())) { |
| return false; |
| } |
| } |
| } |
| for (Node n2 : gr2.getNodes()) { |
| EList<EClass> clan2 = getClan(n2.getType()); |
| for (Node n1 : gr1.getNodes()) { |
| if (clan2.contains(n1.getType())) { |
| return false; |
| } |
| } |
| } |
| return true; |
| } |
| |
| private EList<EClass> getClan(EClass eClass) { |
| EList<EClass> eClasses = new BasicEList<EClass>(); |
| eClasses.add(eClass); |
| eClasses.addAll(getAllSubclasses(eClass)); |
| return eClasses; |
| } |
| |
| private EList<EClass> getAllSubclasses(EClass eClass) { |
| EList<EClass> eClasses = new BasicEList<EClass>(); |
| EPackage ePackage = eClass.getEPackage(); |
| TreeIterator<EObject> iter = ePackage.eAllContents(); |
| while (iter.hasNext()) { |
| EObject eObject = iter.next(); |
| if (eObject instanceof EClass) { |
| EClass clazz = (EClass) eObject; |
| if (clazz.getEAllSuperTypes().contains(eClass)) { |
| eClasses.add(clazz); |
| } |
| } |
| } |
| return eClasses; |
| } |
| |
| private boolean isSubGraph(Graph gr1, Graph gr2) { |
| EList<NodeMapping> nodeMappings = new BasicEList<NodeMapping>(); |
| for (Node n1 : gr1.getNodes()) { |
| for (Node n2 : gr2.getNodes()) { |
| if (n1.getType() == n2.getType()) { |
| if (n2.getNames().containsAll(n1.getNames())) { |
| nodeMappings.add(new NodeMapping(n1, n2)); |
| } |
| } |
| } |
| } |
| if (gr1.getNodes().size() != nodeMappings.size()) { |
| return false; |
| } |
| for (Edge e1 : gr1.getEdges()) { |
| Node src1 = e1.getSource(); |
| NodeMapping srcMapping = getMapping(nodeMappings, src1); |
| Node tgt1 = e1.getTarget(); |
| NodeMapping tgtMapping = getMapping(nodeMappings, tgt1); |
| boolean hasTarget = false; |
| for (Edge e2 : gr2.getEdges()) { |
| Node src2 = e2.getSource(); |
| Node tgt2 = e2.getTarget(); |
| if (e1.getType() == e2.getType() && srcMapping.getTargetNode() == src2 |
| && tgtMapping.getTargetNode() == tgt2) { |
| hasTarget = true; |
| break; |
| } |
| } |
| if (!hasTarget) { |
| return false; |
| } |
| } |
| return true; |
| } |
| |
| private NodeMapping getMapping(EList<NodeMapping> nodeMappings, Node node) { |
| for (NodeMapping nm : nodeMappings) { |
| if (nm.getSourceNode() == node) { |
| return nm; |
| } |
| } |
| return null; |
| } |
| |
| private boolean simplifyTrueOrFalseInFormula() { |
| TreeIterator<EObject> iter = condition.eAllContents(); |
| while (iter.hasNext()) { |
| EObject eObject = iter.next(); |
| if (isAndFormula(eObject)) { |
| Formula formula = (Formula) eObject; |
| EObject container = formula.eContainer(); |
| LaxCondition arg1 = formula.getArguments().get(0); |
| LaxCondition arg2 = formula.getArguments().get(1); |
| if (isTrue(arg1)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg2); |
| } else { |
| return removeArgument(formula, arg1); |
| } |
| } |
| if (isTrue(arg2)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg1); |
| } else { |
| return removeArgument(formula, arg2); |
| } |
| } |
| if (isFalse(arg1)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg1); |
| } else { |
| return removeArgument(formula, arg2); |
| } |
| } |
| if (isFalse(arg2)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg2); |
| } else { |
| return removeArgument(formula, arg1); |
| } |
| } |
| } |
| if (isOrFormula(eObject)) { |
| Formula formula = (Formula) eObject; |
| EObject container = formula.eContainer(); |
| LaxCondition arg1 = formula.getArguments().get(0); |
| LaxCondition arg2 = formula.getArguments().get(1); |
| if (isTrue(arg1)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg1); |
| } else { |
| return removeArgument(formula, arg2); |
| } |
| } |
| if (isTrue(arg2)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg2); |
| } else { |
| return removeArgument(formula, arg1); |
| } |
| } |
| if (isFalse(arg1)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg2); |
| } else { |
| return removeArgument(formula, arg1); |
| } |
| } |
| if (isFalse(arg2)) { |
| if (twoArguments(formula)) { |
| return insert(container, formula, arg1); |
| } else { |
| return removeArgument(formula, arg2); |
| } |
| } |
| } |
| } |
| return false; |
| } |
| |
| private boolean removeArgument(Formula formula, LaxCondition cond) { |
| return formula.getArguments().remove(cond); |
| } |
| |
| private boolean twoArguments(Formula formula) { |
| return (formula.getArguments().size() == 2); |
| } |
| |
| private boolean isFalse(LaxCondition cond) { |
| if (isNotFormula(cond)) { |
| Formula formula = (Formula) cond; |
| return isTrue(formula.getArguments().get(0)); |
| } |
| return false; |
| } |
| |
| private boolean isTrue(LaxCondition cond) { |
| return (cond instanceof True); |
| } |
| |
| private boolean simplifyNotNot() { |
| TreeIterator<EObject> iter = condition.eAllContents(); |
| while (iter.hasNext()) { |
| EObject eObject = iter.next(); |
| if (isNotFormula(eObject)) { |
| Formula formula = (Formula) eObject; |
| if (isNotFormula(formula.getArguments().get(0))) { |
| Formula innerFormula = (Formula) formula.getArguments().get(0); |
| LaxCondition innerCondition = innerFormula.getArguments().get(0); |
| EObject container = formula.eContainer(); |
| return insert(container, formula, innerCondition); |
| } |
| } |
| } |
| return false; |
| } |
| |
| private boolean isNotFormula(EObject eObject) { |
| if (eObject instanceof Formula) { |
| Formula formula = (Formula) eObject; |
| return (formula.getOp().equals(Operator.NOT)); |
| } |
| return false; |
| } |
| |
| private boolean isAndFormula(EObject eObject) { |
| if (eObject instanceof Formula) { |
| Formula formula = (Formula) eObject; |
| return (formula.getOp().equals(Operator.AND)); |
| } |
| return false; |
| } |
| |
| private boolean isOrFormula(EObject eObject) { |
| if (eObject instanceof Formula) { |
| Formula formula = (Formula) eObject; |
| return (formula.getOp().equals(Operator.OR)); |
| } |
| return false; |
| } |
| |
| private boolean isExistsCondition(EObject eObject) { |
| if (eObject instanceof QuantifiedLaxCondition) { |
| QuantifiedLaxCondition cond = (QuantifiedLaxCondition) eObject; |
| return (cond.getQuantifier().equals(Quantifier.EXISTS)); |
| } |
| return false; |
| } |
| } |
