Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../img/srcFileCovDistChart8.png 62% of files have more coverage
64   244   39   4
42   137   0.61   16
16     2.44  
1    
 
  KernelNodeBo       Line # 37 64 39 76.2% 0.76229507
 
  (77)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.module;
17   
18    import org.qedeq.kernel.bo.common.NodeBo;
19    import org.qedeq.kernel.bo.common.QedeqBo;
20    import org.qedeq.kernel.se.base.list.Element;
21    import org.qedeq.kernel.se.base.module.ConditionalProof;
22    import org.qedeq.kernel.se.base.module.FormalProofLineList;
23    import org.qedeq.kernel.se.base.module.FormalProofList;
24    import org.qedeq.kernel.se.base.module.NodeType;
25    import org.qedeq.kernel.se.base.module.Proposition;
26    import org.qedeq.kernel.se.base.module.Reason;
27    import org.qedeq.kernel.se.common.CheckLevel;
28    import org.qedeq.kernel.se.common.ModuleContext;
29    import org.qedeq.kernel.se.dto.module.NodeVo;
30    import org.qedeq.kernel.se.visitor.QedeqNumbers;
31   
32    /**
33    * Business object for node access.
34    *
35    * @author Michael Meyling
36    */
 
37    public class KernelNodeBo implements NodeBo, CheckLevel {
38   
39    /** The plain node data. */
40    private final NodeVo node;
41   
42    /** The module context the node is within. */
43    private final ModuleContext context;
44   
45    /** Parent module the node is within. */
46    private final KernelQedeqBo qedeq;
47   
48    /** Herein are the results of various counters for the node. */
49    private final QedeqNumbers data;
50   
51    /** Are all formal formulas of this node well formed.
52    * See {@link CheckLevel} for value format. */
53    private int wellFormedCheck = UNCHECKED;
54   
55    /** Is this node been successfully formally proved at least once.
56    * See {@link CheckLevel} for value format. */
57    private int provedCheck = UNCHECKED;
58   
59   
60    /**
61    * Constructor.
62    *
63    * @param node The plain node data.
64    * @param context The module context the node is within.
65    * @param qedeq Parent module the node is within.
66    * @param data Herein are the results of various counters for the node.
67    */
 
68  18958 toggle public KernelNodeBo(final NodeVo node, final ModuleContext context, final KernelQedeqBo qedeq,
69    final QedeqNumbers data) {
70  18958 this.node = node;
71  18958 this.context = new ModuleContext(context);
72  18958 this.qedeq = qedeq;
73  18958 this.data = new QedeqNumbers(data);
74    }
75   
76    /**
77    * Get plain node data.
78    *
79    * @return The plain node data.
80    */
 
81  12997 toggle public NodeVo getNodeVo() {
82  12997 return node;
83    }
84   
85    /**
86    * Get module context the node is within.
87    *
88    * @return The module context the node is within.
89    */
 
90  0 toggle public ModuleContext getModuleContext() {
91  0 return context;
92    }
93   
94    /**
95    * Get parent module the node is within.
96    *
97    * @return Parent module the node is within.
98    */
 
99  0 toggle public QedeqBo getParentQedeqBo() {
100  0 return qedeq;
101    }
102   
103    /**
104    * Get parent module the node is within.
105    *
106    * @return Parent module the node is within.
107    */
 
108  157 toggle public KernelQedeqBo getQedeqBo() {
109  157 return qedeq;
110    }
111   
112    /**
113    * Get the results of various counters for the node.
114    *
115    * @return Herein are the results of various counters for the node.
116    */
 
117  1325 toggle public QedeqNumbers getNumbers() {
118  1325 return data;
119    }
120   
121    /**
122    * // FIXME 20110316 m31: we have to solve the uniqueness problem if we have several formal proofs
123    * Is the given name a proof line label within this node?
124    *
125    * @param label Look if this node is a proposition that contains this label name.
126    * @return Answer.
127    */
 
128  4759 toggle public boolean isProofLineLabel(final String label) {
129  4759 if (label == null || label.length() == 0) {
130  0 return false;
131    }
132  4759 final Proposition theorem = getNodeVo().getNodeType().getProposition();
133  4759 if (theorem == null) {
134  150 return false;
135    }
136  4609 final FormalProofList proofs = theorem.getFormalProofList();
137  4609 if (proofs == null) {
138  504 return false;
139    }
140    // iterate through all formal proofs
141  5240 for (int i = 0; i < proofs.size(); i++) {
142  4105 final FormalProofLineList list = proofs.get(i).getFormalProofLineList();
143  4105 if (hasProofLineLabel(label, list)) {
144  2970 return true;
145    }
146    }
147    // nowhere found:
148  1135 return false;
149    }
150   
 
151  6637 toggle private boolean hasProofLineLabel(final String label, final FormalProofLineList list) {
152  6637 if (list == null) {
153  0 return false;
154    }
155  40249 for (int j = 0; j < list.size(); j++) {
156  37470 if (label.equals(list.get(j).getLabel())) {
157  2598 return true;
158    }
159  34872 final Reason reason = list.get(j).getReason();
160  34872 if (reason instanceof ConditionalProof) {
161  2904 final ConditionalProof conditionalProof = (ConditionalProof) reason;
162  2904 if (conditionalProof.getHypothesis() != null) {
163  2904 if (label.equals(conditionalProof.getHypothesis().getLabel())) {
164  372 return true;
165    }
166    }
167  2532 final FormalProofLineList list2 = conditionalProof.getFormalProofLineList();
168  2532 if (hasProofLineLabel(label, list2)) {
169  888 return true;
170    }
171    }
172    }
173  2779 return false;
174    }
175   
176    /**
177    * Set proved parameter. See {@link #isWellFormed()}.
178    *
179    * @param wellFormedCheck Node well formed state.
180    * See {@link CheckLevel} for parameter format.
181    */
 
182  20171 toggle public void setWellFormed(final int wellFormedCheck) {
183  20171 this.wellFormedCheck = wellFormedCheck;
184    }
185   
 
186  140 toggle public boolean isWellFormed() {
187  140 return wellFormedCheck >= SUCCESS;
188    }
189   
 
190  11761 toggle public boolean isNotWellFormed() {
191  11761 return wellFormedCheck < SUCCESS && wellFormedCheck > UNCHECKED;
192    }
193   
194    /**
195    * Set proved parameter. See {@link #isProved()}.
196    *
197    * @param provedCheck Node proved state.
198    * See {@link CheckLevel} for parameter format.
199    */
 
200  548 toggle public void setProved(final int provedCheck) {
201  548 this.provedCheck = provedCheck;
202    }
203   
 
204  944 toggle public boolean isProved() {
205  944 return provedCheck >= SUCCESS;
206    }
207   
 
208  81 toggle public boolean isNotProved() {
209  81 return provedCheck < SUCCESS && provedCheck > UNCHECKED;
210    }
211   
 
212  314 toggle public boolean hasFormula() {
213  314 return null != getFormula();
214    }
215   
 
216  492 toggle public Element getFormula() {
217  492 if (getNodeVo() == null || getNodeVo().getNodeType() == null) {
218  0 return null;
219    }
220  492 final NodeType nodeType = getNodeVo().getNodeType();
221  492 if (nodeType.getProposition() != null) {
222  55 if (nodeType.getProposition().getFormula() != null) {
223  55 return nodeType.getProposition().getFormula().getElement();
224    }
225  0 return null;
226  437 } else if (nodeType.getPredicateDefinition() != null) {
227  0 if (nodeType.getPredicateDefinition().getFormula() != null) {
228  0 return nodeType.getPredicateDefinition().getFormula().getElement();
229    }
230  0 return null;
231  437 } else if (nodeType.getFunctionDefinition() != null) {
232  0 if (nodeType.getFunctionDefinition().getFormula() != null) {
233  0 return nodeType.getFunctionDefinition().getFormula().getElement();
234    }
235  0 return null;
236  437 } else if (nodeType.getAxiom() != null) {
237  437 if (nodeType.getAxiom().getFormula() != null) {
238  437 return nodeType.getAxiom().getFormula().getElement();
239    }
240  0 return null;
241    }
242  0 return null;
243    }
244    }