|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
CalculateTruthDynamicThreeModelTest | Line # 37 | 24 | 10 | 100% |
1.0
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
(48) | |||
Result | |||
0.5
|
org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology44 org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology44 | 1 PASS | |
0.5
|
org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology44b org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology44b | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology28 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology28 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology23 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology23 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology40 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology40 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology13 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology13 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology04 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology04 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology21 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology21 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology41 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology41 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology24 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology24 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology02 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology02 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology10 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology10 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology19 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology19 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology42 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology42 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology11 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology11 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology43 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology43 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology18 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology18 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology37 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology37 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology06 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology06 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology25 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology25 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology07 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology07 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology16 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology16 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology39 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology39 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology12 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology12 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology31 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology31 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology27 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology27 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology30 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology30 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology08 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology08 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology38 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology38 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology15 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology15 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology33 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology33 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology22 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology22 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology36 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology36 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology29 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology29 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology32 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology32 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology17 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology17 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology26 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology26 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology14 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology14 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology09 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology09 | 1 PASS | |
0.29411766
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology20 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology20 | 1 PASS | |
0.2647059
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology05 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology05 | 1 PASS | |
0.2647059
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology35 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology35 | 1 PASS | |
0.2647059
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology03 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology03 | 1 PASS | |
0.2647059
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology34 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology34 | 1 PASS | |
0.2647059
|
org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology01 org.qedeq.kernel.bo.logic.model.CalculateTruthTestCase.testTautology01 | 1 PASS | |
0.029411765
|
org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology47 org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology47 | 1 PASS | |
0.029411765
|
org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology46 org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology46 | 1 PASS | |
0.029411765
|
org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology45 org.qedeq.kernel.bo.logic.model.CalculateTruthDynamicThreeModelTest.testTautology45 | 1 PASS | |
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 | public CalculateTruthDynamicThreeModelTest() { |
45 | 48 | super(new ThreeDynamicModel()); |
46 | } | |
47 | ||
48 | 48 | 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 | 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 | 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 | 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 | 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 | public void testTautology47() throws Exception { |
176 | // ignore | |
177 | } | |
178 | ||
179 | 45 | 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 | } |
|