Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../img/srcFileCovDistChart7.png 74% of files have more coverage
110   308   43   6.47
30   247   0.39   17
17     2.53  
1    
 
  HeuristicCheckerExecutor       Line # 51 110 43 63.1% 0.6305733
 
  (4)
 
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.model.CalculateTruth;
22    import org.qedeq.kernel.bo.logic.model.HeuristicErrorCodes;
23    import org.qedeq.kernel.bo.logic.model.HeuristicException;
24    import org.qedeq.kernel.bo.logic.model.Model;
25    import org.qedeq.kernel.bo.logic.model.ModelFunctionConstant;
26    import org.qedeq.kernel.bo.logic.model.ModelPredicateConstant;
27    import org.qedeq.kernel.bo.logic.model.SixDynamicModel;
28    import org.qedeq.kernel.bo.module.ControlVisitor;
29    import org.qedeq.kernel.bo.module.InternalServiceCall;
30    import org.qedeq.kernel.bo.module.KernelQedeqBo;
31    import org.qedeq.kernel.bo.module.PluginBo;
32    import org.qedeq.kernel.bo.module.PluginExecutor;
33    import org.qedeq.kernel.se.base.list.Element;
34    import org.qedeq.kernel.se.base.module.Axiom;
35    import org.qedeq.kernel.se.base.module.FunctionDefinition;
36    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
37    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
38    import org.qedeq.kernel.se.base.module.PredicateDefinition;
39    import org.qedeq.kernel.se.base.module.Proposition;
40    import org.qedeq.kernel.se.base.module.Rule;
41    import org.qedeq.kernel.se.common.ModuleDataException;
42    import org.qedeq.kernel.se.common.Plugin;
43    import org.qedeq.kernel.se.common.SourceFileExceptionList;
44   
45   
46    /**
47    * Checks if all formulas of a QEDEQ module are well formed.
48    *
49    * @author Michael Meyling
50    */
 
51    public final class HeuristicCheckerExecutor extends ControlVisitor implements PluginExecutor {
52   
53    /** This class. */
54    private static final Class CLASS = HeuristicCheckerExecutor.class;
55   
56    /** Model we use for our heuristic tests. */
57    private Model model;
58   
59    /**
60    * Constructor.
61    *
62    * @param plugin This plugin we work for.
63    * @param qedeq QEDEQ module object.
64    * @param parameters Execution parameters.
65    */
 
66  4 toggle HeuristicCheckerExecutor(final PluginBo plugin, final KernelQedeqBo qedeq,
67    final Parameters parameters) {
68  4 super(plugin, qedeq);
69  4 final String method = "HeuristicChecker(PluginBo, KernelQedeqBo, Map)";
70  4 final String modelClass = parameters.getString("model");
71  4 if (modelClass != null && modelClass.length() > 0) {
72  4 try {
73  4 Class cl = Class.forName(modelClass);
74  4 model = (Model) cl.newInstance();
75    } catch (ClassNotFoundException e) {
76  0 Trace.fatal(CLASS, this, method, "Model class not in class path: "
77    + modelClass, e);
78  0 throw new RuntimeException(e);
79    } catch (InstantiationException e) {
80  0 Trace.fatal(CLASS, this, method, "Model class could not be instanciated: "
81    + modelClass, e);
82  0 throw new RuntimeException(e);
83    } catch (IllegalAccessException e) {
84  0 Trace.fatal(CLASS, this, method,
85    "Programming error, access for instantiation failed for model: "
86    + modelClass, e);
87  0 throw new RuntimeException(e);
88    } catch (RuntimeException e) {
89  0 Trace.fatal(CLASS, this, method,
90    "Programming error, instantiation failed for model: " + modelClass, e);
91  0 throw new RuntimeException(e);
92    }
93    }
94    // fallback is the default model
95  4 if (model == null) {
96  0 model = new SixDynamicModel();
97    }
98    }
99   
 
100  4 toggle private Plugin getPlugin() {
101  4 return (Plugin) getService();
102    }
103   
104   
 
105  4 toggle public Object executePlugin(final InternalServiceCall call, final Object data) {
106  4 final String method = "executePlugin)";
107  4 try {
108  4 QedeqLog.getInstance().logRequest("Heuristic test", getQedeqBo().getUrl());
109  4 traverse(call.getInternalServiceProcess());
110  4 QedeqLog.getInstance().logSuccessfulReply(
111    "Heuristic test succesfull", getQedeqBo().getUrl());
112    } catch (final SourceFileExceptionList e) {
113  0 final String msg = "Test failed";
114  0 Trace.fatal(CLASS, this, method, msg, e);
115  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
116    } catch (final RuntimeException e) {
117  0 Trace.fatal(CLASS, this, method, "unexpected problem", e);
118  0 QedeqLog.getInstance().logFailureReply(
119    "Test failed", getQedeqBo().getUrl(), "unexpected problem: "
120  0 + (e.getMessage() != null ? e.getMessage() : e.toString()));
121    } finally {
122  4 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(),
123    getWarningList());
124    }
125  4 return null;
126    }
127   
128    /**
129    * Check truth value in our model. If it is no tautology an warning is added.
130    * This also happens if our model doesn't support an operator found in the formula.
131    *
132    * @param test Test formula.
133    */
 
134  208 toggle private void test(final Element test) {
135  208 try {
136  182 if (!CalculateTruth.isTautology(getCurrentContext(), model, test)) {
137  14 addWarning(new HeuristicException(HeuristicErrorCodes.EVALUATED_NOT_TRUE_CODE,
138    HeuristicErrorCodes.EVALUATED_NOT_TRUE_TEXT, getCurrentContext()));
139    }
140    } catch (HeuristicException e) {
141  26 addWarning(e);
142    }
143    }
144   
 
145  50 toggle public void visitEnter(final Axiom axiom) throws ModuleDataException {
146  50 if (axiom == null) {
147  0 return;
148    }
149  50 final String context = getCurrentContext().getLocationWithinModule();
150  50 if (axiom.getFormula() != null) {
151  50 setLocationWithinModule(context + ".getFormula().getElement()");
152  50 final Element test = axiom.getFormula().getElement();
153  50 test(test);
154    }
155  50 setLocationWithinModule(context);
156  50 setBlocked(true);
157    }
158   
 
159  50 toggle public void visitLeave(final Axiom axiom) {
160  50 setBlocked(false);
161    }
162   
 
163  4 toggle public void visitEnter(final InitialPredicateDefinition definition)
164    throws ModuleDataException {
165  4 final String method = "visitEnter(PredicateDefinition)";
166  4 if (definition == null) {
167  0 return;
168    }
169  4 final String context = getCurrentContext().getLocationWithinModule();
170  4 try {
171  4 ModelPredicateConstant predicate = new ModelPredicateConstant(definition.getName(),
172    Integer.parseInt(definition.getArgumentNumber()));
173  4 if (null == model.getPredicateConstant(predicate)) {
174  0 setLocationWithinModule(context + ".getName()");
175  0 addWarning(new HeuristicException(
176    HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
177    HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT + predicate,
178    getCurrentContext()));
179    }
180    } catch (NumberFormatException e) {
181  0 Trace.fatal(CLASS, this, method, "not suported argument number: "
182    + definition.getArgumentNumber(), e);
183  0 setLocationWithinModule(context + ".getArgumentNumber()");
184  0 addWarning(new HeuristicException(HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
185    HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT + definition.getArgumentNumber(),
186    getCurrentContext()));
187    }
188  4 setLocationWithinModule(context);
189  4 setBlocked(true);
190    }
191   
 
192  4 toggle public void visitLeave(final InitialPredicateDefinition definition) {
193  4 setBlocked(false);
194    }
195   
 
196  18 toggle public void visitEnter(final PredicateDefinition definition)
197    throws ModuleDataException {
198  18 if (definition == null) {
199  0 return;
200    }
201  18 final String context = getCurrentContext().getLocationWithinModule();
202  18 setLocationWithinModule(context + ".getFormula().getElement()");
203  18 test(definition.getFormula().getElement());
204  18 setLocationWithinModule(context);
205  18 setBlocked(true);
206    }
207   
 
208  18 toggle public void visitLeave(final PredicateDefinition definition) {
209  18 setBlocked(false);
210    }
211   
 
212  0 toggle public void visitEnter(final InitialFunctionDefinition definition)
213    throws ModuleDataException {
214  0 final String method = "visitEnter(FunctionDefinition)";
215  0 if (definition == null) {
216  0 return;
217    }
218  0 final String context = getCurrentContext().getLocationWithinModule();
219  0 try {
220  0 ModelFunctionConstant function = new ModelFunctionConstant(definition.getName(),
221    Integer.parseInt(definition.getArgumentNumber()));
222  0 if (null == model.getFunctionConstant(function)) {
223  0 setLocationWithinModule(context + ".getName()");
224  0 addWarning(new HeuristicException(
225    HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
226    HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT + function,
227    getCurrentContext()));
228    }
229    } catch (NumberFormatException e) {
230  0 Trace.fatal(CLASS, this, method, "not suported argument number: "
231    + definition.getArgumentNumber(), e);
232  0 setLocationWithinModule(context + ".getArgumentNumber()");
233  0 addWarning(new HeuristicException(HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
234    HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT + definition.getArgumentNumber(),
235    getCurrentContext()));
236    }
237  0 setLocationWithinModule(context);
238  0 setBlocked(true);
239    }
240   
 
241  32 toggle public void visitEnter(final FunctionDefinition definition)
242    throws ModuleDataException {
243  32 final String method = "visitEnter(FunctionDefinition)";
244  32 if (definition == null) {
245  0 return;
246    }
247  32 final String context = getCurrentContext().getLocationWithinModule();
248  32 try {
249  32 ModelFunctionConstant function = new ModelFunctionConstant(
250    definition.getName(), Integer.parseInt(definition
251    .getArgumentNumber()));
252  32 if (null == model.getFunctionConstant(function)) {
253  8 setLocationWithinModule(context + ".getName()");
254  8 addWarning(new HeuristicException(
255    HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
256    HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT
257    + function, getCurrentContext()));
258    } else {
259  24 setLocationWithinModule(context + ".getFormula().getElement()");
260  24 test(definition.getFormula().getElement());
261    }
262    } catch (NumberFormatException e) {
263  0 Trace.fatal(CLASS, this, method, "not suported argument number: "
264    + definition.getArgumentNumber(), e);
265  0 setLocationWithinModule(context + ".getArgumentNumber()");
266  0 addWarning(new HeuristicException(
267    HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
268    HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT
269    + definition.getArgumentNumber(),
270    getCurrentContext()));
271    }
272  32 setLocationWithinModule(context);
273  32 setBlocked(true);
274    }
275   
 
276  32 toggle public void visitLeave(final FunctionDefinition definition) {
277  32 setBlocked(false);
278    }
279   
280   
 
281  116 toggle public void visitEnter(final Proposition proposition)
282    throws ModuleDataException {
283  116 if (proposition == null) {
284  0 return;
285    }
286  116 final String context = getCurrentContext().getLocationWithinModule();
287  116 if (proposition.getFormula() != null) {
288  116 setLocationWithinModule(context + ".getFormula().getElement()");
289  116 final Element test = proposition.getFormula().getElement();
290  116 test(test);
291    }
292  116 setLocationWithinModule(context);
293  116 setBlocked(true);
294    }
295   
 
296  116 toggle public void visitLeave(final Proposition definition) {
297  116 setBlocked(false);
298    }
299   
 
300  32 toggle public void visitEnter(final Rule rule) throws ModuleDataException {
301  32 setBlocked(true);
302    }
303   
 
304  32 toggle public void visitLeave(final Rule rule) {
305  32 setBlocked(false);
306    }
307   
308    }