1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
|
|
18 |
|
package org.qedeq.kernel.bo.logic; |
19 |
|
|
20 |
|
import org.qedeq.base.trace.Trace; |
21 |
|
import org.qedeq.kernel.base.list.Atom; |
22 |
|
import org.qedeq.kernel.base.list.Element; |
23 |
|
import org.qedeq.kernel.base.list.ElementList; |
24 |
|
import org.qedeq.kernel.bo.logic.wf.ElementCheckException; |
25 |
|
import org.qedeq.kernel.bo.logic.wf.EverythingExists; |
26 |
|
import org.qedeq.kernel.bo.logic.wf.ExistenceChecker; |
27 |
|
import org.qedeq.kernel.bo.logic.wf.FormulaBasicErrors; |
28 |
|
import org.qedeq.kernel.bo.logic.wf.FormulaCheckException; |
29 |
|
import org.qedeq.kernel.bo.logic.wf.LogicalCheckExceptionList; |
30 |
|
import org.qedeq.kernel.bo.logic.wf.Operators; |
31 |
|
import org.qedeq.kernel.bo.logic.wf.TermCheckException; |
32 |
|
import org.qedeq.kernel.common.ModuleContext; |
33 |
|
import org.qedeq.kernel.dto.list.ElementSet; |
34 |
|
|
35 |
|
|
36 |
|
|
37 |
|
@link |
38 |
|
|
39 |
|
|
40 |
|
|
41 |
|
@link |
42 |
|
|
43 |
|
|
44 |
|
@version |
45 |
|
@author |
46 |
|
|
|
|
| 94,4% |
Uncovered Elements: 24 (429) |
Complexity: 114 |
Complexity Density: 0,41 |
|
47 |
|
public final class FormulaChecker implements Operators, FormulaBasicErrors { |
48 |
|
|
49 |
|
|
50 |
|
|
51 |
|
|
52 |
|
|
53 |
|
|
54 |
|
|
55 |
|
|
56 |
|
|
57 |
|
|
58 |
|
|
59 |
|
|
60 |
|
|
61 |
|
private static final Class CLASS = FormulaChecker.class; |
62 |
|
|
63 |
|
|
64 |
|
private final ModuleContext currentContext; |
65 |
|
|
66 |
|
|
67 |
|
private final ExistenceChecker existenceChecker; |
68 |
|
|
69 |
|
|
70 |
|
private final LogicalCheckExceptionList exceptions; |
71 |
|
|
72 |
|
|
73 |
|
|
74 |
|
|
75 |
|
|
76 |
|
@param |
77 |
|
@param |
78 |
|
@throws |
79 |
|
|
80 |
|
|
81 |
|
|
|
|
| 71,4% |
Uncovered Elements: 2 (7) |
Complexity: 3 |
Complexity Density: 0,6 |
|
82 |
1018
|
private FormulaChecker(final ModuleContext context,... |
83 |
|
final ExistenceChecker existenceChecker) { |
84 |
1018
|
this.existenceChecker = existenceChecker; |
85 |
1018
|
if (existenceChecker.equalityOperatorExists() |
86 |
|
&& !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) { |
87 |
0
|
throw new IllegalArgumentException("equality predicate should exist, but it doesn't"); |
88 |
|
} |
89 |
1018
|
currentContext = new ModuleContext(context); |
90 |
1018
|
exceptions = new LogicalCheckExceptionList(); |
91 |
|
} |
92 |
|
|
93 |
|
|
94 |
|
@link |
95 |
|
|
96 |
|
|
97 |
|
@param |
98 |
|
@param |
99 |
|
@param |
100 |
|
@return |
101 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
102 |
859
|
public static final LogicalCheckExceptionList checkFormula(final Element element,... |
103 |
|
final ModuleContext context, final ExistenceChecker existenceChecker) { |
104 |
859
|
final FormulaChecker checker = new FormulaChecker(context, existenceChecker); |
105 |
859
|
checker.checkFormula(element); |
106 |
859
|
return checker.exceptions; |
107 |
|
} |
108 |
|
|
109 |
|
|
110 |
|
@link |
111 |
|
|
112 |
|
|
113 |
|
|
114 |
|
@link |
115 |
|
|
116 |
|
@param |
117 |
|
@param |
118 |
|
@return |
119 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
120 |
51
|
public static final LogicalCheckExceptionList checkFormula(final Element element,... |
121 |
|
final ModuleContext context) { |
122 |
51
|
return checkFormula(element, context, EverythingExists.getInstance()); |
123 |
|
} |
124 |
|
|
125 |
|
|
126 |
|
@link |
127 |
|
|
128 |
|
|
129 |
|
@param |
130 |
|
@param |
131 |
|
@param |
132 |
|
@return |
133 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0,33 |
|
134 |
159
|
public static final LogicalCheckExceptionList checkTerm(final Element element,... |
135 |
|
final ModuleContext context, final ExistenceChecker existenceChecker) { |
136 |
159
|
final FormulaChecker checker = new FormulaChecker(context, existenceChecker); |
137 |
159
|
checker.checkTerm(element); |
138 |
159
|
return checker.exceptions; |
139 |
|
} |
140 |
|
|
141 |
|
|
142 |
|
@link |
143 |
|
|
144 |
|
|
145 |
|
@link |
146 |
|
|
147 |
|
@param |
148 |
|
@param |
149 |
|
@return |
150 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
151 |
21
|
public static final LogicalCheckExceptionList checkTerm(final Element element,... |
152 |
|
final ModuleContext context) { |
153 |
21
|
return checkTerm(element, context, EverythingExists.getInstance()); |
154 |
|
} |
155 |
|
|
156 |
|
|
157 |
|
@link |
158 |
|
|
159 |
|
@param |
160 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (82) |
Complexity: 22 |
Complexity Density: 0,39 |
|
161 |
8694
|
private final void checkFormula(final Element element) {... |
162 |
8694
|
final String method = "checkFormula"; |
163 |
8694
|
Trace.begin(CLASS, this, method); |
164 |
8694
|
Trace.param(CLASS, this, method, "element", element); |
165 |
8694
|
final String context = getCurrentContext().getLocationWithinModule(); |
166 |
8694
|
Trace.param(CLASS, this, method, "context", context); |
167 |
8694
|
if (!checkList(element)) { |
168 |
7
|
return; |
169 |
|
} |
170 |
8687
|
final ElementList list = element.getList(); |
171 |
8687
|
final String listContext = context + ".getList()"; |
172 |
8687
|
setLocationWithinModule(listContext); |
173 |
8687
|
final String operator = list.getOperator(); |
174 |
8687
|
if (operator.equals(CONJUNCTION_OPERATOR) |
175 |
|
|| operator.equals(DISJUNCTION_OPERATOR) |
176 |
|
|| operator.equals(IMPLICATION_OPERATOR) |
177 |
|
|| operator.equals(EQUIVALENCE_OPERATOR)) { |
178 |
2807
|
Trace.trace(CLASS, this, method, |
179 |
|
"one of (and, or, implication, equivalence) operator found"); |
180 |
2807
|
if (list.size() <= 1) { |
181 |
9
|
handleFormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED, |
182 |
|
MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\"" |
183 |
|
+ operator + "\"", element, getCurrentContext()); |
184 |
9
|
return; |
185 |
|
} |
186 |
2798
|
if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) { |
187 |
1
|
handleFormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED, |
188 |
|
EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\"" |
189 |
|
+ operator + "\"", element, getCurrentContext()); |
190 |
1
|
return; |
191 |
|
} |
192 |
9123
|
for (int i = 0; i < list.size(); i++) { |
193 |
6326
|
setLocationWithinModule(listContext + ".getElement(" + i + ")"); |
194 |
6326
|
checkFormula(list.getElement(i)); |
195 |
|
} |
196 |
2797
|
setLocationWithinModule(listContext); |
197 |
2797
|
checkFreeAndBoundDisjunct(0, list); |
198 |
5880
|
} else if (operator.equals(NEGATION_OPERATOR)) { |
199 |
299
|
Trace.trace(CLASS, this, method, "negation operator found"); |
200 |
299
|
setLocationWithinModule(listContext); |
201 |
299
|
if (list.size() != 1) { |
202 |
2
|
handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED, |
203 |
|
EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"", |
204 |
|
element, getCurrentContext()); |
205 |
2
|
return; |
206 |
|
} |
207 |
297
|
setLocationWithinModule(listContext + ".getElement(0)"); |
208 |
297
|
checkFormula(list.getElement(0)); |
209 |
5581
|
} else if (operator.equals(PREDICATE_VARIABLE) |
210 |
|
|| operator.equals(PREDICATE_CONSTANT)) { |
211 |
4677
|
Trace.trace(CLASS, this, method, "predicate operator found"); |
212 |
4677
|
setLocationWithinModule(listContext); |
213 |
4677
|
if (list.size() < 1) { |
214 |
2
|
handleFormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED, |
215 |
|
AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"", |
216 |
|
element, getCurrentContext()); |
217 |
2
|
return; |
218 |
|
} |
219 |
|
|
220 |
4675
|
setLocationWithinModule(listContext + ".getElement(0)"); |
221 |
4675
|
if (!checkAtomFirst(list.getElement(0))) { |
222 |
8
|
return; |
223 |
|
} |
224 |
|
|
225 |
|
|
226 |
9279
|
for (int i = 1; i < list.size(); i++) { |
227 |
4612
|
setLocationWithinModule(listContext + ".getElement(" + i + ")"); |
228 |
4612
|
checkTerm(list.getElement(i)); |
229 |
|
} |
230 |
|
|
231 |
4667
|
setLocationWithinModule(listContext); |
232 |
4667
|
checkFreeAndBoundDisjunct(1, list); |
233 |
|
|
234 |
|
|
235 |
4667
|
if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists( |
236 |
|
list.getElement(0).getAtom().getString(), list.size() - 1)) { |
237 |
8
|
handleFormulaCheckException(UNKNOWN_PREDICATE_CONSTANT, |
238 |
|
UNKNOWN_PREDICATE_CONSTANT_TEXT + "\"" |
239 |
|
+ list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]", |
240 |
|
element, getCurrentContext()); |
241 |
|
} |
242 |
|
|
243 |
904
|
} else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) |
244 |
|
|| operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR) |
245 |
|
|| operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) { |
246 |
898
|
Trace.trace(CLASS, this, method, "quantifier found"); |
247 |
898
|
setLocationWithinModule(context); |
248 |
898
|
checkQuantifier(element); |
249 |
|
} else { |
250 |
6
|
setLocationWithinModule(listContext + ".getOperator()"); |
251 |
6
|
handleFormulaCheckException(UNKNOWN_LOGICAL_OPERATOR, |
252 |
|
UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"", |
253 |
|
element, getCurrentContext()); |
254 |
|
} |
255 |
|
|
256 |
8665
|
setLocationWithinModule(context); |
257 |
8665
|
Trace.end(CLASS, this, method); |
258 |
|
} |
259 |
|
|
260 |
|
|
261 |
|
|
262 |
|
|
263 |
|
@param |
264 |
|
@throws |
265 |
|
|
266 |
|
|
|
|
| 79,2% |
Uncovered Elements: 11 (53) |
Complexity: 12 |
Complexity Density: 0,31 |
|
267 |
898
|
private void checkQuantifier(final Element element) {... |
268 |
898
|
final String method = "checkQuantifier"; |
269 |
898
|
Trace.begin(CLASS, this, method); |
270 |
898
|
Trace.param(CLASS, this, method, "element", element); |
271 |
|
|
272 |
898
|
final String context = getCurrentContext().getLocationWithinModule(); |
273 |
898
|
Trace.param(CLASS, this, method, "context", context); |
274 |
898
|
checkList(element); |
275 |
898
|
final ElementList list = element.getList(); |
276 |
898
|
final String listContext = context + ".getList()"; |
277 |
898
|
setLocationWithinModule(listContext); |
278 |
898
|
final String operator = list.getOperator(); |
279 |
898
|
if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) |
280 |
|
&& operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR) |
281 |
|
&& operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) { |
282 |
0
|
throw new IllegalArgumentException("quantifier element expected but found: " |
283 |
|
+ element.toString()); |
284 |
|
} |
285 |
898
|
if (list.size() < 2 || list.size() > 3) { |
286 |
0
|
handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED, |
287 |
|
EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext()); |
288 |
0
|
return; |
289 |
|
} |
290 |
|
|
291 |
|
|
292 |
898
|
if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR) |
293 |
|
&& !existenceChecker.equalityOperatorExists()) { |
294 |
0
|
setLocationWithinModule(listContext + ".getOperator()"); |
295 |
0
|
handleFormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED, |
296 |
|
EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext()); |
297 |
|
} |
298 |
|
|
299 |
|
|
300 |
898
|
setLocationWithinModule(listContext + ".getElement(" + 0 + ")"); |
301 |
898
|
checkSubjectVariable(list.getElement(0)); |
302 |
|
|
303 |
|
|
304 |
898
|
setLocationWithinModule(listContext + ".getElement(" + 1 + ")"); |
305 |
898
|
checkFormula(list.getElement(1)); |
306 |
|
|
307 |
898
|
setLocationWithinModule(listContext); |
308 |
|
|
309 |
898
|
if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains( |
310 |
|
list.getElement(0))) { |
311 |
10
|
handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA, |
312 |
|
SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1), |
313 |
|
getCurrentContext()); |
314 |
|
} |
315 |
898
|
if (list.size() > 3) { |
316 |
0
|
handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED, |
317 |
|
EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list, |
318 |
|
getCurrentContext()); |
319 |
0
|
return; |
320 |
|
} |
321 |
898
|
if (list.size() > 2) { |
322 |
|
|
323 |
72
|
setLocationWithinModule(listContext + ".getElement(" + 2 + ")"); |
324 |
72
|
checkFormula(list.getElement(2)); |
325 |
|
|
326 |
|
|
327 |
72
|
setLocationWithinModule(listContext); |
328 |
72
|
if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains( |
329 |
|
list.getElement(0))) { |
330 |
3
|
handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA, |
331 |
|
SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2), |
332 |
|
getCurrentContext()); |
333 |
3
|
return; |
334 |
|
} |
335 |
69
|
setLocationWithinModule(listContext); |
336 |
69
|
checkFreeAndBoundDisjunct(1, list); |
337 |
|
} |
338 |
|
|
339 |
895
|
setLocationWithinModule(context); |
340 |
895
|
Trace.end(CLASS, this, method); |
341 |
|
} |
342 |
|
|
343 |
|
|
344 |
|
@link |
345 |
|
|
346 |
|
@param |
347 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (77) |
Complexity: 18 |
Complexity Density: 0,35 |
|
348 |
6521
|
private void checkTerm(final Element element) {... |
349 |
6521
|
final String method = "checkTerm"; |
350 |
6521
|
Trace.begin(CLASS, this, method); |
351 |
6521
|
Trace.param(CLASS, this, method, "element", element); |
352 |
|
|
353 |
6521
|
final String context = getCurrentContext().getLocationWithinModule(); |
354 |
6521
|
Trace.param(CLASS, this, method, "context", context); |
355 |
6521
|
if (!checkList(element)) { |
356 |
4
|
return; |
357 |
|
} |
358 |
6517
|
final ElementList list = element.getList(); |
359 |
6517
|
final String listContext = context + ".getList()"; |
360 |
6517
|
setLocationWithinModule(listContext); |
361 |
6517
|
final String operator = list.getOperator(); |
362 |
6517
|
if (operator.equals(SUBJECT_VARIABLE)) { |
363 |
4768
|
checkSubjectVariable(element); |
364 |
1749
|
} else if (operator.equals(FUNCTION_CONSTANT) |
365 |
|
|| operator.equals(FUNCTION_VARIABLE)) { |
366 |
|
|
367 |
|
|
368 |
1494
|
if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) { |
369 |
1
|
handleTermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED, |
370 |
|
AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext()); |
371 |
1
|
return; |
372 |
|
} |
373 |
|
|
374 |
|
|
375 |
1493
|
if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) { |
376 |
2
|
handleTermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED, |
377 |
|
MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext()); |
378 |
2
|
return; |
379 |
|
} |
380 |
|
|
381 |
|
|
382 |
1491
|
setLocationWithinModule(listContext + ".getElement(0)"); |
383 |
1491
|
if (!checkAtomFirst(list.getElement(0))) { |
384 |
7
|
return; |
385 |
|
} |
386 |
|
|
387 |
|
|
388 |
1484
|
setLocationWithinModule(listContext); |
389 |
3234
|
for (int i = 1; i < list.size(); i++) { |
390 |
1750
|
setLocationWithinModule(listContext + ".getElement(" + i + ")"); |
391 |
1750
|
checkTerm(list.getElement(i)); |
392 |
|
} |
393 |
|
|
394 |
1484
|
setLocationWithinModule(listContext); |
395 |
1484
|
checkFreeAndBoundDisjunct(1, list); |
396 |
|
|
397 |
|
|
398 |
1484
|
setLocationWithinModule(listContext); |
399 |
1484
|
if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists( |
400 |
|
list.getElement(0).getAtom().getString(), list.size() - 1)) { |
401 |
2
|
handleFormulaCheckException(UNKNOWN_FUNCTION_CONSTANT, |
402 |
|
UNKNOWN_FUNCTION_CONSTANT_TEXT + "\"" |
403 |
|
+ list.getElement(0).getAtom().getString() + "\"", element, |
404 |
|
getCurrentContext()); |
405 |
|
} |
406 |
|
|
407 |
255
|
} else if (operator.equals(CLASS_OP)) { |
408 |
|
|
409 |
244
|
if (list.size() != 2) { |
410 |
2
|
handleTermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED, |
411 |
|
EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext()); |
412 |
2
|
return; |
413 |
|
} |
414 |
|
|
415 |
242
|
setLocationWithinModule(listContext + ".getElement(" + 0 + ")"); |
416 |
242
|
if (!isSubjectVariable(list.getElement(0))) { |
417 |
1
|
handleTermCheckException(SUBJECT_VARIABLE_EXPECTED, |
418 |
|
SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext()); |
419 |
|
} |
420 |
|
|
421 |
|
|
422 |
242
|
setLocationWithinModule(listContext + ".getElement(" + 1 + ")"); |
423 |
242
|
checkFormula(list.getElement(1)); |
424 |
|
|
425 |
|
|
426 |
242
|
setLocationWithinModule(listContext); |
427 |
242
|
if (!existenceChecker.classOperatorExists()) { |
428 |
2
|
handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN, |
429 |
|
CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext()); |
430 |
|
} |
431 |
|
|
432 |
|
|
433 |
242
|
setLocationWithinModule(listContext + ".getElement(" + 0 + ")"); |
434 |
242
|
if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains( |
435 |
|
list.getElement(0))) { |
436 |
1
|
handleTermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA, |
437 |
|
SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0), |
438 |
|
getCurrentContext()); |
439 |
|
} |
440 |
|
|
441 |
|
} else { |
442 |
11
|
setLocationWithinModule(listContext + ".getOperator()"); |
443 |
11
|
handleTermCheckException(UNKNOWN_TERM_OPERATOR, |
444 |
|
UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext()); |
445 |
|
} |
446 |
|
|
447 |
6505
|
setLocationWithinModule(context); |
448 |
6505
|
Trace.end(CLASS, this, method); |
449 |
|
} |
450 |
|
|
451 |
|
|
452 |
|
|
453 |
|
|
454 |
|
|
455 |
|
@param |
456 |
|
@param |
457 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (22) |
Complexity: 4 |
Complexity Density: 0,25 |
|
458 |
9017
|
private void checkFreeAndBoundDisjunct(final int start,... |
459 |
|
final ElementList list) { |
460 |
|
|
461 |
9017
|
final String context = getCurrentContext().getLocationWithinModule(); |
462 |
9017
|
final ElementSet free = new ElementSet(); |
463 |
9017
|
final ElementSet bound = new ElementSet(); |
464 |
21843
|
for (int i = start; i < list.size(); i++) { |
465 |
12826
|
setLocationWithinModule(context + ".getElement(" + i + ")"); |
466 |
12826
|
final ElementSet newFree |
467 |
|
= getFreeSubjectVariables(list.getElement(i)); |
468 |
12826
|
final ElementSet newBound |
469 |
|
= FormulaChecker.getBoundSubjectVariables(list.getElement(i)); |
470 |
12826
|
final ElementSet interBound = newFree.newIntersection(bound); |
471 |
12826
|
if (!interBound.isEmpty()) { |
472 |
20
|
handleFormulaCheckException(FREE_VARIABLE_ALREADY_BOUND, |
473 |
|
FREE_VARIABLE_ALREADY_BOUND_TEXT |
474 |
|
+ interBound, list.getElement(i), getCurrentContext()); |
475 |
|
} |
476 |
12826
|
final ElementSet interFree = newBound.newIntersection(free); |
477 |
12826
|
if (!interFree.isEmpty()) { |
478 |
16
|
handleFormulaCheckException(BOUND_VARIABLE_ALREADY_FREE, |
479 |
|
BOUND_VARIABLE_ALREADY_FREE_TEXT |
480 |
|
+ interFree, list.getElement(i), getCurrentContext()); |
481 |
|
} |
482 |
12826
|
bound.union(newBound); |
483 |
12826
|
free.union(newFree); |
484 |
|
} |
485 |
|
|
486 |
9017
|
setLocationWithinModule(context); |
487 |
|
} |
488 |
|
|
489 |
|
|
490 |
|
|
491 |
|
@link |
492 |
|
|
493 |
|
@param |
494 |
|
@return |
495 |
|
|
|
|
| 75% |
Uncovered Elements: 6 (24) |
Complexity: 12 |
Complexity Density: 0,86 |
|
496 |
48888
|
private final boolean isSubjectVariable(final Element element) {... |
497 |
48888
|
if (element == null || !element.isList() || element.getList() == null) { |
498 |
13964
|
return false; |
499 |
|
} |
500 |
34924
|
final ElementList list = element.getList(); |
501 |
34924
|
if (list.getOperator().equals(SUBJECT_VARIABLE)) { |
502 |
15155
|
if (list.size() != 1) { |
503 |
0
|
return false; |
504 |
|
} |
505 |
15155
|
final Element first = element.getList().getElement(0); |
506 |
15155
|
if (first == null || !first.isAtom() || first.getAtom() == null) { |
507 |
0
|
return false; |
508 |
|
} |
509 |
15155
|
final Atom atom = first.getAtom(); |
510 |
15155
|
if (atom.getString() == null || atom.getAtom().getString() == null |
511 |
|
|| atom.getString().length() == 0) { |
512 |
0
|
return false; |
513 |
|
} |
514 |
|
} else { |
515 |
19769
|
return false; |
516 |
|
} |
517 |
15155
|
return true; |
518 |
|
} |
519 |
|
|
520 |
|
|
521 |
|
|
522 |
|
@link |
523 |
|
|
524 |
|
@param |
525 |
|
@return |
526 |
|
|
|
|
| 91,7% |
Uncovered Elements: 2 (24) |
Complexity: 5 |
Complexity Density: 0,31 |
|
527 |
5666
|
private boolean checkSubjectVariable(final Element element) {... |
528 |
|
|
529 |
|
|
530 |
5666
|
final String context = getCurrentContext().getLocationWithinModule(); |
531 |
5666
|
if (!checkList(element)) { |
532 |
0
|
return false; |
533 |
|
} |
534 |
5666
|
setLocationWithinModule(context + ".getList()"); |
535 |
5666
|
if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) { |
536 |
5663
|
if (element.getList().size() != 1) { |
537 |
2
|
handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED, |
538 |
|
EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext()); |
539 |
2
|
return false; |
540 |
|
} |
541 |
|
|
542 |
5661
|
setLocationWithinModule(context + ".getList().getElement(0)"); |
543 |
5661
|
if (checkAtomFirst(element.getList().getElement(0))) { |
544 |
5660
|
return false; |
545 |
|
} |
546 |
|
} else { |
547 |
3
|
setLocationWithinModule(context + ".getList().getOperator()"); |
548 |
3
|
handleFormulaCheckException(SUBJECT_VARIABLE_EXPECTED, |
549 |
|
SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext()); |
550 |
3
|
return false; |
551 |
|
} |
552 |
|
|
553 |
1
|
setLocationWithinModule(context); |
554 |
1
|
return true; |
555 |
|
} |
556 |
|
|
557 |
|
|
558 |
|
|
559 |
|
|
560 |
|
|
561 |
|
@param |
562 |
|
@return |
563 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (23) |
Complexity: 9 |
Complexity Density: 0,69 |
|
564 |
48646
|
private final ElementSet getFreeSubjectVariables(final Element element) {... |
565 |
48646
|
final ElementSet free = new ElementSet(); |
566 |
48646
|
if (isSubjectVariable(element)) { |
567 |
14914
|
free.add(element); |
568 |
33732
|
} else if (element.isList()) { |
569 |
19768
|
final ElementList list = element.getList(); |
570 |
19768
|
final String operator = list.getOperator(); |
571 |
19768
|
if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) |
572 |
|
|| operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR) |
573 |
|
|| operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR) |
574 |
|
|| operator.equals(CLASS_OP)) { |
575 |
3572
|
for (int i = 1; i < list.size(); i++) { |
576 |
1810
|
free.union(getFreeSubjectVariables(list.getElement(i))); |
577 |
|
} |
578 |
1762
|
free.remove(list.getElement(0)); |
579 |
|
} else { |
580 |
52016
|
for (int i = 0; i < list.size(); i++) { |
581 |
34010
|
free.union(getFreeSubjectVariables(list.getElement(i))); |
582 |
|
} |
583 |
|
} |
584 |
|
} |
585 |
48646
|
return free; |
586 |
|
} |
587 |
|
|
588 |
|
|
589 |
|
|
590 |
|
|
591 |
|
@param |
592 |
|
@return |
593 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (19) |
Complexity: 8 |
Complexity Density: 0,73 |
|
594 |
74063
|
public static final ElementSet getBoundSubjectVariables(final Element element) {... |
595 |
74063
|
final ElementSet bound = new ElementSet(); |
596 |
74063
|
if (element.isList()) { |
597 |
40372
|
ElementList list = element.getList(); |
598 |
40372
|
final String operator = list.getOperator(); |
599 |
|
|
600 |
40372
|
if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR) |
601 |
|
|| operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR) |
602 |
|
|| operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR) |
603 |
|
|| operator.equals(CLASS_OP)) { |
604 |
|
|
605 |
2032
|
bound.add(list.getElement(0)); |
606 |
|
|
607 |
4128
|
for (int i = 1; i < list.size(); i++) { |
608 |
2096
|
bound.union(FormulaChecker.getBoundSubjectVariables( |
609 |
|
list.getElement(i))); |
610 |
|
} |
611 |
|
} else { |
612 |
|
|
613 |
96269
|
for (int i = 0; i < list.size(); i++) { |
614 |
57929
|
bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i))); |
615 |
|
} |
616 |
|
} |
617 |
|
} |
618 |
74063
|
return bound; |
619 |
|
} |
620 |
|
|
621 |
|
|
622 |
|
|
623 |
|
|
624 |
|
|
625 |
|
@param |
626 |
|
@return |
627 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (32) |
Complexity: 6 |
Complexity Density: 0,27 |
|
628 |
21779
|
private boolean checkList(final Element element) {... |
629 |
|
|
630 |
21779
|
final String context = getCurrentContext().getLocationWithinModule(); |
631 |
21779
|
if (element == null) { |
632 |
2
|
handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL, |
633 |
|
ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext()); |
634 |
2
|
return false; |
635 |
|
} |
636 |
21777
|
if (!element.isList()) { |
637 |
2
|
handleElementCheckException(LIST_EXPECTED, |
638 |
|
LIST_EXPECTED_TEXT, element, getCurrentContext()); |
639 |
2
|
return false; |
640 |
|
} |
641 |
21775
|
final ElementList list = element.getList(); |
642 |
21775
|
setLocationWithinModule(context + ".getList()"); |
643 |
21775
|
if (list == null) { |
644 |
2
|
handleElementCheckException(LIST_MUST_NOT_BE_NULL, |
645 |
|
LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext()); |
646 |
2
|
return false; |
647 |
|
} |
648 |
21773
|
final String operator = list.getOperator(); |
649 |
21773
|
setLocationWithinModule(context + ".getList().getOperator()"); |
650 |
21773
|
if (operator == null) { |
651 |
2
|
handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL, |
652 |
|
OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT + "\"" |
653 |
|
+ operator + "\"", element, getCurrentContext()); |
654 |
2
|
return false; |
655 |
|
} |
656 |
21771
|
if (operator.length() == 0) { |
657 |
3
|
handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY, |
658 |
|
OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\"" |
659 |
|
+ operator + "\"", element, getCurrentContext()); |
660 |
3
|
return false; |
661 |
|
} |
662 |
|
|
663 |
21768
|
setLocationWithinModule(context); |
664 |
21768
|
return true; |
665 |
|
} |
666 |
|
|
667 |
|
|
668 |
|
|
669 |
|
|
670 |
|
|
671 |
|
@param |
672 |
|
@return |
673 |
|
|
|
|
| 90% |
Uncovered Elements: 3 (30) |
Complexity: 6 |
Complexity Density: 0,3 |
|
674 |
11827
|
private boolean checkAtomFirst(final Element element) {... |
675 |
|
|
676 |
11827
|
final String context = getCurrentContext().getLocationWithinModule(); |
677 |
11827
|
if (element == null) { |
678 |
0
|
handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL, |
679 |
|
ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext()); |
680 |
0
|
return false; |
681 |
|
} |
682 |
11827
|
if (!element.isAtom()) { |
683 |
9
|
handleElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, |
684 |
|
FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext()); |
685 |
9
|
return false; |
686 |
|
} |
687 |
11818
|
final Atom atom = element.getAtom(); |
688 |
11818
|
setLocationWithinModule(context + ".getAtom()"); |
689 |
11818
|
if (atom == null) { |
690 |
2
|
handleElementCheckException(ATOM_MUST_NOT_BE_NULL, |
691 |
|
ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext()); |
692 |
2
|
return false; |
693 |
|
} |
694 |
11816
|
if (atom.getString() == null) { |
695 |
2
|
handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL, |
696 |
|
ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext()); |
697 |
2
|
return false; |
698 |
|
} |
699 |
11814
|
if (atom.getString().length() == 0) { |
700 |
3
|
handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY, |
701 |
|
ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext()); |
702 |
3
|
return false; |
703 |
|
} |
704 |
|
|
705 |
11811
|
setLocationWithinModule(context); |
706 |
11811
|
return true; |
707 |
|
} |
708 |
|
|
709 |
|
|
710 |
|
@link |
711 |
|
|
712 |
|
@param |
713 |
|
@param |
714 |
|
@param |
715 |
|
@param |
716 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0,5 |
|
717 |
86
|
private void handleFormulaCheckException(final int code, final String msg,... |
718 |
|
final Element element, final ModuleContext context) { |
719 |
86
|
final FormulaCheckException ex = new FormulaCheckException(code, msg, element, context); |
720 |
86
|
exceptions.add(ex); |
721 |
|
} |
722 |
|
|
723 |
|
|
724 |
|
@link |
725 |
|
|
726 |
|
@param |
727 |
|
@param |
728 |
|
@param |
729 |
|
@param |
730 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0,5 |
|
731 |
18
|
private void handleTermCheckException(final int code, final String msg,... |
732 |
|
final Element element, final ModuleContext context) { |
733 |
18
|
final TermCheckException ex = new TermCheckException(code, msg, element, context); |
734 |
18
|
exceptions.add(ex); |
735 |
|
} |
736 |
|
|
737 |
|
|
738 |
|
@link |
739 |
|
|
740 |
|
@param |
741 |
|
@param |
742 |
|
@param |
743 |
|
@param |
744 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0,5 |
|
745 |
27
|
private void handleElementCheckException(final int code, final String msg,... |
746 |
|
final Element element, final ModuleContext context) { |
747 |
27
|
final ElementCheckException ex = new ElementCheckException(code, msg, element, context); |
748 |
27
|
exceptions.add(ex); |
749 |
|
} |
750 |
|
|
751 |
|
|
752 |
|
|
753 |
|
|
754 |
|
@param |
755 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
756 |
195119
|
protected void setLocationWithinModule(final String locationWithinModule) {... |
757 |
195119
|
getCurrentContext().setLocationWithinModule(locationWithinModule); |
758 |
|
} |
759 |
|
|
760 |
|
|
761 |
|
|
762 |
|
|
763 |
|
@return |
764 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
765 |
259652
|
protected final ModuleContext getCurrentContext() {... |
766 |
259652
|
return currentContext; |
767 |
|
} |
768 |
|
|
769 |
|
} |