Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
17   175   9   1.89
0   75   0.53   9
9     1  
1    
 
  CalculateTruthUnaryModelTest       Line # 27 17 9 100% 1.0
 
  (8)
 
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.model;
17   
18    import org.qedeq.kernel.se.base.list.Element;
19    import org.qedeq.kernel.xml.parser.BasicParser;
20   
21   
22    /**
23    * Testing the truth calculation with zero model.
24    *
25    * @author Michael Meyling
26    */
 
27    public class CalculateTruthUnaryModelTest extends CalculateTruthTestCase {
28   
29    /**
30    * Constructor.
31    */
 
32  47 toggle public CalculateTruthUnaryModelTest() {
33  47 super(new UnaryModel());
34    }
35   
36    /**
37    * Function: isTautology(Element)
38    * Type: positive (only in this model!!!)
39    * Data: A(x,y) <-> A(y,x)
40    *
41    * @throws Exception Test failed.
42    */
 
43  1 toggle public void testTautology19() throws Exception {
44  1 final Element ele = BasicParser.createElement(
45    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
46    + "<PREDVAR id=\"A\"><VAR id=\"y\"/><VAR id=\"x\"/></PREDVAR></EQUI>");
47    // System.out.println(ele.toString());
48  1 assertTrue(isTautology(ele));
49    }
50   
51    /**
52    * Function: isTautology(Element)
53    * Type: positive
54    * Type: positive (only in this model!!!)
55    *
56    * @throws Exception Test failed.
57    */
 
58  1 toggle public void testTautology20() throws Exception {
59  1 final Element ele = BasicParser.createElement(
60    "<EQUI><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
61    + "<PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"x\"/></PREDVAR></EQUI>");
62    // System.out.println(ele.toString());
63  1 assertTrue(isTautology(ele));
64    }
65   
66    /**
67    * Function: isTautology(Element)
68    * Type: positive (only in this model!!!)
69    * Data: A(y) <-> A(x)
70    *
71    * @throws Exception Test failed.
72    */
 
73  1 toggle public void testTautology21() throws Exception {
74  1 final Element ele = BasicParser.createElement(
75    "<EQUI><PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR>"
76    + "<PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR></EQUI>");
77    // System.out.println(ele.toString());
78  1 assertTrue(isTautology(ele));
79    }
80   
81    /**
82    * Function: isTautology(Element)
83    * Type: positive (only in this model!!!)
84    * Data: \forall x \forall y (A(x) -> A(y))
85    *
86    * @throws Exception Test failed.
87    */
 
88  1 toggle public void testTautology28() throws Exception {
89  1 final Element ele = BasicParser.createElement(
90    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><IMPL><PREDVAR id=\"A\"><VAR id=\"x\"/></PREDVAR>"
91    + "<PREDVAR id=\"A\"><VAR id=\"y\"/></PREDVAR></IMPL></FORALL></FORALL>");
92    // System.out.println(ele.toString());
93  1 assertTrue(isTautology(ele));
94    }
95   
96    /**
97    * Function: isTautology(Element)
98    * Type: positive (only in this model!!!)
99    * Data: \forall x \forall A(x,y): A(y,x))
100    *
101    * @throws Exception Test failed.
102    */
 
103  1 toggle public void testTautology31() throws Exception {
104  1 final Element ele = BasicParser.createElement(
105    "<FORALL><VAR id=\"x\"/><FORALL><VAR id=\"y\"/><PREDVAR id=\"A\"><VAR id=\"x\"/><VAR id=\"y\"/></PREDVAR>"
106    + "<PREDVAR id=\"A\"><VAR id=\"y\"/><VAR id=\"x\"/></PREDVAR></FORALL></FORALL>");
107    // System.out.println(ele.toString());
108  1 assertTrue(isTautology(ele));
109    }
110   
111    /**
112    * Function: isTautology(Element)
113    * Type: positive (only in this model!!!)
114    * Data: \exists! y (y = y)
115    *
116    * @throws Exception Test failed.
117    */
 
118  1 toggle public void testTautology34() throws Exception {
119  1 final Element ele = BasicParser.createElement(
120    "<EXISTSU><VAR id=\"y\"/><PREDCON id=\"equal\"><VAR id=\"y\"/><VAR id=\"y\"/></PREDCON>"
121    + "</EXISTSU>");
122    // System.out.println(ele.toString());
123  1 assertTrue(isTautology(ele));
124    }
125   
126    /**
127    * Function: isTautology(Element)
128    * Type: positive (only in this model!!!)
129    * Data: f(x) = f(y)
130    *
131    * @throws Exception Test failed.
132    */
 
133  1 toggle public void testTautology37() throws Exception {
134  1 final Element ele = BasicParser.createElement(
135    "<PREDCON id=\"equal\"><FUNVAR id=\"f\"><VAR id=\"x\"/></FUNVAR>"
136    + "<FUNVAR id=\"f\"><VAR id=\"y\"/></FUNVAR></PREDCON>");
137    // System.out.println(ele.toString());
138  1 assertTrue(isTautology(ele));
139    }
140   
141    /**
142    * Function: isTautology(Element)
143    * Type: positive (only in this model!!!)
144    * Data: \forall x (\phi(x) <-> A) <-> (\forall x (\phi(x)) <-> A)
145    *
146    * @throws Exception Test failed.
147    */
 
148  1 toggle public void testTautology41() throws Exception {
149  1 final Element ele = BasicParser.createElement(
150    "\n <EQUI>"
151    + "\n <FORALL>"
152    + "\n <VAR id=\"x\" />"
153    + "\n <EQUI>"
154    + "\n <PREDVAR id=\"\\phi\">"
155    + "\n <VAR id=\"x\" />"
156    + "\n </PREDVAR>"
157    + "\n <PREDVAR id=\"A\" />"
158    + "\n </EQUI>"
159    + "\n </FORALL>"
160    + "\n <EQUI>"
161    + "\n <FORALL>"
162    + "\n <VAR id=\"x\" />"
163    + "\n <PREDVAR id=\"\\phi\">"
164    + "\n <VAR id=\"x\" />"
165    + "\n </PREDVAR>"
166    + "\n </FORALL>"
167    + "\n <PREDVAR id=\"A\" />"
168    + "\n </EQUI>"
169    + "\n </EQUI>"
170    );
171    // System.out.println(ele.toString());
172  1 assertTrue(isTautology(ele));
173    }
174   
175    }