0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.service.logic;
0017
0018 import java.util.HashMap;
0019 import java.util.Iterator;
0020 import java.util.Map;
0021
0022 import org.qedeq.base.io.Parameters;
0023 import org.qedeq.base.io.Version;
0024 import org.qedeq.base.trace.Trace;
0025 import org.qedeq.base.utility.EqualsUtility;
0026 import org.qedeq.base.utility.StringUtility;
0027 import org.qedeq.kernel.bo.common.ServiceProcess;
0028 import org.qedeq.kernel.bo.log.QedeqLog;
0029 import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl;
0030 import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
0031 import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory;
0032 import org.qedeq.kernel.bo.logic.common.FormulaUtility;
0033 import org.qedeq.kernel.bo.logic.common.FunctionConstant;
0034 import org.qedeq.kernel.bo.logic.common.FunctionKey;
0035 import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
0036 import org.qedeq.kernel.bo.logic.common.PredicateConstant;
0037 import org.qedeq.kernel.bo.logic.common.PredicateKey;
0038 import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
0039 import org.qedeq.kernel.bo.module.ControlVisitor;
0040 import org.qedeq.kernel.bo.module.InternalServiceProcess;
0041 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
0042 import org.qedeq.kernel.bo.module.KernelQedeqBo;
0043 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
0044 import org.qedeq.kernel.bo.module.PluginExecutor;
0045 import org.qedeq.kernel.bo.service.dependency.LoadRequiredModulesPlugin;
0046 import org.qedeq.kernel.se.base.list.Element;
0047 import org.qedeq.kernel.se.base.list.ElementList;
0048 import org.qedeq.kernel.se.base.module.Axiom;
0049 import org.qedeq.kernel.se.base.module.ChangedRule;
0050 import org.qedeq.kernel.se.base.module.ChangedRuleList;
0051 import org.qedeq.kernel.se.base.module.ConditionalProof;
0052 import org.qedeq.kernel.se.base.module.FormalProof;
0053 import org.qedeq.kernel.se.base.module.FormalProofLine;
0054 import org.qedeq.kernel.se.base.module.FormalProofLineList;
0055 import org.qedeq.kernel.se.base.module.Formula;
0056 import org.qedeq.kernel.se.base.module.FunctionDefinition;
0057 import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
0058 import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
0059 import org.qedeq.kernel.se.base.module.PredicateDefinition;
0060 import org.qedeq.kernel.se.base.module.Proposition;
0061 import org.qedeq.kernel.se.base.module.Reason;
0062 import org.qedeq.kernel.se.base.module.Rule;
0063 import org.qedeq.kernel.se.base.module.Specification;
0064 import org.qedeq.kernel.se.base.module.SubstFree;
0065 import org.qedeq.kernel.se.base.module.SubstFunc;
0066 import org.qedeq.kernel.se.base.module.SubstPred;
0067 import org.qedeq.kernel.se.common.CheckLevel;
0068 import org.qedeq.kernel.se.common.IllegalModuleDataException;
0069 import org.qedeq.kernel.se.common.ModuleDataException;
0070 import org.qedeq.kernel.se.common.Plugin;
0071 import org.qedeq.kernel.se.common.RuleKey;
0072 import org.qedeq.kernel.se.common.SourceFileException;
0073 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0074 import org.qedeq.kernel.se.dto.list.ElementSet;
0075 import org.qedeq.kernel.se.state.WellFormedState;
0076
0077
0078 /**
0079 * Checks if all formulas of a QEDEQ module are well formed.
0080 * This plugin assumes all required modules are loaded!
0081 *
0082 * @author Michael Meyling
0083 */
0084 public final class WellFormedCheckerExecutor extends ControlVisitor implements PluginExecutor {
0085
0086 /** This class. */
0087 private static final Class CLASS = WellFormedCheckerExecutor.class;
0088
0089 /** Class definition via formula rule key. */
0090 private static final RuleKey CLASS_DEFINITION_VIA_FORMULA_RULE
0091 = new RuleKey("CLASS_DEFINITION_BY_FORMULA", "1.00.00");
0092
0093 /** Existence checker for predicate and function constants and rules. */
0094 private ModuleConstantsExistenceCheckerImpl existence;
0095
0096 /** Factory for generating new checkers. */
0097 private FormulaCheckerFactory checkerFactory = null;
0098
0099 /** Parameters for checker. */
0100 private Parameters parameters;
0101
0102 /**
0103 * Constructor.
0104 *
0105 * @param plugin This plugin we work for.
0106 * @param qedeq QEDEQ BO object.
0107 * @param parameters Parameters.
0108 */
0109 WellFormedCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
0110 final Parameters parameters) {
0111 super(plugin, qedeq);
0112 final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)";
0113 this.parameters = parameters;
0114 final String checkerFactoryClass = parameters.getString("checkerFactory");
0115 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
0116 try {
0117 Class cl = Class.forName(checkerFactoryClass);
0118 checkerFactory = (FormulaCheckerFactory) cl.newInstance();
0119 } catch (ClassNotFoundException e) {
0120 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: "
0121 + checkerFactoryClass, e);
0122 } catch (InstantiationException e) {
0123 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: "
0124 + checkerFactoryClass, e);
0125 } catch (IllegalAccessException e) {
0126 Trace.fatal(CLASS, this, method,
0127 "Programming error, access for instantiation failed for model: "
0128 + checkerFactoryClass, e);
0129 } catch (RuntimeException e) {
0130 Trace.fatal(CLASS, this, method,
0131 "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
0132 }
0133 }
0134 // fallback is the default checker factory
0135 if (checkerFactory == null) {
0136 checkerFactory = new FormulaCheckerFactoryImpl();
0137 }
0138 }
0139
0140 private Parameters getParameters() {
0141 return parameters;
0142 }
0143
0144 public Object executePlugin(final InternalServiceProcess process, final Object data) {
0145 if (getQedeqBo().isWellFormed()) {
0146 return Boolean.TRUE;
0147 }
0148 QedeqLog.getInstance().logRequest(
0149 "Check logical well formedness", getQedeqBo().getUrl());
0150 if (!getQedeqBo().hasLoadedRequiredModules()) {
0151 getServices().executePlugin(LoadRequiredModulesPlugin.class.getName(),
0152 getQedeqBo(), null, process);
0153 }
0154 if (!getQedeqBo().hasLoadedRequiredModules()) {
0155 final String msg = "Check of logical well formedness failed";
0156 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
0157 "Not all required modules could be loaded.");
0158 return Boolean.FALSE;
0159 }
0160 getQedeqBo().setWellFormedProgressState(getPlugin(), WellFormedState.STATE_EXTERNAL_CHECKING);
0161 final SourceFileExceptionList sfl = new SourceFileExceptionList();
0162 final Map rules = new HashMap(); // map RuleKey to KernelQedeqBo
0163 final KernelModuleReferenceList list = getQedeqBo().getKernelRequiredModules();
0164 for (int i = 0; i < list.size(); i++) {
0165 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
0166 getServices().checkWellFormedness(list.getKernelQedeqBo(i), process);
0167 if (!list.getKernelQedeqBo(i).isWellFormed()) {
0168 ModuleDataException md = new CheckRequiredModuleException(
0169 LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
0170 LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
0171 + list.getQedeqBo(i).getModuleAddress(),
0172 list.getModuleContext(i));
0173 sfl.add(getQedeqBo().createSourceFileException(getPlugin(), md));
0174 }
0175 final ModuleConstantsExistenceChecker existenceChecker
0176 = list.getKernelQedeqBo(i).getExistenceChecker();
0177 if (existenceChecker != null) {
0178 final Iterator iter = existenceChecker.getRules().keySet().iterator();
0179 while (iter.hasNext()) {
0180 final RuleKey key = (RuleKey) iter.next();
0181 final KernelQedeqBo newQedeq = existenceChecker.getQedeq(key);
0182 final KernelQedeqBo previousQedeq = (KernelQedeqBo) rules.get(key);
0183 if (previousQedeq != null && !newQedeq.equals(previousQedeq)) {
0184 ModuleDataException md = new CheckRequiredModuleException(
0185 LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE,
0186 LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT
0187 + key + " " + previousQedeq.getUrl() + " " + newQedeq.getUrl(),
0188 list.getModuleContext(i));
0189 sfl.add(getQedeqBo().createSourceFileException(getPlugin(), md));
0190 } else {
0191 rules.put(key, newQedeq);
0192 }
0193 }
0194 }
0195 }
0196 // has at least one import errors?
0197 if (sfl.size() > 0) {
0198 getQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
0199 final String msg = "Check of logical well formedness failed";
0200 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
0201 StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
0202 return Boolean.FALSE;
0203 }
0204 getQedeqBo().setWellFormedProgressState(getPlugin(), WellFormedState.STATE_INTERNAL_CHECKING);
0205
0206 try {
0207 traverse(process);
0208 } catch (SourceFileExceptionList e) {
0209 getQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_INTERNAL_CHECKING_FAILED, e);
0210 getQedeqBo().setExistenceChecker(existence);
0211 final String msg = "Check of logical well formedness failed";
0212 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
0213 StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
0214 return Boolean.FALSE;
0215 }
0216 getQedeqBo().setWellFormed(existence);
0217 QedeqLog.getInstance().logSuccessfulReply(
0218 "Check of logical well formedness successful", getQedeqBo().getUrl());
0219 return Boolean.TRUE;
0220 }
0221
0222 public void traverse(final ServiceProcess process) throws SourceFileExceptionList {
0223 try {
0224 this.existence = new ModuleConstantsExistenceCheckerImpl(getQedeqBo());
0225 } catch (ModuleDataException me) {
0226 addError(me);
0227 throw getErrorList();
0228 }
0229 super.traverse(process);
0230
0231 // check if we have the important module parts
0232 setLocationWithinModule("");
0233 if (getQedeqBo().getQedeq().getHeader() == null) {
0234 addError(new IllegalModuleDataException(
0235 LogicErrors.MODULE_HAS_NO_HEADER_CODE,
0236 LogicErrors.MODULE_HAS_NO_HEADER_TEXT,
0237 getCurrentContext()));
0238 }
0239 if (getQedeqBo().getQedeq().getHeader().getSpecification() == null) {
0240 addError(new IllegalModuleDataException(
0241 LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_CODE,
0242 LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT,
0243 getCurrentContext()));
0244 }
0245 }
0246
0247 public void visitEnter(final Specification specification) throws ModuleDataException {
0248 if (specification == null) {
0249 return;
0250 }
0251 final String context = getCurrentContext().getLocationWithinModule();
0252 // we start checking if we have a correct version format
0253 setLocationWithinModule(context + ".getRuleVersion()");
0254 final String version = specification.getRuleVersion();
0255 try {
0256 new Version(version);
0257 } catch (RuntimeException e) {
0258 addError(new IllegalModuleDataException(
0259 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
0260 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
0261 getCurrentContext()));
0262 }
0263 }
0264
0265 public void visitEnter(final Axiom axiom) throws ModuleDataException {
0266 if (axiom == null) {
0267 return;
0268 }
0269 final String context = getCurrentContext().getLocationWithinModule();
0270 // we start checking
0271 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0272 if (axiom.getFormula() != null) {
0273 setLocationWithinModule(context + ".getFormula().getElement()");
0274 final Formula formula = axiom.getFormula();
0275 LogicalCheckExceptionList list =
0276 checkerFactory.createFormulaChecker().checkFormula(
0277 formula.getElement(), getCurrentContext(), existence);
0278 for (int i = 0; i < list.size(); i++) {
0279 addError(list.get(i));
0280 }
0281 } else {
0282 getNodeBo().setWellFormed(CheckLevel.FAILURE);
0283 }
0284 // if we found no errors this node is ok
0285 if (!getNodeBo().isNotWellFormed()) {
0286 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0287 }
0288 setLocationWithinModule(context);
0289 setBlocked(true);
0290 }
0291
0292 public void visitLeave(final Axiom axiom) {
0293 setBlocked(false);
0294 }
0295
0296 public void visitEnter(final PredicateDefinition definition)
0297 throws ModuleDataException {
0298 if (definition == null) {
0299 return;
0300 }
0301 final String context = getCurrentContext().getLocationWithinModule();
0302 // we start checking
0303 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0304 final PredicateKey predicateKey = new PredicateKey(definition.getName(),
0305 definition.getArgumentNumber());
0306 // we misuse a do loop to be able to break
0307 do {
0308 if (existence.predicateExists(predicateKey)) {
0309 addError(new IllegalModuleDataException(
0310 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
0311 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey,
0312 getCurrentContext()));
0313 break;
0314 }
0315 if (definition.getFormula() == null) {
0316 addError(new IllegalModuleDataException(
0317 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
0318 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
0319 getCurrentContext()));
0320 break;
0321 }
0322 final Element completeFormula = definition.getFormula().getElement();
0323 if (completeFormula == null) {
0324 addError(new IllegalModuleDataException(
0325 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
0326 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
0327 getCurrentContext()));
0328 break;
0329 }
0330 setLocationWithinModule(context + ".getFormula().getElement()");
0331 if (completeFormula.isAtom()) {
0332 addError(new IllegalModuleDataException(
0333 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
0334 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
0335 getCurrentContext()));
0336 break;
0337 }
0338 final ElementList equi = completeFormula.getList();
0339 final String operator = equi.getOperator();
0340 if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR)
0341 || equi.size() != 2) {
0342 addError(new IllegalModuleDataException(
0343 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
0344 LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
0345 getCurrentContext()));
0346 break;
0347 }
0348 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)");
0349 if (equi.getElement(0).isAtom()) {
0350 addError(new IllegalModuleDataException(
0351 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
0352 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
0353 getCurrentContext()));
0354 break;
0355 }
0356 final ElementList predicate = equi.getElement(0).getList();
0357 if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) {
0358 addError(new IllegalModuleDataException(
0359 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
0360 LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
0361 getCurrentContext()));
0362 break;
0363 }
0364 final Element definingFormula = equi.getElement(1);
0365
0366 final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula);
0367 for (int i = 0; i < predicate.size(); i++) {
0368 setLocationWithinModule(context
0369 + ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")");
0370 if (i == 0) {
0371 if (!predicate.getElement(0).isAtom()
0372 || !EqualsUtility.equals(definition.getName(),
0373 predicate.getElement(0).getAtom().getString())) {
0374 addError(new IllegalModuleDataException(
0375 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE,
0376 LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT
0377 + StringUtility.quote(definition.getName()) + " - "
0378 + StringUtility.quote(predicate.getElement(0).getAtom().getString()),
0379 getCurrentContext()));
0380 continue;
0381 }
0382 } else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) {
0383 addError(new IllegalModuleDataException(
0384 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
0385 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i),
0386 getCurrentContext()));
0387 continue;
0388 }
0389 setLocationWithinModule(context
0390 + ".getFormula().getElement().getList().getElement(1)");
0391 if (i != 0 && !free.contains(predicate.getElement(i))) {
0392 addError(new IllegalModuleDataException(
0393 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
0394 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i),
0395 getCurrentContext()));
0396 }
0397 }
0398 setLocationWithinModule(context + ".getFormula().getElement()");
0399 if (predicate.size() - 1 != free.size()) {
0400 addError(new IllegalModuleDataException(
0401 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
0402 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
0403 getCurrentContext()));
0404 }
0405 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
0406 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
0407 definingFormula, getCurrentContext(), existence);
0408 for (int i = 0; i < list.size(); i++) {
0409 addError(list.get(i));
0410 }
0411 if (list.size() > 0) {
0412 break;
0413 }
0414 setLocationWithinModule(context + ".getFormula().getElement().getList()");
0415 final PredicateConstant constant = new PredicateConstant(predicateKey,
0416 equi, getCurrentContext());
0417 setLocationWithinModule(context);
0418 if (existence.predicateExists(predicateKey)) {
0419 addError(new IllegalModuleDataException(
0420 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
0421 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
0422 + predicateKey, getCurrentContext()));
0423 break;
0424 }
0425 // a final check, we don't expect any new errors here, but hey - we want to be very sure!
0426 if (!getNodeBo().isNotWellFormed()) {
0427 existence.add(constant);
0428 setLocationWithinModule(context + ".getFormula().getElement()");
0429 final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker()
0430 .checkFormula(completeFormula, getCurrentContext(), existence);
0431 for (int i = 0; i < errorlist.size(); i++) {
0432 addError(errorlist.get(i));
0433 }
0434 }
0435 } while (false);
0436
0437 // check if we just found the identity operator
0438 setLocationWithinModule(context);
0439 if ("2".equals(predicateKey.getArguments())
0440 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
0441 existence.setIdentityOperatorDefined(predicateKey.getName(),
0442 getQedeqBo(), getCurrentContext());
0443 }
0444 // if we found no errors this node is ok
0445 if (!getNodeBo().isNotWellFormed()) {
0446 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0447 }
0448 setBlocked(true);
0449 }
0450
0451 public void visitLeave(final PredicateDefinition definition) {
0452 setBlocked(false);
0453 }
0454
0455 public void visitEnter(final InitialPredicateDefinition definition)
0456 throws ModuleDataException {
0457 if (definition == null) {
0458 return;
0459 }
0460 final String context = getCurrentContext().getLocationWithinModule();
0461 // we start checking
0462 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0463 final PredicateKey predicateKey = new PredicateKey(
0464 definition.getName(), definition.getArgumentNumber());
0465 setLocationWithinModule(context);
0466 if (existence.predicateExists(predicateKey)) {
0467 addError(new IllegalModuleDataException(
0468 LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
0469 LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
0470 + predicateKey, getCurrentContext()));
0471 }
0472 existence.add(definition);
0473 // check if we just found the identity operator
0474 if ("2".equals(predicateKey.getArguments())
0475 && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
0476 existence.setIdentityOperatorDefined(predicateKey.getName(),
0477 getQedeqBo(), getCurrentContext());
0478 }
0479 // if we found no errors this node is ok
0480 if (!getNodeBo().isNotWellFormed()) {
0481 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0482 }
0483 setBlocked(true);
0484 }
0485
0486 public void visitLeave(final InitialPredicateDefinition definition) {
0487 setBlocked(false);
0488 }
0489
0490 public void visitEnter(final InitialFunctionDefinition definition)
0491 throws ModuleDataException {
0492 if (definition == null) {
0493 return;
0494 }
0495 final String context = getCurrentContext().getLocationWithinModule();
0496 // we start checking
0497 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0498 final FunctionKey function = new FunctionKey(definition.getName(),
0499 definition.getArgumentNumber());
0500 if (existence.functionExists(function)) {
0501 addError(new IllegalModuleDataException(
0502 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
0503 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
0504 getCurrentContext()));
0505 }
0506 existence.add(definition);
0507 setLocationWithinModule(context);
0508 // if we found no errors this node is ok
0509 if (!getNodeBo().isNotWellFormed()) {
0510 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0511 }
0512 setBlocked(true);
0513 }
0514
0515 public void visitLeave(final InitialFunctionDefinition definition) {
0516 setBlocked(false);
0517 }
0518
0519 public void visitEnter(final FunctionDefinition definition)
0520 throws ModuleDataException {
0521 if (definition == null) {
0522 return;
0523 }
0524 final String context = getCurrentContext().getLocationWithinModule();
0525 // we start checking
0526 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0527 final FunctionKey function = new FunctionKey(definition.getName(),
0528 definition.getArgumentNumber());
0529 // we misuse a do loop to be able to break
0530 do {
0531 if (existence.functionExists(function)) {
0532 addError(new IllegalModuleDataException(
0533 LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
0534 LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
0535 + function, getCurrentContext()));
0536 break;
0537 }
0538 if (definition.getFormula() == null) {
0539 addError(new IllegalModuleDataException(
0540 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
0541 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
0542 getCurrentContext()));
0543 break;
0544 }
0545 final Formula formulaArgument = definition.getFormula();
0546 setLocationWithinModule(context + ".getFormula()");
0547 if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) {
0548 addError(new IllegalModuleDataException(
0549 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
0550 LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
0551 getCurrentContext()));
0552 break;
0553 }
0554 final ElementList formula = formulaArgument.getElement().getList();
0555 setLocationWithinModule(context + ".getFormula().getElement().getList()");
0556 if (!existence.identityOperatorExists()) {
0557 addError(new IllegalModuleDataException(
0558 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE,
0559 LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT,
0560 getCurrentContext()));
0561 break;
0562 }
0563 if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) {
0564 addError(new IllegalModuleDataException(
0565 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
0566 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
0567 getCurrentContext()));
0568 break;
0569 }
0570 if (formula.size() != 3) {
0571 addError(new IllegalModuleDataException(
0572 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
0573 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
0574 getCurrentContext()));
0575 break;
0576 }
0577 if (!formula.getElement(0).isAtom()) {
0578 addError(new IllegalModuleDataException(
0579 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
0580 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
0581 getCurrentContext()));
0582 break;
0583 }
0584 if (!EqualsUtility.equals(existence.getIdentityOperator(),
0585 formula.getElement(0).getAtom().getString())) {
0586 addError(new IllegalModuleDataException(
0587 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
0588 LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
0589 getCurrentContext()));
0590 break;
0591 }
0592 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
0593 if (formula.getElement(1).isAtom()) {
0594 addError(new IllegalModuleDataException(
0595 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
0596 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
0597 getCurrentContext()));
0598 break;
0599 }
0600 final ElementList functionConstant = formula.getElement(1).getList();
0601 if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) {
0602 addError(new IllegalModuleDataException(
0603 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
0604 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
0605 getCurrentContext()));
0606 break;
0607 }
0608 setLocationWithinModule(context
0609 + ".getFormula().getElement().getList().getElement(1).getList()");
0610 final int size = functionConstant.size();
0611 if (!("" + (size - 1)).equals(definition.getArgumentNumber())) {
0612 addError(new IllegalModuleDataException(
0613 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
0614 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
0615 getCurrentContext()));
0616 break;
0617 }
0618 setLocationWithinModule(context
0619 + ".getFormula().getElement().getList().getElement(1).getList().getElement(0)");
0620 if (!functionConstant.getElement(0).isAtom()) {
0621 addError(new IllegalModuleDataException(
0622 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
0623 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
0624 getCurrentContext()));
0625 break;
0626 }
0627 if (!EqualsUtility.equals(definition.getName(),
0628 functionConstant.getElement(0).getAtom().getString())) {
0629 addError(new IllegalModuleDataException(
0630 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
0631 LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
0632 getCurrentContext()));
0633 break;
0634 }
0635 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
0636 if (formula.getElement(2).isAtom()) {
0637 addError(new IllegalModuleDataException(
0638 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE,
0639 LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT,
0640 getCurrentContext()));
0641 break;
0642 }
0643 final ElementList term = formula.getElement(2).getList();
0644 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
0645 final ElementSet free = FormulaUtility.getFreeSubjectVariables(term);
0646 if (size - 1 != free.size()) {
0647 addError(new IllegalModuleDataException(
0648 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
0649 LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
0650 getCurrentContext()));
0651 break;
0652 }
0653 if (functionConstant.getElement(0).isList()
0654 || !EqualsUtility.equals(function.getName(),
0655 functionConstant.getElement(0).getAtom().getString())) {
0656 addError(new IllegalModuleDataException(
0657 LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_CODE,
0658 LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_TEXT
0659 + function.getName(), getCurrentContext()));
0660 }
0661 for (int i = 1; i < size; i++) {
0662 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"
0663 + ".getList().getElement(" + i + ")");
0664 if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) {
0665 addError(new IllegalModuleDataException(
0666 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
0667 LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT
0668 + functionConstant.getElement(i), getCurrentContext()));
0669 }
0670 if (!free.contains(functionConstant.getElement(i))) {
0671 addError(new IllegalModuleDataException(
0672 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
0673 LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
0674 + functionConstant.getElement(i), getCurrentContext()));
0675 }
0676 }
0677 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
0678 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker()
0679 .checkTerm(term, getCurrentContext(), existence);
0680 for (int i = 0; i < list.size(); i++) {
0681 addError(list.get(i));
0682 }
0683 if (list.size() > 0) {
0684 break;
0685 }
0686 setLocationWithinModule(context + ".getFormula().getElement()");
0687 // if we found no errors
0688 if (!getNodeBo().isNotWellFormed()) {
0689 existence.add(new FunctionConstant(function, formula, getCurrentContext()));
0690 // a final check, we don't expect any new errors here, but hey - we want to be very sure!
0691 final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker()
0692 .checkFormula(formulaArgument.getElement(), getCurrentContext(), existence);
0693 for (int i = 0; i < listComplete.size(); i++) {
0694 addError(listComplete.get(i));
0695 }
0696 }
0697 } while (false);
0698 setLocationWithinModule(context);
0699 // if we found no errors this node is ok
0700 if (!getNodeBo().isNotWellFormed()) {
0701 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0702 }
0703 setBlocked(true);
0704 }
0705
0706 public void visitLeave(final FunctionDefinition definition) {
0707 setBlocked(false);
0708 }
0709
0710 public void visitEnter(final Proposition proposition)
0711 throws ModuleDataException {
0712 if (proposition == null) {
0713 return;
0714 }
0715 final String context = getCurrentContext().getLocationWithinModule();
0716 // we start checking
0717 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0718 if (proposition.getFormula() != null) {
0719 setLocationWithinModule(context + ".getFormula().getElement()");
0720 final Formula formula = proposition.getFormula();
0721 LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
0722 formula.getElement(), getCurrentContext(), existence);
0723 for (int i = 0; i < list.size(); i++) {
0724 addError(list.get(i));
0725 }
0726 } else { // no formula
0727 getNodeBo().setWellFormed(CheckLevel.FAILURE);
0728 }
0729 if (proposition.getFormalProofList() != null) {
0730 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
0731 final FormalProof proof = proposition.getFormalProofList().get(i);
0732 if (proof != null) {
0733 final FormalProofLineList list = proof.getFormalProofLineList();
0734 setLocationWithinModule(context + ".getFormalProofList().get("
0735 + i + ").getFormalProofLineList()");
0736 checkFormalProof(list);
0737 }
0738 }
0739 }
0740 setLocationWithinModule(context);
0741 // if we found no errors this node is ok
0742 if (!getNodeBo().isNotWellFormed()) {
0743 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0744 }
0745 setBlocked(true);
0746 }
0747
0748 /**
0749 * Check formal proof formulas.
0750 *
0751 * @param list List of lines.
0752 */
0753 private void checkFormalProof(final FormalProofLineList list) {
0754 final String context = getCurrentContext().getLocationWithinModule();
0755 if (list != null) {
0756 for (int i = 0; i < list.size(); i++) {
0757 final FormalProofLine line = list.get(i);
0758 setLocationWithinModule(context + ".get(" + i + ")");
0759 checkProofLine(line);
0760 }
0761 }
0762 }
0763
0764 /**
0765 * Check well-formedness of proof lines.
0766 *
0767 * @param line Check formulas and terms of this proof line.
0768 */
0769 private void checkProofLine(final FormalProofLine line) {
0770 if (line instanceof ConditionalProof) {
0771 checkProofLine((ConditionalProof) line);
0772 return;
0773 }
0774 final String context = getCurrentContext().getLocationWithinModule();
0775 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
0776 if (line != null) {
0777 final Formula formula = line.getFormula();
0778 if (formula != null) {
0779 setLocationWithinModule(context + ".getFormula().getElement()");
0780 elist = checkerFactory.createFormulaChecker().checkFormula(
0781 formula.getElement(), getCurrentContext(), existence);
0782 for (int k = 0; k < elist.size(); k++) {
0783 addError(elist.get(k));
0784 }
0785 }
0786 final Reason reason = line.getReason();
0787 if (reason != null) {
0788 if (reason instanceof SubstFree) {
0789 final SubstFree subst = (SubstFree) reason;
0790 if (subst.getSubstFree().getSubstituteTerm() != null) {
0791 setLocationWithinModule(context
0792 + ".getReason().getSubstFree().getSubstituteTerm()");
0793 elist = checkerFactory.createFormulaChecker().checkTerm(
0794 subst.getSubstFree().getSubstituteTerm(),
0795 getCurrentContext(), existence);
0796 }
0797 } else if (reason instanceof SubstPred) {
0798 final SubstPred subst = (SubstPred) reason;
0799 if (subst.getSubstPred().getSubstituteFormula() != null) {
0800 setLocationWithinModule(context
0801 + ".getReason().getSubstPred().getSubstituteFormula()");
0802 elist = checkerFactory.createFormulaChecker().checkFormula(
0803 subst.getSubstPred().getSubstituteFormula(),
0804 getCurrentContext(), existence);
0805 }
0806 } else if (reason instanceof SubstFunc) {
0807 final SubstFunc subst = (SubstFunc) reason;
0808 if (subst.getSubstFunc().getSubstituteTerm() != null) {
0809 setLocationWithinModule(context
0810 + ".getReason().getSubstFunc().getSubstituteTerm()");
0811 elist = checkerFactory.createFormulaChecker().checkTerm(
0812 subst.getSubstFunc().getSubstituteTerm(),
0813 getCurrentContext(), existence);
0814 }
0815 }
0816 for (int k = 0; k < elist.size(); k++) {
0817 addError(elist.get(k));
0818 }
0819 }
0820 }
0821 }
0822
0823 /**
0824 * Check well-formedness of proof lines.
0825 *
0826 * @param line Check formulas and terms of this proof line.
0827 */
0828 private void checkProofLine(final ConditionalProof line) {
0829 final String context = getCurrentContext().getLocationWithinModule();
0830 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
0831 if (line != null) {
0832 {
0833 final Formula formula = line.getFormula();
0834 if (formula != null && formula.getElement() != null) {
0835 setLocationWithinModule(context + ".getFormula().getElement()");
0836 elist = checkerFactory.createFormulaChecker().checkFormula(
0837 formula.getElement(), getCurrentContext(), existence);
0838 for (int k = 0; k < elist.size(); k++) {
0839 addError(elist.get(k));
0840 }
0841 }
0842 }
0843 if (line.getHypothesis() != null) {
0844 final Formula formula = line.getHypothesis().getFormula();;
0845 if (formula != null && formula.getElement() != null) {
0846 setLocationWithinModule(context
0847 + ".getHypothesis().getFormula().getElement()");
0848 elist = checkerFactory.createFormulaChecker().checkFormula(
0849 formula.getElement(), getCurrentContext(), existence);
0850 for (int k = 0; k < elist.size(); k++) {
0851 addError(elist.get(k));
0852 }
0853 }
0854 }
0855 if (line.getFormalProofLineList() != null) {
0856 setLocationWithinModule(context + ".getFormalProofLineList()");
0857 checkFormalProof(line.getFormalProofLineList());
0858 }
0859 if (line.getConclusion() != null) {
0860 final Formula formula = line.getConclusion().getFormula();;
0861 if (formula != null && formula.getElement() != null) {
0862 setLocationWithinModule(context
0863 + ".getConclusion().getFormula().getElement()");
0864 elist = checkerFactory.createFormulaChecker().checkFormula(
0865 formula.getElement(), getCurrentContext(), existence);
0866 for (int k = 0; k < elist.size(); k++) {
0867 addError(elist.get(k));
0868 }
0869 }
0870 }
0871 }
0872 }
0873
0874 public void visitLeave(final Proposition definition) {
0875 setBlocked(false);
0876 }
0877
0878 public void visitEnter(final Rule rule) throws ModuleDataException {
0879 final String context = getCurrentContext().getLocationWithinModule();
0880 // we start checking
0881 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
0882 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
0883 if (rule.getName() != null && rule.getName().length() > 0 && rule.getVersion() != null
0884 && rule.getVersion().length() > 0) {
0885 try {
0886 setLocationWithinModule(context + ".getVersion()");
0887 new Version(rule.getVersion());
0888 } catch (RuntimeException e) {
0889 addError(new IllegalModuleDataException(
0890 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
0891 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
0892 getCurrentContext()));
0893 }
0894 if (existence.ruleExists(ruleKey)) {
0895 addError(new IllegalModuleDataException(
0896 LogicErrors.RULE_ALREADY_DEFINED_CODE,
0897 LogicErrors.RULE_ALREADY_DEFINED_TEXT
0898 + ruleKey + " " + existence.getQedeq(ruleKey).getUrl(),
0899 getCurrentContext()));
0900 } else {
0901 if (CLASS_DEFINITION_VIA_FORMULA_RULE.equals(ruleKey)) {
0902 // TODO 20080114 m31: check if this rule can be proposed
0903 // are the preconditions for using this rule fulfilled?
0904 existence.setClassOperatorModule(getQedeqBo(),
0905 getCurrentContext());
0906 }
0907 existence.add(ruleKey, rule);
0908 }
0909 if (rule.getChangedRuleList() != null) {
0910 final ChangedRuleList list = rule.getChangedRuleList();
0911 for (int i = 0; i < list.size(); i++) {
0912 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ")");
0913 final ChangedRule r = list.get(i);
0914 if (r == null || r.getName() == null || r.getName().length() <= 0
0915 || r.getVersion() == null || r.getVersion().length() <= 0) {
0916 addError(new IllegalModuleDataException(
0917 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
0918 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
0919 + (r == null ? "null" : r.getName() + " [" + r.getVersion() + "]"),
0920 getCurrentContext()));
0921 continue;
0922 }
0923 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
0924 final String ruleName = r.getName();
0925 final String ruleVersion = r.getVersion();
0926 try {
0927 new Version(ruleVersion);
0928 } catch (RuntimeException e) {
0929 addError(new IllegalModuleDataException(
0930 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
0931 LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
0932 getCurrentContext()));
0933 }
0934 RuleKey key1 = getLocalRuleKey(ruleName);
0935 if (key1 == null) {
0936 key1 = existence.getParentRuleKey(ruleName);
0937 }
0938 if (key1 == null) {
0939 addError(new IllegalModuleDataException(
0940 LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_CODE,
0941 LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_TEXT
0942 + ruleName, getCurrentContext()));
0943 } else {
0944 final RuleKey key2 = new RuleKey(ruleName, ruleVersion);
0945 if (existence.ruleExists(key2)) {
0946 addError(new IllegalModuleDataException(
0947 LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_CODE,
0948 LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_TEXT
0949 + ruleName, getCurrentContext(), getQedeqBo().getLabels()
0950 .getRuleContext(key2)));
0951 } else {
0952 try {
0953 if (!Version.less(key1.getVersion(), key2.getVersion())) {
0954 addError(new IllegalModuleDataException(
0955 LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE,
0956 LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT
0957 + key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels()
0958 .getRuleContext(key2)));
0959 }
0960 } catch (RuntimeException e) {
0961 addError(new IllegalModuleDataException(
0962 LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE,
0963 LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT
0964 + key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels()
0965 .getRuleContext(key2)));
0966 }
0967 }
0968 existence.add(key2, rule);
0969 }
0970 }
0971 }
0972 } else {
0973 addError(new IllegalModuleDataException(
0974 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
0975 LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
0976 + ruleKey, getCurrentContext()));
0977 }
0978 // if we found no errors this node is ok
0979 if (!getNodeBo().isNotWellFormed()) {
0980 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
0981 }
0982 setBlocked(true);
0983 }
0984
0985 public void visitLeave(final Rule rule) {
0986 setBlocked(false);
0987 }
0988
0989 protected void addError(final ModuleDataException me) {
0990 if (getNodeBo() != null) {
0991 getNodeBo().setWellFormed(CheckLevel.FAILURE);
0992 }
0993 super.addError(me);
0994 }
0995
0996 protected void addError(final SourceFileException me) {
0997 if (getNodeBo() != null) {
0998 getNodeBo().setWellFormed(CheckLevel.FAILURE);
0999 }
1000 super.addError(me);
1001 }
1002
1003 }
|