Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
97   242   22   6.47
4   187   0.23   15
15     1.47  
1    
 
  FormulaCheckerContextTest       Line # 60 97 22 94.8% 0.94827586
 
  (12)
 
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.logic.wf;
17   
18    import java.io.File;
19    import java.io.IOException;
20    import java.util.HashMap;
21    import java.util.Map;
22   
23    import javax.xml.parsers.ParserConfigurationException;
24   
25    import org.qedeq.base.io.Parameters;
26    import org.qedeq.base.io.UrlUtility;
27    import org.qedeq.base.trace.Trace;
28    import org.qedeq.base.utility.YodaUtility;
29    import org.qedeq.kernel.bo.logic.common.FormulaChecker;
30    import org.qedeq.kernel.bo.logic.common.LogicalCheckException;
31    import org.qedeq.kernel.bo.module.InternalServiceCall;
32    import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
33    import org.qedeq.kernel.bo.module.KernelQedeqBo;
34    import org.qedeq.kernel.bo.module.QedeqFileDao;
35    import org.qedeq.kernel.bo.service.control.DefaultKernelQedeqBo;
36    import org.qedeq.kernel.bo.service.control.ModuleLabelsCreator;
37    import org.qedeq.kernel.bo.service.control.QedeqVoBuilder;
38    import org.qedeq.kernel.bo.service.logic.WellFormedCheckerExecutor;
39    import org.qedeq.kernel.bo.service.logic.WellFormedCheckerPlugin;
40    import org.qedeq.kernel.bo.test.DummyPlugin;
41    import org.qedeq.kernel.bo.test.KernelFacade;
42    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
43    import org.qedeq.kernel.se.common.ModuleAddress;
44    import org.qedeq.kernel.se.common.ModuleDataException;
45    import org.qedeq.kernel.se.common.SourceFileException;
46    import org.qedeq.kernel.se.common.SourceFileExceptionList;
47    import org.qedeq.kernel.se.dto.module.QedeqVo;
48    import org.qedeq.kernel.se.visitor.InterruptException;
49    import org.qedeq.kernel.xml.dao.XmlQedeqFileDao;
50    import org.qedeq.kernel.xml.handler.common.SaxDefaultHandler;
51    import org.qedeq.kernel.xml.handler.module.QedeqHandler;
52    import org.qedeq.kernel.xml.parser.SaxParser;
53    import org.xml.sax.SAXException;
54   
55    /**
56    * Test logic tests for QEDEQ modules.
57    *
58    * @author Michael Meyling
59    */
 
60    public final class FormulaCheckerContextTest extends QedeqBoTestCase {
61   
62    /** This class. */
63    private static final Class CLASS = FormulaChecker.class;
64    private InternalServiceCall call;
65   
66   
 
67  12 toggle protected void tearDown() throws Exception {
68  12 endServiceCall(call);
69  12 super.tearDown();
70    }
71   
 
72  1 toggle public void testNegative00() throws Exception {
73  1 try {
74  1 check(getFile("qedeq_error_sample_00.xml"));
75  0 fail("SourceFileExceptionList expected");
76    } catch (SourceFileExceptionList ex) {
77  1 Trace.trace(CLASS, this, "testNegative00", ex);
78  1 assertEquals(1, ex.size());
79  1 final SourceFileException check = ex.get(0);
80    // check.printStackTrace();
81  1 assertEquals(9001, check.getErrorCode());
82  1 assertEquals(36, check.getSourceArea().getStartPosition().getRow());
83  1 assertEquals(1, check.getSourceArea().getStartPosition().getColumn());
84  1 assertEquals(36, check.getSourceArea().getEndPosition().getRow());
85  1 assertEquals(20, check.getSourceArea().getEndPosition().getColumn());
86    }
87    }
88   
 
89  1 toggle public void testNegative01() throws Exception {
90  1 try {
91  1 check(getFile("qedeq_error_sample_01.xml"));
92  0 fail("SourceFileExceptionList expected");
93    } catch (SourceFileExceptionList ex) {
94  1 Trace.trace(CLASS, this, "testNegative01", ex);
95  1 assertEquals(1, ex.size());
96  1 final SourceFileException check = ex.get(0);
97  1 assertEquals(9001, check.getErrorCode());
98  1 assertEquals(39, check.getSourceArea().getStartPosition().getRow());
99  1 assertEquals(1, check.getSourceArea().getStartPosition().getColumn());
100  1 assertEquals(39, check.getSourceArea().getEndPosition().getRow());
101  1 assertEquals(35, check.getSourceArea().getEndPosition().getColumn());
102    }
103    }
104   
 
105  1 toggle public void testNegative02() throws Exception {
106  1 try {
107  1 check(getFile("qedeq_error_sample_02.xml"));
108  0 fail("SourceFileExceptionList expected");
109    } catch (SourceFileExceptionList sfl) {
110  1 Trace.trace(CLASS, this, "testNegative02", sfl);
111  1 final Exception e = (Exception) sfl.get(0).getCause();
112  1 Trace.param(CLASS, this, "testNegative02", "name", e.getClass().getName());
113  1 assertTrue(e instanceof LogicalCheckException);
114  1 final LogicalCheckException check = (LogicalCheckException) e;
115  1 assertEquals(30550, check.getErrorCode());
116  1 assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNode().getNodeType().getAxiom().getFormula().getElement().getList().getElement(1).getList()", check.getContext().getLocationWithinModule());
117  1 assertNull(check.getReferenceContext());
118    }
119    }
120   
 
121  1 toggle public void testNegative03() throws Exception {
122  1 try {
123  1 check(getFile("qedeq_error_sample_03.xml"));
124  0 fail("SourceFileExceptionList expected");
125    } catch (SourceFileExceptionList sfl) {
126  1 Trace.trace(CLASS, this, "testNegative03", sfl);
127  1 final Exception e = (Exception) sfl.get(0).getCause();
128  1 assertTrue(e instanceof LogicalCheckException);
129  1 final LogicalCheckException check = (LogicalCheckException) e;
130  1 assertEquals(30770, check.getErrorCode());
131  1 assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNode().getNodeType().getAxiom().getFormula().getElement().getList().getElement(1)", check.getContext().getLocationWithinModule());
132  1 assertNull(check.getReferenceContext());
133    }
134    }
135   
 
136  1 toggle public void testNegative04() throws Exception {
137  1 try {
138  1 checkViaKernel(getFile("qedeq_error_sample_04.xml"));
139  0 fail("SourceFileExceptionList expected");
140    } catch (SourceFileExceptionList sfl) {
141  1 Trace.trace(CLASS, this, "testNegative04", sfl);
142  1 final Exception e = (Exception) sfl.get(0).getCause();
143  1 assertTrue(e instanceof LogicalCheckException);
144  1 final LogicalCheckException check = (LogicalCheckException) e;
145  1 assertEquals(30780, check.getErrorCode());
146  1 assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNode().getNodeType().getAxiom().getFormula().getElement().getList().getElement(1)", check.getContext().getLocationWithinModule());
147  1 assertNull(check.getReferenceContext());
148    }
149    }
150   
 
151  1 toggle public void testPositive01() throws Exception {
152  1 checkViaKernel(getDocFile("math/qedeq_logic_v1.xml"));
153    }
154   
 
155  1 toggle public void testPositive02() throws Exception {
156  1 checkViaKernel(getDocFile("sample/qedeq_sample1.xml"));
157    }
158   
 
159  1 toggle public void testPositive03() throws Exception {
160  1 checkViaKernel(getDocFile("sample/qedeq_sample2.xml"));
161    }
162   
 
163  1 toggle public void testPositive03b() throws Exception {
164  1 checkViaKernel(getDocFile("sample/qedeq_sample3.xml"));
165    }
166   
 
167  1 toggle public void testPositive04() throws Exception {
168  1 checkViaKernel(getDocFile("math/qedeq_set_theory_v1.xml"));
169    }
170   
 
171  1 toggle public void testPositive05() throws Exception {
172  1 checkViaKernel(getDocFile("project/qedeq_basic_concept.xml"));
173    }
174   
 
175  1 toggle public void testPositive06() throws Exception {
176  1 checkViaKernel(getDocFile("project/qedeq_logic_language.xml"));
177    }
178   
179    /**
180    * Check logic of QEDEQ module given as XML file.
181    *
182    * @param xmlFile Module file to check.
183    */
 
184  4 toggle public void check(final File xmlFile) throws IOException,
185    ParserConfigurationException, SAXException, ModuleDataException,
186    SourceFileExceptionList, NoSuchFieldException {
187  4 final ModuleAddress context = getServices().getModuleAddress(
188    UrlUtility.toUrl(xmlFile.getAbsoluteFile()));
189  4 SaxDefaultHandler handler = new SaxDefaultHandler(new DummyPlugin());
190  4 QedeqHandler simple = new QedeqHandler(handler);
191  4 handler.setBasisDocumentHandler(simple);
192  4 SaxParser parser = new SaxParser(DummyPlugin.getInstance(), handler);
193  4 parser.parse(xmlFile, xmlFile.getPath());
194  2 final QedeqVo qedeq = (QedeqVo) simple.getQedeq();
195  2 final QedeqFileDao loader = new XmlQedeqFileDao();
196  2 loader.setServices(getInternalServices());
197  2 final DefaultKernelQedeqBo prop = (DefaultKernelQedeqBo) KernelFacade
198    .getKernelContext().getQedeqBo(context);
199  2 prop.setQedeqFileDao(loader);
200  2 YodaUtility.setFieldContent(prop, "qedeq", qedeq);
201  2 final ModuleLabelsCreator creator = new ModuleLabelsCreator(DummyPlugin.getInstance(),
202    prop);
203  2 call = createServiceCall("check", prop);
204  2 creator.createLabels(call.getInternalServiceProcess());
205  2 prop.setLoaded(QedeqVoBuilder.createQedeq(prop.getModuleAddress(), qedeq),
206    creator.getLabels(), creator.getConverter(), creator.getTextConverter());
207  2 prop.setLoadedImports(new KernelModuleReferenceList());
208  2 prop.setLoadedRequiredModules();
209  2 final WellFormedCheckerPlugin plugin = new WellFormedCheckerPlugin();
210  2 final Map parameters = new HashMap();
211  2 parameters.put("checkerFactory", TestFormulaCheckerFactoryImpl.class.getName());
212  2 final WellFormedCheckerExecutor checker = (WellFormedCheckerExecutor) plugin.createExecutor(
213    prop, new Parameters(parameters));
214  2 checker.executePlugin(call, null);
215  2 if (prop.hasErrors()) {
216  2 throw prop.getErrors();
217    }
218    }
219   
220    /**
221    * Check logic of QEDEQ module given as XML file.
222    *
223    * @param xmlFile Module file to check.
224    */
 
225  8 toggle public void checkViaKernel(final File xmlFile) throws SourceFileExceptionList, IOException, InterruptException {
226  8 final ModuleAddress address = getServices().getModuleAddress(
227    UrlUtility.toUrl(xmlFile.getAbsoluteFile()));
228  8 KernelQedeqBo qedeqBo= (KernelQedeqBo) getServices().loadModule(address);
229  8 final WellFormedCheckerPlugin plugin = new WellFormedCheckerPlugin();
230  8 final Map parameters = new HashMap();
231  8 parameters.put("checkerFactory", TestFormulaCheckerFactoryImpl.class.getName());
232  8 final WellFormedCheckerExecutor checker = (WellFormedCheckerExecutor) plugin.createExecutor(
233    qedeqBo, new Parameters(parameters));
234  8 call = createServiceCall("check", qedeqBo);
235  8 checker.executePlugin(call, null);
236  8 if (qedeqBo.hasErrors()) {
237    // qedeqBo.getErrors().get(0).printStackTrace(System.out);
238  1 throw qedeqBo.getErrors();
239    }
240    }
241   
242    }