Clover Coverage Report
Coverage timestamp: Sat Sep 18 2010 04:09:52 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
122   783   32   3.81
0   485   0.26   32
32     1  
1    
 
  FormulaCheckerQuantifiersTest       Line # 30 122 32 100% 1.0
 
No Tests
 
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   
16    package org.qedeq.kernel.bo.logic.wf;
17   
18    import org.qedeq.kernel.base.list.Element;
19    import org.qedeq.kernel.bo.logic.FormulaChecker;
20    import org.qedeq.kernel.common.DefaultModuleAddress;
21    import org.qedeq.kernel.common.ModuleContext;
22   
23    /**
24    * For testing the {@link org.qedeq.kernel.bo.logic.FormulaChecker}.
25    * Testing formulas made of quantifiers.
26    *
27    * @version $Revision: 1.1 $
28    * @author Michael Meyling
29    */
 
30    public class FormulaCheckerQuantifiersTest extends AbstractFormulaChecker {
31   
32    private ModuleContext context;
33   
 
34  30 toggle protected void setUp() throws Exception {
35  30 context = new ModuleContext(new DefaultModuleAddress("http://memory.org/sample.xml"), "getElement()");
36    }
37   
 
38  30 toggle protected void tearDown() throws Exception {
39  30 context = null;
40    }
41   
42    /**
43    * Function: checkFormula(Element)
44    * Type: positive
45    * Data: all x A
46    *
47    * @throws Exception Test failed.
48    */
 
49  1 toggle public void testQuantifiersPositive01() throws Exception {
50  1 final Element ele = TestParser.createElement(
51    "<FORALL><VAR id=\"x\" /><PREDVAR id=\"A\"/></FORALL>");
52    // System.out.println(ele.toString());
53  1 assertFalse(FormulaChecker.checkFormula(ele, context).hasErrors());
54  1 assertFalse(FormulaChecker.checkFormula(ele, context, getChecker()).hasErrors());
55  1 assertFalse(FormulaChecker.checkFormula(ele, context, getCheckerWithoutClass())
56    .hasErrors());
57    }
58   
59    /**
60    * Function: checkFormula(Element)
61    * Type: positive
62    * Data: exists x A
63    *
64    * @throws Exception Test failed.
65    */
 
66  1 toggle public void testQuantifiersPositive02() throws Exception {
67  1 final Element ele = TestParser.createElement(
68    "<EXISTS><VAR id=\"x\" /><PREDVAR id=\"A\"/></EXISTS>");
69    // System.out.println(ele.toString());
70  1 assertFalse(FormulaChecker.checkFormula(ele, context).hasErrors());
71  1 assertFalse(FormulaChecker.checkFormula(ele, context, getChecker()).hasErrors());
72  1 assertFalse(FormulaChecker.checkFormula(ele, context, getCheckerWithoutClass())
73    .hasErrors());
74    }
75   
76    /**
77    * Function: checkFormula(Element)
78    * Type: positive
79    * Data: exists! x A
80    *
81    * @throws Exception Test failed.
82    */
 
83  1 toggle public void testQuantifiersPositive03() throws Exception {
84  1 final Element ele = TestParser.createElement(
85    "<EXISTSU><VAR id=\"x\" /><PREDVAR id=\"A\"/></EXISTSU>");
86    // System.out.println(ele.toString());
87  1 assertFalse(FormulaChecker.checkFormula(ele, context).hasErrors());
88  1 assertFalse(FormulaChecker.checkFormula(ele, context, getChecker()).hasErrors());
89  1 assertFalse(FormulaChecker.checkFormula(ele, context, getCheckerWithoutClass())
90    .hasErrors());
91    }
92   
93    /**
94    * Function: checkFormula(Element)
95    * Type: positive
96    * Data: all x phi(x): A
97    *
98    * @throws Exception Test failed.
99    */
 
100  1 toggle public void testQuantifiersPositive04() throws Exception {
101  1 final Element ele = TestParser.createElement(
102    "<FORALL>" +
103    " <VAR id=\"x\" />" +
104    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
105    " <PREDVAR id=\"A\"/>" +
106    "</FORALL>");
107    // System.out.println(ele.toString());
108  1 assertFalse(FormulaChecker.checkFormula(ele, context).hasErrors());
109  1 assertFalse(FormulaChecker.checkFormula(ele, context, getChecker()).hasErrors());
110  1 assertFalse(FormulaChecker.checkFormula(ele, context, getCheckerWithoutClass())
111    .hasErrors());
112    }
113   
114    /**
115    * Function: checkFormula(Element)
116    * Type: positive
117    * Data: exists x phi(x) A
118    *
119    * @throws Exception Test failed.
120    */
 
121  1 toggle public void testQuantifiersPositive05() throws Exception {
122  1 final Element ele = TestParser.createElement(
123    "<EXISTS>" +
124    " <VAR id=\"x\" />" +
125    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
126    " <PREDVAR id=\"A\"/>" +
127    "</EXISTS>");
128    // System.out.println(ele.toString());
129  1 assertFalse(FormulaChecker.checkFormula(ele, context).hasErrors());
130  1 assertFalse(FormulaChecker.checkFormula(ele, context, getChecker()).hasErrors());
131  1 assertFalse(FormulaChecker.checkFormula(ele, context, getCheckerWithoutClass())
132    .hasErrors());
133    }
134   
135    /**
136    * Function: checkFormula(Element)
137    * Type: positive
138    * Data: exists! x phi(x): A
139    *
140    * @throws Exception Test failed.
141    */
 
142  1 toggle public void testQuantifiersPositive06() throws Exception {
143  1 final Element ele = TestParser.createElement(
144    "<EXISTSU>" +
145    " <VAR id=\"x\" />" +
146    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
147    " <PREDVAR id=\"A\"/>" +
148    "</EXISTSU>");
149    // System.out.println(ele.toString());
150  1 assertFalse(FormulaChecker.checkFormula(ele, context).hasErrors());
151  1 assertFalse(FormulaChecker.checkFormula(ele, context, getChecker()).hasErrors());
152  1 assertFalse(FormulaChecker.checkFormula(ele, context, getCheckerWithoutClass())
153    .hasErrors());
154    }
155   
156    /**
157    * Function: checkFormula(Element)
158    * Type: negative, code 30540, missing subject variable
159    * Data: all phi(x) A
160    *
161    * @throws Exception Test failed.
162    */
 
163  1 toggle public void testQuantifiersNegative01() throws Exception {
164  1 final Element ele = TestParser.createElement(
165    "<FORALL>" +
166    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
167    " <PREDVAR id=\"A\"/>" +
168    "</FORALL>");
169    // System.out.println(ele.toString());
170  1 LogicalCheckExceptionList list =
171    FormulaChecker.checkFormula(ele, context, getChecker());
172  1 assertEquals(1, list.size());
173  1 assertEquals(30540, list.get(0).getErrorCode());
174    }
175   
176    /**
177    * Function: checkFormula(Element)
178    * Type: negative, code 30540, missing subject variable
179    * Data: exists phi(x) A
180    *
181    * @throws Exception Test failed.
182    */
 
183  1 toggle public void testQuantifiersNegative02() throws Exception {
184  1 final Element ele = TestParser.createElement(
185    "<EXISTS>" +
186    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
187    " <PREDVAR id=\"A\"/>" +
188    "</EXISTS>");
189    // System.out.println(ele.toString());
190  1 LogicalCheckExceptionList list =
191    FormulaChecker.checkFormula(ele, context, getChecker());
192  1 assertEquals(1, list.size());
193  1 assertEquals(30540, list.get(0).getErrorCode());
194    }
195   
196    /**
197    * Function: checkFormula(Element)
198    * Type: negative, code 30540, missing subject variable
199    * Data: exists! phi(x): A
200    *
201    * @throws Exception Test failed.
202    */
 
203  1 toggle public void testQuantifiersNegative03() throws Exception {
204  1 final Element ele = TestParser.createElement(
205    "<EXISTSU>" +
206    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
207    " <PREDVAR id=\"A\"/>" +
208    "</EXISTSU>");
209    // System.out.println(ele.toString());
210  1 LogicalCheckExceptionList list =
211    FormulaChecker.checkFormula(ele, context, getChecker());
212  1 assertEquals(1, list.size());
213  1 assertEquals(30540, list.get(0).getErrorCode());
214    }
215   
216    /**
217    * Function: checkFormula(Element)
218    * Type: negative, code 30550, subject already bound
219    * Data: all x all x phi(x)
220    *
221    * @throws Exception Test failed.
222    */
 
223  1 toggle public void testQuantifiersNegative04() throws Exception {
224  1 final Element ele = TestParser.createElement(
225    "<FORALL>" +
226    " <VAR id=\"x\" />" +
227    " <FORALL>" +
228    " <VAR id=\"x\" />" +
229    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
230    " </FORALL>" +
231    "</FORALL>");
232    // System.out.println(ele.toString());
233  1 LogicalCheckExceptionList list =
234    FormulaChecker.checkFormula(ele, context, getChecker());
235  1 assertEquals(1, list.size());
236  1 assertEquals(30550, list.get(0).getErrorCode());
237    }
238   
239    /**
240    * Function: checkFormula(Element)
241    * Type: negative, code 30550, subject variable already bound
242    * Data: all x phi(x) all x phi(x)
243    *
244    * @throws Exception Test failed.
245    */
 
246  1 toggle public void testQuantifiersNegative05() throws Exception {
247  1 final Element ele = TestParser.createElement(
248    "<FORALL>" +
249    " <VAR id=\"x\" />" +
250    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
251    " <FORALL>" +
252    " <VAR id=\"x\" />" +
253    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
254    " </FORALL>" +
255    "</FORALL>");
256    // System.out.println(ele.toString());
257  1 LogicalCheckExceptionList list =
258    FormulaChecker.checkFormula(ele, context, getChecker());
259  1 assertEquals(1, list.size());
260  1 assertEquals(30550, list.get(0).getErrorCode());
261    }
262   
263    /**
264    * Function: checkFormula(Element)
265    * Type: negative, code 30550, subject variable already bound
266    * Data: all x phi({x | phi(x)})
267    *
268    * @throws Exception Test failed.
269    */
 
270  1 toggle public void testQuantifiersNegative06() throws Exception {
271  1 final Element ele = TestParser.createElement(
272    "<FORALL>" +
273    " <VAR id=\"x\" />" +
274    " <PREDVAR id=\"phi\">" +
275    " <CLASS>" +
276    " <VAR id=\"x\" />" +
277    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
278    " </CLASS>" +
279    " </PREDVAR>" +
280    "</FORALL>");
281    // System.out.println(ele.toString());
282  1 LogicalCheckExceptionList list =
283    FormulaChecker.checkFormula(ele, context, getChecker());
284  1 assertEquals(1, list.size());
285  1 assertEquals(30550, list.get(0).getErrorCode());
286    }
287   
288    /**
289    * Function: checkFormula(Element)
290    * Type: negative, code 30550, subject already bound
291    * Data: exists x all x phi(x)
292    *
293    * @throws Exception Test failed.
294    */
 
295  1 toggle public void testQuantifiersNegative07() throws Exception {
296  1 final Element ele = TestParser.createElement(
297    "<EXISTS>" +
298    " <VAR id=\"x\" />" +
299    " <FORALL>" +
300    " <VAR id=\"x\" />" +
301    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
302    " </FORALL>" +
303    "</EXISTS>");
304    // System.out.println(ele.toString());
305  1 LogicalCheckExceptionList list =
306    FormulaChecker.checkFormula(ele, context, getChecker());
307  1 assertEquals(1, list.size());
308  1 assertEquals(30550, list.get(0).getErrorCode());
309    }
310   
311    /**
312    * Function: checkFormula(Element)
313    * Type: negative, code 30550, subject variable already bound
314    * Data: exists x phi(x) exists x phi(x)
315    *
316    * @throws Exception Test failed.
317    */
 
318  1 toggle public void testQuantifiersNegative08() throws Exception {
319  1 final Element ele = TestParser.createElement(
320    "<EXISTS>" +
321    " <VAR id=\"x\" />" +
322    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
323    " <EXISTS>" +
324    " <VAR id=\"x\" />" +
325    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
326    " </EXISTS>" +
327    "</EXISTS>");
328    // System.out.println(ele.toString());
329  1 LogicalCheckExceptionList list =
330    FormulaChecker.checkFormula(ele, context, getChecker());
331  1 assertEquals(1, list.size());
332  1 assertEquals(30550, list.get(0).getErrorCode());
333    }
334   
335    /**
336    * Function: checkFormula(Element)
337    * Type: negative, code 30550, subject variable already bound
338    * Data: exists x phi({x | phi(x)})
339    *
340    * @throws Exception Test failed.
341    */
 
342  1 toggle public void testQuantifiersNegative09() throws Exception {
343  1 final Element ele = TestParser.createElement(
344    "<EXISTS>" +
345    " <VAR id=\"x\" />" +
346    " <PREDVAR id=\"phi\">" +
347    " <CLASS>" +
348    " <VAR id=\"x\" />" +
349    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
350    " </CLASS>" +
351    " </PREDVAR>" +
352    "</EXISTS>");
353    // System.out.println(ele.toString());
354  1 LogicalCheckExceptionList list =
355    FormulaChecker.checkFormula(ele, context, getChecker());
356  1 assertEquals(1, list.size());
357  1 assertEquals(30550, list.get(0).getErrorCode());
358    }
359   
360    /**
361    * Function: checkFormula(Element)
362    * Type: negative, code 30550, subject already bound
363    * Data: exists! x all x phi(x)
364    *
365    * @throws Exception Test failed.
366    */
 
367  1 toggle public void testQuantifiersNegative10() throws Exception {
368  1 final Element ele = TestParser.createElement(
369    "<EXISTSU>" +
370    " <VAR id=\"x\" />" +
371    " <FORALL>" +
372    " <VAR id=\"x\" />" +
373    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
374    " </FORALL>" +
375    "</EXISTSU>");
376    // System.out.println(ele.toString());
377  1 LogicalCheckExceptionList list =
378    FormulaChecker.checkFormula(ele, context, getChecker());
379  1 assertEquals(1, list.size());
380  1 assertEquals(30550, list.get(0).getErrorCode());
381    }
382   
383    /**
384    * Function: checkFormula(Element)
385    * Type: negative, code 30550, subject variable already bound
386    * Data: exists! x phi(x) exists! x phi(x)
387    *
388    * @throws Exception Test failed.
389    */
 
390  1 toggle public void testQuantifiersNegative11() throws Exception {
391  1 final Element ele = TestParser.createElement(
392    "<EXISTSU>" +
393    " <VAR id=\"x\" />" +
394    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
395    " <EXISTSU>" +
396    " <VAR id=\"x\" />" +
397    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
398    " </EXISTSU>" +
399    "</EXISTSU>");
400    // System.out.println(ele.toString());
401  1 LogicalCheckExceptionList list =
402    FormulaChecker.checkFormula(ele, context, getChecker());
403  1 assertEquals(1, list.size());
404  1 assertEquals(30550, list.get(0).getErrorCode());
405    }
406   
407    /**
408    * Function: checkFormula(Element)
409    * Type: negative, code 30550, subject variable already bound
410    * Data: exists! x phi({x | phi(x)})
411    *
412    * @throws Exception Test failed.
413    */
 
414  1 toggle public void testQuantifiersNegative12() throws Exception {
415  1 final Element ele = TestParser.createElement(
416    "<EXISTSU>" +
417    " <VAR id=\"x\" />" +
418    " <PREDVAR id=\"phi\">" +
419    " <CLASS>" +
420    " <VAR id=\"x\" />" +
421    " <PREDVAR id=\"phi\"><VAR id=\"x\" /></PREDVAR>" +
422    " </CLASS>" +
423    " </PREDVAR>" +
424    "</EXISTSU>");
425    // System.out.println(ele.toString());
426  1 LogicalCheckExceptionList list =
427    FormulaChecker.checkFormula(ele, context, getChecker());
428  1 assertEquals(1, list.size());
429  1 assertEquals(30550, list.get(0).getErrorCode());
430    }
431   
432    /**
433    * Function: checkFormula(Element)
434    * Type: negative, code 30570, mixed free bound
435    * Data: all x phi(x, y): phi({y | A)})
436    *
437    * @throws Exception Test failed.
438    */
 
439  1 toggle public void testQuantifiersNegative16() throws Exception {
440  1 final Element ele = TestParser.createElement(
441    "<FORALL>" +
442    " <VAR id=\"x\" />" +
443    " <PREDVAR id=\"phi\">" +
444    " <VAR id=\"x\" />" +
445    " <VAR id=\"y\" />" +
446    " </PREDVAR>" +
447    " <PREDVAR id=\"phi\">" +
448    " <CLASS>" +
449    " <VAR id=\"y\" />" +
450    " <PREDVAR id=\"A\"/>" +
451    " </CLASS>" +
452    " </PREDVAR>" +
453    "</FORALL>");
454    // System.out.println(ele.toString());
455  1 LogicalCheckExceptionList list =
456    FormulaChecker.checkFormula(ele, context, getChecker());
457  1 assertEquals(1, list.size());
458  1 assertEquals(30770, list.get(0).getErrorCode());
459    }
460   
461    /**
462    * Function: checkFormula(Element)
463    * Type: negative, code 30570, mixed free bound
464    * Data: exists x phi(x, y): phi({y | A)})
465    *
466    * @throws Exception Test failed.
467    */
 
468  1 toggle public void testQuantifiersNegative17() throws Exception {
469  1 final Element ele = TestParser.createElement(
470    "<EXISTS>" +
471    " <VAR id=\"x\" />" +
472    " <PREDVAR id=\"phi\">" +
473    " <VAR id=\"x\" />" +
474    " <VAR id=\"y\" />" +
475    " </PREDVAR>" +
476    " <PREDVAR id=\"phi\">" +
477    " <CLASS>" +
478    " <VAR id=\"y\" />" +
479    " <PREDVAR id=\"A\"/>" +
480    " </CLASS>" +
481    " </PREDVAR>" +
482    "</EXISTS>");
483    // System.out.println(ele.toString());
484  1 LogicalCheckExceptionList list =
485    FormulaChecker.checkFormula(ele, context, getChecker());
486  1 assertEquals(1, list.size());
487  1 assertEquals(30770, list.get(0).getErrorCode());
488    }
489   
490    /**
491    * Function: checkFormula(Element)
492    * Type: negative, code 30570, mixed free bound
493    * Data: exists! x phi(x, y): phi({y | A)})
494    *
495    * @throws Exception Test failed.
496    */
 
497  1 toggle public void testQuantifiersNegative18() throws Exception {
498  1 final Element ele = TestParser.createElement(
499    "<EXISTSU>" +
500    " <VAR id=\"x\" />" +
501    " <PREDVAR id=\"phi\">" +
502    " <VAR id=\"x\" />" +
503    " <VAR id=\"y\" />" +
504    " </PREDVAR>" +
505    " <PREDVAR id=\"phi\">" +
506    " <CLASS>" +
507    " <VAR id=\"y\" />" +
508    " <PREDVAR id=\"A\"/>" +
509    " </CLASS>" +
510    " </PREDVAR>" +
511    "</EXISTSU>");
512    // System.out.println(ele.toString());
513  1 LogicalCheckExceptionList list =
514    FormulaChecker.checkFormula(ele, context, getChecker());
515  1 assertEquals(1, list.size());
516  1 assertEquals(30770, list.get(0).getErrorCode());
517    }
518   
519    /**
520    * Function: checkFormula(Element)
521    * Type: negative, code 30570, mixed free bound
522    * Data: all x phi(x, y): all y A
523    *
524    * @throws Exception Test failed.
525    */
 
526  1 toggle public void testQuantifiersNegative19() throws Exception {
527  1 final Element ele = TestParser.createElement(
528    "<FORALL>" +
529    " <VAR id=\"x\" />" +
530    " <PREDVAR id=\"phi\">" +
531    " <VAR id=\"x\" />" +
532    " <VAR id=\"y\" />" +
533    " </PREDVAR>" +
534    " <FORALL>" +
535    " <VAR id=\"y\" />" +
536    " <PREDVAR id=\"A\"/>" +
537    " </FORALL>" +
538    "</FORALL>");
539    // System.out.println(ele.toString());
540  1 LogicalCheckExceptionList list =
541    FormulaChecker.checkFormula(ele, context, getChecker());
542  1 assertEquals(1, list.size());
543  1 assertEquals(30770, list.get(0).getErrorCode());
544    }
545   
546    /**
547    * Function: checkFormula(Element)
548    * Type: negative, code 30570, mixed free bound
549    * Data: exists x phi(x, y): all y A
550    *
551    * @throws Exception Test failed.
552    */
 
553  1 toggle public void testQuantifiersNegative20() throws Exception {
554  1 final Element ele = TestParser.createElement(
555    "<EXISTS>" +
556    " <VAR id=\"x\" />" +
557    " <PREDVAR id=\"phi\">" +
558    " <VAR id=\"x\" />" +
559    " <VAR id=\"y\" />" +
560    " </PREDVAR>" +
561    " <FORALL>" +
562    " <VAR id=\"y\" />" +
563    " <PREDVAR id=\"A\"/>" +
564    " </FORALL>" +
565    "</EXISTS>");
566    // System.out.println(ele.toString());
567  1 LogicalCheckExceptionList list =
568    FormulaChecker.checkFormula(ele, context, getChecker());
569  1 assertEquals(1, list.size());
570  1 assertEquals(30770, list.get(0).getErrorCode());
571    }
572   
573    /**
574    * Function: checkFormula(Element)
575    * Type: negative, code 30570, mixed free bound
576    * Data: exists! x phi(x, y): exists! y phi(y) A
577    *
578    * @throws Exception Test failed.
579    */
 
580  1 toggle public void testQuantifiersNegative21() throws Exception {
581  1 final Element ele = TestParser.createElement(
582    "<EXISTSU>" +
583    " <VAR id=\"x\" />" +
584    " <PREDVAR id=\"phi\">" +
585    " <VAR id=\"x\" />" +
586    " <VAR id=\"y\" />" +
587    " </PREDVAR>" +
588    " <EXISTSU>" +
589    " <VAR id=\"y\" />" +
590    " <PREDVAR id=\"phi\">" +
591    " <VAR id=\"y\" />" +
592    " </PREDVAR>" +
593    " <PREDVAR id=\"A\"/>" +
594    " </EXISTSU>" +
595    "</EXISTSU>");
596    // System.out.println(ele.toString());
597  1 LogicalCheckExceptionList list =
598    FormulaChecker.checkFormula(ele, context, getChecker());
599  1 assertEquals(1, list.size());
600  1 assertEquals(30770, list.get(0).getErrorCode());
601    }
602   
603    /**
604    * Function: checkFormula(Element)
605    * Type: negative, code 30580, mixed free bound
606    * Data: all x phi(x, {y | A)}): phi(x, y)
607    *
608    * @throws Exception Test failed.
609    */
 
610  1 toggle public void testQuantifiersNegative22() throws Exception {
611  1 final Element ele = TestParser.createElement(
612    "<FORALL>" +
613    " <VAR id=\"x\" />" +
614    " <PREDVAR id=\"phi\">" +
615    " <VAR id=\"x\" />" +
616    " <CLASS>" +
617    " <VAR id=\"y\" />" +
618    " <PREDVAR id=\"A\"/>" +
619    " </CLASS>" +
620    " </PREDVAR>" +
621    " <PREDVAR id=\"phi\">" +
622    " <VAR id=\"x\" />" +
623    " <VAR id=\"y\" />" +
624    " </PREDVAR>" +
625    "</FORALL>");
626    // System.out.println(ele.toString());
627  1 LogicalCheckExceptionList list =
628    FormulaChecker.checkFormula(ele, context, getChecker());
629  1 assertEquals(1, list.size());
630  1 assertEquals(30780, list.get(0).getErrorCode());
631    }
632   
633    /**
634    * Function: checkFormula(Element)
635    * Type: negative, code 30580, mixed free bound
636    * Data: exists x phi(x, {y | A)}) phi(x, y)
637    *
638    * @throws Exception Test failed.
639    */
 
640  1 toggle public void testQuantifiersNegative23() throws Exception {
641  1 final Element ele = TestParser.createElement(
642    "<EXISTS>" +
643    " <VAR id=\"x\" />" +
644    " <PREDVAR id=\"phi\">" +
645    " <VAR id=\"x\" />" +
646    " <CLASS>" +
647    " <VAR id=\"y\" />" +
648    " <PREDVAR id=\"A\"/>" +
649    " </CLASS>" +
650    " </PREDVAR>" +
651    " <PREDVAR id=\"phi\">" +
652    " <VAR id=\"x\" />" +
653    " <VAR id=\"y\" />" +
654    " </PREDVAR>" +
655    "</EXISTS>");
656    // System.out.println(ele.toString());
657  1 LogicalCheckExceptionList list =
658    FormulaChecker.checkFormula(ele, context, getChecker());
659  1 assertEquals(1, list.size());
660  1 assertEquals(30780, list.get(0).getErrorCode());
661    }
662   
663    /**
664    * Function: checkFormula(Element)
665    * Type: negative, code 30580, mixed free bound
666    * Data: exists! x phi({y | A)}, x): phi(x, y)
667    *
668    * @throws Exception Test failed.
669    */
 
670  1 toggle public void testQuantifiersNegative24() throws Exception {
671  1 final Element ele = TestParser.createElement(
672    "<EXISTSU>" +
673    " <VAR id=\"x\" />" +
674    " <PREDVAR id=\"phi\">" +
675    " <CLASS>" +
676    " <VAR id=\"y\" />" +
677    " <PREDVAR id=\"A\"/>" +
678    " </CLASS>" +
679    " <VAR id=\"x\" />" +
680    " </PREDVAR>" +
681    " <PREDVAR id=\"phi\">" +
682    " <VAR id=\"x\" />" +
683    " <VAR id=\"y\" />" +
684    " </PREDVAR>" +
685    "</EXISTSU>");
686    // System.out.println(ele.toString());
687  1 LogicalCheckExceptionList list =
688    FormulaChecker.checkFormula(ele, context, getChecker());
689  1 assertEquals(1, list.size());
690  1 assertEquals(30780, list.get(0).getErrorCode());
691    }
692   
693    /**
694    * Function: checkFormula(Element)
695    * Type: negative, code 30580, mixed free bound
696    * Data: all x (all y psi(x)): phi(x, y)
697    *
698    * @throws Exception Test failed.
699    */
 
700  1 toggle public void testQuantifiersNegative25() throws Exception {
701  1 final Element ele = TestParser.createElement(
702    "<FORALL>" +
703    " <VAR id=\"x\" />" +
704    " <FORALL>" +
705    " <VAR id=\"y\" />" +
706    " <PREDVAR id=\"psi\">" +
707    " <VAR id=\"x\" />" +
708    " </PREDVAR>" +
709    " </FORALL>" +
710    " <PREDVAR id=\"phi\">" +
711    " <VAR id=\"x\" />" +
712    " <VAR id=\"y\" />" +
713    " </PREDVAR>" +
714    "</FORALL>");
715    // System.out.println(ele.toString());
716  1 LogicalCheckExceptionList list =
717    FormulaChecker.checkFormula(ele, context, getChecker());
718  1 assertEquals(1, list.size());
719  1 assertEquals(30780, list.get(0).getErrorCode());
720    }
721   
722    /**
723    * Function: checkFormula(Element)
724    * Type: negative, code 30580, mixed free bound
725    * Data: exists x (all y phi(x, y)): phi(x, y)
726    *
727    * @throws Exception Test failed.
728    */
 
729  1 toggle public void testQuantifiersNegative26() throws Exception {
730  1 final Element ele = TestParser.createElement(
731    "<EXISTS>" +
732    " <VAR id=\"x\" />" +
733    " <FORALL>" +
734    " <VAR id=\"y\" />" +
735    " <PREDVAR id=\"phi\">" +
736    " <VAR id=\"x\" />" +
737    " <VAR id=\"y\" />" +
738    " </PREDVAR>" +
739    " </FORALL>" +
740    " <PREDVAR id=\"phi\">" +
741    " <VAR id=\"x\" />" +
742    " <VAR id=\"y\" />" +
743    " </PREDVAR>" +
744    "</EXISTS>");
745    // System.out.println(ele.toString());
746  1 LogicalCheckExceptionList list =
747    FormulaChecker.checkFormula(ele, context, getChecker());
748  1 assertEquals(1, list.size());
749  1 assertEquals(30780, list.get(0).getErrorCode());
750    }
751   
752    /**
753    * Function: checkFormula(Element)
754    * Type: negative, code 30580, mixed free bound
755    * Data: exists! x (exists! y phi(y, x) A): phi(x, y)
756    *
757    * @throws Exception Test failed.
758    */
 
759  1 toggle public void testQuantifiersNegative27() throws Exception {
760  1 final Element ele = TestParser.createElement(
761    "<EXISTSU>" +
762    " <VAR id=\"x\" />" +
763    " <EXISTSU>" +
764    " <VAR id=\"y\" />" +
765    " <PREDVAR id=\"phi\">" +
766    " <VAR id=\"y\" />" +
767    " <VAR id=\"x\" />" +
768    " </PREDVAR>" +
769    " <PREDVAR id=\"A\"/>" +
770    " </EXISTSU>" +
771    " <PREDVAR id=\"phi\">" +
772    " <VAR id=\"x\" />" +
773    " <VAR id=\"y\" />" +
774    " </PREDVAR>" +
775    "</EXISTSU>");
776    // System.out.println(ele.toString());
777  1 LogicalCheckExceptionList list =
778    FormulaChecker.checkFormula(ele, context, getChecker());
779  1 assertEquals(1, list.size());
780  1 assertEquals(30780, list.get(0).getErrorCode());
781    }
782   
783    }
 
CloverReport generated by Clover Code Coverage v2.3.1
Sat Sep 18 2010 04:09:52 UTC.		   Clover: Open Source License registered to qedeq.org .