Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../img/srcFileCovDistChart5.png 87% of files have more coverage
96   299   42   5.05
24   234   0.44   19
19     2.21  
1    
 
  SimpleProofFinderExecutor       Line # 60 96 42 48.9% 0.48920864
 
  (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   
16    package org.qedeq.kernel.bo.service.logic;
17   
18    import java.io.File;
19   
20    import org.qedeq.base.io.Parameters;
21    import org.qedeq.base.trace.Trace;
22    import org.qedeq.base.utility.YodaUtility;
23    import org.qedeq.kernel.bo.log.ModuleLogListener;
24    import org.qedeq.kernel.bo.log.QedeqLog;
25    import org.qedeq.kernel.bo.logic.ProofFinderFactoryImpl;
26    import org.qedeq.kernel.bo.logic.proof.common.ProofFinder;
27    import org.qedeq.kernel.bo.logic.proof.common.ProofFinderFactory;
28    import org.qedeq.kernel.bo.logic.proof.common.ProofFoundException;
29    import org.qedeq.kernel.bo.logic.proof.common.ProofNotFoundException;
30    import org.qedeq.kernel.bo.module.ControlVisitor;
31    import org.qedeq.kernel.bo.module.InternalServiceCall;
32    import org.qedeq.kernel.bo.module.KernelQedeqBo;
33    import org.qedeq.kernel.bo.module.PluginExecutor;
34    import org.qedeq.kernel.bo.module.QedeqFileDao;
35    import org.qedeq.kernel.se.base.module.Axiom;
36    import org.qedeq.kernel.se.base.module.FormalProofLineList;
37    import org.qedeq.kernel.se.base.module.FunctionDefinition;
38    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
39    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
40    import org.qedeq.kernel.se.base.module.PredicateDefinition;
41    import org.qedeq.kernel.se.base.module.Proposition;
42    import org.qedeq.kernel.se.base.module.Rule;
43    import org.qedeq.kernel.se.common.ModuleDataException;
44    import org.qedeq.kernel.se.common.Plugin;
45    import org.qedeq.kernel.se.common.SourceFileExceptionList;
46    import org.qedeq.kernel.se.dto.module.AddVo;
47    import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
48    import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
49    import org.qedeq.kernel.se.dto.module.FormalProofVo;
50    import org.qedeq.kernel.se.dto.module.FormulaVo;
51    import org.qedeq.kernel.se.dto.module.PropositionVo;
52    import org.qedeq.kernel.se.state.WellFormedState;
53   
54   
55    /**
56    * Finds simple formal proofs.
57    *
58    * @author Michael Meyling
59    */
 
60    public final class SimpleProofFinderExecutor extends ControlVisitor implements PluginExecutor {
61   
62    /** This class. */
63    private static final Class CLASS = SimpleProofFinderExecutor.class;
64   
65    /** Factory for generating new checkers. */
66    private ProofFinderFactory finderFactory = null;
67   
68    /** List of axioms, definitions and propositions. */
69    private FormalProofLineListVo validFormulas;
70   
71    /** Save changed modules directly? */
72    private boolean noSave;
73   
74    /** Currently running proof finder. */
75    private ProofFinder finder;
76   
77    /** All parameters for this search. */
78    private Parameters parameters;
79   
80    /**
81    * Constructor.
82    *
83    * @param plugin This plugin we work for.
84    * @param qedeq QEDEQ BO object.
85    * @param parameters Parameters.
86    */
 
87  3 toggle SimpleProofFinderExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
88    final Parameters parameters) {
89  3 super(plugin, qedeq);
90  3 final String method = "SimpleProofFinderExecutor(Plugin, KernelQedeqBo, Map)";
91  3 final String finderFactoryClass = parameters.getString("checkerFactory");
92  3 if (finderFactoryClass != null && finderFactoryClass.length() > 0) {
93  0 try {
94  0 Class cl = Class.forName(finderFactoryClass);
95  0 finderFactory = (ProofFinderFactory) cl.newInstance();
96    } catch (ClassNotFoundException e) {
97  0 Trace.fatal(CLASS, this, method, "ProofFinderFactory class not in class path: "
98    + finderFactoryClass, e);
99    } catch (InstantiationException e) {
100  0 Trace.fatal(CLASS, this, method, "ProofFinderFactory class could not be instanciated: "
101    + finderFactoryClass, e);
102    } catch (IllegalAccessException e) {
103  0 Trace.fatal(CLASS, this, method,
104    "Programming error, access for instantiation failed for model: "
105    + finderFactoryClass, e);
106    } catch (RuntimeException e) {
107  0 Trace.fatal(CLASS, this, method,
108    "Programming error, instantiation failed for model: " + finderFactoryClass, e);
109    }
110    }
111    // fallback is the default finder factory
112  3 if (finderFactory == null) {
113  3 finderFactory = new ProofFinderFactoryImpl();
114    }
115  3 noSave = parameters.getBoolean("noSave");
116  3 this.parameters = parameters;
117    }
118   
 
119  3 toggle private Plugin getPlugin() {
120  3 return (Plugin) getService();
121    }
122   
 
123  3 toggle public Object executePlugin(final InternalServiceCall call, final Object data) {
124  3 getServices().checkWellFormedness(call.getInternalServiceProcess(), getQedeqBo());
125  3 QedeqLog.getInstance().logRequest("Trying to create formal proofs", getQedeqBo().getUrl());
126  3 try {
127  3 validFormulas = new FormalProofLineListVo();
128  3 traverse(call.getInternalServiceProcess());
129  3 QedeqLog.getInstance().logSuccessfulReply(
130    "Proof creation finished for", getQedeqBo().getUrl());
131    } catch (SourceFileExceptionList e) {
132  0 final String msg = "Proof creation not (fully?) successful";
133  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(), e.getMessage());
134  0 return Boolean.FALSE;
135    } finally {
136  3 getQedeqBo().addPluginErrorsAndWarnings(getPlugin(), getErrorList(), getWarningList());
137    }
138  3 return Boolean.TRUE;
139    }
140   
 
141  14 toggle public void visitEnter(final Axiom axiom) throws ModuleDataException {
142  14 if (axiom == null) {
143  0 return;
144    }
145  14 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
146    new AddVo(getNodeBo().getNodeVo().getId())));
147  14 setBlocked(true);
148    }
149   
 
150  14 toggle public void visitLeave(final Axiom axiom) {
151  14 setBlocked(false);
152    }
153   
 
154  0 toggle public void visitEnter(final PredicateDefinition definition)
155    throws ModuleDataException {
156  0 if (definition == null) {
157  0 return;
158    }
159  0 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
160    new AddVo(getNodeBo().getNodeVo().getId())));
161  0 setBlocked(true);
162    }
163   
 
164  0 toggle public void visitLeave(final PredicateDefinition definition) {
165  0 setBlocked(false);
166    }
167   
 
168  0 toggle public void visitEnter(final InitialPredicateDefinition definition)
169    throws ModuleDataException {
170  0 setBlocked(true);
171    }
172   
 
173  0 toggle public void visitLeave(final InitialPredicateDefinition definition) {
174  0 setBlocked(false);
175    }
176   
 
177  0 toggle public void visitEnter(final InitialFunctionDefinition definition)
178    throws ModuleDataException {
179  0 setBlocked(true);
180    }
181   
 
182  0 toggle public void visitLeave(final InitialFunctionDefinition definition) {
183  0 setBlocked(false);
184    }
185   
 
186  0 toggle public void visitEnter(final FunctionDefinition definition)
187    throws ModuleDataException {
188  0 if (definition == null) {
189  0 return;
190    }
191  0 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
192    new AddVo(getNodeBo().getNodeVo().getId())));
193  0 setBlocked(true);
194    }
195   
 
196  0 toggle public void visitLeave(final FunctionDefinition definition) {
197  0 setBlocked(false);
198    }
199   
 
200  13 toggle public void visitEnter(final Proposition proposition)
201    throws ModuleDataException {
202  13 final String method = "visitEnter(Proposition)";
203  13 Trace.begin(CLASS, this, method);
204  13 if (proposition == null) {
205  0 Trace.end(CLASS, this, method);
206  0 return;
207    }
208  13 if (proposition.getFormalProofList() == null) {
209  6 FormalProofLineList proof = null;
210    // we try finding a proof
211  6 try {
212  6 finder = finderFactory.createProofFinder();
213  6 finder.findProof(proposition.getFormula().getElement(), validFormulas,
214    getCurrentContext(), parameters, new ModuleLogListener() {
 
215  181 toggle public void logMessageState(final String text) {
216  181 QedeqLog.getInstance().logMessageState(text, getQedeqBo().getUrl());
217    }
218    }, getQedeqBo().getElement2Utf8());
219    } catch (ProofFoundException e) {
220  6 proof = e.getProofLines();
221    } catch (ProofNotFoundException e) {
222  0 addWarning(e);
223    } finally {
224  6 finder = null; // so we always new if we are currently searching
225    }
226  6 if (proof != null) {
227  6 QedeqLog.getInstance().logMessage("proof found for "
228    + super.getLocationDescription());
229    // TODO 20110323 m31: we do a dirty cast to modify the current module
230  6 Object state;
231  6 try {
232  6 state = YodaUtility.getFieldValue(getQedeqBo(), "stateManager");
233  6 YodaUtility.executeMethod(state, "setWellFormedState", new Class[] {
234    WellFormedState.class},
235    new Object[] {WellFormedState.STATE_UNCHECKED});
236  6 ((PropositionVo) proposition).addFormalProof(new FormalProofVo(proof));
237  6 YodaUtility.executeMethod(state, "setErrors", new Class[] {
238    SourceFileExceptionList.class},
239    new Object[] {null});
240    } catch (Exception e) {
241  0 final String msg = "changing properties failed";
242  0 Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e);
243  0 QedeqLog.getInstance().logMessage(msg + " " + e.toString());
244    }
245    } else {
246  0 QedeqLog.getInstance().logMessage("proof not found for "
247    + super.getLocationDescription());
248    }
249  6 if (proof != null && !noSave) {
250  0 final File file = getServices().getLocalFilePath(
251    getQedeqBo().getModuleAddress());
252  0 try {
253  0 QedeqLog.getInstance().logMessage(
254    "Saving file \"" + file + "\"");
255  0 QedeqFileDao dao = getServices().getQedeqFileDao();
256  0 dao.saveQedeq(getInternalServiceCall().getInternalServiceProcess(), getQedeqBo(), file);
257  0 if (!getQedeqBo().getModuleAddress().isFileAddress()) {
258  0 QedeqLog.getInstance().logMessage("Only the the buffered file changed!");
259    }
260    } catch (Exception e) {
261  0 final String msg = "Saving file \"" + file + "\" failed";
262  0 Trace.fatal(CLASS, "visitEnter(Proposition)", msg, e);
263  0 QedeqLog.getInstance().logMessage(msg + " " + e.toString());
264    }
265    }
266    } else {
267  7 Trace.info(CLASS, method, "has already a proof: "
268    + super.getLocationDescription());
269  7 validFormulas.add(new FormalProofLineVo(new FormulaVo(getNodeBo().getFormula()),
270    new AddVo(getNodeBo().getNodeVo().getId())));
271    }
272  13 setBlocked(true);
273  13 Trace.end(CLASS, this, method);
274    }
275   
 
276  13 toggle public void visitLeave(final Proposition definition) {
277  13 setBlocked(false);
278    }
279   
 
280  24 toggle public void visitEnter(final Rule rule) throws ModuleDataException {
281  24 if (rule == null) {
282  0 return;
283    }
284  24 setBlocked(true);
285    }
286   
 
287  24 toggle public void visitLeave(final Rule rule) {
288  24 setBlocked(false);
289    }
290   
 
291  0 toggle public String getLocationDescription() {
292  0 final String s = super.getLocationDescription();
293  0 if (finder == null) {
294  0 return s;
295    }
296  0 return s + " " + finder.getExecutionActionDescription();
297    }
298   
299    }