0001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
0002 *
0003 * Copyright 2000-2011, 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.io.File;
0019 import java.io.FileFilter;
0020 import java.io.FileNotFoundException;
0021 import java.io.FileOutputStream;
0022 import java.io.IOException;
0023 import java.io.InputStream;
0024 import java.io.Reader;
0025 import java.io.UnsupportedEncodingException;
0026 import java.lang.reflect.InvocationTargetException;
0027 import java.net.HttpURLConnection;
0028 import java.net.MalformedURLException;
0029 import java.net.URL;
0030 import java.net.URLConnection;
0031 import java.net.URLEncoder;
0032 import java.util.ArrayList;
0033 import java.util.List;
0034
0035 import org.apache.commons.httpclient.DefaultHttpMethodRetryHandler;
0036 import org.apache.commons.httpclient.HttpClient;
0037 import org.apache.commons.httpclient.HttpStatus;
0038 import org.apache.commons.httpclient.methods.GetMethod;
0039 import org.apache.commons.httpclient.params.HttpMethodParams;
0040 import org.qedeq.base.io.IoUtility;
0041 import org.qedeq.base.io.Parameters;
0042 import org.qedeq.base.io.SourceArea;
0043 import org.qedeq.base.io.TextInput;
0044 import org.qedeq.base.trace.Trace;
0045 import org.qedeq.base.utility.StringUtility;
0046 import org.qedeq.base.utility.YodaUtility;
0047 import org.qedeq.kernel.bo.KernelContext;
0048 import org.qedeq.kernel.bo.common.KernelProperties;
0049 import org.qedeq.kernel.bo.common.QedeqBo;
0050 import org.qedeq.kernel.bo.common.ServiceModule;
0051 import org.qedeq.kernel.bo.common.ServiceProcess;
0052 import org.qedeq.kernel.bo.log.QedeqLog;
0053 import org.qedeq.kernel.bo.module.InternalKernelServices;
0054 import org.qedeq.kernel.bo.module.KernelQedeqBo;
0055 import org.qedeq.kernel.bo.module.QedeqFileDao;
0056 import org.qedeq.kernel.bo.service.logic.FormalProofCheckerPlugin;
0057 import org.qedeq.kernel.bo.service.logic.SimpleProofFinderPlugin;
0058 import org.qedeq.kernel.bo.service.logic.WellFormedCheckerPlugin;
0059 import org.qedeq.kernel.se.base.module.Qedeq;
0060 import org.qedeq.kernel.se.base.module.Specification;
0061 import org.qedeq.kernel.se.common.DefaultModuleAddress;
0062 import org.qedeq.kernel.se.common.DefaultSourceFileExceptionList;
0063 import org.qedeq.kernel.se.common.LoadingState;
0064 import org.qedeq.kernel.se.common.ModuleAddress;
0065 import org.qedeq.kernel.se.common.ModuleDataException;
0066 import org.qedeq.kernel.se.common.Plugin;
0067 import org.qedeq.kernel.se.common.SourceFileException;
0068 import org.qedeq.kernel.se.common.SourceFileExceptionList;
0069 import org.qedeq.kernel.se.config.QedeqConfig;
0070 import org.qedeq.kernel.se.dto.module.QedeqVo;
0071
0072
0073 /**
0074 * This class provides a default implementation for the QEDEQ module services.
0075 *
0076 * @author Michael Meyling
0077 */
0078 public class DefaultInternalKernelServices implements ServiceModule, InternalKernelServices, Plugin {
0079
0080 /** This class. */
0081 private static final Class CLASS = DefaultInternalKernelServices.class;
0082
0083 /** For synchronized waiting. */
0084 private static final Object MONITOR = new Object();
0085
0086 /** Number of method calls. */
0087 private volatile int processCounter = 0;
0088
0089 /** Collection of already known QEDEQ modules. */
0090 private KernelQedeqBoStorage modules;
0091
0092 /** Config access. */
0093 private final QedeqConfig config;
0094
0095 /** Basic kernel properties. */
0096 private final KernelProperties kernel;
0097
0098 /** This instance nows how to load a module from the file system. */
0099 private final QedeqFileDao qedeqFileDao;
0100
0101 /** This instance manages plugins. */
0102 private final PluginManager pluginManager;
0103
0104 /** This instance manages service processes. */
0105 private final ServiceProcessManager processManager;
0106
0107 /** Validate module dependencies and status. */
0108 private boolean validate = true;
0109
0110 /**
0111 * Constructor.
0112 *
0113 * @param config For config access.
0114 * @param kernel For kernel properties.
0115 * @param loader For loading QEDEQ modules.
0116 */
0117 public DefaultInternalKernelServices(final QedeqConfig config, final KernelProperties kernel,
0118 final QedeqFileDao loader) {
0119 this.config = config;
0120 this.kernel = kernel;
0121 this.qedeqFileDao = loader;
0122 processManager = new ServiceProcessManager();
0123 pluginManager = new PluginManager(this, processManager);
0124 loader.setServices(this);
0125
0126 // pluginManager.addPlugin(MultiProofFinderPlugin.class.getName());
0127 pluginManager.addPlugin("org.qedeq.kernel.bo.service.unicode.Qedeq2UnicodeTextPlugin");
0128 pluginManager.addPlugin("org.qedeq.kernel.bo.service.latex.Qedeq2LatexPlugin");
0129 pluginManager.addPlugin("org.qedeq.kernel.bo.service.unicode.Qedeq2Utf8Plugin");
0130 // pluginManager.addPlugin("org.qedeq.kernel.bo.service.heuristic.HeuristicCheckerPlugin");
0131 pluginManager.addPlugin(FormalProofCheckerPlugin.class.getName());
0132 pluginManager.addPlugin("org.qedeq.kernel.bo.service.heuristic.DynamicHeuristicCheckerPlugin");
0133 pluginManager.addPlugin(SimpleProofFinderPlugin.class.getName());
0134
0135 }
0136
0137 public void startupServices() {
0138 modules = new KernelQedeqBoStorage();
0139 if (config.isAutoReloadLastSessionChecked()) {
0140 autoReloadLastSessionChecked();
0141 }
0142 }
0143
0144 public void shutdownServices() {
0145 processManager.terminateAndRemoveAllServiceProcesses();
0146 modules.removeAllModules();
0147 modules = null;
0148 // clear thread interrupt flag because we might have interrupted ourself
0149 Thread.interrupted();
0150 }
0151
0152 /**
0153 * If configured load all QEDEQ modules that where successfully loaded the last time.
0154 */
0155 public void autoReloadLastSessionChecked() {
0156 if (config.isAutoReloadLastSessionChecked()) {
0157 final Thread thread = new Thread() {
0158 public void run() {
0159 final String method = "autoReloadLastSessionChecked.thread.run()";
0160 try {
0161 Trace.begin(CLASS, this, method);
0162 QedeqLog.getInstance().logMessage(
0163 "Trying to load previously successfully loaded modules.");
0164 final int number = config.getPreviouslyCheckedModules().length;
0165 if (loadPreviouslySuccessfullyLoadedModules()) {
0166 QedeqLog.getInstance().logMessage(
0167 "Loading of " + number + " previously successfully loaded module"
0168 + (number != 1 ? "s" : "") + " successfully done.");
0169 } else {
0170 QedeqLog.getInstance().logMessage(
0171 "Loading of all previously successfully checked modules failed. "
0172 + number + " module" + (number != 1 ? "s" : "")
0173 + " were tried.");
0174 }
0175 } catch (Exception e) {
0176 Trace.trace(CLASS, this, method, e);
0177 } finally {
0178 Trace.end(CLASS, this, method);
0179 }
0180 }
0181 };
0182 thread.setDaemon(true);
0183 thread.start();
0184 }
0185 }
0186
0187 public void removeAllModules() {
0188 do {
0189 synchronized (this) {
0190 if (processCounter == 0) {
0191 getModules().removeAllModules();
0192 return;
0193 }
0194 }
0195 // we must wait for the other processes to stop (so that processCounter == 0)
0196 synchronized (MONITOR) {
0197 try {
0198 MONITOR.wait(10000);
0199 } catch (InterruptedException e) {
0200 }
0201 }
0202 } while (true);
0203
0204 }
0205
0206 /**
0207 * Remove a QEDEQ module from memory.
0208 *
0209 * @param address Remove module identified by this address.
0210 */
0211 public void removeModule(final ModuleAddress address) {
0212 final QedeqBo prop = getQedeqBo(address);
0213 if (prop != null) {
0214 QedeqLog.getInstance().logRequest("Removing module", address.getUrl());
0215 try {
0216 removeModule(getModules().getKernelQedeqBo(this, address));
0217 } catch (final RuntimeException e) {
0218 QedeqLog.getInstance().logFailureReply(
0219 "Remove failed", address.getUrl(), e.getMessage());
0220 }
0221
0222 if (validate) {
0223 modules.validateDependencies();
0224 }
0225 }
0226 }
0227
0228 /**
0229 * Remove a QEDEQ module from memory. This method must block all other methods and if this
0230 * method runs no other is allowed to run
0231 *
0232 * @param prop Remove module identified by this property.
0233 */
0234 private void removeModule(final DefaultKernelQedeqBo prop) {
0235 do {
0236 synchronized (this) {
0237 if (processCounter == 0) { // no other method is allowed to run
0238 // TODO mime 20080319: one could call prop.setLoadingProgressState(
0239 // LoadingState.STATE_DELETED) alone but that would
0240 // miss to inform the KernelQedeqBoPool. How do we inform the pool?
0241 // must the StateManager have a reference to it?
0242 prop.delete();
0243 getModules().removeModule(prop);
0244 return;
0245 }
0246 }
0247 // we must wait for the other processes to stop (so that processCounter == 0)
0248 synchronized (MONITOR) {
0249 try {
0250 MONITOR.wait(10000);
0251 } catch (InterruptedException e) {
0252 }
0253 }
0254 } while (true);
0255
0256 }
0257
0258 /**
0259 * Clear local file buffer and all loaded QEDEQ modules.
0260 *
0261 * @return Successful?
0262 */
0263 public boolean clearLocalBuffer() {
0264 final String method = "clearLocalBuffer";
0265 try {
0266 QedeqLog.getInstance().logMessage(
0267 "Clear local buffer from all QEDEQ files.");
0268 removeAllModules();
0269 final File bufferDir = getBufferDirectory().getCanonicalFile();
0270 if (bufferDir.exists() && !IoUtility.deleteDir(bufferDir, new FileFilter() {
0271 public boolean accept(final File pathname) {
0272 return pathname.getName().endsWith(".xml");
0273 }
0274 })) {
0275 throw new IOException("buffer could not be deleted: " + bufferDir);
0276 }
0277 QedeqLog.getInstance().logMessage("Local buffer was cleared.");
0278 return true;
0279 } catch (IOException e) {
0280 Trace.fatal(CLASS, this, method, "IO access problem", e);
0281 QedeqLog.getInstance().logMessage(
0282 "Local buffer not cleared. IO access problem. " + e.getMessage());
0283 return false;
0284 } catch (final RuntimeException e) {
0285 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0286 QedeqLog.getInstance().logMessage(
0287 "Local buffer not cleared. " + e.getMessage());
0288 return false;
0289 }
0290 }
0291
0292 public QedeqBo loadModule(final ModuleAddress address) {
0293 final String method = "loadModule(ModuleAddress)";
0294 processInc();
0295 final DefaultKernelQedeqBo prop = getModules().getKernelQedeqBo(this, address);
0296 try {
0297 synchronized (prop) {
0298 if (prop.isLoaded()) {
0299 return prop;
0300 }
0301 QedeqLog.getInstance().logRequest("Load module", address.getUrl());
0302 if (prop.getModuleAddress().isFileAddress()) {
0303 loadLocalModule(prop);
0304 } else {
0305 // search in local file buffer
0306 try {
0307 getCanonicalReadableFile(prop);
0308 } catch (ModuleFileNotFoundException e) { // file not found
0309 // we will continue by creating a local copy
0310 saveQedeqFromWebToBuffer(prop);
0311 }
0312 loadBufferedModule(prop);
0313 }
0314 QedeqLog.getInstance().logSuccessfulReply(
0315 "Successfully loaded", address.getUrl());
0316 }
0317 } catch (SourceFileExceptionList e) {
0318 Trace.trace(CLASS, this, method, e);
0319 QedeqLog.getInstance().logFailureState("Loading of module failed!", address.getUrl(),
0320 e.toString());
0321 } catch (final RuntimeException e) {
0322 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0323 QedeqLog.getInstance().logFailureReply("Loading failed", address.getUrl(), e.getMessage());
0324 } finally {
0325 processDec();
0326 }
0327 return prop;
0328 }
0329
0330 /**
0331 * Load buffered QEDEQ module file.
0332 *
0333 * @param prop Load this.
0334 * @throws SourceFileExceptionList Loading or QEDEQ module failed.
0335 */
0336 private void loadBufferedModule(final DefaultKernelQedeqBo prop)
0337 throws SourceFileExceptionList {
0338 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_BUFFER);
0339 final File localFile;
0340 try {
0341 localFile = getCanonicalReadableFile(prop);
0342 } catch (ModuleFileNotFoundException e) {
0343 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0344 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_CODE,
0345 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_TEXT,
0346 prop.getUrl(), e);
0347 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
0348 throw sfl;
0349 }
0350
0351 prop.setQedeqFileDao(getQedeqFileDao()); // remember loader for this module
0352 final Qedeq qedeq;
0353 try {
0354 qedeq = getQedeqFileDao().loadQedeq(prop, localFile);
0355 } catch (SourceFileExceptionList sfl) {
0356 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_BUFFER_FAILED, sfl);
0357 throw sfl;
0358 }
0359 setCopiedQedeq(prop, qedeq);
0360 }
0361
0362 /**
0363 * Load QEDEQ module file with file loader.
0364 *
0365 * @param prop Load this.
0366 * @throws SourceFileExceptionList Loading or copying QEDEQ module failed.
0367 */
0368 private void loadLocalModule(final DefaultKernelQedeqBo prop) throws SourceFileExceptionList {
0369 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE);
0370 final File localFile;
0371 try {
0372 localFile = getCanonicalReadableFile(prop);
0373 } catch (ModuleFileNotFoundException e) {
0374 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0375 ServiceErrors.LOADING_FROM_LOCAL_FILE_FAILED_CODE,
0376 ServiceErrors.LOADING_FROM_LOCAL_FILE_FAILED_TEXT,
0377 prop.getUrl(), e);
0378 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE_FAILED, sfl);
0379 throw sfl;
0380 }
0381 prop.setQedeqFileDao(getQedeqFileDao()); // remember loader for this module
0382
0383 final Qedeq qedeq;
0384 try {
0385 qedeq = getQedeqFileDao().loadQedeq(prop, localFile);
0386 } catch (SourceFileExceptionList sfl) {
0387 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_LOCAL_FILE_FAILED, sfl);
0388 throw sfl;
0389 }
0390 setCopiedQedeq(prop, qedeq);
0391 }
0392
0393 private void setCopiedQedeq(final DefaultKernelQedeqBo prop, final Qedeq qedeq)
0394 throws SourceFileExceptionList {
0395 final String method = "setCopiedQedeq(DefaultKernelQedeqBo, Qedeq)";
0396 prop.setLoadingProgressState(LoadingState.STATE_LOADING_INTO_MEMORY);
0397 QedeqVo vo = null;
0398 try {
0399 vo = QedeqVoBuilder.createQedeq(prop.getModuleAddress(), qedeq);
0400 } catch (RuntimeException e) {
0401 Trace.fatal(CLASS, this, method, "looks like a programming error", e);
0402 final SourceFileExceptionList xl = createSourceFileExceptionList(
0403 ServiceErrors.RUNTIME_ERROR_CODE,
0404 ServiceErrors.RUNTIME_ERROR_TEXT,
0405 prop.getModuleAddress().getUrl(), e);
0406 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, xl);
0407 throw xl;
0408 } catch (ModuleDataException e) {
0409 if (e.getCause() != null) {
0410 Trace.fatal(CLASS, this, method, "looks like a programming error", e.getCause());
0411 } else {
0412 Trace.fatal(CLASS, this, method, "looks like a programming error", e);
0413 }
0414 final SourceFileExceptionList xl = prop.createSourceFileExceptionList(this, e, qedeq);
0415 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, xl);
0416 throw xl;
0417 }
0418 prop.setQedeqVo(vo);
0419 // TODO 20110213 m31: perhaps we need a new state, pre loaded? So when we put more
0420 // label testing into the moduleLabelCreator, we still can launch some plugins
0421 // On the other side: Label checking is only possible, if all referenced modules can
0422 // be loaded.
0423 //
0424 // Correct labels are necessary for many plugins (e.g. LaTeX and UTF-8 generation).
0425 // So a label checker must be run before that.
0426 // It might be a good idea to put it into the formal logic checker.
0427 // We could make a FormalChecker plugin. This starts loading required modules, checks
0428 // the labels and checks if the formulas are correctly written.
0429 // So we get some sub status (for every check) and an overall status (all checks
0430 // green). Later on the formal proof checker can be integrated too.
0431 // This should be the extended load status.
0432 final ModuleLabelsCreator moduleNodesCreator = new ModuleLabelsCreator(this, prop);
0433 try {
0434 moduleNodesCreator.createLabels();
0435 prop.setLoaded(vo, moduleNodesCreator.getLabels(), moduleNodesCreator.getConverter(),
0436 moduleNodesCreator.getTextConverter());
0437 } catch (SourceFileExceptionList sfl) {
0438 prop.setLoadingFailureState(LoadingState.STATE_LOADING_INTO_MEMORY_FAILED, sfl);
0439 throw sfl;
0440 }
0441 }
0442
0443 /**
0444 * Check if file exists and is readable. Checks the local buffer file for a buffered module or
0445 * the module file address directly. Returns canonical file path.
0446 *
0447 * @param prop Check for this file.
0448 * @return Canonical file path.
0449 * @throws ModuleFileNotFoundException File doesn't exist or is not readable.
0450 */
0451 private File getCanonicalReadableFile(final QedeqBo prop) throws ModuleFileNotFoundException {
0452 final String method = "getCanonicalReadableFile(File)";
0453 final File localFile = getLocalFilePath(prop.getModuleAddress());
0454 final File file;
0455 try {
0456 file = localFile.getCanonicalFile();
0457 } catch (IOException e) {
0458 Trace.trace(CLASS, this, method, e);
0459 throw new ModuleFileNotFoundException("file path not correct: " + localFile);
0460 }
0461 if (!file.canRead()) {
0462 Trace.trace(CLASS, this, method, "file not readable=" + file);
0463 throw new ModuleFileNotFoundException("file not readable: " + file);
0464 }
0465 return file;
0466 }
0467
0468 /**
0469 * Load specified QEDEQ module from QEDEQ parent module.
0470 *
0471 * @param parent Parent module address.
0472 * @param spec Specification for another QEDEQ module.
0473 * @return Loaded module.
0474 * @throws SourceFileExceptionList Loading failed.
0475 */
0476 public KernelQedeqBo loadModule(final ModuleAddress parent, final Specification spec)
0477 throws SourceFileExceptionList {
0478
0479 final String method = "loadModule(Module, Specification)";
0480 Trace.begin(CLASS, this, method);
0481 Trace.trace(CLASS, this, method, spec);
0482 processInc();
0483 DefaultKernelQedeqBo prop = null; // currently tried module
0484 try {
0485 final ModuleAddress[] modulePaths;
0486 try {
0487 modulePaths = parent.getModulePaths(spec);
0488 } catch (IOException e) {
0489 Trace.fatal(CLASS, this, method, "getting module path failed", e); // TODO 20110308 m31: make constant
0490 throw createSourceFileExceptionList(
0491 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_CODE,
0492 ServiceErrors.LOADING_FROM_FILE_BUFFER_FAILED_TEXT,
0493 parent.getUrl(), e);
0494 }
0495
0496 // now we iterate over the possible module addresses
0497 for (int i = 0; i < modulePaths.length; i++) {
0498 prop = getModules().getKernelQedeqBo(this, modulePaths[i]);
0499 Trace.trace(CLASS, this, method, "synchronizing at prop=" + prop);
0500 synchronized (prop) {
0501 if (prop.isLoaded()) {
0502 return (prop);
0503 }
0504 try {
0505 if (prop.getModuleAddress().isFileAddress()) {
0506 loadLocalModule(prop);
0507 } else {
0508 // search in local file buffer
0509 try {
0510 getCanonicalReadableFile(prop);
0511 } catch (ModuleFileNotFoundException e) { // file not found
0512 // we will continue by creating a local copy
0513 saveQedeqFromWebToBuffer(prop);
0514 }
0515 loadBufferedModule(prop);
0516 }
0517 // success!
0518 return prop;
0519 } catch (SourceFileExceptionList e) {
0520 Trace.trace(CLASS, this, method, e);
0521 if (i + 1 < modulePaths.length) {
0522 QedeqLog.getInstance().logMessage("trying alternate path");
0523 // we continue with the next path
0524 } else {
0525 // we surrender
0526 throw e;
0527 }
0528 }
0529 }
0530 }
0531 return prop; // never called, only here to soothe the compiler
0532 } catch (final RuntimeException e) {
0533 Trace.fatal(CLASS, this, method, "unexpected problem", e);
0534 QedeqLog.getInstance().logFailureReply("Loading failed", prop.getUrl(), e.getMessage());
0535 throw e;
0536 } finally {
0537 processDec();
0538 Trace.end(CLASS, this, method);
0539 }
0540 }
0541
0542 public ModuleAddress[] getAllLoadedModules() {
0543 return getModules().getAllLoadedModules();
0544 }
0545
0546 public boolean loadRequiredModules(final ModuleAddress address) {
0547 final DefaultKernelQedeqBo prop = (DefaultKernelQedeqBo) loadModule(address);
0548 if (prop.hasBasicFailures()) {
0549 return false;
0550 }
0551 return LoadRequiredModules.loadRequired(this, prop);
0552 }
0553
0554 /**
0555 * Load all previously checked QEDEQ modules.
0556 *
0557 * @return Successfully reloaded all modules.
0558 */
0559 public boolean loadPreviouslySuccessfullyLoadedModules() {
0560 processInc();
0561 try {
0562 final String[] list = config.getPreviouslyCheckedModules();
0563 boolean errors = false;
0564 for (int i = 0; i < list.length; i++) {
0565 try {
0566 final ModuleAddress address = getModuleAddress(list[i]);
0567 final QedeqBo prop = loadModule(address);
0568 if (prop.hasErrors()) {
0569 errors = true;
0570 }
0571 } catch (IOException e) {
0572 Trace.fatal(CLASS, this, "loadPreviouslySuccessfullyLoadedModules",
0573 "internal error: " + "saved URLs are malformed", e);
0574 errors = true;
0575 }
0576 }
0577 return !errors;
0578 } finally {
0579 processDec();
0580 }
0581 }
0582
0583 // LATER mime 20070326: dynamic loading from web page directory
0584 public boolean loadAllModulesFromQedeq() {
0585 processInc();
0586 try {
0587 final String prefix = "http://www.qedeq.org/" + kernel.getKernelVersionDirectory() + "/";
0588 final String[] list = new String[] {
0589 prefix + "doc/math/qedeq_logic_v1.xml",
0590 prefix + "doc/math/qedeq_formal_logic_v1.xml",
0591 prefix + "doc/math/qedeq_set_theory_v1.xml",
0592 prefix + "doc/project/qedeq_basic_concept.xml",
0593 prefix + "doc/project/qedeq_logic_language.xml",
0594 prefix + "sample/qedeq_sample1.xml",
0595 prefix + "sample/qedeq_sample2.xml",
0596 prefix + "sample/qedeq_sample3.xml",
0597 prefix + "sample/qedeq_sample4.xml",
0598 prefix + "sample/qedeq_error_sample_00.xml",
0599 prefix + "sample/qedeq_error_sample_01.xml",
0600 prefix + "sample/qedeq_error_sample_02.xml",
0601 prefix + "sample/qedeq_error_sample_03.xml",
0602 prefix + "sample/qedeq_error_sample_04.xml",
0603 prefix + "sample/qedeq_error_sample_05.xml",
0604 prefix + "sample/qedeq_error_sample_12.xml",
0605 prefix + "sample/qedeq_error_sample_13.xml",
0606 prefix + "sample/qedeq_error_sample_14.xml",
0607 prefix + "sample/qedeq_error_sample_15.xml",
0608 prefix + "sample/qedeq_error_sample_16.xml",
0609 prefix + "sample/qedeq_error_sample_17.xml",
0610 prefix + "sample/qedeq_error_sample_18.xml"};
0611 boolean errors = false;
0612 for (int i = 0; i < list.length; i++) {
0613 try {
0614 final ModuleAddress address = getModuleAddress(list[i]);
0615 final QedeqBo prop = loadModule(address);
0616 if (prop.hasErrors()) {
0617 errors = true;
0618 }
0619 } catch (IOException e) {
0620 Trace.fatal(CLASS, this, "loadPreviouslySuccessfullyLoadedModules",
0621 "internal error: " + "saved URLs are malformed", e);
0622 errors = true;
0623 }
0624 }
0625 return !errors;
0626 } finally {
0627 processDec();
0628 }
0629 }
0630
0631 /**
0632 * Make local copy of a module if it is no file address.
0633 *
0634 * @param prop Module properties.
0635 * @throws SourceFileExceptionList Address was malformed or the file can not be found.
0636 */
0637 private void saveQedeqFromWebToBuffer(final DefaultKernelQedeqBo prop)
0638 throws SourceFileExceptionList {
0639 final String method = "saveQedeqFromWebToBuffer(DefaultKernelQedeqBo)";
0640 Trace.begin(CLASS, this, method);
0641
0642 // if we are not web started and running under Java 1.4 we use apache commons
0643 // httpclient library (so we can set timeouts)
0644 if (!KernelContext.getInstance().isSetConnectionTimeOutSupported()
0645 && !IoUtility.isWebStarted()) {
0646 saveQedeqFromWebToBufferApache(prop);
0647 Trace.end(CLASS, this, method);
0648 return;
0649 }
0650
0651 // set proxy properties according to kernel configuration (if not webstarted)
0652 if (!IoUtility.isWebStarted()) {
0653 if (config.getHttpProxyHost() != null) {
0654 System.setProperty("http.proxyHost", config.getHttpProxyHost());
0655 }
0656 if (config.getHttpProxyPort() != null) {
0657 System.setProperty("http.proxyPort", config.getHttpProxyPort());
0658 }
0659 if (config.getHttpNonProxyHosts() != null) {
0660 System.setProperty("http.nonProxyHosts", config.getHttpNonProxyHosts());
0661 }
0662 }
0663
0664 if (prop.getModuleAddress().isFileAddress()) { // this is already a local file
0665 Trace.fatal(CLASS, this, method, "tried to make a local copy for a local module", null);
0666 Trace.end(CLASS, this, method);
0667 return;
0668 }
0669 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_WEB);
0670
0671 FileOutputStream out = null;
0672 InputStream in = null;
0673 final File f = getLocalFilePath(prop.getModuleAddress());
0674 try {
0675 final URLConnection connection = new URL(prop.getUrl()).openConnection();
0676
0677 if (connection instanceof HttpURLConnection) {
0678 final HttpURLConnection httpConnection = (HttpURLConnection) connection;
0679 // if we are running at least under Java 1.5 the following code should be executed
0680 if (KernelContext.getInstance().isSetConnectionTimeOutSupported()) {
0681 try {
0682 YodaUtility.executeMethod(httpConnection, "setConnectTimeout",
0683 new Class[] {Integer.TYPE}, new Object[] {new Integer(
0684 config.getConnectTimeout())});
0685 } catch (NoSuchMethodException e) {
0686 Trace.fatal(CLASS, this, method,
0687 "URLConnection.setConnectTimeout was previously found", e);
0688 } catch (InvocationTargetException e) {
0689 Trace.fatal(CLASS, this, method,
0690 "URLConnection.setConnectTimeout throwed an error", e);
0691 }
0692 }
0693 // if we are running at least under Java 1.5 the following code should be executed
0694 if (KernelContext.getInstance().isSetReadTimeoutSupported()) {
0695 try {
0696 YodaUtility.executeMethod(httpConnection, "setReadTimeout",
0697 new Class[] {Integer.TYPE}, new Object[] {new Integer(
0698 config.getReadTimeout())});
0699 } catch (NoSuchMethodException e) {
0700 Trace.fatal(CLASS, this, method,
0701 "URLConnection.setReadTimeout was previously found", e);
0702 } catch (InvocationTargetException e) {
0703 Trace.fatal(CLASS, this, method,
0704 "URLConnection.setReadTimeout throwed an error", e);
0705 }
0706 }
0707 int responseCode = httpConnection.getResponseCode();
0708 if (responseCode == 200) {
0709 in = httpConnection.getInputStream();
0710 } else {
0711 in = httpConnection.getErrorStream();
0712 final String errorText = IoUtility.loadStreamWithoutException(in, 1000);
0713 throw new IOException("Response code from HTTP server was " + responseCode
0714 + (errorText.length() > 0 ? "\nResponse text from HTTP server was:\n"
0715 + errorText : ""));
0716 }
0717 } else {
0718 Trace.paramInfo(CLASS, this, method, "connection.getClass", connection.getClass()
0719 .toString());
0720 in = connection.getInputStream();
0721 }
0722
0723 if (!prop.getUrl().equals(connection.getURL().toString())) {
0724 throw new FileNotFoundException("\"" + prop.getUrl() + "\" was substituted by "
0725 + "\"" + connection.getURL() + "\" from server");
0726 }
0727 final int maximum = connection.getContentLength();
0728 IoUtility.createNecessaryDirectories(f);
0729 out = new FileOutputStream(f);
0730 final byte[] buffer = new byte[4096];
0731 int bytesRead; // bytes read during one buffer read
0732 int position = 0; // current reading position within the whole document
0733 // continue writing
0734 while ((bytesRead = in.read(buffer)) != -1) {
0735 position += bytesRead;
0736 out.write(buffer, 0, bytesRead);
0737 if (maximum > 0) {
0738 long completeness = (long) (position * 100 / maximum);
0739 if (completeness < 0) {
0740 completeness = 0;
0741 }
0742 if (completeness > 100) {
0743 completeness = 100;
0744 }
0745 prop.setLoadingCompleteness((int) completeness);
0746 }
0747 }
0748 prop.setLoadingCompleteness(100);
0749 } catch (IOException e) {
0750 Trace.trace(CLASS, this, method, e);
0751 IoUtility.close(out);
0752 out = null;
0753 try {
0754 f.delete();
0755 } catch (Exception ex) {
0756 Trace.trace(CLASS, this, method, ex);
0757 }
0758 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0759 ServiceErrors.LOADING_FROM_WEB_FAILED_CODE,
0760 ServiceErrors.LOADING_FROM_WEB_FAILED_TEXT,
0761 prop.getUrl(), e);
0762 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_WEB_FAILED, sfl);
0763 Trace.trace(CLASS, this, method, "Couldn't access " + prop.getUrl());
0764 throw sfl;
0765 } finally {
0766 IoUtility.close(out);
0767 IoUtility.close(in);
0768 Trace.end(CLASS, this, method);
0769 }
0770 }
0771
0772 /**
0773 * Make local copy of a http accessable module if it is no file address.
0774 * This method uses apaches HttpClient, but it dosn't work under webstart with proxy
0775 * configuration. If we don't use this method, the apache commons-httpclient
0776 * library can be removed
0777 *
0778 * @param prop Module properties.
0779 * @throws SourceFileExceptionList Address was malformed or the file can not be found.
0780 */
0781 private void saveQedeqFromWebToBufferApache(final DefaultKernelQedeqBo prop)
0782 throws SourceFileExceptionList {
0783 final String method = "saveQedeqFromWebToBufferOld(DefaultKernelQedeqBo)";
0784 Trace.begin(CLASS, this, method);
0785
0786 if (prop.getModuleAddress().isFileAddress()) { // this is already a local file
0787 Trace.fatal(CLASS, this, method, "tried to make a local copy for a local module", null);
0788 Trace.end(CLASS, this, method);
0789 return;
0790 }
0791 prop.setLoadingProgressState(LoadingState.STATE_LOADING_FROM_WEB);
0792
0793 final File f = getLocalFilePath(prop.getModuleAddress());
0794 // Create an instance of HttpClient.
0795 HttpClient client = new HttpClient();
0796
0797 // set proxy properties according to kernel configuration (if not webstarted)
0798 if (!IoUtility.isWebStarted() && config.getHttpProxyHost() != null) {
0799 final String pHost = config.getHttpProxyHost();
0800 int pPort = 80;
0801 if (config.getHttpProxyPort() != null) {
0802 try {
0803 pPort = Integer.parseInt(config.getHttpProxyPort());
0804 } catch (RuntimeException e) {
0805 Trace.fatal(CLASS, this, method, "proxy port not numeric: "
0806 + config.getHttpProxyPort(), e);
0807 }
0808 }
0809 if (pHost.length() > 0) {
0810 client.getHostConfiguration().setProxy(pHost, pPort);
0811 }
0812 }
0813
0814 // Create a method instance.
0815 GetMethod httpMethod = new GetMethod(prop.getUrl());
0816
0817 try {
0818 // Provide custom retry handler is necessary
0819 httpMethod.getParams().setParameter(HttpMethodParams.RETRY_HANDLER,
0820 new DefaultHttpMethodRetryHandler(3, false));
0821
0822 httpMethod.getParams().setSoTimeout(config.getConnectTimeout());
0823 // Throws IOException on TimeOut.
0824
0825 int statusCode = client.executeMethod(httpMethod);
0826
0827 if (statusCode != HttpStatus.SC_OK) {
0828 throw new FileNotFoundException("Problems loading: " + prop.getUrl() + "\n"
0829 + httpMethod.getStatusLine());
0830 }
0831
0832 // Read the response body.
0833 byte[] responseBody = httpMethod.getResponseBody();
0834 IoUtility.createNecessaryDirectories(f);
0835 IoUtility.saveFileBinary(f, responseBody);
0836 prop.setLoadingCompleteness(100);
0837 } catch (IOException e) {
0838 Trace.trace(CLASS, this, method, e);
0839 try {
0840 f.delete();
0841 } catch (Exception ex) {
0842 Trace.trace(CLASS, this, method, ex);
0843 }
0844 final SourceFileExceptionList sfl = createSourceFileExceptionList(
0845 ServiceErrors.LOADING_FROM_WEB_FAILED_CODE,
0846 ServiceErrors.LOADING_FROM_WEB_FAILED_TEXT,
0847 prop.getUrl(), e);
0848 prop.setLoadingFailureState(LoadingState.STATE_LOADING_FROM_WEB_FAILED, sfl);
0849 Trace.trace(CLASS, this, method, "Couldn't access " + prop.getUrl());
0850 throw sfl;
0851 } finally {
0852 // Release the connection.
0853 httpMethod.releaseConnection();
0854 Trace.end(CLASS, this, method);
0855 }
0856 }
0857
0858 public final File getLocalFilePath(final ModuleAddress address) {
0859 final String method = "getLocalFilePath(ModuleAddress)";
0860 URL url;
0861 try {
0862 url = new URL(address.getUrl());
0863 } catch (MalformedURLException e) {
0864 Trace.fatal(CLASS, this, method, "Could not get local file path.", e);
0865 return null;
0866 }
0867 Trace.param(CLASS, this, method, "protocol", url.getProtocol());
0868 Trace.param(CLASS, this, method, "host", url.getHost());
0869 Trace.param(CLASS, this, method, "port", url.getPort());
0870 Trace.param(CLASS, this, method, "path", url.getPath());
0871 Trace.param(CLASS, this, method, "file", url.getFile());
0872 if (address.isFileAddress()) {
0873 try {
0874 return IoUtility.toFile(url.getFile());
0875 } catch (IllegalArgumentException e) {
0876 // should not occur because check for validy must be done in constructor of address
0877 Trace.fatal(CLASS, this, method, "Loading failed of local file with URL=" + url, e);
0878 throw new RuntimeException(e);
0879 }
0880 }
0881 StringBuffer file = new StringBuffer(url.getFile());
0882 StringUtility.replace(file, "_", "_1"); // remember all '_'
0883 StringUtility.replace(file, "/", "_2"); // preserve all '/'
0884 String encoded = file.toString(); // fallback file name
0885 try {
0886 encoded = URLEncoder.encode(file.toString(), "UTF-8");
0887 } catch (UnsupportedEncodingException e) {
0888 // should not occur
0889 Trace.trace(CLASS, method, e);
0890 }
0891 file.setLength(0);
0892 file.append(encoded);
0893 StringUtility.replace(file, "#", "##"); // escape all '#'
0894 StringUtility.replace(file, "_2", "#"); // from '/' into '#'
0895 StringUtility.replace(file, "_1", "_"); // from '_' into '_'
0896 // mime 2010-06-25: use if we throw no RuntimException
0897 // StringBuffer adr = new StringBuffer(url.toExternalForm());
0898 final StringBuffer adr;
0899 try {
0900 adr = new StringBuffer(new URL(url.getProtocol(), url.getHost(), url.getPort(), file
0901 .toString()).toExternalForm());
0902 } catch (MalformedURLException e) {
0903 Trace.fatal(CLASS, this, method, "unexpected", e);
0904 throw new RuntimeException(e);
0905 }
0906 // escape characters:
0907 StringUtility.replace(adr, "://", "_"); // before host
0908 StringUtility.replace(adr, ":", "_"); // before protocol
0909 return new File(getBufferDirectory(), adr.toString());
0910 }
0911
0912 /**
0913 * Increment intern process counter.
0914 */
0915 private synchronized void processInc() {
0916 this.processCounter++;
0917 }
0918
0919 /**
0920 * Decrement intern process counter.
0921 */
0922 private synchronized void processDec() {
0923 this.processCounter--;
0924 }
0925
0926 public File getBufferDirectory() {
0927 return config.getBufferDirectory();
0928 }
0929
0930 public File getGenerationDirectory() {
0931 return config.getGenerationDirectory();
0932 }
0933
0934 public KernelQedeqBo getKernelQedeqBo(final ModuleAddress address) {
0935 return getModules().getKernelQedeqBo(this, address);
0936 }
0937
0938 public QedeqBo getQedeqBo(final ModuleAddress address) {
0939 return getModules().getKernelQedeqBo(this, address);
0940 }
0941
0942 public ModuleAddress getModuleAddress(final URL url) throws IOException {
0943 return new DefaultModuleAddress(url);
0944 }
0945
0946 public ModuleAddress getModuleAddress(final String url) throws IOException {
0947 return new DefaultModuleAddress(url);
0948 }
0949
0950 public ModuleAddress getModuleAddress(final File file) throws IOException {
0951 return new DefaultModuleAddress(file);
0952 }
0953
0954 public String getSource(final ModuleAddress address) throws IOException {
0955 final KernelQedeqBo bo = getKernelQedeqBo(address);
0956 if (bo.getLoadingState().equals(LoadingState.STATE_UNDEFINED)
0957 || bo.getLoadingState().equals(LoadingState.STATE_LOADING_FROM_WEB)
0958 || bo.getLoadingState().equals(LoadingState.STATE_LOADING_FROM_WEB_FAILED)) {
0959 return null;
0960 }
0961 final StringBuffer buffer = new StringBuffer();
0962 final Reader reader = getQedeqFileDao().getModuleReader(bo);
0963 try {
0964 IoUtility.loadReader(reader, buffer);
0965 } finally {
0966 IoUtility.close(reader);
0967 }
0968 return buffer.toString();
0969 }
0970
0971 public boolean checkModule(final ModuleAddress address) {
0972 final String method = "checkModule(ModuleAddress)";
0973 final DefaultKernelQedeqBo prop = modules.getKernelQedeqBo(this, address);
0974 // did we check this already?
0975 if (prop.isChecked()) {
0976 return true; // everything is OK
0977 }
0978 try {
0979 // TODO 20110606 m31: perhaps this should be a real plugin and is managed by the PluginManager?
0980 // perhaps we have to make a difference between normal and hidden internal plugins?
0981 final WellFormedCheckerPlugin checker = new WellFormedCheckerPlugin();
0982 // set default plugin values for not yet set parameters
0983 final Parameters parameters = KernelContext.getInstance().getConfig().getPluginEntries(checker);
0984 checker.setDefaultValuesForEmptyPluginParameters(parameters);
0985 KernelContext.getInstance().getConfig().setPluginKeyValues(checker, parameters);
0986 checker.createExecutor(prop, parameters).executePlugin();
0987 } catch (final RuntimeException e) {
0988 final String msg = "Check of logical correctness failed";
0989 Trace.fatal(CLASS, this, method, msg, e);
0990 QedeqLog.getInstance().logFailureReply(msg, address.getUrl(), e.getMessage());
0991 throw e;
0992 } finally {
0993 if (validate) {
0994 modules.validateDependencies();
0995 }
0996 }
0997 return prop.isChecked();
0998 }
0999
1000 /**
1001 * Add plugin to services.
1002 *
1003 * @param pluginClass Plugin class to instantiate.
1004 * @throws RuntimeException Addition failed.
1005 */
1006 public void addPlugin(final String pluginClass) {
1007 pluginManager.addPlugin(pluginClass);
1008 }
1009
1010 public Plugin[] getPlugins() {
1011 return pluginManager.getPlugins();
1012 }
1013
1014 public Object executePlugin(final String id, final ModuleAddress address) {
1015 return pluginManager.executePlugin(id, getKernelQedeqBo(address));
1016 }
1017
1018 public void clearAllPluginResults(final ModuleAddress address) {
1019 pluginManager.clearAllPluginResults(getKernelQedeqBo(address));
1020 }
1021
1022 public ServiceProcess[] getServiceProcesses() {
1023 return processManager.getServiceProcesses();
1024 }
1025
1026 public void stopAllPluginExecutions() {
1027 processManager.terminateAllServiceProcesses();
1028 }
1029
1030
1031 /**
1032 * Get all loaded QEDEQ modules.
1033 *
1034 * @return All QEDEQ modules.
1035 */
1036 private KernelQedeqBoStorage getModules() {
1037 return modules;
1038 }
1039
1040 public SourceFileExceptionList createSourceFileExceptionList(final int code,
1041 final String message, final String address, final IOException e) {
1042 return new DefaultSourceFileExceptionList(new SourceFileException(this,
1043 code, message, e, new SourceArea(address), null));
1044 }
1045
1046 public SourceFileExceptionList createSourceFileExceptionList(final int code,
1047 final String message, final String address, final RuntimeException e) {
1048 return new DefaultSourceFileExceptionList(new SourceFileException(this,
1049 code, message, e, new SourceArea(address), null));
1050 }
1051
1052 public SourceFileExceptionList createSourceFileExceptionList(final int code,
1053 final String message, final String address, final Exception e) {
1054 return new DefaultSourceFileExceptionList(new SourceFileException(this,
1055 code, message, e, new SourceArea(address), null));
1056 }
1057
1058 /**
1059 * Get description of source file exception list.
1060 *
1061 * @param address Get description for this module exceptions.
1062 * @return Error description and location.
1063 */
1064 public String[] getSourceFileExceptionList(final ModuleAddress address) {
1065 final List list = new ArrayList();
1066 final KernelQedeqBo bo = getKernelQedeqBo(address);
1067 final SourceFileExceptionList sfl = bo.getErrors();
1068 if (sfl.size() > 0) {
1069 final StringBuffer buffer = new StringBuffer();
1070 do {
1071 Reader reader = null;
1072 try {
1073 reader = getQedeqFileDao().getModuleReader(bo);
1074 IoUtility.loadReader(reader, buffer);
1075 } catch (IOException e) {
1076 IoUtility.close(reader);
1077 for (int i = 0; i < sfl.size(); i++) {
1078 list.add(sfl.get(i).getDescription());
1079 }
1080 break; // out of do while
1081 }
1082 final TextInput input = new TextInput(buffer);
1083 try {
1084 input.setPosition(0);
1085 final StringBuffer buf = new StringBuffer();
1086 for (int i = 0; i < sfl.size(); i++) {
1087 buf.setLength(0);
1088 final SourceFileException sf = sfl.get(i);
1089 buf.append(sf.getDescription());
1090 try {
1091 if (sf.getSourceArea() != null
1092 && sf.getSourceArea().getStartPosition() != null) {
1093 buf.append("\n");
1094 input.setRow(sf.getSourceArea().getStartPosition().getRow());
1095 buf.append(StringUtility.replace(input.getLine(), "\t", " "));
1096 buf.append("\n");
1097 final StringBuffer whitespace = StringUtility.getSpaces(sf
1098 .getSourceArea().getStartPosition().getColumn() - 1);
1099 buffer.append(whitespace);
1100 buffer.append("^");
1101 }
1102 } catch (Exception e) {
1103 Trace.trace(CLASS, this, "getSourceFileExceptionList(ModuleAddress)", e);
1104 }
1105 list.add(buf.toString());
1106 }
1107 } finally {
1108 IoUtility.close(input);
1109 }
1110 break; // out of do while
1111 } while (true);
1112 }
1113 return (String[]) list.toArray(new String[list.size()]);
1114 }
1115
1116 public String getPluginId() {
1117 return CLASS.getName();
1118 }
1119
1120 public String getPluginActionName() {
1121 return "Basis";
1122 }
1123 public QedeqFileDao getQedeqFileDao() {
1124 return qedeqFileDao;
1125 }
1126
1127 public String getPluginDescription() {
1128 return "provides basic services for loading QEDEQ modules";
1129 }
1130
1131 public QedeqConfig getConfig() {
1132 return config;
1133 }
1134
1135 public String getKernelVersionDirectory() {
1136 return kernel.getKernelVersionDirectory();
1137 }
1138
1139 public String getBuildId() {
1140 return kernel.getBuildId();
1141 }
1142
1143 public String getDedication() {
1144 return kernel.getDedication();
1145 }
1146
1147 public String getDescriptiveKernelVersion() {
1148 return kernel.getDescriptiveKernelVersion();
1149 }
1150
1151 public String getKernelCodeName() {
1152 return kernel.getKernelCodeName();
1153 }
1154
1155 public String getKernelVersion() {
1156 return kernel.getKernelVersion();
1157 }
1158
1159 public String getMaximalRuleVersion() {
1160 return kernel.getMaximalRuleVersion();
1161 }
1162
1163 public boolean isRuleVersionSupported(final String ruleVersion) {
1164 return kernel.isRuleVersionSupported(ruleVersion);
1165 }
1166
1167 public boolean isSetConnectionTimeOutSupported() {
1168 return kernel.isSetConnectionTimeOutSupported();
1169 }
1170
1171 public boolean isSetReadTimeoutSupported() {
1172 return kernel.isSetReadTimeoutSupported();
1173 }
1174
1175 }
|