0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
0004 *
0005 * "Hilbert II" is free software; you can redistribute
0006 * it and/or modify it under the terms of the GNU General Public
0007 * License as published by the Free Software Foundation; either
0008 * version 2 of the License, or (at your option) any later version.
0009 *
0010 * This program is distributed in the hope that it will be useful,
0011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
0012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0013 * GNU General Public License for more details.
0014 */
0015
0016 package org.qedeq.kernel.bo.service;
0017
0018 import java.util.ArrayList;
0019 import java.util.List;
0020
0021 import org.qedeq.base.trace.Trace;
0022 import org.qedeq.base.utility.StringUtility;
0023 import org.qedeq.kernel.bo.log.ModuleEventLog;
0024 import org.qedeq.kernel.bo.module.InternalPluginBo;
0025 import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
0026 import org.qedeq.kernel.bo.module.ModuleConstantsExistenceChecker;
0027 import org.qedeq.kernel.bo.module.ModuleLabels;
0028 import org.qedeq.kernel.se.common.ModuleDataException;
0029 import org.qedeq.kernel.se.common.Plugin;
0030 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0031 import org.qedeq.kernel.se.dto.module.QedeqVo;
0032 import org.qedeq.kernel.se.state.AbstractState;
0033 import org.qedeq.kernel.se.state.DependencyState;
0034 import org.qedeq.kernel.se.state.FormallyProvedState;
0035 import org.qedeq.kernel.se.state.LoadingImportsState;
0036 import org.qedeq.kernel.se.state.LoadingState;
0037 import org.qedeq.kernel.se.state.WellFormedState;
0038
0039
0040 /**
0041 * Changes the states of {@link org.qedeq.kernel.bo.service.DefaultKernelQedeqBo}s.
0042 * All state changing is done here.
0043 *
0044 * @author Michael Meyling
0045 */
0046 public class StateManager {
0047
0048 /** This class. */
0049 private static final Class CLASS = StateManager.class;
0050
0051 /** Main BO to care about. */
0052 private final DefaultKernelQedeqBo bo;
0053
0054 /** Completeness during loading from web. */
0055 private int loadingCompleteness;
0056
0057 /** Describes QEDEQ module loading state. */
0058 private LoadingState loadingState;
0059
0060 /** Describes QEDEQ module loading imports state. */
0061 private LoadingImportsState loadingImportsState;
0062
0063 /** Describes QEDEQ module dependency state. */
0064 private DependencyState dependencyState;
0065
0066 /** Describes QEDEQ module well formed state. */
0067 private WellFormedState wellFormedState;
0068
0069 /** Describes QEDEQ module formally proved state. */
0070 private FormallyProvedState formallyProvedState;
0071
0072 /** Holds QEDEQ module plugin results. */
0073 private PluginResultManager pluginResults;
0074
0075 /** Failure exceptions for basic operations. */
0076 private SourceFileExceptionList errors;
0077
0078 /** Currently running plugin. Might be <code>null</code>. */
0079 private Plugin currentlyRunningPlugin;
0080
0081
0082 StateManager(final DefaultKernelQedeqBo bo) {
0083 this.bo = bo;
0084 loadingState = LoadingState.STATE_UNDEFINED;
0085 loadingCompleteness = 0;
0086 loadingImportsState = LoadingImportsState.STATE_UNDEFINED;
0087 dependencyState = DependencyState.STATE_UNDEFINED;
0088 wellFormedState = WellFormedState.STATE_UNCHECKED;
0089 formallyProvedState = FormallyProvedState.STATE_UNCHECKED;
0090 pluginResults = new PluginResultManager();
0091 }
0092
0093 /**
0094 * Delete QEDEQ module. Invalidates all dependent modules.
0095 */
0096 public void delete() {
0097 checkIfDeleted();
0098 invalidateOtherDependentModulesToLoaded();
0099 setLoadingState(LoadingState.STATE_DELETED);
0100 bo.setQedeqVo(null);
0101 bo.getKernelRequiredModules().clear();
0102 bo.getDependentModules().clear();
0103 bo.setLabels(null);
0104 setDependencyState(DependencyState.STATE_UNDEFINED);
0105 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0106 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0107 setErrors(null);
0108 ModuleEventLog.getInstance().removeModule(bo);
0109 }
0110
0111 /**
0112 * Is the module in a failure state? That is the case if loading of module or imported modules
0113 * failed or the logical check failed. Possible plugin failures don't matter.
0114 *
0115 * @return Failure during loading or logical check occurred.
0116 */
0117 public boolean hasBasicFailures() {
0118 return loadingState.isFailure() || dependencyState.isFailure()
0119 || wellFormedState.isFailure() || formallyProvedState.isFailure();
0120 }
0121
0122 /**
0123 * Has the module any errors? This includes loading, importing, logical and plugin errors.
0124 *
0125 * @return Errors occurred.
0126 */
0127 public boolean hasErrors() {
0128 return hasBasicFailures() || (getErrors() != null && getErrors().size() > 0);
0129 }
0130
0131 /**
0132 * Has the module any warnings? This includes loading, importing, logical and plugin warnings.
0133 *
0134 * @return Warnings occurred.
0135 */
0136 public boolean hasWarnings() {
0137 return (getWarnings() != null && getWarnings().size() > 0);
0138 }
0139
0140 /**
0141 * Set completeness percentage.
0142 *
0143 * @param completeness Completeness of loading into memory.
0144 */
0145 public void setLoadingCompleteness(final int completeness) {
0146 this.loadingCompleteness = completeness;
0147 }
0148
0149 /**
0150 * Get loading completeness percentage.
0151 *
0152 * @return Completeness as percent number.
0153 */
0154 public int getLoadingCompleteness() {
0155 return this.loadingCompleteness;
0156 }
0157
0158 /**
0159 * Get loading state.
0160 *
0161 * @return Loading state.
0162 */
0163 public LoadingState getLoadingState() {
0164 return this.loadingState;
0165 }
0166
0167 /**
0168 * Is the module loaded?
0169 *
0170 * @return Is the module loaded?
0171 */
0172 public boolean isLoaded() {
0173 return loadingState == LoadingState.STATE_LOADED;
0174 }
0175
0176 /**
0177 * Set loading progress module state.
0178 *
0179 * @param plugin Plugin that sets the state.
0180 * @param state Module loading state. Must not be <code>null</code>.
0181 * @throws IllegalStateException State is a failure state or module loaded state.
0182 */
0183 public void setLoadingProgressState(final Plugin plugin , final LoadingState state) {
0184 checkIfDeleted();
0185 if (state == LoadingState.STATE_LOADED) {
0186 throw new IllegalArgumentException(
0187 "this state could only be set by calling method setLoaded");
0188 }
0189 if (state != LoadingState.STATE_DELETED && state.isFailure()) {
0190 throw new IllegalArgumentException(
0191 "this is a failure state, call setLoadingFailureState for " + state);
0192 }
0193 // if module has no loading state we give him one before creating an event
0194 if (getLoadingState() == LoadingState.STATE_UNDEFINED) {
0195 setLoadingState(state);
0196 ModuleEventLog.getInstance().addModule(bo);
0197 }
0198 if (state == LoadingState.STATE_DELETED) {
0199 throw new IllegalArgumentException(
0200 "call delete for " + state);
0201 }
0202 setLoadingState(state);
0203 setCurrentlyRunningPlugin(plugin);
0204 bo.setQedeqVo(null);
0205 bo.getKernelRequiredModules().clear();
0206 bo.getDependentModules().clear();
0207 bo.setLabels(null);
0208 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
0209 setDependencyState(DependencyState.STATE_UNDEFINED);
0210 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0211 setErrors(null);
0212 ModuleEventLog.getInstance().stateChanged(bo);
0213 }
0214
0215 /**
0216 * Set failure module state.
0217 *
0218 * @param state Module loading state. Must not be <code>null</code>.
0219 * @param e Exception that occurred during loading. Must not be <code>null</code>.
0220 * @throws IllegalArgumentException <code>state</code> is no failure state
0221 */
0222 public void setLoadingFailureState(final LoadingState state,
0223 final SourceFileExceptionList e) {
0224 if (e == null) {
0225 throw new NullPointerException("Exception must not be null");
0226 }
0227 checkIfDeleted();
0228 if (!state.isFailure()) {
0229 throw new IllegalArgumentException(
0230 "this is no failure state, call setLoadingProgressState");
0231 }
0232 // if module has no loading state we give him one before creating an event
0233 if (getLoadingState() == LoadingState.STATE_UNDEFINED) {
0234 setLoadingState(state);
0235 ModuleEventLog.getInstance().addModule(bo);
0236 }
0237 bo.setQedeqVo(null);
0238 bo.getKernelRequiredModules().clear();
0239 bo.getDependentModules().clear();
0240 bo.setLabels(null);
0241 setLoadingState(state);
0242 setCurrentlyRunningPlugin(null);
0243 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
0244 setDependencyState(DependencyState.STATE_UNDEFINED);
0245 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0246 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0247 setErrors(e);
0248 ModuleEventLog.getInstance().stateChanged(bo);
0249 }
0250
0251 /**
0252 * Set loading state to "loaded". Also puts <code>null</code> to
0253 * {@link DefaultKernelQedeqBo#getLabels()}.
0254 *
0255 * @param qedeq This module was loaded. Must not be <code>null</code>.
0256 * @param labels Module labels.
0257 * @throws NullPointerException One argument was <code>null</code>.
0258 */
0259 public void setLoaded(final QedeqVo qedeq, final ModuleLabels labels) {
0260 checkIfDeleted();
0261 if (qedeq == null) {
0262 throw new NullPointerException("Qedeq is null");
0263 }
0264 setCurrentlyRunningPlugin(null);
0265 setLoadingState(LoadingState.STATE_LOADED);
0266 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
0267 setDependencyState(DependencyState.STATE_UNDEFINED);
0268 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0269 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0270 setErrors(null);
0271 bo.setQedeqVo(qedeq);
0272 bo.getKernelRequiredModules().clear();
0273 bo.getDependentModules().clear();
0274 bo.setLabels(labels);
0275 ModuleEventLog.getInstance().stateChanged(bo);
0276 }
0277
0278 /**
0279 * Set loading imports progress module state.
0280 *
0281 * @param plugin Plugin that sets the state.
0282 * @param state Module state. Must not be <code>null</code>.
0283 * @throws IllegalStateException Module is not yet loaded.
0284 * @throws IllegalArgumentException <code>state</code> is failure state or loaded required
0285 * state.
0286 * @throws NullPointerException <code>state</code> is <code>null</code>.
0287 */
0288 public void setLoadingImportsProgressState(final Plugin plugin, final LoadingImportsState state) {
0289 checkIfDeleted();
0290 if (!isLoaded() && state != LoadingImportsState.STATE_UNDEFINED) {
0291 throw new IllegalStateException("module is not yet loaded");
0292 }
0293 if (state.isFailure()) {
0294 throw new IllegalArgumentException(
0295 "this is a failure state, call setLoadingImportsFailureState");
0296 }
0297 if (state == LoadingImportsState.STATE_LOADED_IMPORTED_MODULES) {
0298 throw new IllegalArgumentException(
0299 "this state could only be set by calling method setLoadedImports");
0300 }
0301 ModuleEventLog.getInstance().stateChanged(bo);
0302 }
0303
0304 /**
0305 * Set failure module state.
0306 *
0307 * @param state Module loading imports state. Must not be <code>null</code>.
0308 * @param e Exception that occurred during loading. Must not be <code>null</code>.
0309 * @throws IllegalStateException Module is not yet loaded.
0310 * @throws IllegalArgumentException <code>state</code> is no failure state.
0311 * @throws NullPointerException <code>state</code> is <code>null</code>.
0312 */
0313 public void setLoadingImportsFailureState(final LoadingImportsState state,
0314 final SourceFileExceptionList e) {
0315 if (e == null) {
0316 throw new NullPointerException("Exception must not be null");
0317 }
0318 checkIfDeleted();
0319 if (!isLoaded()) {
0320 throw new IllegalStateException("module is not yet loaded");
0321 }
0322 if (!state.isFailure()) {
0323 throw new IllegalArgumentException(
0324 "this is no failure state, call setLoadingProgressState");
0325 }
0326 setLoadingImportsState(state);
0327 setCurrentlyRunningPlugin(null);
0328 setErrors(e);
0329 ModuleEventLog.getInstance().stateChanged(bo);
0330 }
0331
0332 /**
0333 * Get loading imports state.
0334 *
0335 * @return Dependency state.
0336 */
0337 public LoadingImportsState getLoadingImportsState() {
0338 return this.loadingImportsState;
0339 }
0340
0341 /**
0342 * Is the module loaded?
0343 *
0344 * @return Is the module loaded?
0345 */
0346 public boolean hasLoadedImports() {
0347 return loadingImportsState == LoadingImportsState.STATE_LOADED_IMPORTED_MODULES;
0348 }
0349
0350 /**
0351 * Set dependency progress module state.
0352 *
0353 * @param plugin Plugin that sets the state.
0354 * @param state Module state. Must not be <code>null</code>.
0355 * @throws IllegalStateException Module is not yet loaded.
0356 * @throws IllegalArgumentException <code>state</code> is failure state or loaded required
0357 * state.
0358 * @throws NullPointerException <code>state</code> is <code>null</code>.
0359 */
0360 public void setDependencyProgressState(final Plugin plugin, final DependencyState state) {
0361 checkIfDeleted();
0362 if (!isLoaded() && state != DependencyState.STATE_UNDEFINED) {
0363 throw new IllegalStateException("module is not yet loaded");
0364 }
0365 if (state.isFailure()) {
0366 throw new IllegalArgumentException(
0367 "this is a failure state, call setDependencyFailureState");
0368 }
0369 if (state == DependencyState.STATE_LOADED_REQUIRED_MODULES) {
0370 throw new IllegalArgumentException(
0371 "this state could only be set by calling method setLoadedRequiredModules");
0372 }
0373 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0374 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0375 setDependencyState(state);
0376 setCurrentlyRunningPlugin(null);
0377 setErrors(null);
0378 ModuleEventLog.getInstance().stateChanged(bo);
0379 }
0380
0381 /**
0382 * Set failure module state.
0383 *
0384 * @param state Module dependency state. Must not be <code>null</code>.
0385 * @param e Exception that occurred during loading. Must not be <code>null</code>.
0386 * @throws IllegalStateException Module is not yet loaded.
0387 * @throws IllegalArgumentException <code>state</code> is no failure state.
0388 * @throws NullPointerException <code>state</code> is <code>null</code>.
0389 */
0390 public void setDependencyFailureState(final DependencyState state,
0391 final SourceFileExceptionList e) {
0392 if (e == null) {
0393 throw new NullPointerException("Exception must not be null");
0394 }
0395 checkIfDeleted();
0396 if (!isLoaded()) {
0397 throw new IllegalStateException("module is not yet loaded");
0398 }
0399 if (!state.isFailure()) {
0400 throw new IllegalArgumentException(
0401 "this is no failure state, call setLoadingProgressState");
0402 }
0403 setDependencyState(state);
0404 setCurrentlyRunningPlugin(null);
0405 setErrors(e);
0406 ModuleEventLog.getInstance().stateChanged(bo);
0407 }
0408
0409 /**
0410 * Get dependency state.
0411 *
0412 * @return Dependency state.
0413 */
0414 public DependencyState getDependencyState() {
0415 return this.dependencyState;
0416 }
0417
0418 /**
0419 * Reset all (recursive) dependent modules (if any) to state loaded.
0420 */
0421 private void invalidateOtherDependentModulesToLoaded() {
0422 final String method = "invalidateOtherDependModulesToLoaded";
0423 Trace.begin(CLASS, this, method);
0424 Trace.param(CLASS, this, method, "bo", bo);
0425 if (hasLoadedRequiredModules()) {
0426 final KernelModuleReferenceList dependent = bo.getDependentModules();
0427 Trace.trace(CLASS, this, method, "begin list of dependent modules");
0428 // remember dependent modules
0429 final List list = new ArrayList();
0430 for (int i = 0; i < dependent.size(); i++) {
0431 Trace.param(CLASS, this, method, "" + i, dependent.getKernelQedeqBo(i));
0432 list.add(dependent.getKernelQedeqBo(i));
0433 }
0434 Trace.trace(CLASS, this, method, "end list of dependent modules");
0435 for (int i = 0; i < list.size(); i++) {
0436 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) list.get(i);
0437 // work on it, if still in list of dependent modules
0438 if (dependent.contains(ref)) {
0439 ref.getStateManager().invalidateDependentModulesToLoaded();
0440 }
0441 }
0442 list.clear();
0443 dependent.clear();
0444
0445 final KernelModuleReferenceList required = bo.getKernelRequiredModules();
0446 for (int i = 0; i < required.size(); i++) {
0447 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) required.getKernelQedeqBo(i);
0448 Trace.param(CLASS, this, method, "remove dependence from", ref);
0449 ref.getDependentModules().remove(bo);
0450 }
0451 required.clear();
0452 }
0453 Trace.end(CLASS, this, method);
0454 }
0455
0456 /**
0457 * Reset this and all (recursive) dependent modules (if any) to state loaded.
0458 */
0459 private void invalidateDependentModulesToLoaded() {
0460 final String method = "invalidateDependentModulesToLoaded";
0461 Trace.begin(CLASS, this, method);
0462 Trace.param(CLASS, this, method, "bo", bo);
0463 if (hasLoadedRequiredModules()) {
0464 final KernelModuleReferenceList dependent = bo.getDependentModules();
0465 Trace.trace(CLASS, this, method, "begin list of dependent modules");
0466 // remember dependent modules
0467 final List list = new ArrayList();
0468 for (int i = 0; i < dependent.size(); i++) {
0469 Trace.param(CLASS, this, method, "" + i, dependent.getKernelQedeqBo(i));
0470 list.add(dependent.getKernelQedeqBo(i));
0471 }
0472 Trace.trace(CLASS, this, method, "end list of dependent modules");
0473 for (int i = 0; i < list.size(); i++) {
0474 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) list.get(i);
0475 // work on it, if still in list of dependent modules
0476 if (dependent.contains(ref)) {
0477 ref.getStateManager().invalidateDependentModulesToLoaded();
0478 }
0479 }
0480 list.clear();
0481 dependent.clear();
0482
0483 final KernelModuleReferenceList required = bo.getKernelRequiredModules();
0484 for (int i = 0; i < required.size(); i++) {
0485 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) required.getKernelQedeqBo(i);
0486 Trace.param(CLASS, this, method, "remove dependence from", ref);
0487 ref.getDependentModules().remove(bo);
0488 }
0489 required.clear();
0490
0491 invalidateThisModuleToLoaded();
0492 setLoadingState(LoadingState.STATE_LOADED);
0493 ModuleEventLog.getInstance().stateChanged(bo);
0494 }
0495 Trace.end(CLASS, this, method);
0496 }
0497
0498 /**
0499 * Reset this and all (recursive) dependent modules (if any) to state loaded.
0500 */
0501 private void invalidateDependentModulesToLoadedImports() {
0502 final String method = "invalidateDependentModulesToLoadedImports";
0503 Trace.begin(CLASS, this, method);
0504 Trace.param(CLASS, this, method, "bo", bo);
0505 if (hasLoadedImports()) {
0506 final KernelModuleReferenceList dependent = bo.getDependentModules();
0507 Trace.trace(CLASS, this, method, "begin list of dependent modules");
0508 // remember dependent modules
0509 final List list = new ArrayList();
0510 for (int i = 0; i < dependent.size(); i++) {
0511 Trace.param(CLASS, this, method, "" + i, dependent.getKernelQedeqBo(i));
0512 list.add(dependent.getKernelQedeqBo(i));
0513 }
0514 Trace.trace(CLASS, this, method, "end list of dependent modules");
0515 for (int i = 0; i < list.size(); i++) {
0516 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) list.get(i);
0517 // work on it, if still in list of dependent modules
0518 if (dependent.contains(ref)) {
0519 ref.getStateManager().invalidateDependentModulesToLoadedImports();
0520 }
0521 }
0522 list.clear();
0523
0524 invalidateThisModuleToLoadedImports();
0525 ModuleEventLog.getInstance().stateChanged(bo);
0526 }
0527 Trace.end(CLASS, this, method);
0528 }
0529
0530 /**
0531 * Reset all (recursive) dependent modules (if any) to state loaded required.
0532 */
0533 private void invalidateOtherDependentModulesToLoadedRequired() {
0534 if (isWellFormed()) {
0535 final KernelModuleReferenceList dependent = bo.getDependentModules();
0536 for (int i = 0; i < dependent.size(); i++) {
0537 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
0538 ref.getStateManager().invalidateDependentModulesToLoadedRequired();
0539 }
0540 }
0541 }
0542
0543 /**
0544 * Reset this and all (recursive) dependent modules (if any) to state loaded required.
0545 */
0546 private void invalidateDependentModulesToLoadedRequired() {
0547 if (isWellFormed()) {
0548 final KernelModuleReferenceList dependent = bo.getDependentModules();
0549 for (int i = 0; i < dependent.size(); i++) {
0550 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
0551 ref.getStateManager().invalidateDependentModulesToLoadedRequired();
0552 }
0553 invalidateThisModuleToLoadedReqired();
0554 ModuleEventLog.getInstance().stateChanged(bo);
0555 }
0556 }
0557
0558 /**
0559 * Reset all (recursive) dependent modules (if any) to state well formed.
0560 */
0561 private void invalidateOtherDependentModulesToWellFormed() {
0562 if (isFullyFormallyProved()) {
0563 final KernelModuleReferenceList dependent = bo.getDependentModules();
0564 for (int i = 0; i < dependent.size(); i++) {
0565 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
0566 ref.getStateManager().invalidateDependentModulesToWellFormed();
0567 }
0568 }
0569 }
0570
0571 /**
0572 * Reset this and all (recursive) dependent modules (if any) to state well formed.
0573 */
0574 private void invalidateDependentModulesToWellFormed() {
0575 if (isFullyFormallyProved()) {
0576 final KernelModuleReferenceList dependent = bo.getDependentModules();
0577 for (int i = 0; i < dependent.size(); i++) {
0578 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
0579 ref.getStateManager().invalidateDependentModulesToWellFormed();
0580 }
0581 invalidateThisModuleToWellFormed();
0582 ModuleEventLog.getInstance().stateChanged(bo);
0583 }
0584 }
0585
0586 private void invalidateThisModuleToLoaded() {
0587 if (isLoaded()) {
0588 setLoadingState(LoadingState.STATE_LOADED);
0589 setLoadingImportsState(LoadingImportsState.STATE_UNDEFINED);
0590 setDependencyState(DependencyState.STATE_UNDEFINED);
0591 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0592 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0593 bo.getKernelRequiredModules().clear();
0594 setErrors(null);
0595 }
0596 }
0597
0598 private void invalidateThisModuleToLoadedImports() {
0599 if (hasLoadedImports()) {
0600 setLoadingImportsState(LoadingImportsState.STATE_LOADED_IMPORTED_MODULES);
0601 setDependencyState(DependencyState.STATE_UNDEFINED);
0602 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0603 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0604 setErrors(null);
0605 }
0606 }
0607
0608 private void invalidateThisModuleToLoadedReqired() {
0609 if (hasLoadedRequiredModules()) {
0610 setDependencyState(DependencyState.STATE_LOADED_REQUIRED_MODULES);
0611 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0612 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0613 setErrors(null);
0614 }
0615 }
0616
0617 private void invalidateThisModuleToWellFormed() {
0618 if (isWellFormed()) {
0619 setWellFormedState(WellFormedState.STATE_CHECKED);
0620 setFormallyProvedState(FormallyProvedState.STATE_UNCHECKED);
0621 setErrors(null);
0622 }
0623 }
0624
0625 private void invalidateThisModuleToFormallyProved() {
0626 if (isFullyFormallyProved()) {
0627 setFormallyProvedState(FormallyProvedState.STATE_CHECKED);
0628 setErrors(null);
0629 }
0630 }
0631
0632 /**
0633 * Are all required modules loaded?
0634 *
0635 * @return All required modules are loaded?
0636 */
0637 public boolean hasLoadedRequiredModules() {
0638 return isLoaded() && dependencyState == DependencyState.STATE_LOADED_REQUIRED_MODULES;
0639 }
0640
0641 /**
0642 * Set loaded imports state.
0643 *
0644 * @param required URLs of all referenced modules. Must not be <code>null</code>.
0645 * @throws IllegalStateException Module is not yet loaded.
0646 */
0647 public void setLoadedImports(final KernelModuleReferenceList required) {
0648 checkIfDeleted();
0649 if (!isLoaded()) {
0650 throw new IllegalStateException(
0651 "Loaded imported modules can only be set if module is loaded."
0652 + "\"\nCurrently the status for the module"
0653 + "\"" + bo.getName() + "\" is \"" + bo.getLoadingState() + "\"");
0654 }
0655 setLoadingImportsState(LoadingImportsState.STATE_LOADED_IMPORTED_MODULES);
0656 setDependencyState(DependencyState.STATE_UNDEFINED);
0657 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0658 setCurrentlyRunningPlugin(null);
0659 setErrors(null);
0660 bo.getKernelRequiredModules().set(required);
0661 ModuleEventLog.getInstance().stateChanged(bo);
0662 }
0663
0664 /**
0665 * Set loaded required requirements state.
0666 *
0667 * @throws IllegalStateException Module is not yet loaded.
0668 */
0669 public void setLoadedRequiredModules() {
0670 checkIfDeleted();
0671 if (!isLoaded()) {
0672 throw new IllegalStateException(
0673 "Required modules can only be set if module is loaded."
0674 + "\"\nCurrently the status for the module"
0675 + "\"" + bo.getName() + "\" is \"" + bo.getLoadingState() + "\"");
0676 }
0677 KernelModuleReferenceList required = bo.getKernelRequiredModules();
0678 for (int i = 0; i < required.size(); i++) {
0679 DefaultKernelQedeqBo current = (DefaultKernelQedeqBo) required.getKernelQedeqBo(i);
0680 try {
0681 current.getDependentModules().add(required.getModuleContext(i),
0682 required.getLabel(i), bo);
0683 } catch (ModuleDataException me) { // should never happen
0684 throw new RuntimeException(me);
0685 }
0686 }
0687 setDependencyState(DependencyState.STATE_LOADED_REQUIRED_MODULES);
0688 setWellFormedState(WellFormedState.STATE_UNCHECKED);
0689 setCurrentlyRunningPlugin(null);
0690 setErrors(null);
0691 ModuleEventLog.getInstance().stateChanged(bo);
0692 }
0693
0694 /**
0695 * Set logic checked state. Also set the predicate and function existence checker.
0696 *
0697 * @param checker Checks if a predicate or function constant is defined.
0698 */
0699 public void setWellFormed(final ModuleConstantsExistenceChecker checker) {
0700 checkIfDeleted();
0701 if (!hasLoadedRequiredModules()) {
0702 throw new IllegalStateException(
0703 "Checked can only be set if all required modules are loaded."
0704 + "\"\nCurrently the status for the module"
0705 + "\"" + bo.getName() + "\" is \"" + bo.getLoadingState() + "\"");
0706 }
0707 setWellFormedState(WellFormedState.STATE_CHECKED);
0708 setCurrentlyRunningPlugin(null);
0709 bo.setExistenceChecker(checker);
0710 ModuleEventLog.getInstance().stateChanged(bo);
0711 }
0712
0713 /**
0714 * Set checking for well formed progress module state. Must not be <code>null</code>.
0715 *
0716 * @param plugin Plugin that sets the state.
0717 * @param state module state
0718 */
0719 public void setWellFormedProgressState(final Plugin plugin, final WellFormedState state) {
0720 if (getDependencyState().getCode()
0721 < DependencyState.STATE_LOADED_REQUIRED_MODULES.getCode()
0722 && state != WellFormedState.STATE_UNCHECKED) {
0723 throw new IllegalArgumentException(
0724 "this state could only be set if all required modules are loaded ");
0725 }
0726 if (state.isFailure()) {
0727 throw new IllegalArgumentException(
0728 "this is a failure state, call setWellFormedFailureState");
0729 }
0730 if (state == WellFormedState.STATE_CHECKED) {
0731 throw new IllegalArgumentException(
0732 "set with setChecked(ExistenceChecker)");
0733 }
0734 setWellFormedState(state);
0735 setCurrentlyRunningPlugin(plugin);
0736 setErrors(null);
0737 ModuleEventLog.getInstance().stateChanged(bo);
0738 }
0739
0740 /**
0741 * Set failure module state.
0742 *
0743 * @param state module state
0744 * @param e Exception that occurred during loading.
0745 * @throws IllegalArgumentException <code>state</code> is no failure state
0746 */
0747 public void setWellFormedFailureState(final WellFormedState state,
0748 final SourceFileExceptionList e) {
0749 if ((!isLoaded() || !hasLoadedRequiredModules())
0750 && state != WellFormedState.STATE_UNCHECKED) {
0751 throw new IllegalArgumentException(
0752 "this state could only be set if all required modules are loaded ");
0753 }
0754 if (!state.isFailure()) {
0755 throw new IllegalArgumentException(
0756 "this is no failure state, call setWellFormedProgressState");
0757 }
0758 setWellFormedState(state);
0759 setCurrentlyRunningPlugin(null);
0760 setErrors(e);
0761 ModuleEventLog.getInstance().stateChanged(bo);
0762 }
0763
0764 /**
0765 * Set checking for formally proved progress module state. Must not be <code>null</code>.
0766 *
0767 * @param plugin Plugin that sets the state.
0768 * @param state module state
0769 */
0770 public void setFormallyProvedProgressState(final Plugin plugin, final FormallyProvedState state) {
0771 if (getDependencyState().getCode()
0772 < DependencyState.STATE_LOADED_REQUIRED_MODULES.getCode()
0773 && state != FormallyProvedState.STATE_UNCHECKED) {
0774 throw new IllegalArgumentException(
0775 "this state could only be set if all required modules are loaded ");
0776 }
0777 if (state.isFailure()) {
0778 throw new IllegalArgumentException(
0779 "this is a failure state, call setFormallyProvedFailureState");
0780 }
0781 // if (state == FormallyProvedState.STATE_CHECKED) {
0782 // // FIXME 20130220 m31: do we need something simular?
0783 // throw new IllegalArgumentException(
0784 // "set with setChecked(ExistenceChecker)");
0785 // }
0786 setFormallyProvedState(state);
0787 setCurrentlyRunningPlugin(plugin);
0788 setErrors(null);
0789 ModuleEventLog.getInstance().stateChanged(bo);
0790 }
0791
0792 /**
0793 * Set failure module state.
0794 *
0795 * @param state module state
0796 * @param e Exception that occurred during loading.
0797 * @throws IllegalArgumentException <code>state</code> is no failure state
0798 */
0799 public void setFormallyProvedFailureState(final FormallyProvedState state,
0800 final SourceFileExceptionList e) {
0801 if ((!isLoaded() || !hasLoadedRequiredModules())
0802 && state != FormallyProvedState.STATE_UNCHECKED) {
0803 throw new IllegalArgumentException(
0804 "this state could only be set if all required modules are well formed ");
0805 }
0806 if (!state.isFailure()) {
0807 throw new IllegalArgumentException(
0808 "this is no failure state, call setFormallyProvedProgressState");
0809 }
0810 setFormallyProvedState(state);
0811 setCurrentlyRunningPlugin(null);
0812 setErrors(e);
0813 ModuleEventLog.getInstance().stateChanged(bo);
0814 }
0815
0816 /**
0817 * Checks if the current instance is already deleted.
0818 *
0819 * @throws IllegalStateException Module is already deleted.
0820 */
0821 private void checkIfDeleted() {
0822 if (getLoadingState() == LoadingState.STATE_DELETED) {
0823 throw new IllegalStateException("module is already deleted: " + bo.getUrl());
0824 }
0825 }
0826
0827 /**
0828 * Was the module successfully checked for well formedness errors?
0829 *
0830 * @return Successfully checked for being well formed?
0831 */
0832 public boolean isWellFormed() {
0833 return hasLoadedRequiredModules() && wellFormedState == WellFormedState.STATE_CHECKED;
0834 }
0835
0836 /**
0837 * Get the well formed state.
0838 *
0839 * @return Well formed state.
0840 */
0841 public WellFormedState getWellFormedState() {
0842 return this.wellFormedState;
0843 }
0844
0845 /**
0846 * Was the module successfully checked having formally correct proofs?
0847 *
0848 * @return Successfully checked for having formally correct proofs?
0849 */
0850 public boolean isFullyFormallyProved() {
0851 return isWellFormed() && formallyProvedState == FormallyProvedState.STATE_CHECKED;
0852 }
0853
0854 /**
0855 * Get the formally proved state.
0856 *
0857 * @return Formally proved state.
0858 */
0859 public FormallyProvedState getFormallyProvedState() {
0860 return this.formallyProvedState;
0861 }
0862
0863 /**
0864 * Get a description of the current state the module is in.
0865 *
0866 * @return Textual representation of module state.
0867 */
0868 public String getStateDescription() {
0869 String result = "";
0870 if (loadingState == LoadingState.STATE_LOADING_FROM_WEB) {
0871 result = loadingState.getText() + " (" + loadingCompleteness + "%)";
0872 } else if (!isLoaded()) {
0873 result = loadingState.getText();
0874 } else if (!hasLoadedImports()) {
0875 if (loadingImportsState == LoadingImportsState.STATE_UNDEFINED) {
0876 result = loadingState.getText();
0877 } else {
0878 result = loadingImportsState.getText();
0879 }
0880 } else if (!hasLoadedRequiredModules()) {
0881 if (dependencyState == DependencyState.STATE_UNDEFINED) {
0882 result = loadingImportsState.getText();
0883 } else {
0884 result = dependencyState.getText();
0885 }
0886 } else if (!isWellFormed()) {
0887 if (wellFormedState == WellFormedState.STATE_UNCHECKED) {
0888 result = dependencyState.getText();
0889 } else {
0890 result = wellFormedState.getText();
0891 }
0892 } else if (!isFullyFormallyProved()) {
0893 if (formallyProvedState == FormallyProvedState.STATE_UNCHECKED) {
0894 result = wellFormedState.getText();
0895 } else {
0896 result = formallyProvedState.getText();
0897 }
0898 } else {
0899 result = formallyProvedState.getText();
0900 }
0901 final String pluginState = pluginResults.getPluginStateDescription();
0902 if (pluginState.length() > 0) {
0903 result += "; " + pluginState;
0904 }
0905 return result;
0906 }
0907
0908 /**
0909 * Get the current state of associate module.
0910 *
0911 * @return Current module state.
0912 */
0913 public AbstractState getCurrentState() {
0914 if (!isLoaded()) {
0915 return loadingState;
0916 } else if (!hasLoadedImports()) {
0917 if (loadingImportsState == LoadingImportsState.STATE_UNDEFINED) {
0918 return loadingState;
0919 }
0920 return loadingImportsState;
0921 } else if (!hasLoadedRequiredModules()) {
0922 if (dependencyState == DependencyState.STATE_UNDEFINED) {
0923 return loadingImportsState;
0924 }
0925 return dependencyState;
0926 } else if (!isWellFormed()) {
0927 if (wellFormedState == WellFormedState.STATE_UNCHECKED) {
0928 return dependencyState;
0929 }
0930 return wellFormedState;
0931 } else if (!isFullyFormallyProved()) {
0932 if (formallyProvedState == FormallyProvedState.STATE_UNCHECKED) {
0933 return wellFormedState;
0934 }
0935 return formallyProvedState;
0936 } else {
0937 return formallyProvedState;
0938 }
0939 }
0940
0941 /**
0942 * Get the last successful state we were in.
0943 * As there are: undefined, loaded, loaded required, fully formally proved.
0944 *
0945 * @return Previous major error free state.
0946 */
0947 public AbstractState getLastSuccesfulState() {
0948 if (!isLoaded()) {
0949 return LoadingState.STATE_UNDEFINED;
0950 } else if (!hasLoadedImports()) {
0951 return LoadingState.STATE_LOADED;
0952 } else if (!hasLoadedRequiredModules()) {
0953 return LoadingImportsState.STATE_LOADED_IMPORTED_MODULES;
0954 } else if (!isWellFormed()) {
0955 return DependencyState.STATE_LOADED_REQUIRED_MODULES;
0956 } else if (!isFullyFormallyProved()) {
0957 return WellFormedState.STATE_CHECKED;
0958 } else {
0959 return FormallyProvedState.STATE_CHECKED;
0960 }
0961 }
0962
0963 /**
0964 * Set {@link LoadingState}. Doesn't do any status handling. Only for internal use.
0965 *
0966 * @param state Set this loading state.
0967 */
0968 protected void setLoadingState(final LoadingState state) {
0969 this.loadingState = state;
0970 }
0971
0972 /**
0973 * Set {@link LoadingImportsState}. Doesn't do any status handling. Only for internal use.
0974 *
0975 * @param state Set this loading state.
0976 */
0977 protected void setLoadingImportsState(final LoadingImportsState state) {
0978 this.loadingImportsState = state;
0979 }
0980
0981 /**
0982 * Set {@link DependencyState}. Doesn't do any status handling. Only for internal use.
0983 *
0984 * @param state Set this dependency state.
0985 */
0986 protected void setDependencyState(final DependencyState state) {
0987 this.dependencyState = state;
0988 }
0989
0990 /**
0991 * Set {@link WellFormedState}. Doesn't do any status handling. Only for internal use.
0992 *
0993 * @param state Set this logical state.
0994 */
0995 protected void setWellFormedState(final WellFormedState state) {
0996 this.wellFormedState = state;
0997 }
0998
0999 /**
1000 * Set {@link FormallyProvedState}. Doesn't do any status handling. Only for internal use.
1001 *
1002 * @param state Set this logical state.
1003 */
1004 protected void setFormallyProvedState(final FormallyProvedState state) {
1005 this.formallyProvedState = state;
1006 }
1007
1008 /**
1009 * Get all errors.
1010 *
1011 * @return Errors. Is a newly created list.
1012 */
1013 public SourceFileExceptionList getErrors() {
1014 final SourceFileExceptionList result = new SourceFileExceptionList(errors);
1015 result.add(pluginResults.getAllErrors());
1016 return result;
1017 }
1018
1019 /**
1020 * Get all warnings.
1021 *
1022 * @return Warnings. Is a newly created list.
1023 */
1024 public SourceFileExceptionList getWarnings() {
1025 final SourceFileExceptionList result = new SourceFileExceptionList();
1026 result.add(pluginResults.getAllWarnings());
1027 return result;
1028 }
1029
1030 /**
1031 * Get the currently running plugin (if any).
1032 *
1033 * @return Currently running plugin. Might be <code>null</code>.
1034 */
1035 public Plugin getCurrentlyRunningPlugin() {
1036 return currentlyRunningPlugin;
1037 }
1038
1039 /**
1040 * Set the currently running plugin (if any).
1041 *
1042 * @param currentlyRunningPlugin Currently running plugin. Might be <code>null</code>.
1043 */
1044 public void setCurrentlyRunningPlugin(final Plugin currentlyRunningPlugin) {
1045 this.currentlyRunningPlugin = currentlyRunningPlugin;
1046 }
1047
1048 /**
1049 * Set {@link SourceFileExceptionList}. Doesn't do any status handling. Only for internal use.
1050 *
1051 * @param errors Set this error list. If this is <code>null</code> the errors are cleared!
1052 */
1053 protected void setErrors(final SourceFileExceptionList errors) {
1054 this.errors = errors;
1055 // TODO mime 20100625: "if errors==null" this should be a new function "clearErrors" or other
1056 if (errors == null) {
1057 pluginResults = new PluginResultManager();
1058 }
1059 }
1060
1061 /**
1062 * Add the plugin execution errors and warnings.
1063 *
1064 * @param plugin Plugin that was executed.
1065 * @param errors Resulting errors.
1066 * @param warnings Resulting warnings.
1067 */
1068 public void addPluginResults(final Plugin plugin, final SourceFileExceptionList errors,
1069 final SourceFileExceptionList warnings) {
1070 if (plugin instanceof InternalPluginBo) {
1071 throw new RuntimeException(
1072 "Programming error: an internal plugin should not add exeptions here!\n"
1073 + plugin.getClass().getName());
1074 }
1075 pluginResults.addResult(plugin, errors, warnings);
1076 ModuleEventLog.getInstance().stateChanged(bo);
1077 }
1078
1079 /**
1080 * Remove all plugin errors and warnings.
1081 */
1082 public void removeAllPluginResults() {
1083 pluginResults.removeAllResults();
1084 ModuleEventLog.getInstance().stateChanged(bo);
1085 }
1086
1087 /**
1088 * Print the dependence tree to <code>System.out</code>.
1089 */
1090 public void printDependencyTree() {
1091 printDependencyTree(0);
1092 System.out.println();
1093 }
1094
1095 private void printDependencyTree(final int tab) {
1096 System.out.println(StringUtility.getSpaces(tab) + bo.getName());
1097 final int newTab = tab + bo.getName().length();
1098 final KernelModuleReferenceList dependent = bo.getDependentModules();
1099 for (int i = 0; i < dependent.size(); i++) {
1100 DefaultKernelQedeqBo ref = (DefaultKernelQedeqBo) dependent.getKernelQedeqBo(i);
1101 ref.getStateManager().printDependencyTree(newTab);
1102 }
1103 }
1104
1105 }
|