1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
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 |
|
|
57 |
|
|
58 |
|
@author |
59 |
|
|
|
|
| 94.8% |
Uncovered Elements: 6 (116) |
Complexity: 22 |
Complexity Density: 0.23 |
|
60 |
|
public final class FormulaCheckerContextTest extends QedeqBoTestCase { |
61 |
|
|
62 |
|
|
63 |
|
private static final Class CLASS = FormulaChecker.class; |
64 |
|
private InternalServiceCall call; |
65 |
|
|
66 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0.5 |
|
67 |
12
|
protected void tearDown() throws Exception {... |
68 |
12
|
endServiceCall(call); |
69 |
12
|
super.tearDown(); |
70 |
|
} |
71 |
|
|
|
|
| 90.9% |
Uncovered Elements: 1 (11) |
Complexity: 2 |
Complexity Density: 0.18 |
1
PASS
|
|
72 |
1
|
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 |
|
|
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 |
|
|
|
|
| 90.9% |
Uncovered Elements: 1 (11) |
Complexity: 2 |
Complexity Density: 0.18 |
1
PASS
|
|
89 |
1
|
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 |
|
|
|
|
| 90.9% |
Uncovered Elements: 1 (11) |
Complexity: 2 |
Complexity Density: 0.18 |
1
PASS
|
|
105 |
1
|
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 |
|
|
|
|
| 90% |
Uncovered Elements: 1 (10) |
Complexity: 2 |
Complexity Density: 0.2 |
1
PASS
|
|
121 |
1
|
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 |
|
|
|
|
| 90% |
Uncovered Elements: 1 (10) |
Complexity: 2 |
Complexity Density: 0.2 |
1
PASS
|
|
136 |
1
|
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 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
151 |
1
|
public void testPositive01() throws Exception {... |
152 |
1
|
checkViaKernel(getDocFile("math/qedeq_logic_v1.xml")); |
153 |
|
} |
154 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
155 |
1
|
public void testPositive02() throws Exception {... |
156 |
1
|
checkViaKernel(getDocFile("sample/qedeq_sample1.xml")); |
157 |
|
} |
158 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
159 |
1
|
public void testPositive03() throws Exception {... |
160 |
1
|
checkViaKernel(getDocFile("sample/qedeq_sample2.xml")); |
161 |
|
} |
162 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
163 |
1
|
public void testPositive03b() throws Exception {... |
164 |
1
|
checkViaKernel(getDocFile("sample/qedeq_sample3.xml")); |
165 |
|
} |
166 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
167 |
1
|
public void testPositive04() throws Exception {... |
168 |
1
|
checkViaKernel(getDocFile("math/qedeq_set_theory_v1.xml")); |
169 |
|
} |
170 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
171 |
1
|
public void testPositive05() throws Exception {... |
172 |
1
|
checkViaKernel(getDocFile("project/qedeq_basic_concept.xml")); |
173 |
|
} |
174 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
1
PASS
|
|
175 |
1
|
public void testPositive06() throws Exception {... |
176 |
1
|
checkViaKernel(getDocFile("project/qedeq_logic_language.xml")); |
177 |
|
} |
178 |
|
|
179 |
|
|
180 |
|
|
181 |
|
|
182 |
|
@param |
183 |
|
|
|
|
| 96.3% |
Uncovered Elements: 1 (27) |
Complexity: 2 |
Complexity Density: 0.08 |
|
184 |
4
|
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 |
|
|
222 |
|
|
223 |
|
@param |
224 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (12) |
Complexity: 2 |
Complexity Density: 0.2 |
|
225 |
8
|
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 |
|
|
238 |
1
|
throw qedeqBo.getErrors(); |
239 |
|
} |
240 |
|
} |
241 |
|
|
242 |
|
} |