Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../img/srcFileCovDistChart4.png 93% of files have more coverage
168   465   72   6.72
54   365   0.43   25
25     2.88  
1    
 
  DynamicHeuristicCheckerExecutor       Line # 57 168 72 40.1% 0.4008097
 
  (1)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.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    * Check if formulas are valid in our model.
54    *
55    * @author Michael Meyling
56    */
 
57    public final class DynamicHeuristicCheckerExecutor extends ControlVisitor implements PluginExecutor {
58   
59    /** This class. */
60    private static final Class CLASS = DynamicHeuristicCheckerExecutor.class;
61   
62    /** Interpretation for variables. */
63    private final DynamicDirectInterpreter interpreter;
64   
65    /** Current condition. */
66    private DefaultElementList condition;
67   
68    /**
69    * Constructor.
70    *
71    * @param plugin This plugin we work for.
72    * @param qedeq QEDEQ module object.
73    * @param parameters Execution parameters.
74    */
 
75  1 toggle 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    // fallback is the default model
101  1 if (model == null) {
102  0 model = new FourDynamicModel();
103    }
104  1 this.interpreter = new DynamicDirectInterpreter(qedeq, model);
105    }
106   
 
107  1 toggle private Plugin getPlugin() {
108  1 return (Plugin) getService();
109    }
110   
 
111  1 toggle 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    // first we try to get more information about required modules and their predicates..
116  1 try {
117  1 getServices().checkWellFormedness(call.getInternalServiceProcess(), getQedeqBo());
118    } catch (Exception e) {
119    // we continue and ignore external predicates
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    * Check truth value in our model. If it is no tautology an warning is added.
143    * This also happens if our model doesn't support an operator found in the formula.
144    *
145    * @param test Test formula.
146    */
 
147  3 toggle private void test(final Element test) {
148  3 boolean useCondition = condition.size() > 0; //Assume that we start with an implication,
149    // but the real context begins after skipping ".getList().getElement(1)"
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    // TODO 20101015 m31: better exception handling would be better!
165  0 final String begin = getCurrentContext().getLocationWithinModule();
166    // is the error context at the same location? if not we have a problem with a referenced
167    // predicate or function constant and we take the currrent context instead
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 { // must be an error in the condition and for that we have no context
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    // TODO 20101015 m31: better exception handling would be better!
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    * Test if given formula is a tautology. This is done by checking a model and
203    * iterating through variable values.
204    *
205    * @param moduleContext Here we are within a module.
206    * @param formula Formula.
207    * @return Is this formula a tautology according to our tests.
208    * @throws HeuristicException Evaluation failed.
209    */
 
210  3 toggle 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    // System.out.println(interpreter.toString());
218  36 } while (result && interpreter.next());
219    // if (!result) {
220    // System.out.println(interpreter);
221    // }
222    // System.out.println("interpretation finished - and result is = " + result);
223    } finally {
224  3 interpreter.clearVariables();
225    }
226  3 return result;
227    }
228   
229   
 
230  1 toggle 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   
 
245  1 toggle public void visitLeave(final Axiom axiom) {
246  1 setBlocked(false);
247    }
248   
 
249  1 toggle 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    // check if model contains predicate
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   
 
284  1 toggle public void visitLeave(final InitialPredicateDefinition definition) {
285  1 setBlocked(false);
286    }
287   
 
288  1 toggle 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    // test new predicate constant: must always be successful otherwise there
299    // must be a programming error or the predicate definition is not formal correct
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   
 
314  1 toggle public void visitLeave(final PredicateDefinition definition) {
315  1 setBlocked(false);
316    }
317   
 
318  0 toggle 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    // check if model contains predicate
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   
 
352  0 toggle public void visitLeave(final InitialFunctionDefinition definition) {
353  0 setBlocked(false);
354    }
355   
 
356  0 toggle 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    // test new predicate constant: must always be successful otherwise there
365    // must be a programming error or the predicate definition is not formal correct
366  0 setLocationWithinModule(context + ".getFormula().getElement()");
367  0 test(definition.getFormula().getElement());
368  0 setLocationWithinModule(context);
369  0 setBlocked(true);
370    }
371   
 
372  0 toggle public void visitLeave(final FunctionDefinition definition) {
373  0 setBlocked(false);
374    }
375   
 
376  4 toggle public void visitEnter(final Node node) {
377  4 QedeqLog.getInstance().logMessageState(super.getLocationDescription(),
378    getQedeqBo().getUrl());
379    }
380   
 
381  1 toggle 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   
 
396  1 toggle public void visitLeave(final Proposition definition) {
397    // nothing to do
398    }
399   
 
400  0 toggle 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   
 
416  0 toggle public void visitLeave(final FormalProofLine line) {
417  0 setBlocked(false);
418    }
419   
 
420  0 toggle public void visitEnter(final ConditionalProof line)
421    throws ModuleDataException {
422  0 if (line == null) {
423  0 return;
424    }
425    // add hypothesis to list of conditions
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   
 
434  0 toggle public void visitLeave(final ConditionalProof line) {
435  0 if (line == null) {
436  0 return;
437    }
438    // remove hypothesis of list of conditions
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   
 
453  0 toggle public void visitEnter(final Rule rule) throws ModuleDataException {
454  0 setBlocked(true);
455    }
456   
 
457  0 toggle public void visitLeave(final Rule rule) {
458  0 setBlocked(false);
459    }
460   
 
461  0 toggle public String getLocationDescription() {
462  0 return super.getLocationDescription() + "\n" + interpreter.toString();
463    }
464   
465    }