1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
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 |
|
|
57 |
|
|
58 |
|
@author |
59 |
|
|
|
|
| 48.9% |
Uncovered Elements: 71 (139) |
Complexity: 42 |
Complexity Density: 0.44 |
|
60 |
|
public final class SimpleProofFinderExecutor extends ControlVisitor implements PluginExecutor { |
61 |
|
|
62 |
|
|
63 |
|
private static final Class CLASS = SimpleProofFinderExecutor.class; |
64 |
|
|
65 |
|
|
66 |
|
private ProofFinderFactory finderFactory = null; |
67 |
|
|
68 |
|
|
69 |
|
private FormalProofLineListVo validFormulas; |
70 |
|
|
71 |
|
|
72 |
|
private boolean noSave; |
73 |
|
|
74 |
|
|
75 |
|
private ProofFinder finder; |
76 |
|
|
77 |
|
|
78 |
|
private Parameters parameters; |
79 |
|
|
80 |
|
|
81 |
|
|
82 |
|
|
83 |
|
@param |
84 |
|
@param |
85 |
|
@param |
86 |
|
|
|
|
| 52.6% |
Uncovered Elements: 9 (19) |
Complexity: 8 |
Complexity Density: 0.53 |
|
87 |
3
|
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 |
|
|
112 |
3
|
if (finderFactory == null) { |
113 |
3
|
finderFactory = new ProofFinderFactoryImpl(); |
114 |
|
} |
115 |
3
|
noSave = parameters.getBoolean("noSave"); |
116 |
3
|
this.parameters = parameters; |
117 |
|
} |
118 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
119 |
3
|
private Plugin getPlugin() {... |
120 |
3
|
return (Plugin) getService(); |
121 |
|
} |
122 |
|
|
|
|
| 72.7% |
Uncovered Elements: 3 (11) |
Complexity: 2 |
Complexity Density: 0.18 |
|
123 |
3
|
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 |
|
|
|
|
| 66.7% |
Uncovered Elements: 2 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
141 |
14
|
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 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
150 |
14
|
public void visitLeave(final Axiom axiom) {... |
151 |
14
|
setBlocked(false); |
152 |
|
} |
153 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
154 |
0
|
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 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
164 |
0
|
public void visitLeave(final PredicateDefinition definition) {... |
165 |
0
|
setBlocked(false); |
166 |
|
} |
167 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
168 |
0
|
public void visitEnter(final InitialPredicateDefinition definition)... |
169 |
|
throws ModuleDataException { |
170 |
0
|
setBlocked(true); |
171 |
|
} |
172 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
173 |
0
|
public void visitLeave(final InitialPredicateDefinition definition) {... |
174 |
0
|
setBlocked(false); |
175 |
|
} |
176 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
177 |
0
|
public void visitEnter(final InitialFunctionDefinition definition)... |
178 |
|
throws ModuleDataException { |
179 |
0
|
setBlocked(true); |
180 |
|
} |
181 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
182 |
0
|
public void visitLeave(final InitialFunctionDefinition definition) {... |
183 |
0
|
setBlocked(false); |
184 |
|
} |
185 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
186 |
0
|
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 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
196 |
0
|
public void visitLeave(final FunctionDefinition definition) {... |
197 |
0
|
setBlocked(false); |
198 |
|
} |
199 |
|
|
|
|
| 56% |
Uncovered Elements: 22 (50) |
Complexity: 11 |
Complexity Density: 0.28 |
|
200 |
13
|
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 |
|
|
211 |
6
|
try { |
212 |
6
|
finder = finderFactory.createProofFinder(); |
213 |
6
|
finder.findProof(proposition.getFormula().getElement(), validFormulas, |
214 |
|
getCurrentContext(), parameters, new ModuleLogListener() { |
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
215 |
181
|
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; |
225 |
|
} |
226 |
6
|
if (proof != null) { |
227 |
6
|
QedeqLog.getInstance().logMessage("proof found for " |
228 |
|
+ super.getLocationDescription()); |
229 |
|
|
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 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
276 |
13
|
public void visitLeave(final Proposition definition) {... |
277 |
13
|
setBlocked(false); |
278 |
|
} |
279 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
280 |
24
|
public void visitEnter(final Rule rule) throws ModuleDataException {... |
281 |
24
|
if (rule == null) { |
282 |
0
|
return; |
283 |
|
} |
284 |
24
|
setBlocked(true); |
285 |
|
} |
286 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
287 |
24
|
public void visitLeave(final Rule rule) {... |
288 |
24
|
setBlocked(false); |
289 |
|
} |
290 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
291 |
0
|
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 |
|
} |