1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
package org.qedeq.kernel.bo.service.logic; |
17 |
|
|
18 |
|
import java.util.HashMap; |
19 |
|
import java.util.Iterator; |
20 |
|
import java.util.Map; |
21 |
|
|
22 |
|
import org.qedeq.base.io.Parameters; |
23 |
|
import org.qedeq.base.io.Version; |
24 |
|
import org.qedeq.base.trace.Trace; |
25 |
|
import org.qedeq.base.utility.EqualsUtility; |
26 |
|
import org.qedeq.base.utility.StringUtility; |
27 |
|
import org.qedeq.kernel.bo.log.QedeqLog; |
28 |
|
import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl; |
29 |
|
import org.qedeq.kernel.bo.logic.common.ExistenceChecker; |
30 |
|
import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory; |
31 |
|
import org.qedeq.kernel.bo.logic.common.FormulaUtility; |
32 |
|
import org.qedeq.kernel.bo.logic.common.FunctionConstant; |
33 |
|
import org.qedeq.kernel.bo.logic.common.FunctionKey; |
34 |
|
import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList; |
35 |
|
import org.qedeq.kernel.bo.logic.common.PredicateConstant; |
36 |
|
import org.qedeq.kernel.bo.logic.common.PredicateKey; |
37 |
|
import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl; |
38 |
|
import org.qedeq.kernel.bo.module.ControlVisitor; |
39 |
|
import org.qedeq.kernel.bo.module.InternalServiceCall; |
40 |
|
import org.qedeq.kernel.bo.module.InternalServiceProcess; |
41 |
|
import org.qedeq.kernel.bo.module.KernelModuleReferenceList; |
42 |
|
import org.qedeq.kernel.bo.module.KernelQedeqBo; |
43 |
|
import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker; |
44 |
|
import org.qedeq.kernel.bo.module.PluginExecutor; |
45 |
|
import org.qedeq.kernel.bo.service.dependency.LoadRequiredModulesPlugin; |
46 |
|
import org.qedeq.kernel.se.base.list.Element; |
47 |
|
import org.qedeq.kernel.se.base.list.ElementList; |
48 |
|
import org.qedeq.kernel.se.base.module.Axiom; |
49 |
|
import org.qedeq.kernel.se.base.module.ChangedRule; |
50 |
|
import org.qedeq.kernel.se.base.module.ChangedRuleList; |
51 |
|
import org.qedeq.kernel.se.base.module.ConditionalProof; |
52 |
|
import org.qedeq.kernel.se.base.module.FormalProof; |
53 |
|
import org.qedeq.kernel.se.base.module.FormalProofLine; |
54 |
|
import org.qedeq.kernel.se.base.module.FormalProofLineList; |
55 |
|
import org.qedeq.kernel.se.base.module.Formula; |
56 |
|
import org.qedeq.kernel.se.base.module.FunctionDefinition; |
57 |
|
import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
58 |
|
import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
59 |
|
import org.qedeq.kernel.se.base.module.PredicateDefinition; |
60 |
|
import org.qedeq.kernel.se.base.module.Proposition; |
61 |
|
import org.qedeq.kernel.se.base.module.Reason; |
62 |
|
import org.qedeq.kernel.se.base.module.Rule; |
63 |
|
import org.qedeq.kernel.se.base.module.Specification; |
64 |
|
import org.qedeq.kernel.se.base.module.SubstFree; |
65 |
|
import org.qedeq.kernel.se.base.module.SubstFunc; |
66 |
|
import org.qedeq.kernel.se.base.module.SubstPred; |
67 |
|
import org.qedeq.kernel.se.common.CheckLevel; |
68 |
|
import org.qedeq.kernel.se.common.IllegalModuleDataException; |
69 |
|
import org.qedeq.kernel.se.common.ModuleDataException; |
70 |
|
import org.qedeq.kernel.se.common.Plugin; |
71 |
|
import org.qedeq.kernel.se.common.RuleKey; |
72 |
|
import org.qedeq.kernel.se.common.SourceFileException; |
73 |
|
import org.qedeq.kernel.se.common.SourceFileExceptionList; |
74 |
|
import org.qedeq.kernel.se.dto.list.ElementSet; |
75 |
|
import org.qedeq.kernel.se.state.WellFormedState; |
76 |
|
import org.qedeq.kernel.se.visitor.InterruptException; |
77 |
|
|
78 |
|
|
79 |
|
|
80 |
|
|
81 |
|
|
82 |
|
|
83 |
|
@author |
84 |
|
|
|
|
| 71.5% |
Uncovered Elements: 194 (680) |
Complexity: 168 |
Complexity Density: 0.4 |
|
85 |
|
public final class WellFormedCheckerExecutor extends ControlVisitor implements PluginExecutor { |
86 |
|
|
87 |
|
|
88 |
|
private static final Class CLASS = WellFormedCheckerExecutor.class; |
89 |
|
|
90 |
|
|
91 |
|
private static final RuleKey CLASS_DEFINITION_VIA_FORMULA_RULE |
92 |
|
= new RuleKey("CLASS_DEFINITION_BY_FORMULA", "1.00.00"); |
93 |
|
|
94 |
|
|
95 |
|
private ModuleConstantsExistenceCheckerImpl existence; |
96 |
|
|
97 |
|
|
98 |
|
private FormulaCheckerFactory checkerFactory = null; |
99 |
|
|
100 |
|
|
101 |
|
|
102 |
|
|
103 |
|
@param |
104 |
|
@param |
105 |
|
@param |
106 |
|
|
|
|
| 58.8% |
Uncovered Elements: 7 (17) |
Complexity: 8 |
Complexity Density: 0.62 |
|
107 |
312
|
WellFormedCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,... |
108 |
|
final Parameters parameters) { |
109 |
312
|
super(plugin, qedeq); |
110 |
312
|
final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)"; |
111 |
312
|
final String checkerFactoryClass = parameters.getString("checkerFactory"); |
112 |
312
|
if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) { |
113 |
312
|
try { |
114 |
312
|
Class cl = Class.forName(checkerFactoryClass); |
115 |
312
|
checkerFactory = (FormulaCheckerFactory) cl.newInstance(); |
116 |
|
} catch (ClassNotFoundException e) { |
117 |
0
|
Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: " |
118 |
|
+ checkerFactoryClass, e); |
119 |
|
} catch (InstantiationException e) { |
120 |
0
|
Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: " |
121 |
|
+ checkerFactoryClass, e); |
122 |
|
} catch (IllegalAccessException e) { |
123 |
0
|
Trace.fatal(CLASS, this, method, |
124 |
|
"Programming error, access for instantiation failed for model: " |
125 |
|
+ checkerFactoryClass, e); |
126 |
|
} catch (RuntimeException e) { |
127 |
0
|
Trace.fatal(CLASS, this, method, |
128 |
|
"Programming error, instantiation failed for model: " + checkerFactoryClass, e); |
129 |
|
} |
130 |
|
} |
131 |
|
|
132 |
312
|
if (checkerFactory == null) { |
133 |
0
|
checkerFactory = new FormulaCheckerFactoryImpl(); |
134 |
|
} |
135 |
|
} |
136 |
|
|
|
|
| 89.2% |
Uncovered Elements: 7 (65) |
Complexity: 12 |
Complexity Density: 0.26 |
|
137 |
312
|
public Object executePlugin(final InternalServiceCall call, final Object data) throws InterruptException {... |
138 |
312
|
if (getQedeqBo().isWellFormed()) { |
139 |
0
|
return Boolean.TRUE; |
140 |
|
} |
141 |
312
|
QedeqLog.getInstance().logRequest( |
142 |
|
"Check logical well formedness", getQedeqBo().getUrl()); |
143 |
312
|
if (!getQedeqBo().hasLoadedRequiredModules()) { |
144 |
124
|
getServices().executePlugin(call.getInternalServiceProcess(), |
145 |
|
LoadRequiredModulesPlugin.class.getName(), getQedeqBo(), null); |
146 |
|
} |
147 |
312
|
if (!getQedeqBo().hasLoadedRequiredModules()) { |
148 |
0
|
final String msg = "Check of logical well formedness failed"; |
149 |
0
|
QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), |
150 |
|
"Not all required modules could be loaded."); |
151 |
0
|
return Boolean.FALSE; |
152 |
|
} |
153 |
312
|
getQedeqBo().setWellFormedProgressState(WellFormedState.STATE_EXTERNAL_CHECKING); |
154 |
312
|
getQedeqBo().getLabels().resetNodesToWellFormedUnchecked(); |
155 |
312
|
final SourceFileExceptionList sfl = new SourceFileExceptionList(); |
156 |
312
|
final Map rules = new HashMap(); |
157 |
312
|
final KernelModuleReferenceList list = getQedeqBo().getKernelRequiredModules(); |
158 |
481
|
for (int i = 0; i < list.size(); i++) { |
159 |
169
|
Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i)); |
160 |
169
|
getServices().checkWellFormedness(call.getInternalServiceProcess(), list.getKernelQedeqBo(i)); |
161 |
169
|
if (!list.getKernelQedeqBo(i).isWellFormed()) { |
162 |
6
|
ModuleDataException md = new CheckRequiredModuleException( |
163 |
|
LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE, |
164 |
|
LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT |
165 |
|
+ list.getQedeqBo(i).getModuleAddress(), |
166 |
|
list.getModuleContext(i)); |
167 |
6
|
sfl.add(getQedeqBo().createSourceFileException(getService(), md)); |
168 |
|
} |
169 |
169
|
final ModuleConstantsExistenceChecker existenceChecker |
170 |
|
= list.getKernelQedeqBo(i).getExistenceChecker(); |
171 |
169
|
if (existenceChecker != null) { |
172 |
169
|
final Iterator iter = existenceChecker.getRules().keySet().iterator(); |
173 |
1551
|
while (iter.hasNext()) { |
174 |
1382
|
final RuleKey key = (RuleKey) iter.next(); |
175 |
1382
|
final KernelQedeqBo newQedeq = existenceChecker.getQedeq(key); |
176 |
1382
|
final KernelQedeqBo previousQedeq = (KernelQedeqBo) rules.get(key); |
177 |
1382
|
if (previousQedeq != null && !newQedeq.equals(previousQedeq)) { |
178 |
2
|
ModuleDataException md = new CheckRequiredModuleException( |
179 |
|
LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE, |
180 |
|
LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT |
181 |
|
+ key + " " + previousQedeq.getUrl() + " " + newQedeq.getUrl(), |
182 |
|
list.getModuleContext(i)); |
183 |
2
|
sfl.add(getQedeqBo().createSourceFileException(getService(), md)); |
184 |
|
} else { |
185 |
1380
|
rules.put(key, newQedeq); |
186 |
|
} |
187 |
|
} |
188 |
|
} |
189 |
|
} |
190 |
|
|
191 |
312
|
if (sfl.size() > 0) { |
192 |
8
|
getQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_EXTERNAL_CHECKING_FAILED, sfl); |
193 |
8
|
final String msg = "Check of logical well formedness failed"; |
194 |
8
|
QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), |
195 |
|
StringUtility.replace(sfl.getMessage(), "\n", "\n\t")); |
196 |
8
|
return Boolean.FALSE; |
197 |
|
} |
198 |
304
|
getQedeqBo().setWellFormedProgressState(WellFormedState.STATE_INTERNAL_CHECKING); |
199 |
|
|
200 |
304
|
try { |
201 |
304
|
traverse(call.getInternalServiceProcess()); |
202 |
|
} catch (SourceFileExceptionList e) { |
203 |
26
|
getQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_INTERNAL_CHECKING_FAILED, e); |
204 |
26
|
getQedeqBo().setExistenceChecker(existence); |
205 |
26
|
final String msg = "Check of logical well formedness failed"; |
206 |
26
|
QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), |
207 |
|
StringUtility.replace(sfl.getMessage(), "\n", "\n\t")); |
208 |
26
|
return Boolean.FALSE; |
209 |
|
} |
210 |
278
|
getQedeqBo().setWellFormed(existence); |
211 |
278
|
QedeqLog.getInstance().logSuccessfulReply( |
212 |
|
"Check of logical well formedness successful", getQedeqBo().getUrl()); |
213 |
278
|
return Boolean.TRUE; |
214 |
|
} |
215 |
|
|
|
|
| 71.4% |
Uncovered Elements: 4 (14) |
Complexity: 4 |
Complexity Density: 0.4 |
|
216 |
304
|
public void traverse(final InternalServiceProcess process) throws SourceFileExceptionList {... |
217 |
304
|
try { |
218 |
304
|
this.existence = new ModuleConstantsExistenceCheckerImpl(getQedeqBo()); |
219 |
|
} catch (ModuleDataException me) { |
220 |
2
|
addError(me); |
221 |
2
|
throw getErrorList(); |
222 |
|
} |
223 |
302
|
super.traverse(process); |
224 |
|
|
225 |
|
|
226 |
278
|
setLocationWithinModule(""); |
227 |
278
|
if (getQedeqBo().getQedeq().getHeader() == null) { |
228 |
0
|
addError(new IllegalModuleDataException( |
229 |
|
LogicErrors.MODULE_HAS_NO_HEADER_CODE, |
230 |
|
LogicErrors.MODULE_HAS_NO_HEADER_TEXT, |
231 |
|
getCurrentContext())); |
232 |
|
} |
233 |
278
|
if (getQedeqBo().getQedeq().getHeader().getSpecification() == null) { |
234 |
0
|
addError(new IllegalModuleDataException( |
235 |
|
LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_CODE, |
236 |
|
LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT, |
237 |
|
getCurrentContext())); |
238 |
|
} |
239 |
|
} |
240 |
|
|
|
|
| 70% |
Uncovered Elements: 3 (10) |
Complexity: 3 |
Complexity Density: 0.38 |
|
241 |
555
|
public void visitEnter(final Specification specification) throws ModuleDataException {... |
242 |
555
|
if (specification == null) { |
243 |
0
|
return; |
244 |
|
} |
245 |
555
|
final String context = getCurrentContext().getLocationWithinModule(); |
246 |
|
|
247 |
555
|
setLocationWithinModule(context + ".getRuleVersion()"); |
248 |
555
|
final String version = specification.getRuleVersion(); |
249 |
555
|
try { |
250 |
555
|
new Version(version); |
251 |
|
} catch (RuntimeException e) { |
252 |
0
|
addError(new IllegalModuleDataException( |
253 |
|
LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE, |
254 |
|
LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(), |
255 |
|
getCurrentContext())); |
256 |
|
} |
257 |
|
} |
258 |
|
|
|
|
| 82.6% |
Uncovered Elements: 4 (23) |
Complexity: 5 |
Complexity Density: 0.33 |
|
259 |
2191
|
public void visitEnter(final Axiom axiom) throws ModuleDataException {... |
260 |
2191
|
if (axiom == null) { |
261 |
0
|
return; |
262 |
|
} |
263 |
2191
|
final String context = getCurrentContext().getLocationWithinModule(); |
264 |
|
|
265 |
2191
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
266 |
2191
|
if (axiom.getFormula() != null) { |
267 |
2191
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
268 |
2191
|
final Formula formula = axiom.getFormula(); |
269 |
2191
|
LogicalCheckExceptionList list = |
270 |
|
checkerFactory.createFormulaChecker().checkFormula( |
271 |
|
formula.getElement(), getCurrentContext(), existence); |
272 |
2203
|
for (int i = 0; i < list.size(); i++) { |
273 |
12
|
addError(list.get(i)); |
274 |
|
} |
275 |
|
} else { |
276 |
0
|
getNodeBo().setWellFormed(CheckLevel.FAILURE); |
277 |
|
} |
278 |
|
|
279 |
2191
|
if (!getNodeBo().isNotWellFormed()) { |
280 |
2181
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
281 |
|
} |
282 |
2191
|
setLocationWithinModule(context); |
283 |
2191
|
setBlocked(true); |
284 |
|
} |
285 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
286 |
2191
|
public void visitLeave(final Axiom axiom) {... |
287 |
2191
|
setBlocked(false); |
288 |
|
} |
289 |
|
|
|
|
| 63.8% |
Uncovered Elements: 42 (116) |
Complexity: 26 |
Complexity Density: 0.35 |
|
290 |
653
|
public void visitEnter(final PredicateDefinition definition)... |
291 |
|
throws ModuleDataException { |
292 |
653
|
if (definition == null) { |
293 |
0
|
return; |
294 |
|
} |
295 |
653
|
final String context = getCurrentContext().getLocationWithinModule(); |
296 |
|
|
297 |
653
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
298 |
653
|
final PredicateKey predicateKey = new PredicateKey(definition.getName(), |
299 |
|
definition.getArgumentNumber()); |
300 |
|
|
301 |
653
|
do { |
302 |
653
|
if (existence.predicateExists(predicateKey)) { |
303 |
0
|
addError(new IllegalModuleDataException( |
304 |
|
LogicErrors.PREDICATE_ALREADY_DEFINED_CODE, |
305 |
|
LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey, |
306 |
|
getCurrentContext())); |
307 |
0
|
break; |
308 |
|
} |
309 |
653
|
if (definition.getFormula() == null) { |
310 |
0
|
addError(new IllegalModuleDataException( |
311 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
312 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
313 |
|
getCurrentContext())); |
314 |
0
|
break; |
315 |
|
} |
316 |
653
|
final Element completeFormula = definition.getFormula().getElement(); |
317 |
653
|
if (completeFormula == null) { |
318 |
0
|
addError(new IllegalModuleDataException( |
319 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
320 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
321 |
|
getCurrentContext())); |
322 |
0
|
break; |
323 |
|
} |
324 |
653
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
325 |
653
|
if (completeFormula.isAtom()) { |
326 |
0
|
addError(new IllegalModuleDataException( |
327 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
328 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
329 |
|
getCurrentContext())); |
330 |
0
|
break; |
331 |
|
} |
332 |
653
|
final ElementList equi = completeFormula.getList(); |
333 |
653
|
final String operator = equi.getOperator(); |
334 |
653
|
if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR) |
335 |
|
|| equi.size() != 2) { |
336 |
0
|
addError(new IllegalModuleDataException( |
337 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE, |
338 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT, |
339 |
|
getCurrentContext())); |
340 |
0
|
break; |
341 |
|
} |
342 |
653
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)"); |
343 |
653
|
if (equi.getElement(0).isAtom()) { |
344 |
0
|
addError(new IllegalModuleDataException( |
345 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE, |
346 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT, |
347 |
|
getCurrentContext())); |
348 |
0
|
break; |
349 |
|
} |
350 |
653
|
final ElementList predicate = equi.getElement(0).getList(); |
351 |
653
|
if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) { |
352 |
0
|
addError(new IllegalModuleDataException( |
353 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE, |
354 |
|
LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT, |
355 |
|
getCurrentContext())); |
356 |
0
|
break; |
357 |
|
} |
358 |
653
|
final Element definingFormula = equi.getElement(1); |
359 |
|
|
360 |
653
|
final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula); |
361 |
2027
|
for (int i = 0; i < predicate.size(); i++) { |
362 |
1374
|
setLocationWithinModule(context |
363 |
|
+ ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")"); |
364 |
1374
|
if (i == 0) { |
365 |
653
|
if (!predicate.getElement(0).isAtom() |
366 |
|
|| !EqualsUtility.equals(definition.getName(), |
367 |
|
predicate.getElement(0).getAtom().getString())) { |
368 |
0
|
addError(new IllegalModuleDataException( |
369 |
|
LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE, |
370 |
|
LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT |
371 |
|
+ StringUtility.quote(definition.getName()) + " - " |
372 |
|
+ StringUtility.quote(predicate.getElement(0).getAtom().getString()), |
373 |
|
getCurrentContext())); |
374 |
0
|
continue; |
375 |
|
} |
376 |
721
|
} else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) { |
377 |
0
|
addError(new IllegalModuleDataException( |
378 |
|
LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE, |
379 |
|
LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i), |
380 |
|
getCurrentContext())); |
381 |
0
|
continue; |
382 |
|
} |
383 |
1374
|
setLocationWithinModule(context |
384 |
|
+ ".getFormula().getElement().getList().getElement(1)"); |
385 |
1374
|
if (i != 0 && !free.contains(predicate.getElement(i))) { |
386 |
1
|
addError(new IllegalModuleDataException( |
387 |
|
LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE, |
388 |
|
LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i), |
389 |
|
getCurrentContext())); |
390 |
|
} |
391 |
|
} |
392 |
653
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
393 |
653
|
if (predicate.size() - 1 != free.size()) { |
394 |
0
|
addError(new IllegalModuleDataException( |
395 |
|
LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE, |
396 |
|
LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT, |
397 |
|
getCurrentContext())); |
398 |
|
} |
399 |
653
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"); |
400 |
653
|
final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula( |
401 |
|
definingFormula, getCurrentContext(), existence); |
402 |
653
|
for (int i = 0; i < list.size(); i++) { |
403 |
0
|
addError(list.get(i)); |
404 |
|
} |
405 |
653
|
if (list.size() > 0) { |
406 |
0
|
break; |
407 |
|
} |
408 |
653
|
setLocationWithinModule(context + ".getFormula().getElement().getList()"); |
409 |
653
|
final PredicateConstant constant = new PredicateConstant(predicateKey, |
410 |
|
equi, getCurrentContext()); |
411 |
653
|
setLocationWithinModule(context); |
412 |
653
|
if (existence.predicateExists(predicateKey)) { |
413 |
0
|
addError(new IllegalModuleDataException( |
414 |
|
LogicErrors.PREDICATE_ALREADY_DEFINED_CODE, |
415 |
|
LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT |
416 |
|
+ predicateKey, getCurrentContext())); |
417 |
0
|
break; |
418 |
|
} |
419 |
|
|
420 |
653
|
if (!getNodeBo().isNotWellFormed()) { |
421 |
652
|
existence.add(constant); |
422 |
652
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
423 |
652
|
final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker() |
424 |
|
.checkFormula(completeFormula, getCurrentContext(), existence); |
425 |
652
|
for (int i = 0; i < errorlist.size(); i++) { |
426 |
0
|
addError(errorlist.get(i)); |
427 |
|
} |
428 |
|
} |
429 |
|
} while (false); |
430 |
|
|
431 |
|
|
432 |
653
|
setLocationWithinModule(context); |
433 |
653
|
if ("2".equals(predicateKey.getArguments()) |
434 |
|
&& ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) { |
435 |
0
|
existence.setIdentityOperatorDefined(predicateKey.getName(), |
436 |
|
getQedeqBo(), getCurrentContext()); |
437 |
|
} |
438 |
|
|
439 |
653
|
if (!getNodeBo().isNotWellFormed()) { |
440 |
652
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
441 |
|
} |
442 |
653
|
setBlocked(true); |
443 |
|
} |
444 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
445 |
653
|
public void visitLeave(final PredicateDefinition definition) {... |
446 |
653
|
setBlocked(false); |
447 |
|
} |
448 |
|
|
|
|
| 77.3% |
Uncovered Elements: 5 (22) |
Complexity: 6 |
Complexity Density: 0.43 |
|
449 |
205
|
public void visitEnter(final InitialPredicateDefinition definition)... |
450 |
|
throws ModuleDataException { |
451 |
205
|
if (definition == null) { |
452 |
0
|
return; |
453 |
|
} |
454 |
205
|
final String context = getCurrentContext().getLocationWithinModule(); |
455 |
|
|
456 |
205
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
457 |
205
|
final PredicateKey predicateKey = new PredicateKey( |
458 |
|
definition.getName(), definition.getArgumentNumber()); |
459 |
205
|
setLocationWithinModule(context); |
460 |
205
|
if (existence.predicateExists(predicateKey)) { |
461 |
0
|
addError(new IllegalModuleDataException( |
462 |
|
LogicErrors.PREDICATE_ALREADY_DEFINED_CODE, |
463 |
|
LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT |
464 |
|
+ predicateKey, getCurrentContext())); |
465 |
|
} |
466 |
205
|
existence.add(definition); |
467 |
|
|
468 |
205
|
if ("2".equals(predicateKey.getArguments()) |
469 |
|
&& ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) { |
470 |
106
|
existence.setIdentityOperatorDefined(predicateKey.getName(), |
471 |
|
getQedeqBo(), getCurrentContext()); |
472 |
|
} |
473 |
|
|
474 |
199
|
if (!getNodeBo().isNotWellFormed()) { |
475 |
199
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
476 |
|
} |
477 |
199
|
setBlocked(true); |
478 |
|
} |
479 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
480 |
199
|
public void visitLeave(final InitialPredicateDefinition definition) {... |
481 |
199
|
setBlocked(false); |
482 |
|
} |
483 |
|
|
|
|
| 0% |
Uncovered Elements: 18 (18) |
Complexity: 4 |
Complexity Density: 0.33 |
|
484 |
0
|
public void visitEnter(final InitialFunctionDefinition definition)... |
485 |
|
throws ModuleDataException { |
486 |
0
|
if (definition == null) { |
487 |
0
|
return; |
488 |
|
} |
489 |
0
|
final String context = getCurrentContext().getLocationWithinModule(); |
490 |
|
|
491 |
0
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
492 |
0
|
final FunctionKey function = new FunctionKey(definition.getName(), |
493 |
|
definition.getArgumentNumber()); |
494 |
0
|
if (existence.functionExists(function)) { |
495 |
0
|
addError(new IllegalModuleDataException( |
496 |
|
LogicErrors.FUNCTION_ALREADY_DEFINED_CODE, |
497 |
|
LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function, |
498 |
|
getCurrentContext())); |
499 |
|
} |
500 |
0
|
existence.add(definition); |
501 |
0
|
setLocationWithinModule(context); |
502 |
|
|
503 |
0
|
if (!getNodeBo().isNotWellFormed()) { |
504 |
0
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
505 |
|
} |
506 |
0
|
setBlocked(true); |
507 |
|
} |
508 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
509 |
0
|
public void visitLeave(final InitialFunctionDefinition definition) {... |
510 |
0
|
setBlocked(false); |
511 |
|
} |
512 |
|
|
|
|
| 58.7% |
Uncovered Elements: 57 (138) |
Complexity: 28 |
Complexity Density: 0.32 |
|
513 |
1045
|
public void visitEnter(final FunctionDefinition definition)... |
514 |
|
throws ModuleDataException { |
515 |
1045
|
if (definition == null) { |
516 |
0
|
return; |
517 |
|
} |
518 |
1045
|
final String context = getCurrentContext().getLocationWithinModule(); |
519 |
|
|
520 |
1045
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
521 |
1045
|
final FunctionKey function = new FunctionKey(definition.getName(), |
522 |
|
definition.getArgumentNumber()); |
523 |
|
|
524 |
1045
|
do { |
525 |
1045
|
if (existence.functionExists(function)) { |
526 |
0
|
addError(new IllegalModuleDataException( |
527 |
|
LogicErrors.FUNCTION_ALREADY_DEFINED_CODE, |
528 |
|
LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT |
529 |
|
+ function, getCurrentContext())); |
530 |
0
|
break; |
531 |
|
} |
532 |
1045
|
if (definition.getFormula() == null) { |
533 |
0
|
addError(new IllegalModuleDataException( |
534 |
|
LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE, |
535 |
|
LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT, |
536 |
|
getCurrentContext())); |
537 |
0
|
break; |
538 |
|
} |
539 |
1045
|
final Formula formulaArgument = definition.getFormula(); |
540 |
1045
|
setLocationWithinModule(context + ".getFormula()"); |
541 |
1045
|
if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) { |
542 |
0
|
addError(new IllegalModuleDataException( |
543 |
|
LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE, |
544 |
|
LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT, |
545 |
|
getCurrentContext())); |
546 |
0
|
break; |
547 |
|
} |
548 |
1045
|
final ElementList formula = formulaArgument.getElement().getList(); |
549 |
1045
|
setLocationWithinModule(context + ".getFormula().getElement().getList()"); |
550 |
1045
|
if (!existence.identityOperatorExists()) { |
551 |
1
|
addError(new IllegalModuleDataException( |
552 |
|
LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE, |
553 |
|
LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT, |
554 |
|
getCurrentContext())); |
555 |
1
|
break; |
556 |
|
} |
557 |
1044
|
if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) { |
558 |
0
|
addError(new IllegalModuleDataException( |
559 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
560 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
561 |
|
getCurrentContext())); |
562 |
0
|
break; |
563 |
|
} |
564 |
1044
|
if (formula.size() != 3) { |
565 |
0
|
addError(new IllegalModuleDataException( |
566 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
567 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
568 |
|
getCurrentContext())); |
569 |
0
|
break; |
570 |
|
} |
571 |
1044
|
if (!formula.getElement(0).isAtom()) { |
572 |
0
|
addError(new IllegalModuleDataException( |
573 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
574 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
575 |
|
getCurrentContext())); |
576 |
0
|
break; |
577 |
|
} |
578 |
1044
|
if (!EqualsUtility.equals(existence.getIdentityOperator(), |
579 |
|
formula.getElement(0).getAtom().getString())) { |
580 |
0
|
addError(new IllegalModuleDataException( |
581 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE, |
582 |
|
LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT, |
583 |
|
getCurrentContext())); |
584 |
0
|
break; |
585 |
|
} |
586 |
1044
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"); |
587 |
1044
|
if (formula.getElement(1).isAtom()) { |
588 |
0
|
addError(new IllegalModuleDataException( |
589 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
590 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
591 |
|
getCurrentContext())); |
592 |
0
|
break; |
593 |
|
} |
594 |
1044
|
final ElementList functionConstant = formula.getElement(1).getList(); |
595 |
1044
|
if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) { |
596 |
0
|
addError(new IllegalModuleDataException( |
597 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
598 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
599 |
|
getCurrentContext())); |
600 |
0
|
break; |
601 |
|
} |
602 |
1044
|
setLocationWithinModule(context |
603 |
|
+ ".getFormula().getElement().getList().getElement(1).getList()"); |
604 |
1044
|
final int size = functionConstant.size(); |
605 |
1044
|
if (!("" + (size - 1)).equals(definition.getArgumentNumber())) { |
606 |
0
|
addError(new IllegalModuleDataException( |
607 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
608 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
609 |
|
getCurrentContext())); |
610 |
0
|
break; |
611 |
|
} |
612 |
1044
|
setLocationWithinModule(context |
613 |
|
+ ".getFormula().getElement().getList().getElement(1).getList().getElement(0)"); |
614 |
1044
|
if (!functionConstant.getElement(0).isAtom()) { |
615 |
0
|
addError(new IllegalModuleDataException( |
616 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
617 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
618 |
|
getCurrentContext())); |
619 |
0
|
break; |
620 |
|
} |
621 |
1044
|
if (!EqualsUtility.equals(definition.getName(), |
622 |
|
functionConstant.getElement(0).getAtom().getString())) { |
623 |
0
|
addError(new IllegalModuleDataException( |
624 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE, |
625 |
|
LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT, |
626 |
|
getCurrentContext())); |
627 |
0
|
break; |
628 |
|
} |
629 |
1044
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)"); |
630 |
1044
|
if (formula.getElement(2).isAtom()) { |
631 |
0
|
addError(new IllegalModuleDataException( |
632 |
|
LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE, |
633 |
|
LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT, |
634 |
|
getCurrentContext())); |
635 |
0
|
break; |
636 |
|
} |
637 |
1044
|
final ElementList term = formula.getElement(2).getList(); |
638 |
1044
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"); |
639 |
1044
|
final ElementSet free = FormulaUtility.getFreeSubjectVariables(term); |
640 |
1044
|
if (size - 1 != free.size()) { |
641 |
0
|
addError(new IllegalModuleDataException( |
642 |
|
LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE, |
643 |
|
LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT, |
644 |
|
getCurrentContext())); |
645 |
0
|
break; |
646 |
|
} |
647 |
1044
|
if (functionConstant.getElement(0).isList() |
648 |
|
|| !EqualsUtility.equals(function.getName(), |
649 |
|
functionConstant.getElement(0).getAtom().getString())) { |
650 |
0
|
addError(new IllegalModuleDataException( |
651 |
|
LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_CODE, |
652 |
|
LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_TEXT |
653 |
|
+ function.getName(), getCurrentContext())); |
654 |
|
} |
655 |
2222
|
for (int i = 1; i < size; i++) { |
656 |
1178
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)" |
657 |
|
+ ".getList().getElement(" + i + ")"); |
658 |
1178
|
if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) { |
659 |
0
|
addError(new IllegalModuleDataException( |
660 |
|
LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE, |
661 |
|
LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT |
662 |
|
+ functionConstant.getElement(i), getCurrentContext())); |
663 |
|
} |
664 |
1178
|
if (!free.contains(functionConstant.getElement(i))) { |
665 |
0
|
addError(new IllegalModuleDataException( |
666 |
|
LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE, |
667 |
|
LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT |
668 |
|
+ functionConstant.getElement(i), getCurrentContext())); |
669 |
|
} |
670 |
|
} |
671 |
1044
|
setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)"); |
672 |
1044
|
final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker() |
673 |
|
.checkTerm(term, getCurrentContext(), existence); |
674 |
1044
|
for (int i = 0; i < list.size(); i++) { |
675 |
0
|
addError(list.get(i)); |
676 |
|
} |
677 |
1044
|
if (list.size() > 0) { |
678 |
0
|
break; |
679 |
|
} |
680 |
1044
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
681 |
|
|
682 |
1044
|
if (!getNodeBo().isNotWellFormed()) { |
683 |
1044
|
existence.add(new FunctionConstant(function, formula, getCurrentContext())); |
684 |
|
|
685 |
1044
|
final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker() |
686 |
|
.checkFormula(formulaArgument.getElement(), getCurrentContext(), existence); |
687 |
1044
|
for (int i = 0; i < listComplete.size(); i++) { |
688 |
0
|
addError(listComplete.get(i)); |
689 |
|
} |
690 |
|
} |
691 |
|
} while (false); |
692 |
1045
|
setLocationWithinModule(context); |
693 |
|
|
694 |
1045
|
if (!getNodeBo().isNotWellFormed()) { |
695 |
1044
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
696 |
|
} |
697 |
1045
|
setBlocked(true); |
698 |
|
} |
699 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
700 |
1045
|
public void visitLeave(final FunctionDefinition definition) {... |
701 |
1045
|
setBlocked(false); |
702 |
|
} |
703 |
|
|
|
|
| 86.1% |
Uncovered Elements: 5 (36) |
Complexity: 8 |
Complexity Density: 0.36 |
|
704 |
4385
|
public void visitEnter(final Proposition proposition)... |
705 |
|
throws ModuleDataException { |
706 |
4385
|
if (proposition == null) { |
707 |
0
|
return; |
708 |
|
} |
709 |
4385
|
final String context = getCurrentContext().getLocationWithinModule(); |
710 |
|
|
711 |
4385
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
712 |
4385
|
if (proposition.getFormula() != null) { |
713 |
4385
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
714 |
4385
|
final Formula formula = proposition.getFormula(); |
715 |
4385
|
LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula( |
716 |
|
formula.getElement(), getCurrentContext(), existence); |
717 |
4391
|
for (int i = 0; i < list.size(); i++) { |
718 |
6
|
addError(list.get(i)); |
719 |
|
} |
720 |
|
} else { |
721 |
0
|
getNodeBo().setWellFormed(CheckLevel.FAILURE); |
722 |
|
} |
723 |
4385
|
if (proposition.getFormalProofList() != null) { |
724 |
1002
|
for (int i = 0; i < proposition.getFormalProofList().size(); i++) { |
725 |
501
|
final FormalProof proof = proposition.getFormalProofList().get(i); |
726 |
501
|
if (proof != null) { |
727 |
501
|
final FormalProofLineList list = proof.getFormalProofLineList(); |
728 |
501
|
setLocationWithinModule(context + ".getFormalProofList().get(" |
729 |
|
+ i + ").getFormalProofLineList()"); |
730 |
501
|
checkFormalProof(list); |
731 |
|
} |
732 |
|
} |
733 |
|
} |
734 |
4385
|
setLocationWithinModule(context); |
735 |
|
|
736 |
4385
|
if (!getNodeBo().isNotWellFormed()) { |
737 |
4380
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
738 |
|
} |
739 |
4385
|
setBlocked(true); |
740 |
|
} |
741 |
|
|
742 |
|
|
743 |
|
|
744 |
|
|
745 |
|
@param |
746 |
|
|
|
|
| 90% |
Uncovered Elements: 1 (10) |
Complexity: 3 |
Complexity Density: 0.5 |
|
747 |
901
|
private void checkFormalProof(final FormalProofLineList list) {... |
748 |
901
|
final String context = getCurrentContext().getLocationWithinModule(); |
749 |
901
|
if (list != null) { |
750 |
6393
|
for (int i = 0; i < list.size(); i++) { |
751 |
5492
|
final FormalProofLine line = list.get(i); |
752 |
5492
|
setLocationWithinModule(context + ".get(" + i + ")"); |
753 |
5492
|
checkProofLine(line); |
754 |
|
} |
755 |
|
} |
756 |
|
} |
757 |
|
|
758 |
|
|
759 |
|
|
760 |
|
|
761 |
|
@param |
762 |
|
|
|
|
| 87.3% |
Uncovered Elements: 7 (55) |
Complexity: 13 |
Complexity Density: 0.42 |
|
763 |
5492
|
private void checkProofLine(final FormalProofLine line) {... |
764 |
5492
|
if (line instanceof ConditionalProof) { |
765 |
400
|
checkProofLine((ConditionalProof) line); |
766 |
400
|
return; |
767 |
|
} |
768 |
5092
|
final String context = getCurrentContext().getLocationWithinModule(); |
769 |
5092
|
LogicalCheckExceptionList elist = new LogicalCheckExceptionList(); |
770 |
5092
|
if (line != null) { |
771 |
5092
|
final Formula formula = line.getFormula(); |
772 |
5092
|
if (formula != null) { |
773 |
5092
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
774 |
5092
|
elist = checkerFactory.createFormulaChecker().checkFormula( |
775 |
|
formula.getElement(), getCurrentContext(), existence); |
776 |
5092
|
for (int k = 0; k < elist.size(); k++) { |
777 |
0
|
addError(elist.get(k)); |
778 |
|
} |
779 |
|
} |
780 |
5092
|
final Reason reason = line.getReason(); |
781 |
5092
|
if (reason != null) { |
782 |
5092
|
if (reason instanceof SubstFree) { |
783 |
175
|
final SubstFree subst = (SubstFree) reason; |
784 |
175
|
if (subst.getSubstFree().getSubstituteTerm() != null) { |
785 |
165
|
setLocationWithinModule(context |
786 |
|
+ ".getReason().getSubstFree().getSubstituteTerm()"); |
787 |
165
|
elist = checkerFactory.createFormulaChecker().checkTerm( |
788 |
|
subst.getSubstFree().getSubstituteTerm(), |
789 |
|
getCurrentContext(), existence); |
790 |
|
} |
791 |
4917
|
} else if (reason instanceof SubstPred) { |
792 |
1909
|
final SubstPred subst = (SubstPred) reason; |
793 |
1909
|
if (subst.getSubstPred().getSubstituteFormula() != null) { |
794 |
1819
|
setLocationWithinModule(context |
795 |
|
+ ".getReason().getSubstPred().getSubstituteFormula()"); |
796 |
1819
|
elist = checkerFactory.createFormulaChecker().checkFormula( |
797 |
|
subst.getSubstPred().getSubstituteFormula(), |
798 |
|
getCurrentContext(), existence); |
799 |
|
} |
800 |
3008
|
} else if (reason instanceof SubstFunc) { |
801 |
51
|
final SubstFunc subst = (SubstFunc) reason; |
802 |
51
|
if (subst.getSubstFunc().getSubstituteTerm() != null) { |
803 |
41
|
setLocationWithinModule(context |
804 |
|
+ ".getReason().getSubstFunc().getSubstituteTerm()"); |
805 |
41
|
elist = checkerFactory.createFormulaChecker().checkTerm( |
806 |
|
subst.getSubstFunc().getSubstituteTerm(), |
807 |
|
getCurrentContext(), existence); |
808 |
|
} |
809 |
|
} |
810 |
5092
|
for (int k = 0; k < elist.size(); k++) { |
811 |
0
|
addError(elist.get(k)); |
812 |
|
} |
813 |
|
} |
814 |
|
} |
815 |
|
} |
816 |
|
|
817 |
|
|
818 |
|
|
819 |
|
|
820 |
|
@param |
821 |
|
|
|
|
| 72.9% |
Uncovered Elements: 13 (48) |
Complexity: 14 |
Complexity Density: 0.5 |
|
822 |
400
|
private void checkProofLine(final ConditionalProof line) {... |
823 |
400
|
final String context = getCurrentContext().getLocationWithinModule(); |
824 |
400
|
LogicalCheckExceptionList elist = new LogicalCheckExceptionList(); |
825 |
400
|
if (line != null) { |
826 |
|
{ |
827 |
400
|
final Formula formula = line.getFormula(); |
828 |
400
|
if (formula != null && formula.getElement() != null) { |
829 |
400
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
830 |
400
|
elist = checkerFactory.createFormulaChecker().checkFormula( |
831 |
|
formula.getElement(), getCurrentContext(), existence); |
832 |
400
|
for (int k = 0; k < elist.size(); k++) { |
833 |
0
|
addError(elist.get(k)); |
834 |
|
} |
835 |
|
} |
836 |
|
} |
837 |
400
|
if (line.getHypothesis() != null) { |
838 |
400
|
final Formula formula = line.getHypothesis().getFormula();; |
839 |
400
|
if (formula != null && formula.getElement() != null) { |
840 |
400
|
setLocationWithinModule(context |
841 |
|
+ ".getHypothesis().getFormula().getElement()"); |
842 |
400
|
elist = checkerFactory.createFormulaChecker().checkFormula( |
843 |
|
formula.getElement(), getCurrentContext(), existence); |
844 |
400
|
for (int k = 0; k < elist.size(); k++) { |
845 |
0
|
addError(elist.get(k)); |
846 |
|
} |
847 |
|
} |
848 |
|
} |
849 |
400
|
if (line.getFormalProofLineList() != null) { |
850 |
400
|
setLocationWithinModule(context + ".getFormalProofLineList()"); |
851 |
400
|
checkFormalProof(line.getFormalProofLineList()); |
852 |
|
} |
853 |
400
|
if (line.getConclusion() != null) { |
854 |
400
|
final Formula formula = line.getConclusion().getFormula();; |
855 |
400
|
if (formula != null && formula.getElement() != null) { |
856 |
400
|
setLocationWithinModule(context |
857 |
|
+ ".getConclusion().getFormula().getElement()"); |
858 |
400
|
elist = checkerFactory.createFormulaChecker().checkFormula( |
859 |
|
formula.getElement(), getCurrentContext(), existence); |
860 |
400
|
for (int k = 0; k < elist.size(); k++) { |
861 |
0
|
addError(elist.get(k)); |
862 |
|
} |
863 |
|
} |
864 |
|
} |
865 |
|
} |
866 |
|
} |
867 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
868 |
4385
|
public void visitLeave(final Proposition definition) {... |
869 |
4385
|
setBlocked(false); |
870 |
|
} |
871 |
|
|
|
|
| 73.5% |
Uncovered Elements: 18 (68) |
Complexity: 23 |
Complexity Density: 0.52 |
|
872 |
1591
|
public void visitEnter(final Rule rule) throws ModuleDataException {... |
873 |
1591
|
final String context = getCurrentContext().getLocationWithinModule(); |
874 |
|
|
875 |
1591
|
getNodeBo().setWellFormed(CheckLevel.UNCHECKED); |
876 |
1591
|
final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion()); |
877 |
1591
|
if (rule.getName() != null && rule.getName().length() > 0 && rule.getVersion() != null |
878 |
|
&& rule.getVersion().length() > 0) { |
879 |
1591
|
try { |
880 |
1591
|
setLocationWithinModule(context + ".getVersion()"); |
881 |
1591
|
new Version(rule.getVersion()); |
882 |
|
} catch (RuntimeException e) { |
883 |
0
|
addError(new IllegalModuleDataException( |
884 |
|
LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE, |
885 |
|
LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(), |
886 |
|
getCurrentContext())); |
887 |
|
} |
888 |
1591
|
if (existence.ruleExists(ruleKey)) { |
889 |
2
|
addError(new IllegalModuleDataException( |
890 |
|
LogicErrors.RULE_ALREADY_DEFINED_CODE, |
891 |
|
LogicErrors.RULE_ALREADY_DEFINED_TEXT |
892 |
|
+ ruleKey + " " + existence.getQedeq(ruleKey).getUrl(), |
893 |
|
getCurrentContext())); |
894 |
|
} else { |
895 |
1589
|
if (CLASS_DEFINITION_VIA_FORMULA_RULE.equals(ruleKey)) { |
896 |
|
|
897 |
|
|
898 |
75
|
existence.setClassOperatorModule(getQedeqBo(), |
899 |
|
getCurrentContext()); |
900 |
|
} |
901 |
1589
|
existence.add(ruleKey, rule); |
902 |
|
} |
903 |
1591
|
if (rule.getChangedRuleList() != null) { |
904 |
8
|
final ChangedRuleList list = rule.getChangedRuleList(); |
905 |
72
|
for (int i = 0; i < list.size(); i++) { |
906 |
64
|
setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ")"); |
907 |
64
|
final ChangedRule r = list.get(i); |
908 |
64
|
if (r == null || r.getName() == null || r.getName().length() <= 0 |
909 |
|
|| r.getVersion() == null || r.getVersion().length() <= 0) { |
910 |
0
|
addError(new IllegalModuleDataException( |
911 |
|
LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE, |
912 |
|
LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT |
913 |
0
|
+ (r == null ? "null" : r.getName() + " [" + r.getVersion() + "]"), |
914 |
|
getCurrentContext())); |
915 |
0
|
continue; |
916 |
|
} |
917 |
64
|
setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()"); |
918 |
64
|
final String ruleName = r.getName(); |
919 |
64
|
final String ruleVersion = r.getVersion(); |
920 |
64
|
try { |
921 |
64
|
new Version(ruleVersion); |
922 |
|
} catch (RuntimeException e) { |
923 |
0
|
addError(new IllegalModuleDataException( |
924 |
|
LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE, |
925 |
|
LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(), |
926 |
|
getCurrentContext())); |
927 |
|
} |
928 |
64
|
RuleKey key1 = getLocalRuleKey(ruleName); |
929 |
64
|
if (key1 == null) { |
930 |
0
|
key1 = existence.getParentRuleKey(ruleName); |
931 |
|
} |
932 |
64
|
if (key1 == null) { |
933 |
0
|
addError(new IllegalModuleDataException( |
934 |
|
LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_CODE, |
935 |
|
LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_TEXT |
936 |
|
+ ruleName, getCurrentContext())); |
937 |
|
} else { |
938 |
64
|
final RuleKey key2 = new RuleKey(ruleName, ruleVersion); |
939 |
64
|
if (existence.ruleExists(key2)) { |
940 |
0
|
addError(new IllegalModuleDataException( |
941 |
|
LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_CODE, |
942 |
|
LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_TEXT |
943 |
|
+ ruleName, getCurrentContext(), getQedeqBo().getLabels() |
944 |
|
.getRuleContext(key2))); |
945 |
|
} else { |
946 |
64
|
try { |
947 |
64
|
if (!Version.less(key1.getVersion(), key2.getVersion())) { |
948 |
0
|
addError(new IllegalModuleDataException( |
949 |
|
LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE, |
950 |
|
LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT |
951 |
|
+ key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels() |
952 |
|
.getRuleContext(key2))); |
953 |
|
} |
954 |
|
} catch (RuntimeException e) { |
955 |
0
|
addError(new IllegalModuleDataException( |
956 |
|
LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE, |
957 |
|
LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT |
958 |
|
+ key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels() |
959 |
|
.getRuleContext(key2))); |
960 |
|
} |
961 |
|
} |
962 |
64
|
existence.add(key2, rule); |
963 |
|
} |
964 |
|
} |
965 |
|
} |
966 |
|
} else { |
967 |
0
|
addError(new IllegalModuleDataException( |
968 |
|
LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE, |
969 |
|
LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT |
970 |
|
+ ruleKey, getCurrentContext())); |
971 |
|
} |
972 |
|
|
973 |
1591
|
if (!getNodeBo().isNotWellFormed()) { |
974 |
1589
|
getNodeBo().setWellFormed(CheckLevel.SUCCESS); |
975 |
|
} |
976 |
1591
|
setBlocked(true); |
977 |
|
} |
978 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
979 |
1591
|
public void visitLeave(final Rule rule) {... |
980 |
1591
|
setBlocked(false); |
981 |
|
} |
982 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
983 |
30
|
protected void addError(final ModuleDataException me) {... |
984 |
30
|
if (getNodeBo() != null) { |
985 |
28
|
getNodeBo().setWellFormed(CheckLevel.FAILURE); |
986 |
|
} |
987 |
30
|
super.addError(me); |
988 |
|
} |
989 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
990 |
30
|
protected void addError(final SourceFileException me) {... |
991 |
30
|
if (getNodeBo() != null) { |
992 |
28
|
getNodeBo().setWellFormed(CheckLevel.FAILURE); |
993 |
|
} |
994 |
30
|
super.addError(me); |
995 |
|
} |
996 |
|
|
997 |
|
} |