Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../img/srcFileCovDistChart7.png 74% of files have more coverage
315   1,041   129   6.3
138   556   0.41   50
50     2.58  
1    
 
  StateManager       Line # 46 315 129 70.2% 0.70178926
 
  (102)
 
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.control;
17   
18    import java.util.ArrayList;
19    import java.util.List;
20   
21    import org.qedeq.base.trace.Trace;
22    import org.qedeq.base.utility.StringUtility;
23    import org.qedeq.kernel.bo.log.ModuleEventLog;
24    import org.qedeq.kernel.bo.module.InternalPluginBo;
25    import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
26    import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
27    import org.qedeq.kernel.bo.module.ModuleLabels;
28    import org.qedeq.kernel.se.common.ModuleDataException;
29    import org.qedeq.kernel.se.common.Plugin;
30    import org.qedeq.kernel.se.common.SourceFileExceptionList;
31    import org.qedeq.kernel.se.dto.module.QedeqVo;
32    import org.qedeq.kernel.se.state.AbstractState;
33    import org.qedeq.kernel.se.state.DependencyState;
34    import org.qedeq.kernel.se.state.FormallyProvedState;
35    import org.qedeq.kernel.se.state.LoadingImportsState;
36    import org.qedeq.kernel.se.state.LoadingState;
37    import org.qedeq.kernel.se.state.WellFormedState;
38   
39   
40    /**
41    * Changes the states of {@link org.qedeq.kernel.bo.service.control.DefaultKernelQedeqBo}s.
42    * All state changing is done here.
43    *
44    * @author Michael Meyling
45    */
 
46    public class StateManager {
47   
48    /** This class. */
49    private static final Class CLASS = StateManager.class;
50   
51    /** Main BO to care about. */
52    private final DefaultKernelQedeqBo bo;
53   
54    /** Completeness during loading from web. */
55    private int loadingCompleteness;
56   
57    /** Describes QEDEQ module loading state. */
58    private LoadingState loadingState;
59   
60    /** Describes QEDEQ module loading imports state. */
61    private LoadingImportsState loadingImportsState;
62   
63    /** Describes QEDEQ module dependency state. */
64    private DependencyState dependencyState;
65   
66    /** Describes QEDEQ module well formed state. */
67    private WellFormedState wellFormedState;
68   
69    /** Describes QEDEQ module formally proved state. */
70    private FormallyProvedState formallyProvedState;
71   
72    /** Holds QEDEQ module plugin results. */
73    private PluginResultManager pluginResults;
74   
75    /** Failure exceptions for basic operations. */
76    private SourceFileExceptionList errors;
77   
 
78  609 toggle StateManager(final DefaultKernelQedeqBo bo) {
79  609 this.bo = bo;
80  609 loadingState = LoadingState.STATE_UNDEFINED;
81  609 loadingCompleteness = 0;
82  609 loadingImportsState = LoadingImportsState.STATE_UNDEFINED;
83  609 dependencyState = DependencyState.STATE_UNDEFINED;
84  609 wellFormedState = WellFormedState.STATE_UNCHECKED;
85  609 formallyProvedState = FormallyProvedState.STATE_UNCHECKED;
86  609 pluginResults = new PluginResultManager();
87    }
88   
89    /**
90    * Delete QEDEQ module. Invalidates all dependent modules.
91    */
 
92  603 toggle public void delete() {
93  603 checkIfDeleted();
94  603 invalidateOtherDependentModulesToLoaded();
95  603 setLoadingState(LoadingState.STATE_DELETED);
96  603 bo.setQedeqVo(null);
97  603 bo.getKernelRequiredModules().clear();
98  603 bo.getDependentModules().clear();
99  603 bo.setLabels(null);
100  603 setDependencyState(DependencyState.STATE_UNDEFINED);
101  603 setWellFormedState(WellFormedState.STATE_UNCHECKED);
102  603 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
103  603 setErrors(null);
104  603 ModuleEventLog.getInstance().removeModule(bo);
105    }
106   
107    /**
108    * Is the module in a failure state? That is the case if loading of module or imported modules
109    * failed or the logical check failed. Possible plugin failures don't matter.
110    *
111    * @return Failure during loading or logical check occurred.
112    */
 
113  798 toggle public boolean hasBasicFailures() {
114  798 return loadingState.isFailure() || dependencyState.isFailure()
115    || wellFormedState.isFailure() || formallyProvedState.isFailure();
116    }
117   
118    /**
119    * Has the module any errors? This includes loading, importing, logical and plugin errors.
120    *
121    * @return Errors occurred.
122    */
 
123  420 toggle public boolean hasErrors() {
124  420 return hasBasicFailures() || (getErrors() != null && getErrors().size() > 0);
125    }
126   
127    /**
128    * Has the module any warnings? This includes loading, importing, logical and plugin warnings.
129    *
130    * @return Warnings occurred.
131    */
 
132  58 toggle public boolean hasWarnings() {
133  58 return (getWarnings() != null && getWarnings().size() > 0);
134    }
135   
136    /**
137    * Set completeness percentage.
138    *
139    * @param completeness Completeness of loading into memory.
140    */
 
141  0 toggle public void setLoadingCompleteness(final int completeness) {
142  0 this.loadingCompleteness = completeness;
143    }
144   
145    /**
146    * Get loading completeness percentage.
147    *
148    * @return Completeness as percent number.
149    */
 
150  0 toggle public int getLoadingCompleteness() {
151  0 return this.loadingCompleteness;
152    }
153   
154    /**
155    * Get loading state.
156    *
157    * @return Loading state.
158    */
 
159  5675 toggle public LoadingState getLoadingState() {
160  5675 return this.loadingState;
161    }
162   
163    /**
164    * Is the module loaded?
165    *
166    * @return Is the module loaded?
167    */
 
168  9011 toggle public boolean isLoaded() {
169  9011 return loadingState == LoadingState.STATE_LOADED;
170    }
171   
172    /**
173    * Set loading progress module state.
174    *
175    * @param state Module loading state. Must not be <code>null</code>.
176    * @throws IllegalStateException State is a failure state or module loaded state.
177    */
 
178  1178 toggle public void setLoadingProgressState(final LoadingState state) {
179  1178 checkIfDeleted();
180  1178 if (state == LoadingState.STATE_LOADED) {
181  1 throw new IllegalArgumentException(
182    "this state could only be set by calling method setLoaded");
183    }
184  1176 if (state != LoadingState.STATE_DELETED && state.isFailure()) {
185  3 throw new IllegalArgumentException(
186    "this is a failure state, call setLoadingFailureState for " + state);
187    }
188    // if module has no loading state we give him one before creating an event
189  1173 if (getLoadingState() == LoadingState.STATE_UNDEFINED) {
190  594 setLoadingState(state);
191  594 ModuleEventLog.getInstance().addModule(bo);
192    }
193  1173 if (state == LoadingState.STATE_DELETED) {
194  0 throw new IllegalArgumentException(
195    "call delete for " + state);
196    }
197  1173 setLoadingState(state);
198  1173 bo.setQedeqVo(null);
199  1173 bo.getKernelRequiredModules().clear();
200  1173 bo.getDependentModules().clear();
201  1173 bo.setLabels(null);
202  1173 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
203  1173 setDependencyState(DependencyState.STATE_UNDEFINED);
204  1173 setWellFormedState(WellFormedState.STATE_UNCHECKED);
205  1173 setErrors(null);
206  1173 ModuleEventLog.getInstance().stateChanged(bo);
207    }
208   
209    /**
210    * Set failure module state.
211    *
212    * @param state Module loading state. Must not be <code>null</code>.
213    * @param e Exception that occurred during loading. Must not be <code>null</code>.
214    * @throws IllegalArgumentException <code>state</code> is no failure state
215    */
 
216  62 toggle public void setLoadingFailureState(final LoadingState state,
217    final SourceFileExceptionList e) {
218  62 if (e == null) {
219  1 throw new NullPointerException("Exception must not be null");
220    }
221  61 checkIfDeleted();
222  59 if (!state.isFailure()) {
223  6 throw new IllegalArgumentException(
224    "this is no failure state, call setLoadingProgressState");
225    }
226    // if module has no loading state we give him one before creating an event
227  53 if (getLoadingState() == LoadingState.STATE_UNDEFINED) {
228  3 setLoadingState(state);
229  3 ModuleEventLog.getInstance().addModule(bo);
230    }
231  53 bo.setQedeqVo(null);
232  53 bo.getKernelRequiredModules().clear();
233  53 bo.getDependentModules().clear();
234  53 bo.setLabels(null);
235  53 setLoadingState(state);
236  53 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
237  53 setDependencyState(DependencyState.STATE_UNDEFINED);
238  53 setWellFormedState(WellFormedState.STATE_UNCHECKED);
239  53 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
240  53 setErrors(e);
241  53 ModuleEventLog.getInstance().stateChanged(bo);
242    }
243   
244    /**
245    * Set loading state to "loaded". Also puts <code>null</code> to
246    * {@link DefaultKernelQedeqBo#getLabels()}.
247    *
248    * @param qedeq This module was loaded. Must not be <code>null</code>.
249    * @param labels Module labels.
250    * @throws NullPointerException One argument was <code>null</code>.
251    */
 
252  583 toggle public void setLoaded(final QedeqVo qedeq, final ModuleLabels labels) {
253  583 checkIfDeleted();
254  583 if (qedeq == null) {
255  0 throw new NullPointerException("Qedeq is null");
256    }
257  583 setLoadingState(LoadingState.STATE_LOADED);
258  583 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
259  583 setDependencyState(DependencyState.STATE_UNDEFINED);
260  583 setWellFormedState(WellFormedState.STATE_UNCHECKED);
261  583 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
262  583 setErrors(null);
263  583 bo.setQedeqVo(qedeq);
264  583 bo.getKernelRequiredModules().clear();
265  583 bo.getDependentModules().clear();
266  583 bo.setLabels(labels);
267  583 ModuleEventLog.getInstance().stateChanged(bo);
268    }
269   
270    /**
271    * Set loading imports progress module state.
272    *
273    * @param state Module state. Must not be <code>null</code>.
274    * @throws IllegalStateException Module is not yet loaded.
275    * @throws IllegalArgumentException <code>state</code> is failure state or loaded required
276    * state.
277    * @throws NullPointerException <code>state</code> is <code>null</code>.
278    */
 
279  0 toggle public void setLoadingImportsProgressState(final LoadingImportsState state) {
280  0 checkIfDeleted();
281  0 if (!isLoaded() && state != LoadingImportsState.STATE_UNDEFINED) {
282  0 throw new IllegalStateException("module is not yet loaded");
283    }
284  0 if (state.isFailure()) {
285  0 throw new IllegalArgumentException(
286    "this is a failure state, call setLoadingImportsFailureState");
287    }
288  0 if (state == LoadingImportsState.STATE_LOADED_IMPORTED_MODULES) {
289  0 throw new IllegalArgumentException(
290    "this state could only be set by calling method setLoadedImports");
291    }
292  0 ModuleEventLog.getInstance().stateChanged(bo);
293    }
294   
295    /**
296    * Set failure module state.
297    *
298    * @param state Module loading imports state. Must not be <code>null</code>.
299    * @param e Exception that occurred during loading. Must not be <code>null</code>.
300    * @throws IllegalStateException Module is not yet loaded.
301    * @throws IllegalArgumentException <code>state</code> is no failure state.
302    * @throws NullPointerException <code>state</code> is <code>null</code>.
303    */
 
304  1 toggle public void setLoadingImportsFailureState(final LoadingImportsState state,
305    final SourceFileExceptionList e) {
306  1 if (e == null) {
307  0 throw new NullPointerException("Exception must not be null");
308    }
309  1 checkIfDeleted();
310  1 if (!isLoaded()) {
311  0 throw new IllegalStateException("module is not yet loaded");
312    }
313  1 if (!state.isFailure()) {
314  0 throw new IllegalArgumentException(
315    "this is no failure state, call setLoadingProgressState");
316    }
317  1 setLoadingImportsState(state);
318  1 setErrors(e);
319  1 ModuleEventLog.getInstance().stateChanged(bo);
320    }
321   
322    /**
323    * Get loading imports state.
324    *
325    * @return Dependency state.
326    */
 
327  0 toggle public LoadingImportsState getLoadingImportsState() {
328  0 return this.loadingImportsState;
329    }
330   
331    /**
332    * Is the module loaded?
333    *
334    * @return Is the module loaded?
335    */
 
336  1436 toggle public boolean hasLoadedImports() {
337  1436 return loadingImportsState == LoadingImportsState.STATE_LOADED_IMPORTED_MODULES;
338    }
339   
340    /**
341    * Set dependency progress module state.
342    *
343    * @param state Module state. Must not be <code>null</code>.
344    * @throws IllegalStateException Module is not yet loaded.
345    * @throws IllegalArgumentException <code>state</code> is failure state or loaded required
346    * state.
347    * @throws NullPointerException <code>state</code> is <code>null</code>.
348    */
 
349  378 toggle public void setDependencyProgressState(final DependencyState state) {
350  378 checkIfDeleted();
351  378 if (!isLoaded() && state != DependencyState.STATE_UNDEFINED) {
352  0 throw new IllegalStateException("module is not yet loaded");
353    }
354  378 if (state.isFailure()) {
355  0 throw new IllegalArgumentException(
356    "this is a failure state, call setDependencyFailureState");
357    }
358  378 if (state == DependencyState.STATE_LOADED_REQUIRED_MODULES) {
359  0 throw new IllegalArgumentException(
360    "this state could only be set by calling method setLoadedRequiredModules");
361    }
362  378 setWellFormedState(WellFormedState.STATE_UNCHECKED);
363  378 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
364  378 setDependencyState(state);
365  378 setErrors(null);
366  378 ModuleEventLog.getInstance().stateChanged(bo);
367    }
368   
369    /**
370    * Set failure module state.
371    *
372    * @param state Module dependency state. Must not be <code>null</code>.
373    * @param e Exception that occurred during loading. Must not be <code>null</code>.
374    * @throws IllegalStateException Module is not yet loaded.
375    * @throws IllegalArgumentException <code>state</code> is no failure state.
376    * @throws NullPointerException <code>state</code> is <code>null</code>.
377    */
 
378  62 toggle public void setDependencyFailureState(final DependencyState state,
379    final SourceFileExceptionList e) {
380  62 if (e == null) {
381  1 throw new NullPointerException("Exception must not be null");
382    }
383  61 checkIfDeleted();
384  61 if (!isLoaded()) {
385  2 throw new IllegalStateException("module is not yet loaded");
386    }
387  59 if (!state.isFailure()) {
388  4 throw new IllegalArgumentException(
389    "this is no failure state, call setLoadingProgressState");
390    }
391  55 setDependencyState(state);
392  55 setErrors(e);
393  55 ModuleEventLog.getInstance().stateChanged(bo);
394    }
395   
396    /**
397    * Get dependency state.
398    *
399    * @return Dependency state.
400    */
 
401  1023 toggle public DependencyState getDependencyState() {
402  1023 return this.dependencyState;
403    }
404   
405    /**
406    * Reset all (recursive) dependent modules (if any) to state loaded.
407    */
 
408  721 toggle private void invalidateOtherDependentModulesToLoaded() {
409  721 final String method = "invalidateOtherDependModulesToLoaded";
410  721 Trace.begin(CLASS, this, method);
411  721 Trace.param(CLASS, this, method, "bo", bo);
412  721 if (hasLoadedRequiredModules()) {
413  319 final KernelModuleReferenceList dependent = bo.getDependentModules();
414  319 Trace.trace(CLASS, this, method, "begin list of dependent modules");
415    // remember dependent modules
416  319 final List list = new ArrayList();
417  459 for (int i = 0; i < dependent.size(); i++) {
418  140 Trace.param(CLASS, this, method, "" + i, dependent.getKernelQedeqBo(i));
419  140 list.add(dependent.getKernelQedeqBo(i));
420    }
421  319 Trace.trace(CLASS, this, method, "end list of dependent modules");
422  459 for (int i = 0; i < list.size(); i++) {
423  140 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) list.get(i);
424    // work on it, if still in list of dependent modules
425  140 if (dependent.contains(ref)) {
426  118 ref.getStateManager().invalidateDependentModulesToLoaded();
427    }
428    }
429  319 list.clear();
430  319 dependent.clear();
431   
432  319 final KernelModuleReferenceList required = bo.getKernelRequiredModules();
433  506 for (int i = 0; i < required.size(); i++) {
434  187 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) required.getKernelQedeqBo(i);
435  187 Trace.param(CLASS, this, method, "remove dependence from", ref);
436  187 ref.getDependentModules().remove(bo);
437    }
438  319 required.clear();
439  319 bo.getLabels().resetNodesToWellFormedUnchecked();
440    }
441  721 Trace.end(CLASS, this, method);
442    }
443   
444    /**
445    * Reset this and all (recursive) dependent modules (if any) to state loaded.
446    */
 
447  118 toggle private void invalidateDependentModulesToLoaded() {
448  118 final String method = "invalidateDependentModulesToLoaded";
449  118 Trace.begin(CLASS, this, method);
450  118 Trace.param(CLASS, this, method, "bo", bo);
451  118 if (hasLoadedRequiredModules()) {
452  118 invalidateOtherDependentModulesToLoaded();
453  118 invalidateThisModuleToLoaded();
454  118 setLoadingState(LoadingState.STATE_LOADED);
455  118 ModuleEventLog.getInstance().stateChanged(bo);
456    }
457  118 Trace.end(CLASS, this, method);
458    }
459   
460    // /**
461    // * Reset this and all (recursive) dependent modules (if any) to state loaded.
462    // */
463    // private void invalidateDependentModulesToLoadedImports() {
464    // final String method = "invalidateDependentModulesToLoadedImports";
465    // Trace.begin(CLASS, this, method);
466    // Trace.param(CLASS, this, method, "bo", bo);
467    // if (hasLoadedImports()) {
468    // final KernelModuleReferenceList dependent = bo.getDependentModules();
469    // Trace.trace(CLASS, this, method, "begin list of dependent modules");
470    // // remember dependent modules
471    // final List list = new ArrayList();
472    // for (int i = 0; i < dependent.size(); i++) {
473    // Trace.param(CLASS, this, method, "" + i, dependent.getKernelQedeqBo(i));
474    // list.add(dependent.getKernelQedeqBo(i));
475    // }
476    // Trace.trace(CLASS, this, method, "end list of dependent modules");
477    // for (int i = 0; i < list.size(); i++) {
478    // DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) list.get(i);
479    // // work on it, if still in list of dependent modules
480    // if (dependent.contains(ref)) {
481    // ref.getStateManager().invalidateDependentModulesToLoadedImports();
482    // }
483    // }
484    // list.clear();
485    //
486    // invalidateThisModuleToLoadedImports();
487    // ModuleEventLog.getInstance().stateChanged(bo);
488    // }
489    // Trace.end(CLASS, this, method);
490    // }
491    //
492    // /**
493    // * Reset all (recursive) dependent modules (if any) to state loaded required.
494    // */
495    // private void invalidateOtherDependentModulesToLoadedRequired() {
496    // if (isWellFormed()) {
497    // final KernelModuleReferenceList dependent = bo.getDependentModules();
498    // for (int i = 0; i < dependent.size(); i++) {
499    // DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
500    // ref.getStateManager().invalidateDependentModulesToLoadedRequired();
501    // }
502    // }
503    // }
504    //
505    // /**
506    // * Reset this and all (recursive) dependent modules (if any) to state loaded required.
507    // */
508    // private void invalidateDependentModulesToLoadedRequired() {
509    // if (isWellFormed()) {
510    // final KernelModuleReferenceList dependent = bo.getDependentModules();
511    // for (int i = 0; i < dependent.size(); i++) {
512    // DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
513    // ref.getStateManager().invalidateDependentModulesToLoadedRequired();
514    // }
515    // invalidateThisModuleToLoadedReqired();
516    // ModuleEventLog.getInstance().stateChanged(bo);
517    // }
518    // }
519    //
520    // /**
521    // * Reset all (recursive) dependent modules (if any) to state well formed.
522    // */
523    // private void invalidateOtherDependentModulesToWellFormed() {
524    // if (isFullyFormallyProved()) {
525    // final KernelModuleReferenceList dependent = bo.getDependentModules();
526    // for (int i = 0; i < dependent.size(); i++) {
527    // DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
528    // ref.getStateManager().invalidateDependentModulesToWellFormed();
529    // }
530    // }
531    // }
532    //
533    // /**
534    // * Reset this and all (recursive) dependent modules (if any) to state well formed.
535    // */
536    // private void invalidateDependentModulesToWellFormed() {
537    // if (isFullyFormallyProved()) {
538    // final KernelModuleReferenceList dependent = bo.getDependentModules();
539    // for (int i = 0; i < dependent.size(); i++) {
540    // DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
541    // ref.getStateManager().invalidateDependentModulesToWellFormed();
542    // }
543    // invalidateThisModuleToWellFormed();
544    // ModuleEventLog.getInstance().stateChanged(bo);
545    // }
546    // }
547   
 
548  118 toggle private void invalidateThisModuleToLoaded() {
549  118 if (isLoaded()) {
550  118 setLoadingState(LoadingState.STATE_LOADED);
551  118 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
552  118 setDependencyState(DependencyState.STATE_UNDEFINED);
553  118 setWellFormedState(WellFormedState.STATE_UNCHECKED);
554  118 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
555  118 bo.getKernelRequiredModules().clear();
556  118 setErrors(null);
557    }
558    }
559   
560    // private void invalidateThisModuleToLoadedImports() {
561    // if (hasLoadedImports()) {
562    // setLoadingImportsState(LoadingImportsState.STATE_LOADED_IMPORTED_MODULES);
563    // setDependencyState(DependencyState.STATE_UNDEFINED);
564    // setWellFormedState(WellFormedState.STATE_UNCHECKED);
565    // setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
566    // setErrors(null);
567    // }
568    // }
569    //
570    // private void invalidateThisModuleToLoadedReqired() {
571    // if (hasLoadedRequiredModules()) {
572    // setDependencyState(DependencyState.STATE_LOADED_REQUIRED_MODULES);
573    // setWellFormedState(WellFormedState.STATE_UNCHECKED);
574    // setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
575    // setErrors(null);
576    // }
577    // }
578    //
579    // private void invalidateThisModuleToWellFormed() {
580    // if (isWellFormed()) {
581    // setWellFormedState(WellFormedState.STATE_CHECKED);
582    // setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
583    // setErrors(null);
584    // }
585    // }
586    //
587    // private void invalidateThisModuleToFormallyProved() {
588    // if (isFullyFormallyProved()) {
589    // setFormallyProvedState(FormallyProvedState.STATE_CHECKED);
590    // setErrors(null);
591    // }
592    // }
593   
594    /**
595    * Are all required modules loaded?
596    *
597    * @return All required modules are loaded?
598    */
 
599  5930 toggle public boolean hasLoadedRequiredModules() {
600  5930 return isLoaded() && dependencyState == DependencyState.STATE_LOADED_REQUIRED_MODULES;
601    }
602   
603    /**
604    * Set loaded imports state.
605    *
606    * @param required URLs of all referenced modules. Must not be <code>null</code>.
607    * @throws IllegalStateException Module is not yet loaded.
608    */
 
609  353 toggle public void setLoadedImports(final KernelModuleReferenceList required) {
610  353 checkIfDeleted();
611  353 if (!isLoaded()) {
612  0 throw new IllegalStateException(
613    "Loaded imported modules can only be set if module is loaded."
614    + "\"\nCurrently the status for the module"
615    + "\"" + bo.getName() + "\" is \"" + bo.getLoadingState() + "\"");
616    }
617  353 setLoadingImportsState(LoadingImportsState.STATE_LOADED_IMPORTED_MODULES);
618  353 setDependencyState(DependencyState.STATE_UNDEFINED);
619  353 setWellFormedState(WellFormedState.STATE_UNCHECKED);
620  353 setErrors(null);
621  353 bo.getKernelRequiredModules().set(required);
622  353 ModuleEventLog.getInstance().stateChanged(bo);
623    }
624   
625    /**
626    * Set loaded required requirements state.
627    *
628    * @throws IllegalStateException Module is not yet loaded.
629    */
 
630  331 toggle public void setLoadedRequiredModules() {
631  331 checkIfDeleted();
632  331 if (!isLoaded()) {
633  0 throw new IllegalStateException(
634    "Required modules can only be set if module is loaded."
635    + "\"\nCurrently the status for the module"
636    + "\"" + bo.getName() + "\" is \"" + bo.getLoadingState() + "\"");
637    }
638  331 KernelModuleReferenceList required = bo.getKernelRequiredModules();
639  524 for (int i = 0; i < required.size(); i++) {
640  193 DefaultKernelQedeqBo current = (DefaultKernelQedeqBo) required.getKernelQedeqBo(i);
641  193 try {
642  193 current.getDependentModules().add(required.getModuleContext(i),
643    required.getLabel(i), bo);
644    } catch (ModuleDataException me) { // should never happen
645  0 throw new RuntimeException(me);
646    }
647    }
648  331 setDependencyState(DependencyState.STATE_LOADED_REQUIRED_MODULES);
649  331 setWellFormedState(WellFormedState.STATE_UNCHECKED);
650  331 setErrors(null);
651  331 ModuleEventLog.getInstance().stateChanged(bo);
652    }
653   
654    /**
655    * Set logic checked state. Also set the predicate and function existence checker.
656    *
657    * @param checker Checks if a predicate or function constant is defined.
658    */
 
659  279 toggle public void setWellFormed(final ModuleConstantsExistenceChecker checker) {
660  279 checkIfDeleted();
661  279 if (!hasLoadedRequiredModules()) {
662  0 throw new IllegalStateException(
663    "Checked can only be set if all required modules are loaded."
664    + "\"\nCurrently the status for the module"
665    + "\"" + bo.getName() + "\" is \"" + bo.getLoadingState() + "\"");
666    }
667  279 setWellFormedState(WellFormedState.STATE_CHECKED);
668  279 bo.setExistenceChecker(checker);
669  279 ModuleEventLog.getInstance().stateChanged(bo);
670    }
671   
672    /**
673    * Set checking for well formed progress module state. Must not be <code>null</code>.
674    *
675    * @param state module state
676    */
 
677  616 toggle public void setWellFormedProgressState(final WellFormedState state) {
678  616 if (getDependencyState().getCode()
679    < DependencyState.STATE_LOADED_REQUIRED_MODULES.getCode()
680    && state != WellFormedState.STATE_UNCHECKED) {
681  0 throw new IllegalArgumentException(
682    "this state could only be set if all required modules are loaded ");
683    }
684  616 if (state.isFailure()) {
685  0 throw new IllegalArgumentException(
686    "this is a failure state, call setWellFormedFailureState");
687    }
688  616 if (state == WellFormedState.STATE_CHECKED) {
689  0 throw new IllegalArgumentException(
690    "set with setChecked(ExistenceChecker)");
691    }
692  616 setWellFormedState(state);
693  616 setErrors(null);
694  616 ModuleEventLog.getInstance().stateChanged(bo);
695    }
696   
697    /**
698    * Set failure module state.
699    *
700    * @param state module state
701    * @param e Exception that occurred during loading.
702    * @throws IllegalArgumentException <code>state</code> is no failure state
703    */
 
704  34 toggle public void setWellFormedFailureState(final WellFormedState state,
705    final SourceFileExceptionList e) {
706  34 if ((!isLoaded() || !hasLoadedRequiredModules())
707    && state != WellFormedState.STATE_UNCHECKED) {
708  0 throw new IllegalArgumentException(
709    "this state could only be set if all required modules are loaded ");
710    }
711  34 if (!state.isFailure()) {
712  0 throw new IllegalArgumentException(
713    "this is no failure state, call setWellFormedProgressState");
714    }
715  34 setWellFormedState(state);
716  34 setErrors(e);
717  34 ModuleEventLog.getInstance().stateChanged(bo);
718    }
719   
720    /**
721    * Set checking for formally proved progress module state. Must not be <code>null</code>.
722    *
723    * @param state module state
724    */
 
725  25 toggle public void setFormallyProvedProgressState(final FormallyProvedState state) {
726  25 if (getDependencyState().getCode()
727    < DependencyState.STATE_LOADED_REQUIRED_MODULES.getCode()
728    && state != FormallyProvedState.STATE_UNCHECKED) {
729  0 throw new IllegalArgumentException(
730    "this state could only be set if all required modules are loaded ");
731    }
732  25 if (state.isFailure()) {
733  0 throw new IllegalArgumentException(
734    "this is a failure state, call setFormallyProvedFailureState");
735    }
736    // if (state == FormallyProvedState.STATE_CHECKED) {
737    // // FIXME 20130220 m31: do we need something simular?
738    // throw new IllegalArgumentException(
739    // "set with setChecked(ExistenceChecker)");
740    // }
741  25 setFormallyProvedState(state);
742  25 setErrors(null);
743  25 ModuleEventLog.getInstance().stateChanged(bo);
744    }
745   
746    /**
747    * Set failure module state.
748    *
749    * @param state module state
750    * @param e Exception that occurred during loading.
751    * @throws IllegalArgumentException <code>state</code> is no failure state
752    */
 
753  5 toggle public void setFormallyProvedFailureState(final FormallyProvedState state,
754    final SourceFileExceptionList e) {
755  5 if ((!isLoaded() || !hasLoadedRequiredModules())
756    && state != FormallyProvedState.STATE_UNCHECKED) {
757  0 throw new IllegalArgumentException(
758    "this state could only be set if all required modules are well formed ");
759    }
760  5 if (!state.isFailure()) {
761  0 throw new IllegalArgumentException(
762    "this is no failure state, call setFormallyProvedProgressState");
763    }
764  5 setFormallyProvedState(state);
765  5 setErrors(e);
766  5 ModuleEventLog.getInstance().stateChanged(bo);
767    }
768   
769    /**
770    * Checks if the current instance is already deleted.
771    *
772    * @throws IllegalStateException Module is already deleted.
773    */
 
774  3828 toggle private void checkIfDeleted() {
775  3828 if (getLoadingState() == LoadingState.STATE_DELETED) {
776  0 throw new IllegalStateException("module is already deleted: " + bo.getUrl());
777    }
778    }
779   
780    /**
781    * Was the module successfully checked for well formedness errors?
782    *
783    * @return Successfully checked for being well formed?
784    */
 
785  1380 toggle public boolean isWellFormed() {
786  1380 return hasLoadedRequiredModules() && wellFormedState == WellFormedState.STATE_CHECKED;
787    }
788   
789    /**
790    * Get the well formed state.
791    *
792    * @return Well formed state.
793    */
 
794  8 toggle public WellFormedState getWellFormedState() {
795  8 return this.wellFormedState;
796    }
797   
798    /**
799    * Was the module successfully checked having formally correct proofs?
800    *
801    * @return Successfully checked for having formally correct proofs?
802    */
 
803  51 toggle public boolean isFullyFormallyProved() {
804  51 return isWellFormed() && formallyProvedState == FormallyProvedState.STATE_CHECKED;
805    }
806   
807    /**
808    * Get the formally proved state.
809    *
810    * @return Formally proved state.
811    */
 
812  0 toggle public FormallyProvedState getFormallyProvedState() {
813  0 return this.formallyProvedState;
814    }
815   
816    /**
817    * Get a description of the current state the module is in.
818    *
819    * @return Textual representation of module state.
820    */
 
821  57 toggle public String getStateDescription() {
822  57 String result = "";
823  57 if (loadingState == LoadingState.STATE_LOADING_FROM_WEB) {
824  0 result = loadingState.getText() + " (" + loadingCompleteness + "%)";
825  57 } else if (!isLoaded()) {
826  6 result = loadingState.getText();
827  51 } else if (!hasLoadedImports()) {
828  3 if (loadingImportsState == LoadingImportsState.STATE_UNDEFINED) {
829  3 result = loadingState.getText();
830    } else {
831  0 result = loadingImportsState.getText();
832    }
833  48 } else if (!hasLoadedRequiredModules()) {
834  6 if (dependencyState == DependencyState.STATE_UNDEFINED) {
835  3 result = loadingImportsState.getText();
836    } else {
837  3 result = dependencyState.getText();
838    }
839  42 } else if (!isWellFormed()) {
840  18 if (wellFormedState == WellFormedState.STATE_UNCHECKED) {
841  6 result = dependencyState.getText();
842    } else {
843  12 result = wellFormedState.getText();
844    }
845  24 } else if (!isFullyFormallyProved()) {
846  21 if (formallyProvedState == FormallyProvedState.STATE_UNCHECKED) {
847  3 result = wellFormedState.getText();
848    } else {
849  18 result = formallyProvedState.getText();
850    }
851    } else {
852  3 result = formallyProvedState.getText();
853    }
854  57 final String pluginState = pluginResults.getPluginStateDescription();
855  57 if (pluginState.length() > 0) {
856  3 result += "; " + pluginState;
857    }
858  57 return result;
859    }
860   
861    /**
862    * Get the current state of associate module.
863    *
864    * @return Current module state.
865    */
 
866  0 toggle public AbstractState getCurrentState() {
867  0 if (!isLoaded()) {
868  0 return loadingState;
869  0 } else if (!hasLoadedImports()) {
870  0 if (loadingImportsState == LoadingImportsState.STATE_UNDEFINED) {
871  0 return loadingState;
872    }
873  0 return loadingImportsState;
874  0 } else if (!hasLoadedRequiredModules()) {
875  0 if (dependencyState == DependencyState.STATE_UNDEFINED) {
876  0 return loadingImportsState;
877    }
878  0 return dependencyState;
879  0 } else if (!isWellFormed()) {
880  0 if (wellFormedState == WellFormedState.STATE_UNCHECKED) {
881  0 return dependencyState;
882    }
883  0 return wellFormedState;
884  0 } else if (!isFullyFormallyProved()) {
885  0 if (formallyProvedState == FormallyProvedState.STATE_UNCHECKED) {
886  0 return wellFormedState;
887    }
888  0 return formallyProvedState;
889    } else {
890  0 return formallyProvedState;
891    }
892    }
893   
894    /**
895    * Get the last successful state we were in.
896    * As there are: undefined, loaded, loaded required, fully formally proved.
897    *
898    * @return Previous major error free state.
899    */
 
900  0 toggle public AbstractState getLastSuccesfulState() {
901  0 if (!isLoaded()) {
902  0 return LoadingState.STATE_UNDEFINED;
903  0 } else if (!hasLoadedImports()) {
904  0 return LoadingState.STATE_LOADED;
905  0 } else if (!hasLoadedRequiredModules()) {
906  0 return LoadingImportsState.STATE_LOADED_IMPORTED_MODULES;
907  0 } else if (!isWellFormed()) {
908  0 return DependencyState.STATE_LOADED_REQUIRED_MODULES;
909  0 } else if (!isFullyFormallyProved()) {
910  0 return WellFormedState.STATE_CHECKED;
911    } else {
912  0 return FormallyProvedState.STATE_CHECKED;
913    }
914    }
915   
916    /**
917    * Set {@link LoadingState}. Doesn't do any status handling. Only for internal use.
918    *
919    * @param state Set this loading state.
920    */
 
921  3245 toggle protected void setLoadingState(final LoadingState state) {
922  3245 this.loadingState = state;
923    }
924   
925    /**
926    * Set {@link LoadingImportsState}. Doesn't do any status handling. Only for internal use.
927    *
928    * @param state Set this loading state.
929    */
 
930  2281 toggle protected void setLoadingImportsState(final LoadingImportsState state) {
931  2281 this.loadingImportsState = state;
932    }
933   
934    /**
935    * Set {@link DependencyState}. Doesn't do any status handling. Only for internal use.
936    *
937    * @param state Set this dependency state.
938    */
 
939  3647 toggle protected void setDependencyState(final DependencyState state) {
940  3647 this.dependencyState = state;
941    }
942   
943    /**
944    * Set {@link WellFormedState}. Doesn't do any status handling. Only for internal use.
945    *
946    * @param state Set this logical state.
947    */
 
948  4527 toggle protected void setWellFormedState(final WellFormedState state) {
949  4527 this.wellFormedState = state;
950    }
951   
952    /**
953    * Set {@link FormallyProvedState}. Doesn't do any status handling. Only for internal use.
954    *
955    * @param state Set this logical state.
956    */
 
957  1765 toggle protected void setFormallyProvedState(final FormallyProvedState state) {
958  1765 this.formallyProvedState = state;
959    }
960   
961    /**
962    * Get all errors.
963    *
964    * @return Errors. Is a newly created list.
965    */
 
966  1195 toggle public SourceFileExceptionList getErrors() {
967  1195 final SourceFileExceptionList result = new SourceFileExceptionList(errors);
968  1195 result.add(pluginResults.getAllErrors());
969  1195 return result;
970    }
971   
972    /**
973    * Get all warnings.
974    *
975    * @return Warnings. Is a newly created list.
976    */
 
977  181 toggle public SourceFileExceptionList getWarnings() {
978  181 final SourceFileExceptionList result = new SourceFileExceptionList();
979  181 result.add(pluginResults.getAllWarnings());
980  181 return result;
981    }
982   
983    /**
984    * Set {@link SourceFileExceptionList}. Doesn't do any status handling. Only for internal use.
985    *
986    * @param errors Set this error list. If this is <code>null</code> the errors are cleared!
987    */
 
988  4334 toggle protected void setErrors(final SourceFileExceptionList errors) {
989  4334 this.errors = errors;
990    // TODO mime 20100625: "if errors==null" this should be a new function "clearErrors" or other
991  4334 if (errors == null) {
992  4186 pluginResults = new PluginResultManager();
993    }
994    }
995   
996    /**
997    * Add the plugin execution errors and warnings.
998    *
999    * @param plugin Plugin that was executed.
1000    * @param errors Resulting errors.
1001    * @param warnings Resulting warnings.
1002    */
 
1003  71 toggle public void addPluginResults(final Plugin plugin, final SourceFileExceptionList errors,
1004    final SourceFileExceptionList warnings) {
1005  71 if (plugin instanceof InternalPluginBo) {
1006  0 throw new RuntimeException(
1007    "Programming error: an internal plugin should not add exeptions here!\n"
1008    + plugin.getClass().getName());
1009    }
1010  71 pluginResults.addResult(plugin, errors, warnings);
1011  71 ModuleEventLog.getInstance().stateChanged(bo);
1012    }
1013   
1014    /**
1015    * Remove all plugin errors and warnings.
1016    */
 
1017  0 toggle public void removeAllPluginResults() {
1018  0 pluginResults.removeAllResults();
1019  0 ModuleEventLog.getInstance().stateChanged(bo);
1020    }
1021   
1022    /**
1023    * Print the dependence tree to <code>System.out</code>.
1024    */
 
1025  0 toggle public void printDependencyTree() {
1026  0 System.out.println("DependencyTree");
1027  0 printDependencyTree(0);
1028  0 System.out.println();
1029    }
1030   
 
1031  0 toggle private void printDependencyTree(final int tab) {
1032  0 System.out.println(StringUtility.getSpaces(tab) + bo.getName());
1033  0 final int newTab = tab + bo.getName().length();
1034  0 final KernelModuleReferenceList dependent = bo.getDependentModules();
1035  0 for (int i = 0; i < dependent.size(); i++) {
1036  0 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
1037  0 ref.getStateManager().printDependencyTree(newTab);
1038    }
1039    }
1040   
1041    }