Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart8.png 62% of files have more coverage
425   997   168   18.48
232   887   0.4   23
23     7.3  
1    
 
  WellFormedCheckerExecutor       Line # 85 425 168 71.5% 0.7147059
 
  (79)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.service.logic;
17   
18    import java.util.HashMap;
19    import java.util.Iterator;
20    import java.util.Map;
21   
22    import org.qedeq.base.io.Parameters;
23    import org.qedeq.base.io.Version;
24    import org.qedeq.base.trace.Trace;
25    import org.qedeq.base.utility.EqualsUtility;
26    import org.qedeq.base.utility.StringUtility;
27    import org.qedeq.kernel.bo.log.QedeqLog;
28    import org.qedeq.kernel.bo.logic.FormulaCheckerFactoryImpl;
29    import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
30    import org.qedeq.kernel.bo.logic.common.FormulaCheckerFactory;
31    import org.qedeq.kernel.bo.logic.common.FormulaUtility;
32    import org.qedeq.kernel.bo.logic.common.FunctionConstant;
33    import org.qedeq.kernel.bo.logic.common.FunctionKey;
34    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
35    import org.qedeq.kernel.bo.logic.common.PredicateConstant;
36    import org.qedeq.kernel.bo.logic.common.PredicateKey;
37    import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl;
38    import org.qedeq.kernel.bo.module.ControlVisitor;
39    import org.qedeq.kernel.bo.module.InternalServiceCall;
40    import org.qedeq.kernel.bo.module.InternalServiceProcess;
41    import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
42    import org.qedeq.kernel.bo.module.KernelQedeqBo;
43    import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
44    import org.qedeq.kernel.bo.module.PluginExecutor;
45    import org.qedeq.kernel.bo.service.dependency.LoadRequiredModulesPlugin;
46    import org.qedeq.kernel.se.base.list.Element;
47    import org.qedeq.kernel.se.base.list.ElementList;
48    import org.qedeq.kernel.se.base.module.Axiom;
49    import org.qedeq.kernel.se.base.module.ChangedRule;
50    import org.qedeq.kernel.se.base.module.ChangedRuleList;
51    import org.qedeq.kernel.se.base.module.ConditionalProof;
52    import org.qedeq.kernel.se.base.module.FormalProof;
53    import org.qedeq.kernel.se.base.module.FormalProofLine;
54    import org.qedeq.kernel.se.base.module.FormalProofLineList;
55    import org.qedeq.kernel.se.base.module.Formula;
56    import org.qedeq.kernel.se.base.module.FunctionDefinition;
57    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
58    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
59    import org.qedeq.kernel.se.base.module.PredicateDefinition;
60    import org.qedeq.kernel.se.base.module.Proposition;
61    import org.qedeq.kernel.se.base.module.Reason;
62    import org.qedeq.kernel.se.base.module.Rule;
63    import org.qedeq.kernel.se.base.module.Specification;
64    import org.qedeq.kernel.se.base.module.SubstFree;
65    import org.qedeq.kernel.se.base.module.SubstFunc;
66    import org.qedeq.kernel.se.base.module.SubstPred;
67    import org.qedeq.kernel.se.common.CheckLevel;
68    import org.qedeq.kernel.se.common.IllegalModuleDataException;
69    import org.qedeq.kernel.se.common.ModuleDataException;
70    import org.qedeq.kernel.se.common.Plugin;
71    import org.qedeq.kernel.se.common.RuleKey;
72    import org.qedeq.kernel.se.common.SourceFileException;
73    import org.qedeq.kernel.se.common.SourceFileExceptionList;
74    import org.qedeq.kernel.se.dto.list.ElementSet;
75    import org.qedeq.kernel.se.state.WellFormedState;
76    import org.qedeq.kernel.se.visitor.InterruptException;
77   
78   
79    /**
80    * Checks if all formulas of a QEDEQ module are well formed.
81    * This plugin assumes all required modules are loaded!
82    *
83    * @author Michael Meyling
84    */
 
85    public final class WellFormedCheckerExecutor extends ControlVisitor implements PluginExecutor {
86   
87    /** This class. */
88    private static final Class CLASS = WellFormedCheckerExecutor.class;
89   
90    /** Class definition via formula rule key. */
91    private static final RuleKey CLASS_DEFINITION_VIA_FORMULA_RULE
92    = new RuleKey("CLASS_DEFINITION_BY_FORMULA", "1.00.00");
93   
94    /** Existence checker for predicate and function constants and rules. */
95    private ModuleConstantsExistenceCheckerImpl existence;
96   
97    /** Factory for generating new checkers. */
98    private FormulaCheckerFactory checkerFactory = null;
99   
100    /**
101    * Constructor.
102    *
103    * @param plugin This plugin we work for.
104    * @param qedeq QEDEQ BO object.
105    * @param parameters Parameters.
106    */
 
107  312 toggle WellFormedCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
108    final Parameters parameters) {
109  312 super(plugin, qedeq);
110  312 final String method = "QedeqBoFormalLogicChecker(Plugin, KernelQedeqBo, Map)";
111  312 final String checkerFactoryClass = parameters.getString("checkerFactory");
112  312 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
113  312 try {
114  312 Class cl = Class.forName(checkerFactoryClass);
115  312 checkerFactory = (FormulaCheckerFactory) cl.newInstance();
116    } catch (ClassNotFoundException e) {
117  0 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class not in class path: "
118    + checkerFactoryClass, e);
119    } catch (InstantiationException e) {
120  0 Trace.fatal(CLASS, this, method, "FormulaCheckerFactory class could not be instanciated: "
121    + checkerFactoryClass, e);
122    } catch (IllegalAccessException e) {
123  0 Trace.fatal(CLASS, this, method,
124    "Programming error, access for instantiation failed for model: "
125    + checkerFactoryClass, e);
126    } catch (RuntimeException e) {
127  0 Trace.fatal(CLASS, this, method,
128    "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
129    }
130    }
131    // fallback is the default checker factory
132  312 if (checkerFactory == null) {
133  0 checkerFactory = new FormulaCheckerFactoryImpl();
134    }
135    }
136   
 
137  312 toggle public Object executePlugin(final InternalServiceCall call, final Object data) throws InterruptException {
138  312 if (getQedeqBo().isWellFormed()) {
139  0 return Boolean.TRUE;
140    }
141  312 QedeqLog.getInstance().logRequest(
142    "Check logical well formedness", getQedeqBo().getUrl());
143  312 if (!getQedeqBo().hasLoadedRequiredModules()) {
144  124 getServices().executePlugin(call.getInternalServiceProcess(),
145    LoadRequiredModulesPlugin.class.getName(), getQedeqBo(), null);
146    }
147  312 if (!getQedeqBo().hasLoadedRequiredModules()) {
148  0 final String msg = "Check of logical well formedness failed";
149  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
150    "Not all required modules could be loaded.");
151  0 return Boolean.FALSE;
152    }
153  312 getQedeqBo().setWellFormedProgressState(WellFormedState.STATE_EXTERNAL_CHECKING);
154  312 getQedeqBo().getLabels().resetNodesToWellFormedUnchecked();
155  312 final SourceFileExceptionList sfl = new SourceFileExceptionList();
156  312 final Map rules = new HashMap(); // map RuleKey to KernelQedeqBo
157  312 final KernelModuleReferenceList list = getQedeqBo().getKernelRequiredModules();
158  481 for (int i = 0; i < list.size(); i++) {
159  169 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
160  169 getServices().checkWellFormedness(call.getInternalServiceProcess(), list.getKernelQedeqBo(i));
161  169 if (!list.getKernelQedeqBo(i).isWellFormed()) {
162  6 ModuleDataException md = new CheckRequiredModuleException(
163    LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
164    LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
165    + list.getQedeqBo(i).getModuleAddress(),
166    list.getModuleContext(i));
167  6 sfl.add(getQedeqBo().createSourceFileException(getService(), md));
168    }
169  169 final ModuleConstantsExistenceChecker existenceChecker
170    = list.getKernelQedeqBo(i).getExistenceChecker();
171  169 if (existenceChecker != null) {
172  169 final Iterator iter = existenceChecker.getRules().keySet().iterator();
173  1551 while (iter.hasNext()) {
174  1382 final RuleKey key = (RuleKey) iter.next();
175  1382 final KernelQedeqBo newQedeq = existenceChecker.getQedeq(key);
176  1382 final KernelQedeqBo previousQedeq = (KernelQedeqBo) rules.get(key);
177  1382 if (previousQedeq != null && !newQedeq.equals(previousQedeq)) {
178  2 ModuleDataException md = new CheckRequiredModuleException(
179    LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE,
180    LogicErrors.RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT
181    + key + " " + previousQedeq.getUrl() + " " + newQedeq.getUrl(),
182    list.getModuleContext(i));
183  2 sfl.add(getQedeqBo().createSourceFileException(getService(), md));
184    } else {
185  1380 rules.put(key, newQedeq);
186    }
187    }
188    }
189    }
190    // has at least one import errors?
191  312 if (sfl.size() > 0) {
192  8 getQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
193  8 final String msg = "Check of logical well formedness failed";
194  8 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
195    StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
196  8 return Boolean.FALSE;
197    }
198  304 getQedeqBo().setWellFormedProgressState(WellFormedState.STATE_INTERNAL_CHECKING);
199   
200  304 try {
201  304 traverse(call.getInternalServiceProcess());
202    } catch (SourceFileExceptionList e) {
203  26 getQedeqBo().setWellfFormedFailureState(WellFormedState.STATE_INTERNAL_CHECKING_FAILED, e);
204  26 getQedeqBo().setExistenceChecker(existence);
205  26 final String msg = "Check of logical well formedness failed";
206  26 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
207    StringUtility.replace(sfl.getMessage(), "\n", "\n\t"));
208  26 return Boolean.FALSE;
209    }
210  278 getQedeqBo().setWellFormed(existence);
211  278 QedeqLog.getInstance().logSuccessfulReply(
212    "Check of logical well formedness successful", getQedeqBo().getUrl());
213  278 return Boolean.TRUE;
214    }
215   
 
216  304 toggle public void traverse(final InternalServiceProcess process) throws SourceFileExceptionList {
217  304 try {
218  304 this.existence = new ModuleConstantsExistenceCheckerImpl(getQedeqBo());
219    } catch (ModuleDataException me) {
220  2 addError(me);
221  2 throw getErrorList();
222    }
223  302 super.traverse(process);
224   
225    // check if we have the important module parts
226  278 setLocationWithinModule("");
227  278 if (getQedeqBo().getQedeq().getHeader() == null) {
228  0 addError(new IllegalModuleDataException(
229    LogicErrors.MODULE_HAS_NO_HEADER_CODE,
230    LogicErrors.MODULE_HAS_NO_HEADER_TEXT,
231    getCurrentContext()));
232    }
233  278 if (getQedeqBo().getQedeq().getHeader().getSpecification() == null) {
234  0 addError(new IllegalModuleDataException(
235    LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_CODE,
236    LogicErrors.MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT,
237    getCurrentContext()));
238    }
239    }
240   
 
241  555 toggle public void visitEnter(final Specification specification) throws ModuleDataException {
242  555 if (specification == null) {
243  0 return;
244    }
245  555 final String context = getCurrentContext().getLocationWithinModule();
246    // we start checking if we have a correct version format
247  555 setLocationWithinModule(context + ".getRuleVersion()");
248  555 final String version = specification.getRuleVersion();
249  555 try {
250  555 new Version(version);
251    } catch (RuntimeException e) {
252  0 addError(new IllegalModuleDataException(
253    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
254    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
255    getCurrentContext()));
256    }
257    }
258   
 
259  2191 toggle public void visitEnter(final Axiom axiom) throws ModuleDataException {
260  2191 if (axiom == null) {
261  0 return;
262    }
263  2191 final String context = getCurrentContext().getLocationWithinModule();
264    // we start checking
265  2191 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
266  2191 if (axiom.getFormula() != null) {
267  2191 setLocationWithinModule(context + ".getFormula().getElement()");
268  2191 final Formula formula = axiom.getFormula();
269  2191 LogicalCheckExceptionList list =
270    checkerFactory.createFormulaChecker().checkFormula(
271    formula.getElement(), getCurrentContext(), existence);
272  2203 for (int i = 0; i < list.size(); i++) {
273  12 addError(list.get(i));
274    }
275    } else {
276  0 getNodeBo().setWellFormed(CheckLevel.FAILURE);
277    }
278    // if we found no errors this node is ok
279  2191 if (!getNodeBo().isNotWellFormed()) {
280  2181 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
281    }
282  2191 setLocationWithinModule(context);
283  2191 setBlocked(true);
284    }
285   
 
286  2191 toggle public void visitLeave(final Axiom axiom) {
287  2191 setBlocked(false);
288    }
289   
 
290  653 toggle public void visitEnter(final PredicateDefinition definition)
291    throws ModuleDataException {
292  653 if (definition == null) {
293  0 return;
294    }
295  653 final String context = getCurrentContext().getLocationWithinModule();
296    // we start checking
297  653 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
298  653 final PredicateKey predicateKey = new PredicateKey(definition.getName(),
299    definition.getArgumentNumber());
300    // we misuse a do loop to be able to break
301  653 do {
302  653 if (existence.predicateExists(predicateKey)) {
303  0 addError(new IllegalModuleDataException(
304    LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
305    LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicateKey,
306    getCurrentContext()));
307  0 break;
308    }
309  653 if (definition.getFormula() == null) {
310  0 addError(new IllegalModuleDataException(
311    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
312    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
313    getCurrentContext()));
314  0 break;
315    }
316  653 final Element completeFormula = definition.getFormula().getElement();
317  653 if (completeFormula == null) {
318  0 addError(new IllegalModuleDataException(
319    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
320    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
321    getCurrentContext()));
322  0 break;
323    }
324  653 setLocationWithinModule(context + ".getFormula().getElement()");
325  653 if (completeFormula.isAtom()) {
326  0 addError(new IllegalModuleDataException(
327    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
328    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
329    getCurrentContext()));
330  0 break;
331    }
332  653 final ElementList equi = completeFormula.getList();
333  653 final String operator = equi.getOperator();
334  653 if (!operator.equals(FormulaCheckerImpl.EQUIVALENCE_OPERATOR)
335    || equi.size() != 2) {
336  0 addError(new IllegalModuleDataException(
337    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE,
338    LogicErrors.PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT,
339    getCurrentContext()));
340  0 break;
341    }
342  653 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(0)");
343  653 if (equi.getElement(0).isAtom()) {
344  0 addError(new IllegalModuleDataException(
345    LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
346    LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
347    getCurrentContext()));
348  0 break;
349    }
350  653 final ElementList predicate = equi.getElement(0).getList();
351  653 if (predicate.getOperator() != FormulaCheckerImpl.PREDICATE_CONSTANT) {
352  0 addError(new IllegalModuleDataException(
353    LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE,
354    LogicErrors.PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT,
355    getCurrentContext()));
356  0 break;
357    }
358  653 final Element definingFormula = equi.getElement(1);
359   
360  653 final ElementSet free = FormulaUtility.getFreeSubjectVariables(definingFormula);
361  2027 for (int i = 0; i < predicate.size(); i++) {
362  1374 setLocationWithinModule(context
363    + ".getFormula().getElement().getList().getElement(0).getList().getElement(" + i + ")");
364  1374 if (i == 0) {
365  653 if (!predicate.getElement(0).isAtom()
366    || !EqualsUtility.equals(definition.getName(),
367    predicate.getElement(0).getAtom().getString())) {
368  0 addError(new IllegalModuleDataException(
369    LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_CODE,
370    LogicErrors.MUST_HAVE_NAME_OF_PREDICATE_TEXT
371    + StringUtility.quote(definition.getName()) + " - "
372    + StringUtility.quote(predicate.getElement(0).getAtom().getString()),
373    getCurrentContext()));
374  0 continue;
375    }
376  721 } else if (!FormulaUtility.isSubjectVariable(predicate.getElement(i))) {
377  0 addError(new IllegalModuleDataException(
378    LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
379    LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT + predicate.getElement(i),
380    getCurrentContext()));
381  0 continue;
382    }
383  1374 setLocationWithinModule(context
384    + ".getFormula().getElement().getList().getElement(1)");
385  1374 if (i != 0 && !free.contains(predicate.getElement(i))) {
386  1 addError(new IllegalModuleDataException(
387    LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
388    LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT + predicate.getElement(i),
389    getCurrentContext()));
390    }
391    }
392  653 setLocationWithinModule(context + ".getFormula().getElement()");
393  653 if (predicate.size() - 1 != free.size()) {
394  0 addError(new IllegalModuleDataException(
395    LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
396    LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
397    getCurrentContext()));
398    }
399  653 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
400  653 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
401    definingFormula, getCurrentContext(), existence);
402  653 for (int i = 0; i < list.size(); i++) {
403  0 addError(list.get(i));
404    }
405  653 if (list.size() > 0) {
406  0 break;
407    }
408  653 setLocationWithinModule(context + ".getFormula().getElement().getList()");
409  653 final PredicateConstant constant = new PredicateConstant(predicateKey,
410    equi, getCurrentContext());
411  653 setLocationWithinModule(context);
412  653 if (existence.predicateExists(predicateKey)) {
413  0 addError(new IllegalModuleDataException(
414    LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
415    LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
416    + predicateKey, getCurrentContext()));
417  0 break;
418    }
419    // a final check, we don't expect any new errors here, but hey - we want to be very sure!
420  653 if (!getNodeBo().isNotWellFormed()) {
421  652 existence.add(constant);
422  652 setLocationWithinModule(context + ".getFormula().getElement()");
423  652 final LogicalCheckExceptionList errorlist = checkerFactory.createFormulaChecker()
424    .checkFormula(completeFormula, getCurrentContext(), existence);
425  652 for (int i = 0; i < errorlist.size(); i++) {
426  0 addError(errorlist.get(i));
427    }
428    }
429    } while (false);
430   
431    // check if we just found the identity operator
432  653 setLocationWithinModule(context);
433  653 if ("2".equals(predicateKey.getArguments())
434    && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
435  0 existence.setIdentityOperatorDefined(predicateKey.getName(),
436    getQedeqBo(), getCurrentContext());
437    }
438    // if we found no errors this node is ok
439  653 if (!getNodeBo().isNotWellFormed()) {
440  652 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
441    }
442  653 setBlocked(true);
443    }
444   
 
445  653 toggle public void visitLeave(final PredicateDefinition definition) {
446  653 setBlocked(false);
447    }
448   
 
449  205 toggle public void visitEnter(final InitialPredicateDefinition definition)
450    throws ModuleDataException {
451  205 if (definition == null) {
452  0 return;
453    }
454  205 final String context = getCurrentContext().getLocationWithinModule();
455    // we start checking
456  205 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
457  205 final PredicateKey predicateKey = new PredicateKey(
458    definition.getName(), definition.getArgumentNumber());
459  205 setLocationWithinModule(context);
460  205 if (existence.predicateExists(predicateKey)) {
461  0 addError(new IllegalModuleDataException(
462    LogicErrors.PREDICATE_ALREADY_DEFINED_CODE,
463    LogicErrors.PREDICATE_ALREADY_DEFINED_TEXT
464    + predicateKey, getCurrentContext()));
465    }
466  205 existence.add(definition);
467    // check if we just found the identity operator
468  205 if ("2".equals(predicateKey.getArguments())
469    && ExistenceChecker.NAME_EQUAL.equals(predicateKey.getName())) {
470  106 existence.setIdentityOperatorDefined(predicateKey.getName(),
471    getQedeqBo(), getCurrentContext());
472    }
473    // if we found no errors this node is ok
474  199 if (!getNodeBo().isNotWellFormed()) {
475  199 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
476    }
477  199 setBlocked(true);
478    }
479   
 
480  199 toggle public void visitLeave(final InitialPredicateDefinition definition) {
481  199 setBlocked(false);
482    }
483   
 
484  0 toggle public void visitEnter(final InitialFunctionDefinition definition)
485    throws ModuleDataException {
486  0 if (definition == null) {
487  0 return;
488    }
489  0 final String context = getCurrentContext().getLocationWithinModule();
490    // we start checking
491  0 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
492  0 final FunctionKey function = new FunctionKey(definition.getName(),
493    definition.getArgumentNumber());
494  0 if (existence.functionExists(function)) {
495  0 addError(new IllegalModuleDataException(
496    LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
497    LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
498    getCurrentContext()));
499    }
500  0 existence.add(definition);
501  0 setLocationWithinModule(context);
502    // if we found no errors this node is ok
503  0 if (!getNodeBo().isNotWellFormed()) {
504  0 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
505    }
506  0 setBlocked(true);
507    }
508   
 
509  0 toggle public void visitLeave(final InitialFunctionDefinition definition) {
510  0 setBlocked(false);
511    }
512   
 
513  1045 toggle public void visitEnter(final FunctionDefinition definition)
514    throws ModuleDataException {
515  1045 if (definition == null) {
516  0 return;
517    }
518  1045 final String context = getCurrentContext().getLocationWithinModule();
519    // we start checking
520  1045 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
521  1045 final FunctionKey function = new FunctionKey(definition.getName(),
522    definition.getArgumentNumber());
523    // we misuse a do loop to be able to break
524  1045 do {
525  1045 if (existence.functionExists(function)) {
526  0 addError(new IllegalModuleDataException(
527    LogicErrors.FUNCTION_ALREADY_DEFINED_CODE,
528    LogicErrors.FUNCTION_ALREADY_DEFINED_TEXT
529    + function, getCurrentContext()));
530  0 break;
531    }
532  1045 if (definition.getFormula() == null) {
533  0 addError(new IllegalModuleDataException(
534    LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
535    LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
536    getCurrentContext()));
537  0 break;
538    }
539  1045 final Formula formulaArgument = definition.getFormula();
540  1045 setLocationWithinModule(context + ".getFormula()");
541  1045 if (formulaArgument.getElement() == null || formulaArgument.getElement().isAtom()) {
542  0 addError(new IllegalModuleDataException(
543    LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE,
544    LogicErrors.NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT,
545    getCurrentContext()));
546  0 break;
547    }
548  1045 final ElementList formula = formulaArgument.getElement().getList();
549  1045 setLocationWithinModule(context + ".getFormula().getElement().getList()");
550  1045 if (!existence.identityOperatorExists()) {
551  1 addError(new IllegalModuleDataException(
552    LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE,
553    LogicErrors.IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT,
554    getCurrentContext()));
555  1 break;
556    }
557  1044 if (!FormulaCheckerImpl.PREDICATE_CONSTANT.equals(formula.getOperator())) {
558  0 addError(new IllegalModuleDataException(
559    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
560    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
561    getCurrentContext()));
562  0 break;
563    }
564  1044 if (formula.size() != 3) {
565  0 addError(new IllegalModuleDataException(
566    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
567    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
568    getCurrentContext()));
569  0 break;
570    }
571  1044 if (!formula.getElement(0).isAtom()) {
572  0 addError(new IllegalModuleDataException(
573    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
574    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
575    getCurrentContext()));
576  0 break;
577    }
578  1044 if (!EqualsUtility.equals(existence.getIdentityOperator(),
579    formula.getElement(0).getAtom().getString())) {
580  0 addError(new IllegalModuleDataException(
581    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE,
582    LogicErrors.DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT,
583    getCurrentContext()));
584  0 break;
585    }
586  1044 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
587  1044 if (formula.getElement(1).isAtom()) {
588  0 addError(new IllegalModuleDataException(
589    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
590    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
591    getCurrentContext()));
592  0 break;
593    }
594  1044 final ElementList functionConstant = formula.getElement(1).getList();
595  1044 if (!FormulaCheckerImpl.FUNCTION_CONSTANT.equals(functionConstant.getOperator())) {
596  0 addError(new IllegalModuleDataException(
597    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
598    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
599    getCurrentContext()));
600  0 break;
601    }
602  1044 setLocationWithinModule(context
603    + ".getFormula().getElement().getList().getElement(1).getList()");
604  1044 final int size = functionConstant.size();
605  1044 if (!("" + (size - 1)).equals(definition.getArgumentNumber())) {
606  0 addError(new IllegalModuleDataException(
607    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
608    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
609    getCurrentContext()));
610  0 break;
611    }
612  1044 setLocationWithinModule(context
613    + ".getFormula().getElement().getList().getElement(1).getList().getElement(0)");
614  1044 if (!functionConstant.getElement(0).isAtom()) {
615  0 addError(new IllegalModuleDataException(
616    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
617    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
618    getCurrentContext()));
619  0 break;
620    }
621  1044 if (!EqualsUtility.equals(definition.getName(),
622    functionConstant.getElement(0).getAtom().getString())) {
623  0 addError(new IllegalModuleDataException(
624    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE,
625    LogicErrors.FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT,
626    getCurrentContext()));
627  0 break;
628    }
629  1044 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
630  1044 if (formula.getElement(2).isAtom()) {
631  0 addError(new IllegalModuleDataException(
632    LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_CODE,
633    LogicErrors.SECOND_OPERAND_MUST_BE_A_TERM_TEXT,
634    getCurrentContext()));
635  0 break;
636    }
637  1044 final ElementList term = formula.getElement(2).getList();
638  1044 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)");
639  1044 final ElementSet free = FormulaUtility.getFreeSubjectVariables(term);
640  1044 if (size - 1 != free.size()) {
641  0 addError(new IllegalModuleDataException(
642    LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE,
643    LogicErrors.NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT,
644    getCurrentContext()));
645  0 break;
646    }
647  1044 if (functionConstant.getElement(0).isList()
648    || !EqualsUtility.equals(function.getName(),
649    functionConstant.getElement(0).getAtom().getString())) {
650  0 addError(new IllegalModuleDataException(
651    LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_CODE,
652    LogicErrors.FUNCTION_NAME_IN_FORMULA_MUST_SAME_TEXT
653    + function.getName(), getCurrentContext()));
654    }
655  2222 for (int i = 1; i < size; i++) {
656  1178 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(1)"
657    + ".getList().getElement(" + i + ")");
658  1178 if (!FormulaUtility.isSubjectVariable(functionConstant.getElement(i))) {
659  0 addError(new IllegalModuleDataException(
660    LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_CODE,
661    LogicErrors.MUST_BE_A_SUBJECT_VARIABLE_TEXT
662    + functionConstant.getElement(i), getCurrentContext()));
663    }
664  1178 if (!free.contains(functionConstant.getElement(i))) {
665  0 addError(new IllegalModuleDataException(
666    LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE,
667    LogicErrors.SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
668    + functionConstant.getElement(i), getCurrentContext()));
669    }
670    }
671  1044 setLocationWithinModule(context + ".getFormula().getElement().getList().getElement(2)");
672  1044 final LogicalCheckExceptionList list = checkerFactory.createFormulaChecker()
673    .checkTerm(term, getCurrentContext(), existence);
674  1044 for (int i = 0; i < list.size(); i++) {
675  0 addError(list.get(i));
676    }
677  1044 if (list.size() > 0) {
678  0 break;
679    }
680  1044 setLocationWithinModule(context + ".getFormula().getElement()");
681    // if we found no errors
682  1044 if (!getNodeBo().isNotWellFormed()) {
683  1044 existence.add(new FunctionConstant(function, formula, getCurrentContext()));
684    // a final check, we don't expect any new errors here, but hey - we want to be very sure!
685  1044 final LogicalCheckExceptionList listComplete = checkerFactory.createFormulaChecker()
686    .checkFormula(formulaArgument.getElement(), getCurrentContext(), existence);
687  1044 for (int i = 0; i < listComplete.size(); i++) {
688  0 addError(listComplete.get(i));
689    }
690    }
691    } while (false);
692  1045 setLocationWithinModule(context);
693    // if we found no errors this node is ok
694  1045 if (!getNodeBo().isNotWellFormed()) {
695  1044 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
696    }
697  1045 setBlocked(true);
698    }
699   
 
700  1045 toggle public void visitLeave(final FunctionDefinition definition) {
701  1045 setBlocked(false);
702    }
703   
 
704  4385 toggle public void visitEnter(final Proposition proposition)
705    throws ModuleDataException {
706  4385 if (proposition == null) {
707  0 return;
708    }
709  4385 final String context = getCurrentContext().getLocationWithinModule();
710    // we start checking
711  4385 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
712  4385 if (proposition.getFormula() != null) {
713  4385 setLocationWithinModule(context + ".getFormula().getElement()");
714  4385 final Formula formula = proposition.getFormula();
715  4385 LogicalCheckExceptionList list = checkerFactory.createFormulaChecker().checkFormula(
716    formula.getElement(), getCurrentContext(), existence);
717  4391 for (int i = 0; i < list.size(); i++) {
718  6 addError(list.get(i));
719    }
720    } else { // no formula
721  0 getNodeBo().setWellFormed(CheckLevel.FAILURE);
722    }
723  4385 if (proposition.getFormalProofList() != null) {
724  1002 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
725  501 final FormalProof proof = proposition.getFormalProofList().get(i);
726  501 if (proof != null) {
727  501 final FormalProofLineList list = proof.getFormalProofLineList();
728  501 setLocationWithinModule(context + ".getFormalProofList().get("
729    + i + ").getFormalProofLineList()");
730  501 checkFormalProof(list);
731    }
732    }
733    }
734  4385 setLocationWithinModule(context);
735    // if we found no errors this node is ok
736  4385 if (!getNodeBo().isNotWellFormed()) {
737  4380 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
738    }
739  4385 setBlocked(true);
740    }
741   
742    /**
743    * Check formal proof formulas.
744    *
745    * @param list List of lines.
746    */
 
747  901 toggle private void checkFormalProof(final FormalProofLineList list) {
748  901 final String context = getCurrentContext().getLocationWithinModule();
749  901 if (list != null) {
750  6393 for (int i = 0; i < list.size(); i++) {
751  5492 final FormalProofLine line = list.get(i);
752  5492 setLocationWithinModule(context + ".get(" + i + ")");
753  5492 checkProofLine(line);
754    }
755    }
756    }
757   
758    /**
759    * Check well-formedness of proof lines.
760    *
761    * @param line Check formulas and terms of this proof line.
762    */
 
763  5492 toggle private void checkProofLine(final FormalProofLine line) {
764  5492 if (line instanceof ConditionalProof) {
765  400 checkProofLine((ConditionalProof) line);
766  400 return;
767    }
768  5092 final String context = getCurrentContext().getLocationWithinModule();
769  5092 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
770  5092 if (line != null) {
771  5092 final Formula formula = line.getFormula();
772  5092 if (formula != null) {
773  5092 setLocationWithinModule(context + ".getFormula().getElement()");
774  5092 elist = checkerFactory.createFormulaChecker().checkFormula(
775    formula.getElement(), getCurrentContext(), existence);
776  5092 for (int k = 0; k < elist.size(); k++) {
777  0 addError(elist.get(k));
778    }
779    }
780  5092 final Reason reason = line.getReason();
781  5092 if (reason != null) {
782  5092 if (reason instanceof SubstFree) {
783  175 final SubstFree subst = (SubstFree) reason;
784  175 if (subst.getSubstFree().getSubstituteTerm() != null) {
785  165 setLocationWithinModule(context
786    + ".getReason().getSubstFree().getSubstituteTerm()");
787  165 elist = checkerFactory.createFormulaChecker().checkTerm(
788    subst.getSubstFree().getSubstituteTerm(),
789    getCurrentContext(), existence);
790    }
791  4917 } else if (reason instanceof SubstPred) {
792  1909 final SubstPred subst = (SubstPred) reason;
793  1909 if (subst.getSubstPred().getSubstituteFormula() != null) {
794  1819 setLocationWithinModule(context
795    + ".getReason().getSubstPred().getSubstituteFormula()");
796  1819 elist = checkerFactory.createFormulaChecker().checkFormula(
797    subst.getSubstPred().getSubstituteFormula(),
798    getCurrentContext(), existence);
799    }
800  3008 } else if (reason instanceof SubstFunc) {
801  51 final SubstFunc subst = (SubstFunc) reason;
802  51 if (subst.getSubstFunc().getSubstituteTerm() != null) {
803  41 setLocationWithinModule(context
804    + ".getReason().getSubstFunc().getSubstituteTerm()");
805  41 elist = checkerFactory.createFormulaChecker().checkTerm(
806    subst.getSubstFunc().getSubstituteTerm(),
807    getCurrentContext(), existence);
808    }
809    }
810  5092 for (int k = 0; k < elist.size(); k++) {
811  0 addError(elist.get(k));
812    }
813    }
814    }
815    }
816   
817    /**
818    * Check well-formedness of proof lines.
819    *
820    * @param line Check formulas and terms of this proof line.
821    */
 
822  400 toggle private void checkProofLine(final ConditionalProof line) {
823  400 final String context = getCurrentContext().getLocationWithinModule();
824  400 LogicalCheckExceptionList elist = new LogicalCheckExceptionList();
825  400 if (line != null) {
826    {
827  400 final Formula formula = line.getFormula();
828  400 if (formula != null && formula.getElement() != null) {
829  400 setLocationWithinModule(context + ".getFormula().getElement()");
830  400 elist = checkerFactory.createFormulaChecker().checkFormula(
831    formula.getElement(), getCurrentContext(), existence);
832  400 for (int k = 0; k < elist.size(); k++) {
833  0 addError(elist.get(k));
834    }
835    }
836    }
837  400 if (line.getHypothesis() != null) {
838  400 final Formula formula = line.getHypothesis().getFormula();;
839  400 if (formula != null && formula.getElement() != null) {
840  400 setLocationWithinModule(context
841    + ".getHypothesis().getFormula().getElement()");
842  400 elist = checkerFactory.createFormulaChecker().checkFormula(
843    formula.getElement(), getCurrentContext(), existence);
844  400 for (int k = 0; k < elist.size(); k++) {
845  0 addError(elist.get(k));
846    }
847    }
848    }
849  400 if (line.getFormalProofLineList() != null) {
850  400 setLocationWithinModule(context + ".getFormalProofLineList()");
851  400 checkFormalProof(line.getFormalProofLineList());
852    }
853  400 if (line.getConclusion() != null) {
854  400 final Formula formula = line.getConclusion().getFormula();;
855  400 if (formula != null && formula.getElement() != null) {
856  400 setLocationWithinModule(context
857    + ".getConclusion().getFormula().getElement()");
858  400 elist = checkerFactory.createFormulaChecker().checkFormula(
859    formula.getElement(), getCurrentContext(), existence);
860  400 for (int k = 0; k < elist.size(); k++) {
861  0 addError(elist.get(k));
862    }
863    }
864    }
865    }
866    }
867   
 
868  4385 toggle public void visitLeave(final Proposition definition) {
869  4385 setBlocked(false);
870    }
871   
 
872  1591 toggle public void visitEnter(final Rule rule) throws ModuleDataException {
873  1591 final String context = getCurrentContext().getLocationWithinModule();
874    // we start checking
875  1591 getNodeBo().setWellFormed(CheckLevel.UNCHECKED);
876  1591 final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion());
877  1591 if (rule.getName() != null && rule.getName().length() > 0 && rule.getVersion() != null
878    && rule.getVersion().length() > 0) {
879  1591 try {
880  1591 setLocationWithinModule(context + ".getVersion()");
881  1591 new Version(rule.getVersion());
882    } catch (RuntimeException e) {
883  0 addError(new IllegalModuleDataException(
884    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
885    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
886    getCurrentContext()));
887    }
888  1591 if (existence.ruleExists(ruleKey)) {
889  2 addError(new IllegalModuleDataException(
890    LogicErrors.RULE_ALREADY_DEFINED_CODE,
891    LogicErrors.RULE_ALREADY_DEFINED_TEXT
892    + ruleKey + " " + existence.getQedeq(ruleKey).getUrl(),
893    getCurrentContext()));
894    } else {
895  1589 if (CLASS_DEFINITION_VIA_FORMULA_RULE.equals(ruleKey)) {
896    // FIXME 20080114 m31: check if this rule can be proposed
897    // are the preconditions for using this rule fulfilled?
898  75 existence.setClassOperatorModule(getQedeqBo(),
899    getCurrentContext());
900    }
901  1589 existence.add(ruleKey, rule);
902    }
903  1591 if (rule.getChangedRuleList() != null) {
904  8 final ChangedRuleList list = rule.getChangedRuleList();
905  72 for (int i = 0; i < list.size(); i++) {
906  64 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ")");
907  64 final ChangedRule r = list.get(i);
908  64 if (r == null || r.getName() == null || r.getName().length() <= 0
909    || r.getVersion() == null || r.getVersion().length() <= 0) {
910  0 addError(new IllegalModuleDataException(
911    LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
912    LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
913  0 + (r == null ? "null" : r.getName() + " [" + r.getVersion() + "]"),
914    getCurrentContext()));
915  0 continue;
916    }
917  64 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
918  64 final String ruleName = r.getName();
919  64 final String ruleVersion = r.getVersion();
920  64 try {
921  64 new Version(ruleVersion);
922    } catch (RuntimeException e) {
923  0 addError(new IllegalModuleDataException(
924    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
925    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + e.getMessage(),
926    getCurrentContext()));
927    }
928  64 RuleKey key1 = getLocalRuleKey(ruleName);
929  64 if (key1 == null) {
930  0 key1 = existence.getParentRuleKey(ruleName);
931    }
932  64 if (key1 == null) {
933  0 addError(new IllegalModuleDataException(
934    LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_CODE,
935    LogicErrors.RULE_WAS_NOT_DECLARED_BEFORE_TEXT
936    + ruleName, getCurrentContext()));
937    } else {
938  64 final RuleKey key2 = new RuleKey(ruleName, ruleVersion);
939  64 if (existence.ruleExists(key2)) {
940  0 addError(new IllegalModuleDataException(
941    LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_CODE,
942    LogicErrors.RULE_HAS_BEEN_DECLARED_BEFORE_TEXT
943    + ruleName, getCurrentContext(), getQedeqBo().getLabels()
944    .getRuleContext(key2)));
945    } else {
946  64 try {
947  64 if (!Version.less(key1.getVersion(), key2.getVersion())) {
948  0 addError(new IllegalModuleDataException(
949    LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE,
950    LogicErrors.NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT
951    + key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels()
952    .getRuleContext(key2)));
953    }
954    } catch (RuntimeException e) {
955  0 addError(new IllegalModuleDataException(
956    LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE,
957    LogicErrors.OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT
958    + key1 + " " + key2, getCurrentContext(), getQedeqBo().getLabels()
959    .getRuleContext(key2)));
960    }
961    }
962  64 existence.add(key2, rule);
963    }
964    }
965    }
966    } else {
967  0 addError(new IllegalModuleDataException(
968    LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_CODE,
969    LogicErrors.RULE_HAS_NO_NAME_OR_VERSION_TEXT
970    + ruleKey, getCurrentContext()));
971    }
972    // if we found no errors this node is ok
973  1591 if (!getNodeBo().isNotWellFormed()) {
974  1589 getNodeBo().setWellFormed(CheckLevel.SUCCESS);
975    }
976  1591 setBlocked(true);
977    }
978   
 
979  1591 toggle public void visitLeave(final Rule rule) {
980  1591 setBlocked(false);
981    }
982   
 
983  30 toggle protected void addError(final ModuleDataException me) {
984  30 if (getNodeBo() != null) {
985  28 getNodeBo().setWellFormed(CheckLevel.FAILURE);
986    }
987  30 super.addError(me);
988    }
989   
 
990  30 toggle protected void addError(final SourceFileException me) {
991  30 if (getNodeBo() != null) {
992  28 getNodeBo().setWellFormed(CheckLevel.FAILURE);
993    }
994  30 super.addError(me);
995    }
996   
997    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .