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