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