Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
24   205   10   3
2   115   0.42   8
8     1.25  
1    
 
  CalculateTruthDynamicThreeModelTest       Line # 37 24 10 100% 1.0
 
  (48)
 
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 java.io.File;
19    import java.util.ArrayList;
20    import java.util.List;
21   
22    import org.qedeq.base.io.UrlUtility;
23    import org.qedeq.kernel.bo.logic.common.SubjectVariable;
24    import org.qedeq.kernel.bo.module.KernelQedeqBo;
25    import org.qedeq.kernel.se.base.list.Element;
26    import org.qedeq.kernel.se.common.DefaultModuleAddress;
27    import org.qedeq.kernel.se.common.ModuleAddress;
28    import org.qedeq.kernel.se.common.ModuleContext;
29    import org.qedeq.kernel.xml.parser.BasicParser;
30   
31   
32    /**
33    * Testing the truth calculation with default model.
34    *
35    * @author Michael Meyling
36    */
 
37    public class CalculateTruthDynamicThreeModelTest extends CalculateTruthTestCase {
38   
39    private DynamicInterpreter interpreter;
40   
41    /**
42    * Constructor.
43    */
 
44  48 toggle public CalculateTruthDynamicThreeModelTest() {
45  48 super(new ThreeDynamicModel());
46    }
47   
 
48  48 toggle public void setUp() throws Exception {
49  48 super.setUp();
50  48 final ModuleAddress address = getServices().getModuleAddress(
51    UrlUtility.toUrl(new File(getDocDir(), "math/qedeq_set_theory_v1.xml")));
52  48 final KernelQedeqBo prop = (KernelQedeqBo) getServices().loadModule(
53    address);
54  48 interpreter = new DynamicInterpreter((DynamicModel) getModel(), prop);
55    }
56   
57    /**
58    * Function: isTautology(Element)
59    * Type: false (in this model)
60    * Data: \exists x \all y (y \in x <-> (isSet(y) n \phi(y)))
61    *
62    * @throws Exception Test failed.
63    */
 
64  1 toggle public void testTautology44b() throws Exception {
65  1 final Element def = BasicParser.createElement(
66    " <EXISTS>\n"
67    + " <VAR id=\"y\"/>\n"
68    + " <PREDCON ref=\"in\">\n"
69    + " <VAR id=\"x\"/>\n"
70    + " <VAR id=\"y\"/>\n"
71    + " </PREDCON>\n"
72    + " </EXISTS>\n");
73  1 final List variables = new ArrayList();
74  1 variables.add(new SubjectVariable("x"));
75  1 interpreter.addPredicateConstant(new ModelPredicateConstant("isSet", 1), variables, def.getList());
76  1 final Element ele = BasicParser.createElement(
77    " <EXISTS>\n"
78    + " <VAR id=\"x\"/>\n"
79    + " <FORALL>\n"
80    + " <VAR id=\"y\"/>\n"
81    + " <EQUI>\n"
82    + " <PREDCON ref=\"in\">\n"
83    + " <VAR id=\"y\"/>\n"
84    + " <VAR id=\"x\"/>\n"
85    + " </PREDCON>\n"
86    + " <AND>\n"
87    + " <PREDCON ref=\"isSet\">\n"
88    + " <VAR id=\"y\"/>\n"
89    + " </PREDCON>\n"
90    + " <PREDVAR id=\"\\phi\">\n"
91    + " <VAR id=\"y\"/>\n"
92    + " </PREDVAR>\n"
93    + " </AND>\n"
94    + " </EQUI>\n"
95    + " </FORALL>\n"
96    + " </EXISTS>\n"
97    );
98    // System.out.println(ele.toString());
99  1 assertFalse(isTautology(ele));
100    }
101   
102    /**
103    * Function: isTautology(Element)
104    * Type: false (in this model)
105    * Data: (y \in {x | \phi(x)} <-> (isSet(y) n \phi(y))
106    *
107    * @throws Exception Test failed.
108    */
 
109  1 toggle public void testTautology44() throws Exception {
110  1 final Element def = BasicParser.createElement(
111    " <EXISTS>\n"
112    + " <VAR id=\"y\"/>\n"
113    + " <PREDCON ref=\"in\">\n"
114    + " <VAR id=\"x\"/>\n"
115    + " <VAR id=\"y\"/>\n"
116    + " </PREDCON>\n"
117    + " </EXISTS>\n");
118  1 final List variables = new ArrayList();
119  1 variables.add(new SubjectVariable("x"));
120  1 interpreter.addPredicateConstant(new ModelPredicateConstant("isSet", 1), variables, def.getList());
121  1 final Element ele = BasicParser.createElement(
122    " <EQUI>\n"
123    + " <PREDCON ref=\"in\">\n"
124    + " <VAR id=\"y\"/>\n"
125    + " <CLASS>\n"
126    + " <VAR id=\"x\"/>\n"
127    + " <PREDVAR id=\"\\phi\">\n"
128    + " <VAR id=\"x\"/>\n"
129    + " </PREDVAR>\n"
130    + " </CLASS>\n"
131    + " </PREDCON>\n"
132    + " <AND>\n"
133    + " <PREDCON ref=\"isSet\">\n"
134    + " <VAR id=\"y\"/>\n"
135    + " </PREDCON>\n"
136    + " <PREDVAR id=\"\\phi\">\n"
137    + " <VAR id=\"y\"/>\n"
138    + " </PREDVAR>\n"
139    + " </AND>\n"
140    + " </EQUI>\n"
141    );
142    // System.out.println(ele.toString());
143  1 assertFalse(isTautology(ele));
144    }
145   
146    /**
147    * Function: isTautology(Element)
148    * Type: not tested
149    * Data: see below
150    *
151    * @throws Exception Test failed.
152    */
 
153  1 toggle public void testTautology45() throws Exception {
154    // ignore
155    }
156   
157    /**
158    * Function: isTautology(Element)
159    * Type: not tested
160    * Data: x <= y <-> x n C(y) = 0
161    *
162    * @throws Exception Test failed.
163    */
 
164  1 toggle public void testTautology46() throws Exception {
165    // ignore
166    }
167   
168    /**
169    * Function: isTautology(Element)
170    * Type: not tested
171    * Data: see below
172    *
173    * @throws Exception Test failed.
174    */
 
175  1 toggle public void testTautology47() throws Exception {
176    // ignore
177    }
178   
 
179  45 toggle protected boolean isTautology(final Element formula) throws HeuristicException {
180  45 boolean result = true;
181  45 ModuleContext context = new ModuleContext(new DefaultModuleAddress());
182  45 try {
183  45 do {
184    // System.out.println(interpreter.toString());
185    // if (interpreter.toString().indexOf("subject variables {y={{}}}") >= 0
186    // if (interpreter.toString().indexOf("predicate variables {\\phi(*)=={{}}}") >= 0) {
187    // Trace.setTraceOn(true);
188    // System.out.println("Know!");
189    // }
190  1956 result &= interpreter.calculateValue(new ModuleContext(context), formula);
191    // if (interpreter.toString().indexOf("predicate variables {\\phi(*)=={{}}}") >= 0) {
192    // Trace.setTraceOn(false);
193    // }
194  1956 } while (result && interpreter.next());
195    // if (!result) {
196    // System.out.println(interpreter);
197    // }
198    // System.out.println("interpretation finished - and result is = " + result);
199    } finally {
200  45 interpreter.clearVariables();
201    }
202  45 return result;
203    }
204   
205    }
 
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 .