1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
package org.qedeq.kernel.bo.service.heuristic; |
17 |
|
|
18 |
|
import org.qedeq.base.io.Parameters; |
19 |
|
import org.qedeq.base.trace.Trace; |
20 |
|
import org.qedeq.kernel.bo.log.QedeqLog; |
21 |
|
import org.qedeq.kernel.bo.logic.common.Operators; |
22 |
|
import org.qedeq.kernel.bo.logic.model.DynamicDirectInterpreter; |
23 |
|
import org.qedeq.kernel.bo.logic.model.DynamicModel; |
24 |
|
import org.qedeq.kernel.bo.logic.model.FourDynamicModel; |
25 |
|
import org.qedeq.kernel.bo.logic.model.HeuristicErrorCodes; |
26 |
|
import org.qedeq.kernel.bo.logic.model.HeuristicException; |
27 |
|
import org.qedeq.kernel.bo.logic.model.ModelFunctionConstant; |
28 |
|
import org.qedeq.kernel.bo.logic.model.ModelPredicateConstant; |
29 |
|
import org.qedeq.kernel.bo.module.ControlVisitor; |
30 |
|
import org.qedeq.kernel.bo.module.InternalServiceCall; |
31 |
|
import org.qedeq.kernel.bo.module.KernelQedeqBo; |
32 |
|
import org.qedeq.kernel.bo.module.PluginBo; |
33 |
|
import org.qedeq.kernel.bo.module.PluginExecutor; |
34 |
|
import org.qedeq.kernel.se.base.list.Element; |
35 |
|
import org.qedeq.kernel.se.base.module.Axiom; |
36 |
|
import org.qedeq.kernel.se.base.module.ConditionalProof; |
37 |
|
import org.qedeq.kernel.se.base.module.FormalProofLine; |
38 |
|
import org.qedeq.kernel.se.base.module.FunctionDefinition; |
39 |
|
import org.qedeq.kernel.se.base.module.InitialFunctionDefinition; |
40 |
|
import org.qedeq.kernel.se.base.module.InitialPredicateDefinition; |
41 |
|
import org.qedeq.kernel.se.base.module.Node; |
42 |
|
import org.qedeq.kernel.se.base.module.PredicateDefinition; |
43 |
|
import org.qedeq.kernel.se.base.module.Proposition; |
44 |
|
import org.qedeq.kernel.se.base.module.Rule; |
45 |
|
import org.qedeq.kernel.se.common.ModuleContext; |
46 |
|
import org.qedeq.kernel.se.common.ModuleDataException; |
47 |
|
import org.qedeq.kernel.se.common.Plugin; |
48 |
|
import org.qedeq.kernel.se.common.SourceFileExceptionList; |
49 |
|
import org.qedeq.kernel.se.dto.list.DefaultElementList; |
50 |
|
|
51 |
|
|
52 |
|
|
53 |
|
|
54 |
|
|
55 |
|
@author |
56 |
|
|
|
|
| 40.1% |
Uncovered Elements: 148 (247) |
Complexity: 72 |
Complexity Density: 0.43 |
|
57 |
|
public final class DynamicHeuristicCheckerExecutor extends ControlVisitor implements PluginExecutor { |
58 |
|
|
59 |
|
|
60 |
|
private static final Class CLASS = DynamicHeuristicCheckerExecutor.class; |
61 |
|
|
62 |
|
|
63 |
|
private final DynamicDirectInterpreter interpreter; |
64 |
|
|
65 |
|
|
66 |
|
private DefaultElementList condition; |
67 |
|
|
68 |
|
|
69 |
|
|
70 |
|
|
71 |
|
@param |
72 |
|
@param |
73 |
|
@param |
74 |
|
|
|
|
| 63.2% |
Uncovered Elements: 7 (19) |
Complexity: 8 |
Complexity Density: 0.53 |
|
75 |
1
|
DynamicHeuristicCheckerExecutor(final PluginBo plugin, final KernelQedeqBo qedeq,... |
76 |
|
final Parameters parameters) { |
77 |
1
|
super(plugin, qedeq); |
78 |
1
|
final String method = "DynamicHeuristicChecker(PluginBo, QedeqBo, Map)"; |
79 |
1
|
final String modelClass = parameters.getString("model"); |
80 |
1
|
DynamicModel model = null; |
81 |
1
|
if (modelClass != null && modelClass.length() > 0) { |
82 |
1
|
try { |
83 |
1
|
Class cl = Class.forName(modelClass); |
84 |
1
|
model = (DynamicModel) cl.newInstance(); |
85 |
|
} catch (ClassNotFoundException e) { |
86 |
0
|
Trace.fatal(CLASS, this, method, "Model class not in class path: " |
87 |
|
+ modelClass, e); |
88 |
|
} catch (InstantiationException e) { |
89 |
0
|
Trace.fatal(CLASS, this, method, "Model class could not be instanciated: " |
90 |
|
+ modelClass, e); |
91 |
|
} catch (IllegalAccessException e) { |
92 |
0
|
Trace.fatal(CLASS, this, method, |
93 |
|
"Programming error, access for instantiation failed for model: " |
94 |
|
+ modelClass, e); |
95 |
|
} catch (RuntimeException e) { |
96 |
0
|
Trace.fatal(CLASS, this, method, |
97 |
|
"Programming error, instantiation failed for model: " + modelClass, e); |
98 |
|
} |
99 |
|
} |
100 |
|
|
101 |
1
|
if (model == null) { |
102 |
0
|
model = new FourDynamicModel(); |
103 |
|
} |
104 |
1
|
this.interpreter = new DynamicDirectInterpreter(qedeq, model); |
105 |
|
} |
106 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
107 |
1
|
private Plugin getPlugin() {... |
108 |
1
|
return (Plugin) getService(); |
109 |
|
} |
110 |
|
|
|
|
| 55.6% |
Uncovered Elements: 8 (18) |
Complexity: 5 |
Complexity Density: 0.31 |
|
111 |
1
|
public Object executePlugin(final InternalServiceCall call, final Object data) {... |
112 |
1
|
final String method = "executePlugin()"; |
113 |
1
|
try { |
114 |
1
|
QedeqLog.getInstance().logRequest("Dynamic heuristic test", getQedeqBo().getUrl()); |
115 |
|
|
116 |
1
|
try { |
117 |
1
|
getServices().checkWellFormedness(call.getInternalServiceProcess(), getQedeqBo()); |
118 |
|
} catch (Exception e) { |
119 |
|
|
120 |
0
|
Trace.trace(CLASS, method, e); |
121 |
|
} |
122 |
1
|
condition = new DefaultElementList(Operators.CONJUNCTION_OPERATOR); |
123 |
1
|
traverse(call.getInternalServiceProcess()); |
124 |
1
|
QedeqLog.getInstance().logSuccessfulReply( |
125 |
|
"Heuristic test succesfull", getQedeqBo().getUrl()); |
126 |
|
} catch (final SourceFileExceptionList e) { |
127 |
0
|
final String msg = "Test failed"; |
128 |
0
|
Trace.fatal(CLASS, this, method, msg, e); |
129 |
0
|
QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage()); |
130 |
|
} catch (final RuntimeException e) { |
131 |
0
|
Trace.fatal(CLASS, this, method, "unexpected problem", e); |
132 |
0
|
QedeqLog.getInstance().logFailureReply( |
133 |
|
"Test failed", getQedeqBo().getUrl(), "unexpected problem: " |
134 |
0
|
+ (e.getMessage() != null ? e.getMessage() : e.toString())); |
135 |
|
} finally { |
136 |
1
|
getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList()); |
137 |
|
} |
138 |
1
|
return null; |
139 |
|
} |
140 |
|
|
141 |
|
|
142 |
|
|
143 |
|
|
144 |
|
|
145 |
|
@param |
146 |
|
|
|
|
| 18.9% |
Uncovered Elements: 30 (37) |
Complexity: 11 |
Complexity Density: 0.44 |
|
147 |
3
|
private void test(final Element test) {... |
148 |
3
|
boolean useCondition = condition.size() > 0; |
149 |
|
|
150 |
3
|
try { |
151 |
3
|
Element toast = test; |
152 |
3
|
if (condition.size() > 0) { |
153 |
0
|
final DefaultElementList withCondition = new DefaultElementList(Operators.IMPLICATION_OPERATOR); |
154 |
0
|
withCondition.add(condition); |
155 |
0
|
withCondition.add(test); |
156 |
0
|
toast = withCondition; |
157 |
|
} |
158 |
3
|
if (!isTautology(getCurrentContext(), toast)) { |
159 |
0
|
addWarning(new HeuristicException(HeuristicErrorCodes.EVALUATED_NOT_TRUE_CODE, |
160 |
|
HeuristicErrorCodes.EVALUATED_NOT_TRUE_TEXT + " (\"" |
161 |
|
+ interpreter.getModel().getName() + "\")", getCurrentContext())); |
162 |
|
} |
163 |
|
} catch (HeuristicException h) { |
164 |
|
|
165 |
0
|
final String begin = getCurrentContext().getLocationWithinModule(); |
166 |
|
|
167 |
|
|
168 |
0
|
if (!getCurrentContext().getModuleLocation().equals(h.getContext().getModuleLocation()) |
169 |
|
|| !h.getContext().getLocationWithinModule().startsWith(begin)) { |
170 |
0
|
addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
171 |
|
getCurrentContext())); |
172 |
|
} else { |
173 |
0
|
String further = h.getContext().getLocationWithinModule().substring(begin.length()); |
174 |
0
|
if (useCondition) { |
175 |
0
|
if (further.startsWith(".getList().getElement(1)")) { |
176 |
0
|
further = further.substring(".getList().getElement(1)".length()); |
177 |
0
|
addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
178 |
|
new ModuleContext(h.getContext().getModuleLocation(), begin + further))); |
179 |
|
} else { |
180 |
0
|
addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
181 |
|
getCurrentContext())); |
182 |
|
} |
183 |
|
} else { |
184 |
0
|
addWarning(h); |
185 |
|
} |
186 |
|
} |
187 |
|
} catch (RuntimeException e) { |
188 |
0
|
Trace.fatal(CLASS, this, "test(Element)", "unexpected runtime exception", e); |
189 |
0
|
if (e.getCause() != null && e.getCause() instanceof HeuristicException) { |
190 |
|
|
191 |
0
|
HeuristicException h = (HeuristicException) e.getCause(); |
192 |
0
|
addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(), |
193 |
|
getCurrentContext())); |
194 |
|
} else { |
195 |
0
|
addWarning(new HeuristicException(HeuristicErrorCodes.RUNTIME_EXCEPTION_CODE, |
196 |
|
HeuristicErrorCodes.RUNTIME_EXCEPTION_TEXT + e, getCurrentContext())); |
197 |
|
} |
198 |
|
} |
199 |
|
} |
200 |
|
|
201 |
|
|
202 |
|
|
203 |
|
|
204 |
|
|
205 |
|
@param |
206 |
|
@param |
207 |
|
@return |
208 |
|
@throws |
209 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (9) |
Complexity: 3 |
Complexity Density: 0.43 |
|
210 |
3
|
private boolean isTautology(final ModuleContext moduleContext, final Element formula)... |
211 |
|
throws HeuristicException { |
212 |
3
|
boolean result = true; |
213 |
3
|
ModuleContext context = moduleContext; |
214 |
3
|
try { |
215 |
3
|
do { |
216 |
36
|
result &= interpreter.calculateValue(new ModuleContext(context), formula); |
217 |
|
|
218 |
36
|
} while (result && interpreter.next()); |
219 |
|
|
220 |
|
|
221 |
|
|
222 |
|
|
223 |
|
} finally { |
224 |
3
|
interpreter.clearVariables(); |
225 |
|
} |
226 |
3
|
return result; |
227 |
|
} |
228 |
|
|
229 |
|
|
|
|
| 78.6% |
Uncovered Elements: 3 (14) |
Complexity: 3 |
Complexity Density: 0.3 |
|
230 |
1
|
public void visitEnter(final Axiom axiom) throws ModuleDataException {... |
231 |
1
|
if (axiom == null) { |
232 |
0
|
return; |
233 |
|
} |
234 |
1
|
final String context = getCurrentContext().getLocationWithinModule(); |
235 |
1
|
QedeqLog.getInstance().logMessageState("\ttesting axiom", getQedeqBo().getUrl()); |
236 |
1
|
if (axiom.getFormula() != null) { |
237 |
1
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
238 |
1
|
final Element test = axiom.getFormula().getElement(); |
239 |
1
|
test(test); |
240 |
|
} |
241 |
1
|
setLocationWithinModule(context); |
242 |
1
|
setBlocked(true); |
243 |
|
} |
244 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
245 |
1
|
public void visitLeave(final Axiom axiom) {... |
246 |
1
|
setBlocked(false); |
247 |
|
} |
248 |
|
|
|
|
| 57.9% |
Uncovered Elements: 8 (19) |
Complexity: 4 |
Complexity Density: 0.27 |
|
249 |
1
|
public void visitEnter(final InitialPredicateDefinition definition)... |
250 |
|
throws ModuleDataException { |
251 |
1
|
final String method = "visitEnter(InitialPredicateDefinition)"; |
252 |
1
|
if (definition == null) { |
253 |
0
|
return; |
254 |
|
} |
255 |
1
|
QedeqLog.getInstance().logMessageState("\ttesting initial predicate definition", |
256 |
|
getQedeqBo().getUrl()); |
257 |
1
|
final String context = getCurrentContext().getLocationWithinModule(); |
258 |
1
|
try { |
259 |
1
|
ModelPredicateConstant predicate = new ModelPredicateConstant( |
260 |
|
definition.getName(), Integer.parseInt(definition |
261 |
|
.getArgumentNumber())); |
262 |
|
|
263 |
1
|
if (!interpreter.hasPredicateConstant(predicate)) { |
264 |
0
|
setLocationWithinModule(context + ".getName()"); |
265 |
0
|
addWarning(new HeuristicException( |
266 |
|
HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE, |
267 |
|
HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT |
268 |
|
+ predicate, getCurrentContext())); |
269 |
|
} |
270 |
|
} catch (NumberFormatException e) { |
271 |
0
|
Trace.fatal(CLASS, this, method, "not suported argument number: " |
272 |
|
+ definition.getArgumentNumber(), e); |
273 |
0
|
setLocationWithinModule(context + ".getArgumentNumber()"); |
274 |
0
|
addWarning(new HeuristicException( |
275 |
|
HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE, |
276 |
|
HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT |
277 |
|
+ definition.getArgumentNumber(), |
278 |
|
getCurrentContext())); |
279 |
|
} |
280 |
1
|
setLocationWithinModule(context); |
281 |
1
|
setBlocked(true); |
282 |
|
} |
283 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
284 |
1
|
public void visitLeave(final InitialPredicateDefinition definition) {... |
285 |
1
|
setBlocked(false); |
286 |
|
} |
287 |
|
|
|
|
| 66.7% |
Uncovered Elements: 5 (15) |
Complexity: 3 |
Complexity Density: 0.23 |
|
288 |
1
|
public void visitEnter(final PredicateDefinition definition)... |
289 |
|
throws ModuleDataException { |
290 |
1
|
final String method = "visitEnter(PredicateDefinition)"; |
291 |
1
|
if (definition == null) { |
292 |
0
|
return; |
293 |
|
} |
294 |
1
|
QedeqLog.getInstance().logMessageState("\ttesting predicate definition", |
295 |
|
getQedeqBo().getUrl()); |
296 |
1
|
final String context = getCurrentContext().getLocationWithinModule(); |
297 |
1
|
try { |
298 |
|
|
299 |
|
|
300 |
1
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
301 |
1
|
test(definition.getFormula().getElement()); |
302 |
|
} catch (NumberFormatException e) { |
303 |
0
|
Trace.fatal(CLASS, this, method, "not suported argument number: " |
304 |
|
+ definition.getArgumentNumber(), e); |
305 |
0
|
setLocationWithinModule(context + ".getArgumentNumber()"); |
306 |
0
|
addWarning(new HeuristicException(HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE, |
307 |
|
HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT + definition.getArgumentNumber(), |
308 |
|
getCurrentContext())); |
309 |
|
} |
310 |
1
|
setLocationWithinModule(context); |
311 |
1
|
setBlocked(true); |
312 |
|
} |
313 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
314 |
1
|
public void visitLeave(final PredicateDefinition definition) {... |
315 |
1
|
setBlocked(false); |
316 |
|
} |
317 |
|
|
|
|
| 0% |
Uncovered Elements: 19 (19) |
Complexity: 4 |
Complexity Density: 0.27 |
|
318 |
0
|
public void visitEnter(final InitialFunctionDefinition definition)... |
319 |
|
throws ModuleDataException { |
320 |
0
|
final String method = "visitEnter(InitialFunctionDefinition)"; |
321 |
0
|
if (definition == null) { |
322 |
0
|
return; |
323 |
|
} |
324 |
0
|
QedeqLog.getInstance().logMessageState("\ttesting initial function definition", |
325 |
|
getQedeqBo().getUrl()); |
326 |
0
|
final String context = getCurrentContext().getLocationWithinModule(); |
327 |
0
|
try { |
328 |
0
|
ModelFunctionConstant function = new ModelFunctionConstant(definition.getName(), |
329 |
|
Integer.parseInt(definition.getArgumentNumber())); |
330 |
0
|
if (!interpreter.hasFunctionConstant(function)) { |
331 |
|
|
332 |
0
|
setLocationWithinModule(context + ".getName()"); |
333 |
0
|
addWarning(new HeuristicException( |
334 |
|
HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE, |
335 |
|
HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT |
336 |
|
+ function, getCurrentContext())); |
337 |
|
} |
338 |
|
} catch (NumberFormatException e) { |
339 |
0
|
Trace.fatal(CLASS, this, method, "not suported argument number: " |
340 |
|
+ definition.getArgumentNumber(), e); |
341 |
0
|
setLocationWithinModule(context + ".getArgumentNumber()"); |
342 |
0
|
addWarning(new HeuristicException( |
343 |
|
HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE, |
344 |
|
HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT |
345 |
|
+ definition.getArgumentNumber(), |
346 |
|
getCurrentContext())); |
347 |
|
} |
348 |
0
|
setLocationWithinModule(context); |
349 |
0
|
setBlocked(true); |
350 |
|
} |
351 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
352 |
0
|
public void visitLeave(final InitialFunctionDefinition definition) {... |
353 |
0
|
setBlocked(false); |
354 |
|
} |
355 |
|
|
|
|
| 0% |
Uncovered Elements: 10 (10) |
Complexity: 2 |
Complexity Density: 0.25 |
|
356 |
0
|
public void visitEnter(final FunctionDefinition definition)... |
357 |
|
throws ModuleDataException { |
358 |
0
|
if (definition == null) { |
359 |
0
|
return; |
360 |
|
} |
361 |
0
|
QedeqLog.getInstance().logMessageState("\ttesting function definition", |
362 |
|
getQedeqBo().getUrl()); |
363 |
0
|
final String context = getCurrentContext().getLocationWithinModule(); |
364 |
|
|
365 |
|
|
366 |
0
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
367 |
0
|
test(definition.getFormula().getElement()); |
368 |
0
|
setLocationWithinModule(context); |
369 |
0
|
setBlocked(true); |
370 |
|
} |
371 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
372 |
0
|
public void visitLeave(final FunctionDefinition definition) {... |
373 |
0
|
setBlocked(false); |
374 |
|
} |
375 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
376 |
4
|
public void visitEnter(final Node node) {... |
377 |
4
|
QedeqLog.getInstance().logMessageState(super.getLocationDescription(), |
378 |
|
getQedeqBo().getUrl()); |
379 |
|
} |
380 |
|
|
|
|
| 76.9% |
Uncovered Elements: 3 (13) |
Complexity: 3 |
Complexity Density: 0.33 |
|
381 |
1
|
public void visitEnter(final Proposition proposition)... |
382 |
|
throws ModuleDataException { |
383 |
1
|
if (proposition == null) { |
384 |
0
|
return; |
385 |
|
} |
386 |
1
|
QedeqLog.getInstance().logMessageState("\ttesting proposition", getQedeqBo().getUrl()); |
387 |
1
|
final String context = getCurrentContext().getLocationWithinModule(); |
388 |
1
|
if (proposition.getFormula() != null) { |
389 |
1
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
390 |
1
|
final Element test = proposition.getFormula().getElement(); |
391 |
1
|
test(test); |
392 |
|
} |
393 |
1
|
setLocationWithinModule(context); |
394 |
|
} |
395 |
|
|
|
|
| - |
Uncovered Elements: 0 (0) |
Complexity: 1 |
Complexity Density: - |
|
396 |
1
|
public void visitLeave(final Proposition definition) {... |
397 |
|
|
398 |
|
} |
399 |
|
|
|
|
| 0% |
Uncovered Elements: 13 (13) |
Complexity: 3 |
Complexity Density: 0.33 |
|
400 |
0
|
public void visitEnter(final FormalProofLine line)... |
401 |
|
throws ModuleDataException { |
402 |
0
|
if (line == null) { |
403 |
0
|
return; |
404 |
|
} |
405 |
0
|
QedeqLog.getInstance().logMessageState("\t\ttesting line " + line.getLabel(), |
406 |
|
getQedeqBo().getUrl()); |
407 |
0
|
final String context = getCurrentContext().getLocationWithinModule(); |
408 |
0
|
if (line.getFormula() != null) { |
409 |
0
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
410 |
0
|
test(line.getFormula().getElement()); |
411 |
|
} |
412 |
0
|
setLocationWithinModule(context); |
413 |
0
|
setBlocked(true); |
414 |
|
} |
415 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
416 |
0
|
public void visitLeave(final FormalProofLine line) {... |
417 |
0
|
setBlocked(false); |
418 |
|
} |
419 |
|
|
|
|
| 0% |
Uncovered Elements: 9 (9) |
Complexity: 5 |
Complexity Density: 1 |
|
420 |
0
|
public void visitEnter(final ConditionalProof line)... |
421 |
|
throws ModuleDataException { |
422 |
0
|
if (line == null) { |
423 |
0
|
return; |
424 |
|
} |
425 |
|
|
426 |
0
|
if (line.getHypothesis() != null && line.getHypothesis().getFormula() != null |
427 |
|
&& line.getHypothesis().getFormula().getElement() != null) { |
428 |
0
|
condition.add(line.getHypothesis().getFormula().getElement()); |
429 |
0
|
QedeqLog.getInstance().logMessageState("\t\tadd condit. " |
430 |
|
+ line.getHypothesis().getLabel(), getQedeqBo().getUrl()); |
431 |
|
} |
432 |
|
} |
433 |
|
|
|
|
| 0% |
Uncovered Elements: 16 (16) |
Complexity: 6 |
Complexity Density: 0.6 |
|
434 |
0
|
public void visitLeave(final ConditionalProof line) {... |
435 |
0
|
if (line == null) { |
436 |
0
|
return; |
437 |
|
} |
438 |
|
|
439 |
0
|
if (line.getHypothesis() != null && line.getHypothesis().getFormula() != null |
440 |
|
&& line.getHypothesis().getFormula().getElement() != null) { |
441 |
0
|
condition.remove(condition.size() - 1); |
442 |
|
} |
443 |
0
|
QedeqLog.getInstance().logMessageState("\t\ttesting line " |
444 |
|
+ line.getConclusion().getLabel(), getQedeqBo().getUrl()); |
445 |
0
|
final String context = getCurrentContext().getLocationWithinModule(); |
446 |
0
|
if (line.getConclusion().getFormula() != null) { |
447 |
0
|
setLocationWithinModule(context + ".getConclusion().getFormula().getElement()"); |
448 |
0
|
final Element test = line.getConclusion().getFormula().getElement(); |
449 |
0
|
test(test); |
450 |
|
} |
451 |
|
} |
452 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
453 |
0
|
public void visitEnter(final Rule rule) throws ModuleDataException {... |
454 |
0
|
setBlocked(true); |
455 |
|
} |
456 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
457 |
0
|
public void visitLeave(final Rule rule) {... |
458 |
0
|
setBlocked(false); |
459 |
|
} |
460 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
461 |
0
|
public String getLocationDescription() {... |
462 |
0
|
return super.getLocationDescription() + "\n" + interpreter.toString(); |
463 |
|
} |
464 |
|
|
465 |
|
} |