Clover Coverage Report
Coverage timestamp: Sat Sep 18 2010 04:09:52 UTC
170   384   22   13.08
18   251   0.13   13
13     1.69  
1    
 
  ModuleConstantsExistenceCheckerTest       Line # 34 170 22 88.1% 0.880597
 
  (9)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2010, 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    package org.qedeq.kernel.bo.service;
16   
17    import org.qedeq.base.test.QedeqTestCase;
18    import org.qedeq.kernel.base.module.FunctionDefinition;
19    import org.qedeq.kernel.base.module.PredicateDefinition;
20    import org.qedeq.kernel.bo.context.KernelContext;
21    import org.qedeq.kernel.bo.logic.wf.ExistenceChecker;
22    import org.qedeq.kernel.bo.logic.wf.Function;
23    import org.qedeq.kernel.bo.logic.wf.Predicate;
24    import org.qedeq.kernel.bo.test.KernelFacade;
25    import org.qedeq.kernel.common.DefaultModuleAddress;
26    import org.qedeq.kernel.common.ModuleAddress;
27    import org.qedeq.kernel.common.SourceFileExceptionList;
28   
29    /**
30    * For testing of checking existence of module constants.
31    *
32    * @author Michael Meyling
33    */
 
34    public class ModuleConstantsExistenceCheckerTest extends QedeqTestCase {
35   
 
36  9 toggle protected void setUp() throws Exception {
37  9 super.setUp();
38  9 KernelFacade.startup();
39    }
40   
 
41  9 toggle protected void tearDown() throws Exception {
42  9 KernelFacade.shutdown();
43  9 super.tearDown();
44    }
45   
 
46  0 toggle public ModuleConstantsExistenceCheckerTest() {
47  0 super();
48    }
49   
 
50  9 toggle public ModuleConstantsExistenceCheckerTest(final String name) {
51  9 super(name);
52    }
53   
54    /**
55    * Load following dependencies:
56    * <pre>
57    * 011 -> 012(a)
58    * 011 -> 012(b)
59    * </pre>
60    * In <code>012</code> the identity operator is defined.
61    *
62    * @throws Exception
63    */
 
64  1 toggle public void testModuleConstancsExistenceChecker_01() throws Exception {
65  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC011.xml"));
66  1 if (!KernelContext.getInstance().checkModule(address)) {
67  0 KernelContext.getInstance().getQedeqBo(address).getErrors().printStackTrace(System.out);
68  0 throw KernelContext.getInstance().getQedeqBo(address).getErrors();
69    }
70  1 final DefaultKernelQedeqBo qedeq = (DefaultKernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
71  1 SourceFileExceptionList errors = qedeq.getErrors();
72  1 SourceFileExceptionList warnings = qedeq.getWarnings();
73  1 assertNull(warnings);
74  1 assertNull(errors);
75    }
76   
77    /**
78    * Load following dependencies:
79    * <pre>
80    * 021 -> 022
81    * 021 -> 023
82    * </pre>
83    * In <code>022</code> and <code>023</code> the identity operator is defined.
84    *
85    * @throws Exception
86    */
 
87  1 toggle public void testModuleConstancsExistenceChecker_02() throws Exception {
88  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC021.xml"));
89  1 if (!KernelContext.getInstance().checkModule(address)) {
90  1 SourceFileExceptionList errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
91  1 SourceFileExceptionList warnings = KernelContext.getInstance().getQedeqBo(address).getWarnings();
92  1 assertNull(warnings);
93  1 assertEquals(1, errors.size());
94  1 assertEquals(123476, errors.get(0).getErrorCode());
95  1 assertEquals(38, errors.get(0).getSourceArea().getStartPosition().getRow());
96  1 assertEquals(15, errors.get(0).getSourceArea().getStartPosition().getColumn());
97    } else {
98  0 fail("failure for double definition of identity operator expected");
99    }
100    }
101   
102    /**
103    * Load following dependencies:
104    * <pre>
105    * 031 -> 032
106    * 031 -> 033 -> 034
107    * </pre>
108    * In <code>032</code> and <code>034</code> the identity operator is defined.
109    *
110    * @throws Exception
111    */
 
112  1 toggle public void testModuleConstancsExistenceChecker_03() throws Exception {
113  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC031.xml"));
114  1 if (!KernelContext.getInstance().checkModule(address)) {
115  1 SourceFileExceptionList errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
116  1 SourceFileExceptionList warnings = KernelContext.getInstance().getQedeqBo(address).getWarnings();
117  1 assertNull(warnings);
118  1 assertEquals(1, errors.size());
119  1 assertEquals(123476, errors.get(0).getErrorCode());
120  1 assertEquals(38, errors.get(0).getSourceArea().getStartPosition().getRow());
121  1 assertEquals(15, errors.get(0).getSourceArea().getStartPosition().getColumn());
122    } else {
123  0 fail("failure for double definition of identity operator expected");
124    }
125    }
126   
127    /**
128    * Load following dependencies:
129    * <pre>
130    * 041 -> 043 -> 044 -> 042
131    * 041 -> 042
132    * </pre>
133    * In <code>042</code> the identity operator is defined.
134    *
135    * @throws Exception
136    */
 
137  1 toggle public void testModuleConstancsExistenceChecker_04() throws Exception {
138  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC041.xml"));
139  1 SourceFileExceptionList errors;
140  1 if (!KernelContext.getInstance().checkModule(address)) {
141  0 errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
142  0 throw errors;
143    }
144  1 errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
145  1 SourceFileExceptionList warnings = KernelContext.getInstance().getQedeqBo(address).getWarnings();
146  1 assertNull(warnings);
147  1 assertNull(errors);
148    }
149   
150    /**
151    * Load following dependencies:
152    * <pre>
153    * 051 -> 052
154    * </pre>
155    * In <code>052</code> the identity operator is defined.
156    *
157    * @throws Exception
158    */
 
159  1 toggle public void testModuleConstancsExistenceChecker_05() throws Exception {
160  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC051.xml"));
161  1 if (!KernelContext.getInstance().checkModule(address)) {
162  0 KernelContext.getInstance().getQedeqBo(address).getErrors().printStackTrace(System.out);
163  0 throw KernelContext.getInstance().getQedeqBo(address).getErrors();
164    }
165  1 final DefaultKernelQedeqBo qedeq = (DefaultKernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
166  1 SourceFileExceptionList errors = qedeq.getErrors();
167  1 SourceFileExceptionList warnings = qedeq.getWarnings();
168  1 assertNull(warnings);
169  1 assertNull(errors);
170   
171  1 ModuleConstantsExistenceChecker checker = qedeq.getExistenceChecker();
172   
173  1 assertEquals("MCEC052.equal", checker.getIdentityOperator());
174  1 assertFalse(qedeq.equals(checker.getQedeq(new Predicate(ExistenceChecker.NAME_EQUAL, "" + 2))));
175  1 assertNull(checker.getQedeq(new Predicate(ExistenceChecker.NAME_EQUAL, "" + 2)));
176  1 assertNull(checker.getQedeq(new Predicate("unknown." + ExistenceChecker.NAME_EQUAL, "" + 2)));
177  1 assertEquals(KernelContext.getInstance().getQedeqBo(new DefaultModuleAddress(getFile("existence/MCEC052.xml"))),
178    checker.getQedeq(new Predicate("MCEC052." + ExistenceChecker.NAME_EQUAL, "" + 2)));
179    {
180  1 final Predicate predicate = new Predicate("MCEC052." + ExistenceChecker.NAME_EQUAL, "" + 2);
181  1 assertTrue(checker.predicateExists(predicate));
182  1 final PredicateDefinition def = checker.get(predicate);
183  1 assertEquals("#1 \\ = \\ #2", def.getLatexPattern());
184  1 assertEquals("" + 2, def.getArgumentNumber());
185  1 assertNull(def.getFormula());
186  1 assertEquals("equal", def.getName());
187  1 assertEquals(2, def.getVariableList().size());
188    }
189   
190    {
191  1 assertTrue(checker.predicateExists("MCEC052." + ExistenceChecker.NAME_EQUAL, 2));
192  1 final PredicateDefinition def = checker.getPredicate("MCEC052." + ExistenceChecker.NAME_EQUAL, 2);
193  1 assertEquals("#1 \\ = \\ #2", def.getLatexPattern());
194  1 assertEquals("" + 2, def.getArgumentNumber());
195  1 assertNull(def.getFormula());
196  1 assertEquals("equal", def.getName());
197  1 assertEquals(2, def.getVariableList().size());
198    }
199   
200    {
201  1 final Predicate predicate = new Predicate("MCEC052x." + ExistenceChecker.NAME_EQUAL, "" + 2);
202  1 assertFalse(checker.predicateExists(predicate));
203  1 final PredicateDefinition def = checker.get(predicate);
204  1 assertNull(def);
205    }
206   
207    {
208  1 assertFalse(checker.predicateExists("MCEC052x." + ExistenceChecker.NAME_EQUAL, 2));
209  1 final PredicateDefinition def = checker.getPredicate("MCEC052x." + ExistenceChecker.NAME_EQUAL, 2);
210  1 assertNull(def);
211    }
212   
213  1 assertEquals("MCEC052.equal", checker.getIdentityOperator());
214  1 assertFalse(qedeq.equals(checker.getQedeq(new Function("union", "" + 2))));
215  1 assertNull(checker.getQedeq(new Function("union", "" + 2)));
216  1 assertNull(checker.getQedeq(new Function("unknown." + "union", "" + 2)));
217  1 assertEquals(KernelContext.getInstance().getQedeqBo(new DefaultModuleAddress(getFile("existence/MCEC052.xml"))),
218    checker.getQedeq(new Function("MCEC052." + "union", "" + 2)));
219    {
220  1 final Function function = new Function("MCEC052x." + "union", "" + 2);
221  1 assertFalse(checker.functionExists(function));
222  1 assertNull(checker.get(function));
223    }
224    {
225  1 final Function function = new Function("MCEC05." + "union", "" + 2);
226  1 assertFalse(checker.functionExists(function));
227  1 assertNull(checker.get(function));
228    }
229    {
230  1 final Function function = new Function("MCEC052." + "uniont", "" + 2);
231  1 assertFalse(checker.functionExists(function));
232  1 assertNull(checker.get(function));
233    }
234    {
235  1 final Function function = new Function("MCEC052." + "union", "" + 2);
236  1 assertTrue(checker.functionExists(function));
237  1 final FunctionDefinition def2 = checker.get(function);
238  1 assertEquals("(#1 \\cup #2)", def2.getLatexPattern());
239  1 assertEquals("" + 2, def2.getArgumentNumber());
240  1 assertEquals("CLASS ( VAR ( \"z\"), OR ( PREDCON ( \"in\", VAR ( \"z\"), VAR ( \"x\")),"
241    + " PREDCON ( \"in\", VAR ( \"z\"), VAR ( \"y\"))))", def2.getTerm().toString());
242  1 assertEquals("union", def2.getName());
243    }
244    {
245  1 assertTrue(checker.functionExists("MCEC052." + "union", 2));
246  1 final FunctionDefinition def3 = checker.getFunction("MCEC052." + "union", 2);
247  1 assertEquals("(#1 \\cup #2)", def3.getLatexPattern());
248  1 assertEquals("" + 2, def3.getArgumentNumber());
249  1 assertEquals("CLASS ( VAR ( \"z\"), OR ( PREDCON ( \"in\", VAR ( \"z\"), VAR ( \"x\")),"
250    + " PREDCON ( \"in\", VAR ( \"z\"), VAR ( \"y\"))))", def3.getTerm().toString());
251  1 assertEquals("union", def3.getName());
252    }
253    {
254  1 assertFalse(checker.functionExists("MCEC052x." + "union", 2));
255    }
256   
257    }
258   
259    /**
260    * Load following dependencies:
261    * <pre>
262    * 061 -> 062(a)
263    * 061 -> 062(b)
264    * </pre>
265    * In <code>062</code> the identity operator and the class operator is defined.
266    *
267    * @throws Exception
268    */
 
269  1 toggle public void testModuleConstancsExistenceChecker_06() throws Exception {
270  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC061.xml"));
271  1 if (!KernelContext.getInstance().checkModule(address)) {
272  0 KernelContext.getInstance().getQedeqBo(address).getErrors().printStackTrace(System.out);
273  0 throw KernelContext.getInstance().getQedeqBo(address).getErrors();
274    }
275  1 final DefaultKernelQedeqBo qedeq = (DefaultKernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
276  1 SourceFileExceptionList errors = qedeq.getErrors();
277  1 SourceFileExceptionList warnings = qedeq.getWarnings();
278  1 assertNull(warnings);
279  1 assertNull(errors);
280   
281  1 ModuleConstantsExistenceChecker checker = qedeq.getExistenceChecker();
282   
283  1 assertEquals("MCEC062a.equal", checker.getIdentityOperator());
284  1 assertFalse(qedeq.equals(checker.getQedeq(new Predicate(ExistenceChecker.NAME_EQUAL, "" + 2))));
285  1 assertNull(checker.getQedeq(new Predicate(ExistenceChecker.NAME_EQUAL, "" + 2)));
286  1 assertNull(checker.getQedeq(new Predicate("unknown." + ExistenceChecker.NAME_EQUAL, "" + 2)));
287  1 assertEquals(KernelContext.getInstance().getQedeqBo(new DefaultModuleAddress(getFile("existence/MCEC062.xml"))),
288    checker.getQedeq(new Predicate("MCEC062a." + ExistenceChecker.NAME_EQUAL, "" + 2)));
289  1 final PredicateDefinition def = checker.get(new Predicate("MCEC062a." + ExistenceChecker.NAME_EQUAL, "" + 2));
290  1 assertEquals("#1 \\ = \\ #2", def.getLatexPattern());
291  1 assertEquals("" + 2, def.getArgumentNumber());
292  1 assertNull(def.getFormula());
293  1 assertEquals("equal", def.getName());
294  1 assertEquals(2, def.getVariableList().size());
295   
296  1 assertEquals("MCEC062a.equal", checker.getIdentityOperator());
297  1 assertFalse(qedeq.equals(checker.getQedeq(new Function("union", "" + 2))));
298  1 assertNull(checker.getQedeq(new Function("union", "" + 2)));
299  1 assertNull(checker.getQedeq(new Function("unknown." + "union", "" + 2)));
300  1 assertEquals(KernelContext.getInstance().getQedeqBo(new DefaultModuleAddress(getFile("existence/MCEC062.xml"))),
301    checker.getQedeq(new Function("MCEC062a." + "union", "" + 2)));
302  1 final FunctionDefinition def2 = checker.get(new Function("MCEC062a." + "union", "" + 2));
303  1 assertEquals("(#1 \\cup #2)", def2.getLatexPattern());
304  1 assertEquals("" + 2, def2.getArgumentNumber());
305  1 assertEquals("CLASS ( VAR ( \"z\"), OR ( PREDCON ( \"in\", VAR ( \"z\"), VAR ( \"x\")),"
306    + " PREDCON ( \"in\", VAR ( \"z\"), VAR ( \"y\"))))", def2.getTerm().toString());
307  1 assertEquals("union", def2.getName());
308   
309    }
310   
311    /**
312    * Load following dependencies:
313    * <pre>
314    * 071 -> 072
315    * 071 -> 073
316    * </pre>
317    * In <code>072</code> and <code>074</code> the identity operator and the class operator is defined.
318    *
319    * @throws Exception
320    */
 
321  1 toggle public void testModuleConstancsExistenceChecker_07() throws Exception {
322  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC071.xml"));
323  1 if (!KernelContext.getInstance().checkModule(address)) {
324  1 SourceFileExceptionList errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
325  1 SourceFileExceptionList warnings = KernelContext.getInstance().getQedeqBo(address).getWarnings();
326  1 assertNull(warnings);
327  1 assertEquals(1, errors.size());
328  1 assertEquals(123478, errors.get(0).getErrorCode());
329  1 assertEquals(38, errors.get(0).getSourceArea().getStartPosition().getRow());
330  1 assertEquals(15, errors.get(0).getSourceArea().getStartPosition().getColumn());
331    } else {
332  0 fail("failure for double definition of class operator expected");
333    }
334    }
335   
336    /**
337    * Load following dependencies:
338    * <pre>
339    * 081 -> 082 -> 083
340    * </pre>
341    * In <code>081</code> and <code>083</code> the the class operator is defined.
342    *
343    * @throws Exception
344    */
 
345  1 toggle public void testModuleConstancsExistenceChecker_08() throws Exception {
346  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC081.xml"));
347  1 if (!KernelContext.getInstance().checkModule(address)) {
348  1 SourceFileExceptionList errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
349  1 SourceFileExceptionList warnings = KernelContext.getInstance().getQedeqBo(address).getWarnings();
350  1 assertNull(warnings);
351  1 assertEquals(1, errors.size());
352  1 assertEquals(123478, errors.get(0).getErrorCode());
353  1 assertEquals(118, errors.get(0).getSourceArea().getStartPosition().getRow());
354  1 assertEquals(11, errors.get(0).getSourceArea().getStartPosition().getColumn());
355    } else {
356  0 fail("failure for double definition of class operator expected");
357    }
358    }
359   
360    /**
361    * Load following dependencies:
362    * <pre>
363    * 091 -> 092 -> 093
364    * </pre>
365    * In <code>091</code> and <code>093</code> the the identity predicate is defined.
366    *
367    * @throws Exception
368    */
 
369  1 toggle public void testModuleConstancsExistenceChecker_09() throws Exception {
370  1 final ModuleAddress address = new DefaultModuleAddress(getFile("existence/MCEC091.xml"));
371  1 if (!KernelContext.getInstance().checkModule(address)) {
372  1 SourceFileExceptionList errors = KernelContext.getInstance().getQedeqBo(address).getErrors();
373  1 SourceFileExceptionList warnings = KernelContext.getInstance().getQedeqBo(address).getWarnings();
374  1 assertNull(warnings);
375  1 assertEquals(1, errors.size());
376  1 assertEquals(123476, errors.get(0).getErrorCode());
377  1 assertEquals(125, errors.get(0).getSourceArea().getStartPosition().getRow());
378  1 assertEquals(11, errors.get(0).getSourceArea().getStartPosition().getColumn());
379    } else {
380  0 fail("failure for double definition of class operator expected");
381    }
382    }
383   
384    }