Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
118   242   10   11.8
0   167   0.08   10
10     1  
1    
 
  SimpleProofFinderPluginTest       Line # 45 118 10 92.2% 0.921875
 
  (3)
 
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    package org.qedeq.kernel.bo.service.logic;
16   
17    import java.io.File;
18    import java.util.HashMap;
19    import java.util.Map;
20   
21    import org.qedeq.base.io.Parameters;
22    import org.qedeq.kernel.bo.common.QedeqBo;
23    import org.qedeq.kernel.bo.log.LogListenerImpl;
24    import org.qedeq.kernel.bo.log.ModuleEventListenerLog;
25    import org.qedeq.kernel.bo.log.ModuleEventLog;
26    import org.qedeq.kernel.bo.log.QedeqLog;
27    import org.qedeq.kernel.bo.module.KernelNodeBo;
28    import org.qedeq.kernel.bo.module.KernelQedeqBo;
29    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
30    import org.qedeq.kernel.se.common.DefaultModuleAddress;
31    import org.qedeq.kernel.se.common.ModuleAddress;
32    import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
33    import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
34    import org.qedeq.kernel.se.dto.module.FormalProofVo;
35    import org.qedeq.kernel.se.dto.module.NodeVo;
36    import org.qedeq.kernel.se.dto.module.PropositionVo;
37   
38    /**
39    * For testing of loading required QEDEQ modules.
40    *
41    * FIXME m31 20100823: integrate some more unit tests here! Check proof result validity.
42    *
43    * @author Michael Meyling
44    */
 
45    public class SimpleProofFinderPluginTest extends QedeqBoTestCase {
46   
47    private LogListenerImpl listener;
48    private ModuleEventListenerLog moduleListener;
49   
 
50  0 toggle public SimpleProofFinderPluginTest() {
51  0 super();
52    }
53   
 
54  3 toggle public SimpleProofFinderPluginTest(final String name) {
55  3 super(name);
56    }
57   
 
58  3 toggle public void setUp() throws Exception {
59  3 super.setUp();
60  3 listener = new LogListenerImpl();
61  3 QedeqLog.getInstance().addLog(listener);
62  3 moduleListener = new ModuleEventListenerLog();
63  3 ModuleEventLog.getInstance().addLog(moduleListener);
64    }
65   
 
66  3 toggle public void tearDown() throws Exception {
67  3 ModuleEventLog.getInstance().removeLog(moduleListener);
68  3 QedeqLog.getInstance().removeLog(listener);
69  3 super.tearDown();
70    }
71   
72    /**
73    * Try proof finder.
74    *
75    * @throws Exception
76    */
 
77  1 toggle public void testPlugin() throws Exception {
78  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
79    "sample/qedeq_sample3.xml"));
80  1 getServices().checkWellFormedness(address);
81  1 final QedeqBo bo = getServices().getQedeqBo(address);
82  1 assertTrue(bo.isWellFormed());
83  1 assertEquals(0, bo.getWarnings().size());
84  1 assertEquals(0, bo.getErrors().size());
85  1 KernelQedeqBo qedeq = (KernelQedeqBo) bo;
86  1 removeFormalProof(qedeq, "proposition:one");
87  1 removeFormalProof(qedeq, "proposition:two");
88    // addDummyFormalProof(qedeq, "proposition:three"); TODO 20130325 m31: if proof extension
89    // works, this might be useful
90  1 getServices().checkFormallyProved(address);
91  1 assertFalse(getServices().getQedeqBo(address).isFullyFormallyProved());
92  1 final Map parameters = new HashMap();
93  1 parameters.put("noSave", "true");
94  1 parameters.put("extraVars", "0");
95  1 parameters.put("propositionVariableOrder", "2");
96  1 parameters.put("propositionVariableWeight", "3");
97  1 parameters.put("partFormulaWeight", "0");
98  1 parameters.put("disjunctionOrder", "1");
99  1 parameters.put("disjunctionWeight", "3");
100  1 parameters.put("implicationWeight", "0");
101  1 parameters.put("negationWeight", "0");
102  1 parameters.put("conjunctionWeight", "0");
103  1 parameters.put("equivalenceWeight", "0");
104  1 getInternalServices().getConfig().setServiceKeyValues(new SimpleProofFinderPlugin(),
105    new Parameters(parameters));
106  1 getServices().executePlugin(SimpleProofFinderPlugin.class.getName(), address, null);
107  1 getServices().checkFormallyProved(address);
108  1 assertTrue(getServices().getQedeqBo(address).isFullyFormallyProved());
109    }
110   
111    /**
112    * Try proof finder. Removes unused axioms (and is two formulas faster...).
113    *
114    * @throws Exception
115    */
 
116  1 toggle public void testPlugin2() throws Exception {
117  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
118    "sample/qedeq_sample3.xml"));
119  1 getServices().checkWellFormedness(address);
120  1 final QedeqBo bo = getServices().getQedeqBo(address);
121  1 assertTrue(bo.isWellFormed());
122  1 assertEquals(0, bo.getWarnings().size());
123  1 assertEquals(0, bo.getErrors().size());
124  1 KernelQedeqBo qedeq = (KernelQedeqBo) bo;
125  1 removeNodeType(qedeq, "axiom:universalInstantiation");
126  1 removeNodeType(qedeq, "axiom:existencialGeneralization");
127  1 removeFormalProof(qedeq, "proposition:one");
128  1 removeFormalProof(qedeq, "proposition:two");
129    // addDummyFormalProof(qedeq, "proposition:three"); TODO 20130325 m31: if proof extension
130    // works, this might be useful
131  1 removeNodeType(qedeq, "proposition:four");
132  1 removeNodeType(qedeq, "proposition:five");
133  1 removeNodeType(qedeq, "proposition:six");
134  1 removeNodeType(qedeq, "proposition:seven");
135  1 getServices().checkFormallyProved(address);
136  1 assertFalse(getServices().getQedeqBo(address).isFullyFormallyProved());
137  1 final Map parameters = new HashMap();
138  1 parameters.put("noSave", "true");
139  1 parameters.put("extraVars", "0");
140  1 parameters.put("propositionVariableOrder", "2");
141  1 parameters.put("propositionVariableWeight", "3");
142  1 parameters.put("partFormulaWeight", "0");
143  1 parameters.put("disjunctionOrder", "1");
144  1 parameters.put("disjunctionWeight", "3");
145  1 parameters.put("implicationWeight", "0");
146  1 parameters.put("negationWeight", "0");
147  1 parameters.put("conjunctionWeight", "0");
148  1 parameters.put("equivalenceWeight", "0");
149  1 getInternalServices().getConfig().setServiceKeyValues(new SimpleProofFinderPlugin(), new Parameters(parameters));
150  1 getServices().executePlugin(SimpleProofFinderPlugin.class.getName(), address, null);
151  1 getServices().checkFormallyProved(address);
152  1 assertTrue(getServices().getQedeqBo(address).isFullyFormallyProved());
153    }
154   
155    /**
156    * Try proof finder. Removes unused axioms (and is two formulas faster...).
157    *
158    * @throws Exception
159    */
 
160  1 toggle public void testPluginFast() throws Exception {
161  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
162    "sample/qedeq_sample3.xml"));
163  1 getServices().checkWellFormedness(address);
164  1 final QedeqBo bo = getServices().getQedeqBo(address);
165  1 assertTrue(bo.isWellFormed());
166  1 assertEquals(0, bo.getWarnings().size());
167  1 assertEquals(0, bo.getErrors().size());
168  1 KernelQedeqBo qedeq = (KernelQedeqBo) bo;
169  1 removeNodeType(qedeq, "axiom:universalInstantiation");
170  1 removeNodeType(qedeq, "axiom:existencialGeneralization");
171  1 removeFormalProof(qedeq, "proposition:one");
172  1 removeFormalProof(qedeq, "proposition:two");
173    // addDummyFormalProof(qedeq, "proposition:three"); TODO 20130325 m31: if proof extension
174    // works, this might be useful
175  1 removeNodeType(qedeq, "proposition:four");
176  1 removeNodeType(qedeq, "proposition:five");
177  1 removeNodeType(qedeq, "proposition:six");
178  1 removeNodeType(qedeq, "proposition:seven");
179  1 assertFalse(getServices().getQedeqBo(address).isFullyFormallyProved());
180  1 getServices().checkFormallyProved(address);
181  1 assertFalse(getServices().getQedeqBo(address).isFullyFormallyProved());
182  1 final Map parameters = new HashMap();
183  1 parameters.put("noSave", "true");
184  1 parameters.put("extraVars", "0");
185  1 parameters.put("propositionVariableOrder", "2");
186  1 parameters.put("propositionVariableWeight", "3");
187  1 parameters.put("partFormulaOrder", "1");
188  1 parameters.put("partFormulaWeight", "1");
189  1 parameters.put("disjunctionOrder", "1");
190  1 parameters.put("disjunctionWeight", "3");
191  1 parameters.put("implicationWeight", "0");
192  1 parameters.put("negationWeight", "0");
193  1 parameters.put("conjunctionWeight", "0");
194  1 parameters.put("equivalenceWeight", "0");
195  1 getInternalServices().getConfig().setServiceKeyValues(new SimpleProofFinderPlugin(),
196    new Parameters(parameters));
197  1 getServices().executePlugin(SimpleProofFinderPlugin.class.getName(), address, null);
198  1 getServices().checkFormallyProved(address);
199  1 assertTrue(getServices().getQedeqBo(address).isFullyFormallyProved());
200    }
201   
202    /**
203    * Remove formal proof from proposition.
204    *
205    * @param qedeq Module.
206    * @param id Id of proposition where we remove all formal proofs.
207    */
 
208  6 toggle private void removeFormalProof(KernelQedeqBo qedeq, final String id) {
209  6 KernelNodeBo node = qedeq.getLabels().getNode(id);
210  6 PropositionVo proposition = (PropositionVo) node.getNodeVo().getNodeType().getProposition();
211  6 proposition.setFormalProofList(null);
212    }
213   
214    /**
215    * Remove node.
216    *
217    * @param qedeq Module.
218    * @param id Id of node we want to "delete".
219    */
 
220  12 toggle private void removeNodeType(KernelQedeqBo qedeq, final String id) {
221  12 KernelNodeBo node = qedeq.getLabels().getNode(id);
222  12 NodeVo node2 = node.getNodeVo();
223  12 node2.setNodeType(null);
224    }
225   
226    /**
227    * Add empty formal proof list to proposition.
228    *
229    * @param qedeq Module.
230    * @param id Id of proposition where we remove all formal proofs.
231    */
 
232  0 toggle private void addDummyFormalProof(KernelQedeqBo qedeq, final String id) {
233  0 KernelNodeBo node = qedeq.getLabels().getNode(id);
234  0 PropositionVo proposition = (PropositionVo) node.getNodeVo().getNodeType().getProposition();
235  0 final FormalProofVo proof = new FormalProofVo();
236  0 final FormalProofLineListVo lines = new FormalProofLineListVo();
237  0 lines.add(new FormalProofLineVo());
238  0 proof.setFormalProofLineList(lines);
239  0 proposition.addFormalProof(proof);
240    }
241   
242    }
 
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 .