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