From de5f90fe4b31567e842e4b56449a43705bee234f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 29 Sep 2014 15:39:58 +0200 Subject: [PATCH] Rough version of refactored version of processing the options (in terms of computing something). Currently it is only capable of parsing the model and generating a counterexample. Former-commit-id: 6a65cdd6586f8601781c0e3f1a22ab90403a2567 --- .../MILPMinimalLabelSetGenerator.h | 2 + .../SMTMinimalCommandSetGenerator.h | 6 +- src/storm.cpp | 8 +- src/utility/cli.h | 194 +++++++++++++----- 4 files changed, 151 insertions(+), 59 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index d98025597..20656b828 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -12,10 +12,12 @@ #include "src/models/Mdp.h" #include "src/storage/prism/Program.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidStateException.h" +#include "src/utility/graph.h" #include "src/utility/counterexamples.h" #include "src/utility/solver.h" diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 5b3404deb..c961f6fe1 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1781,11 +1781,11 @@ namespace storm { #endif } - static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, std::shared_ptr const> formula) { + static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, std::shared_ptr> const& formula) { #ifdef STORM_HAVE_Z3 std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl; // First, we need to check whether the current formula is an Until-Formula. - std::shared_ptr const> probBoundFormula = std::dynamic_pointer_cast>(formula); + std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formula); if (probBoundFormula.get() == nullptr) { LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."; @@ -1800,7 +1800,7 @@ namespace storm { // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. double bound = probBoundFormula->getBound(); - std::shared_ptr const> pathFormula = probBoundFormula->getChild(); + std::shared_ptr> pathFormula = probBoundFormula->getChild(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); diff --git a/src/storm.cpp b/src/storm.cpp index 6b84773b2..2931b8552 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -14,15 +14,19 @@ int main(const int argc, const char** argv) { try { storm::utility::cli::setUp(); storm::utility::cli::printHeader(argc, argv); - storm::utility::cli::parseOptions(argc, argv); + bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv); + if (!optionsCorrect) { + return -1; + } // From this point on we are ready to carry out the actual computations. storm::utility::cli::processOptions(); // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp(); + return 0; } catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is " << exception.what()); + STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what()); } catch (std::exception const& exception) { STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what()); } diff --git a/src/utility/cli.h b/src/utility/cli.h index f097a6a7c..b428ef4aa 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -6,17 +6,9 @@ #include #include #include +#include -#include "src/utility/OsDetection.h" -#include "src/settings/SettingsManager.h" - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "log4cplus/consoleappender.h" -#include "log4cplus/fileappender.h" -log4cplus::Logger logger; - -// Includes for the linked libraries and versions header +// Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB # include "tbb/tbb_stddef.h" #endif @@ -30,6 +22,34 @@ log4cplus::Logger logger; # include "z3.h" #endif +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" +log4cplus::Logger logger; + +// Headers that provide auxiliary functionality. +#include "src/utility/OsDetection.h" +#include "src/settings/SettingsManager.h" + +// Headers related to parsing. +#include "src/parser/AutoParser.h" +#include "src/parser/PrismParser.h" +#include "src/parser/PrctlParser.h" + +// Model headers. +#include "src/models/AbstractModel.h" + +// Headers of adapters. +#include "src/adapters/ExplicitModelAdapter.h" + +// Headers for counterexample generation. +#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "src/counterexamples/SMTMinimalCommandSetGenerator.h" + +// Headers related to exception handling. +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace utility { namespace cli { @@ -65,7 +85,7 @@ namespace storm { /*! * Sets up the logging to file. */ - void setUpFileLogging() { + void initializeFileLogging() { log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(storm::settings::debugSettings().getLogfilename())); fileLogAppender->setName("mainFileAppender"); fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); @@ -82,6 +102,47 @@ namespace storm { return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); } + /*! + * Prints the header including information about the linked libraries. + */ + void printHeader(const int argc, const char* argv[]) { + std::cout << "StoRM" << std::endl; + std::cout << "-----" << std::endl << std::endl; + + std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH; + if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) { + std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)"; + } + std::cout << " build from revision " << STORM_CPP_VERSION_HASH; + if (STORM_CPP_VERSION_DIRTY == 1) { + std::cout << " (DIRTY)"; + } + std::cout << "." << std::endl; + +#ifdef STORM_HAVE_INTELTBB + std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; +#endif +#ifdef STORM_HAVE_GLPK + std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; +#endif +#ifdef STORM_HAVE_GUROBI + std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; +#endif +#ifdef STORM_HAVE_Z3 + unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; + Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); + std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; +#endif + + // "Compute" the command line argument string with which STORM was invoked. + std::stringstream commandStream; + for (int i = 0; i < argc; ++i) { + commandStream << argv[i] << " "; + } + std::cout << "Command line: " << commandStream.str() << std::endl; + std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; + } + void printUsage() { #ifndef WINDOWS @@ -126,48 +187,6 @@ namespace storm { } - - /*! - * Prints the header. - */ - void printHeader(const int argc, const char* argv[]) { - std::cout << "StoRM" << std::endl; - std::cout << "-----" << std::endl << std::endl; - - std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH; - if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) { - std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)"; - } - std::cout << " build from revision " << STORM_CPP_VERSION_HASH; - if (STORM_CPP_VERSION_DIRTY == 1) { - std::cout << " (DIRTY)"; - } - std::cout << "." << std::endl; - -#ifdef STORM_HAVE_INTELTBB - std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; -#endif -#ifdef STORM_HAVE_GLPK - std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; -#endif -#ifdef STORM_HAVE_GUROBI - std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; -#endif -#ifdef STORM_HAVE_Z3 - unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; - Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); - std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; -#endif - - // "Compute" the command line argument string with which STORM was invoked. - std::stringstream commandStream; - for (int i = 0; i < argc; ++i) { - commandStream << argv[i] << " "; - } - std::cout << "Command line: " << commandStream.str() << std::endl; - std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; - } - /*! * Parses the given command line arguments. * @@ -206,13 +225,80 @@ namespace storm { LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); } if (storm::settings::debugSettings().isLogfileSet()) { - setUpFileLogging(); + initializeFileLogging(); } return true; } + template + std::shared_ptr> buildModel() { + std::shared_ptr> result(nullptr); + + storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); + + if (settings.isExplicitSet()) { + std::string const transitionFile = settings.getTransitionFilename(); + std::string const labelingFile = settings.getLabelingFilename(); + + // Parse (and therefore build) the model. + result = storm::parser::AutoParser::parseModel(transitionFile, labelingFile, settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : "", settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : ""); + } else if (settings.isSymbolicSet()) { + std::string const programFile = settings.getSymbolicModelFilename(); + std::string const constants = settings.getConstantDefinitionString(); + + // Start by parsing the symbolic model file. + storm::prism::Program program = storm::parser::PrismParser::parse(programFile); + + // Then, build the model from the symbolic description. + result = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); + } + + return result; + } + + void generateCounterexample(std::shared_ptr> model, std::shared_ptr> const& formula) { + if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) { + STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); + STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models."); + + std::shared_ptr> mdp = model->as>(); + + // FIXME: re-parse the program. + std::string const programFile = storm::settings::generalSettings().getSymbolicModelFilename(); + std::string const constants = storm::settings::generalSettings().getConstantDefinitionString(); + storm::prism::Program program = storm::parser::PrismParser::parse(programFile); + + // Determine whether we are required to use the MILP-version or the SAT-version. + bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet(); + + if (useMILP) { + storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); + } else { + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formula); + } + + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); + } + } + void processOptions() { + storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); + // Start by parsing/building the model. + std::shared_ptr> model = buildModel(); + + // Print some information about the model. + model->printModelInformationToStream(std::cout); + + // If we were requested to generate a counterexample, we now do so. + if (settings.isCounterexampleSet()) { + STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); + std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty()); + generateCounterexample(model, filterFormula->getChild()); + } } }