001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.heuristic;
017
018 import org.qedeq.base.io.Parameters;
019 import org.qedeq.base.trace.Trace;
020 import org.qedeq.kernel.bo.log.QedeqLog;
021 import org.qedeq.kernel.bo.logic.common.Operators;
022 import org.qedeq.kernel.bo.logic.model.DynamicDirectInterpreter;
023 import org.qedeq.kernel.bo.logic.model.DynamicModel;
024 import org.qedeq.kernel.bo.logic.model.FourDynamicModel;
025 import org.qedeq.kernel.bo.logic.model.HeuristicErrorCodes;
026 import org.qedeq.kernel.bo.logic.model.HeuristicException;
027 import org.qedeq.kernel.bo.logic.model.ModelFunctionConstant;
028 import org.qedeq.kernel.bo.logic.model.ModelPredicateConstant;
029 import org.qedeq.kernel.bo.module.ControlVisitor;
030 import org.qedeq.kernel.bo.module.InternalServiceProcess;
031 import org.qedeq.kernel.bo.module.KernelQedeqBo;
032 import org.qedeq.kernel.bo.module.PluginBo;
033 import org.qedeq.kernel.bo.module.PluginExecutor;
034 import org.qedeq.kernel.se.base.list.Element;
035 import org.qedeq.kernel.se.base.module.Axiom;
036 import org.qedeq.kernel.se.base.module.ConditionalProof;
037 import org.qedeq.kernel.se.base.module.FormalProofLine;
038 import org.qedeq.kernel.se.base.module.FunctionDefinition;
039 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
040 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
041 import org.qedeq.kernel.se.base.module.Node;
042 import org.qedeq.kernel.se.base.module.PredicateDefinition;
043 import org.qedeq.kernel.se.base.module.Proposition;
044 import org.qedeq.kernel.se.base.module.Rule;
045 import org.qedeq.kernel.se.common.ModuleContext;
046 import org.qedeq.kernel.se.common.ModuleDataException;
047 import org.qedeq.kernel.se.common.SourceFileExceptionList;
048 import org.qedeq.kernel.se.dto.list.DefaultElementList;
049
050
051 /**
052 * Check if formulas are valid in our model.
053 *
054 * @author Michael Meyling
055 */
056 public final class DynamicHeuristicCheckerExecutor extends ControlVisitor implements PluginExecutor {
057
058 /** This class. */
059 private static final Class CLASS = DynamicHeuristicCheckerExecutor.class;
060
061 /** Interpretation for variables. */
062 private final DynamicDirectInterpreter interpreter;
063
064 /** Current condition. */
065 private DefaultElementList condition;
066
067 /**
068 * Constructor.
069 *
070 * @param plugin This plugin we work for.
071 * @param qedeq QEDEQ module object.
072 * @param parameters Execution parameters.
073 */
074 DynamicHeuristicCheckerExecutor(final PluginBo plugin, final KernelQedeqBo qedeq,
075 final Parameters parameters) {
076 super(plugin, qedeq);
077 final String method = "DynamicHeuristicChecker(PluginBo, QedeqBo, Map)";
078 final String modelClass = parameters.getString("model");
079 DynamicModel model = null;
080 if (modelClass != null && modelClass.length() > 0) {
081 try {
082 Class cl = Class.forName(modelClass);
083 model = (DynamicModel) cl.newInstance();
084 } catch (ClassNotFoundException e) {
085 Trace.fatal(CLASS, this, method, "Model class not in class path: "
086 + modelClass, e);
087 } catch (InstantiationException e) {
088 Trace.fatal(CLASS, this, method, "Model class could not be instanciated: "
089 + modelClass, e);
090 } catch (IllegalAccessException e) {
091 Trace.fatal(CLASS, this, method,
092 "Programming error, access for instantiation failed for model: "
093 + modelClass, e);
094 } catch (RuntimeException e) {
095 Trace.fatal(CLASS, this, method,
096 "Programming error, instantiation failed for model: " + modelClass, e);
097 }
098 }
099 // fallback is the default model
100 if (model == null) {
101 model = new FourDynamicModel();
102 }
103 this.interpreter = new DynamicDirectInterpreter(qedeq, model);
104 }
105
106 public Object executePlugin(final InternalServiceProcess process, final Object data) {
107 final String method = "executePlugin()";
108 try {
109 QedeqLog.getInstance().logRequest("Dynamic heuristic test", getQedeqBo().getUrl());
110 // first we try to get more information about required modules and their predicates..
111 try {
112 getServices().checkWellFormedness(getQedeqBo(), process);
113 } catch (Exception e) {
114 // we continue and ignore external predicates
115 Trace.trace(CLASS, method, e);
116 }
117 condition = new DefaultElementList(Operators.CONJUNCTION_OPERATOR);
118 traverse(process);
119 QedeqLog.getInstance().logSuccessfulReply(
120 "Heuristic test succesfull", getQedeqBo().getUrl());
121 } catch (final SourceFileExceptionList e) {
122 final String msg = "Test failed";
123 Trace.fatal(CLASS, this, method, msg, e);
124 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
125 } catch (final RuntimeException e) {
126 Trace.fatal(CLASS, this, method, "unexpected problem", e);
127 QedeqLog.getInstance().logFailureReply(
128 "Test failed", getQedeqBo().getUrl(), "unexpected problem: "
129 + (e.getMessage() != null ? e.getMessage() : e.toString()));
130 } finally {
131 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
132 }
133 return null;
134 }
135
136 /**
137 * Check truth value in our model. If it is no tautology an warning is added.
138 * This also happens if our model doesn't support an operator found in the formula.
139 *
140 * @param test Test formula.
141 */
142 private void test(final Element test) {
143 boolean useCondition = condition.size() > 0; //Assume that we start with an implication,
144 // but the real context begins after skipping ".getList().getElement(1)"
145 try {
146 Element toast = test;
147 if (condition.size() > 0) {
148 final DefaultElementList withCondition = new DefaultElementList(Operators.IMPLICATION_OPERATOR);
149 withCondition.add(condition);
150 withCondition.add(test);
151 toast = withCondition;
152 }
153 if (!isTautology(getCurrentContext(), toast)) {
154 addWarning(new HeuristicException(HeuristicErrorCodes.EVALUATED_NOT_TRUE_CODE,
155 HeuristicErrorCodes.EVALUATED_NOT_TRUE_TEXT + " (\""
156 + interpreter.getModel().getName() + "\")", getCurrentContext()));
157 }
158 } catch (HeuristicException h) {
159 // TODO 20101015 m31: better exception handling would be better!
160 final String begin = getCurrentContext().getLocationWithinModule();
161 // is the error context at the same location? if not we have a problem with a referenced
162 // predicate or function constant and we take the currrent context instead
163 if (!getCurrentContext().getModuleLocation().equals(h.getContext().getModuleLocation())
164 || !h.getContext().getLocationWithinModule().startsWith(begin)) {
165 addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(),
166 getCurrentContext()));
167 } else {
168 String further = h.getContext().getLocationWithinModule().substring(begin.length());
169 if (useCondition) {
170 if (further.startsWith(".getList().getElement(1)")) {
171 further = further.substring(".getList().getElement(1)".length());
172 addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(),
173 new ModuleContext(h.getContext().getModuleLocation(), begin + further)));
174 } else { // must be an error in the condition and for that we have no context
175 addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(),
176 getCurrentContext()));
177 }
178 } else {
179 addWarning(h);
180 }
181 }
182 } catch (RuntimeException e) {
183 Trace.fatal(CLASS, this, "test(Element)", "unexpected runtime exception", e);
184 if (e.getCause() != null && e.getCause() instanceof HeuristicException) {
185 // TODO 20101015 m31: better exception handling would be better!
186 HeuristicException h = (HeuristicException) e.getCause();
187 addWarning(new HeuristicException(h.getErrorCode(), h.getMessage(),
188 getCurrentContext()));
189 } else {
190 addWarning(new HeuristicException(HeuristicErrorCodes.RUNTIME_EXCEPTION_CODE,
191 HeuristicErrorCodes.RUNTIME_EXCEPTION_TEXT + e, getCurrentContext()));
192 }
193 }
194 }
195
196 /**
197 * Test if given formula is a tautology. This is done by checking a model and
198 * iterating through variable values.
199 *
200 * @param moduleContext Here we are within a module.
201 * @param formula Formula.
202 * @return Is this formula a tautology according to our tests.
203 * @throws HeuristicException Evaluation failed.
204 */
205 private boolean isTautology(final ModuleContext moduleContext, final Element formula)
206 throws HeuristicException {
207 boolean result = true;
208 ModuleContext context = moduleContext;
209 try {
210 do {
211 result &= interpreter.calculateValue(new ModuleContext(context), formula);
212 // System.out.println(interpreter.toString());
213 } while (result && interpreter.next());
214 // if (!result) {
215 // System.out.println(interpreter);
216 // }
217 // System.out.println("interpretation finished - and result is = " + result);
218 } finally {
219 interpreter.clearVariables();
220 }
221 return result;
222 }
223
224
225 public void visitEnter(final Axiom axiom) throws ModuleDataException {
226 if (axiom == null) {
227 return;
228 }
229 final String context = getCurrentContext().getLocationWithinModule();
230 QedeqLog.getInstance().logMessageState("\ttesting axiom", getQedeqBo().getUrl());
231 if (axiom.getFormula() != null) {
232 setLocationWithinModule(context + ".getFormula().getElement()");
233 final Element test = axiom.getFormula().getElement();
234 test(test);
235 }
236 setLocationWithinModule(context);
237 setBlocked(true);
238 }
239
240 public void visitLeave(final Axiom axiom) {
241 setBlocked(false);
242 }
243
244 public void visitEnter(final InitialPredicateDefinition definition)
245 throws ModuleDataException {
246 final String method = "visitEnter(InitialPredicateDefinition)";
247 if (definition == null) {
248 return;
249 }
250 QedeqLog.getInstance().logMessageState("\ttesting initial predicate definition",
251 getQedeqBo().getUrl());
252 final String context = getCurrentContext().getLocationWithinModule();
253 try {
254 ModelPredicateConstant predicate = new ModelPredicateConstant(
255 definition.getName(), Integer.parseInt(definition
256 .getArgumentNumber()));
257 // check if model contains predicate
258 if (!interpreter.hasPredicateConstant(predicate)) {
259 setLocationWithinModule(context + ".getName()");
260 addWarning(new HeuristicException(
261 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_CODE,
262 HeuristicErrorCodes.UNKNOWN_PREDICATE_CONSTANT_TEXT
263 + predicate, getCurrentContext()));
264 }
265 } catch (NumberFormatException e) {
266 Trace.fatal(CLASS, this, method, "not suported argument number: "
267 + definition.getArgumentNumber(), e);
268 setLocationWithinModule(context + ".getArgumentNumber()");
269 addWarning(new HeuristicException(
270 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
271 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT
272 + definition.getArgumentNumber(),
273 getCurrentContext()));
274 }
275 setLocationWithinModule(context);
276 setBlocked(true);
277 }
278
279 public void visitLeave(final InitialPredicateDefinition definition) {
280 setBlocked(false);
281 }
282
283 public void visitEnter(final PredicateDefinition definition)
284 throws ModuleDataException {
285 final String method = "visitEnter(PredicateDefinition)";
286 if (definition == null) {
287 return;
288 }
289 QedeqLog.getInstance().logMessageState("\ttesting predicate definition",
290 getQedeqBo().getUrl());
291 final String context = getCurrentContext().getLocationWithinModule();
292 try {
293 // test new predicate constant: must always be successful otherwise there
294 // must be a programming error or the predicate definition is not formal correct
295 setLocationWithinModule(context + ".getFormula().getElement()");
296 test(definition.getFormula().getElement());
297 } catch (NumberFormatException e) {
298 Trace.fatal(CLASS, this, method, "not suported argument number: "
299 + definition.getArgumentNumber(), e);
300 setLocationWithinModule(context + ".getArgumentNumber()");
301 addWarning(new HeuristicException(HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
302 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT + definition.getArgumentNumber(),
303 getCurrentContext()));
304 }
305 setLocationWithinModule(context);
306 setBlocked(true);
307 }
308
309 public void visitLeave(final PredicateDefinition definition) {
310 setBlocked(false);
311 }
312
313 public void visitEnter(final InitialFunctionDefinition definition)
314 throws ModuleDataException {
315 final String method = "visitEnter(InitialFunctionDefinition)";
316 if (definition == null) {
317 return;
318 }
319 QedeqLog.getInstance().logMessageState("\ttesting initial function definition",
320 getQedeqBo().getUrl());
321 final String context = getCurrentContext().getLocationWithinModule();
322 try {
323 ModelFunctionConstant function = new ModelFunctionConstant(definition.getName(),
324 Integer.parseInt(definition.getArgumentNumber()));
325 if (!interpreter.hasFunctionConstant(function)) {
326 // check if model contains predicate
327 setLocationWithinModule(context + ".getName()");
328 addWarning(new HeuristicException(
329 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_CODE,
330 HeuristicErrorCodes.UNKNOWN_FUNCTION_CONSTANT_TEXT
331 + function, getCurrentContext()));
332 }
333 } catch (NumberFormatException e) {
334 Trace.fatal(CLASS, this, method, "not suported argument number: "
335 + definition.getArgumentNumber(), e);
336 setLocationWithinModule(context + ".getArgumentNumber()");
337 addWarning(new HeuristicException(
338 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_CODE,
339 HeuristicErrorCodes.UNKNOWN_ARGUMENT_FORMAT_TEXT
340 + definition.getArgumentNumber(),
341 getCurrentContext()));
342 }
343 setLocationWithinModule(context);
344 setBlocked(true);
345 }
346
347 public void visitLeave(final InitialFunctionDefinition definition) {
348 setBlocked(false);
349 }
350
351 public void visitEnter(final FunctionDefinition definition)
352 throws ModuleDataException {
353 if (definition == null) {
354 return;
355 }
356 QedeqLog.getInstance().logMessageState("\ttesting function definition",
357 getQedeqBo().getUrl());
358 final String context = getCurrentContext().getLocationWithinModule();
359 // test new predicate constant: must always be successful otherwise there
360 // must be a programming error or the predicate definition is not formal correct
361 setLocationWithinModule(context + ".getFormula().getElement()");
362 test(definition.getFormula().getElement());
363 setLocationWithinModule(context);
364 setBlocked(true);
365 }
366
367 public void visitLeave(final FunctionDefinition definition) {
368 setBlocked(false);
369 }
370
371 public void visitEnter(final Node node) {
372 QedeqLog.getInstance().logMessageState(super.getLocationDescription(),
373 getQedeqBo().getUrl());
374 }
375
376 public void visitEnter(final Proposition proposition)
377 throws ModuleDataException {
378 if (proposition == null) {
379 return;
380 }
381 QedeqLog.getInstance().logMessageState("\ttesting proposition", getQedeqBo().getUrl());
382 final String context = getCurrentContext().getLocationWithinModule();
383 if (proposition.getFormula() != null) {
384 setLocationWithinModule(context + ".getFormula().getElement()");
385 final Element test = proposition.getFormula().getElement();
386 test(test);
387 }
388 setLocationWithinModule(context);
389 }
390
391 public void visitLeave(final Proposition definition) {
392 // nothing to do
393 }
394
395 public void visitEnter(final FormalProofLine line)
396 throws ModuleDataException {
397 if (line == null) {
398 return;
399 }
400 QedeqLog.getInstance().logMessageState("\t\ttesting line " + line.getLabel(),
401 getQedeqBo().getUrl());
402 final String context = getCurrentContext().getLocationWithinModule();
403 if (line.getFormula() != null) {
404 setLocationWithinModule(context + ".getFormula().getElement()");
405 test(line.getFormula().getElement());
406 }
407 setLocationWithinModule(context);
408 setBlocked(true);
409 }
410
411 public void visitLeave(final FormalProofLine line) {
412 setBlocked(false);
413 }
414
415 public void visitEnter(final ConditionalProof line)
416 throws ModuleDataException {
417 if (line == null) {
418 return;
419 }
420 // add hypothesis to list of conditions
421 if (line.getHypothesis() != null && line.getHypothesis().getFormula() != null
422 && line.getHypothesis().getFormula().getElement() != null) {
423 condition.add(line.getHypothesis().getFormula().getElement());
424 QedeqLog.getInstance().logMessageState("\t\tadd condit. "
425 + line.getHypothesis().getLabel(), getQedeqBo().getUrl());
426 }
427 }
428
429 public void visitLeave(final ConditionalProof line) {
430 if (line == null) {
431 return;
432 }
433 // remove hypothesis of list of conditions
434 if (line.getHypothesis() != null && line.getHypothesis().getFormula() != null
435 && line.getHypothesis().getFormula().getElement() != null) {
436 condition.remove(condition.size() - 1);
437 }
438 QedeqLog.getInstance().logMessageState("\t\ttesting line "
439 + line.getConclusion().getLabel(), getQedeqBo().getUrl());
440 final String context = getCurrentContext().getLocationWithinModule();
441 if (line.getConclusion().getFormula() != null) {
442 setLocationWithinModule(context + ".getConclusion().getFormula().getElement()");
443 final Element test = line.getConclusion().getFormula().getElement();
444 test(test);
445 }
446 }
447
448 public void visitEnter(final Rule rule) throws ModuleDataException {
449 setBlocked(true);
450 }
451
452 public void visitLeave(final Rule rule) {
453 setBlocked(false);
454 }
455
456 public String getLocationDescription() {
457 return super.getLocationDescription() + "\n" + interpreter.toString();
458 }
459
460 }
|