From c8007876ae688c856a0d263e993be790a47886c3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 24 Feb 2015 17:01:18 +0100 Subject: [PATCH] Symbolic models can now be built from the command line. Former-commit-id: 2c239df7545a892e9be26a111ab1fa511613bde7 --- src/models/ModelBase.cpp | 8 ++ src/models/ModelBase.h | 14 +++ src/models/sparse/Model.cpp | 11 ++- src/models/sparse/Model.h | 2 + src/models/sparse/StateLabeling.cpp | 4 +- src/models/symbolic/Model.cpp | 16 ++-- src/models/symbolic/Model.h | 2 + src/models/symbolic/NondeterministicModel.cpp | 15 ++-- src/storage/dd/CuddDd.cpp | 2 +- src/utility/cli.h | 89 ++++++++++--------- 10 files changed, 104 insertions(+), 59 deletions(-) diff --git a/src/models/ModelBase.cpp b/src/models/ModelBase.cpp index 7acfd7cc1..1eff87d18 100644 --- a/src/models/ModelBase.cpp +++ b/src/models/ModelBase.cpp @@ -5,5 +5,13 @@ namespace storm { ModelType ModelBase::getType() const { return modelType; } + + bool ModelBase::isSparseModel() const { + return false; + } + + bool ModelBase::isSymbolicModel() const { + return false; + } } } \ No newline at end of file diff --git a/src/models/ModelBase.h b/src/models/ModelBase.h index c72a2c8df..4dbbca514 100644 --- a/src/models/ModelBase.h +++ b/src/models/ModelBase.h @@ -76,6 +76,20 @@ namespace storm { */ virtual void printModelInformationToStream(std::ostream& out) const = 0; + /*! + * Checks whether the model is a sparse model. + * + * @return True iff the model is a sparse model. + */ + virtual bool isSparseModel() const; + + /*! + * Checks whether the model is a symbolic model. + * + * @return True iff the model is a symbolic model. + */ + virtual bool isSymbolicModel() const; + private: // The type of the model. ModelType modelType; diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 62b3e68ce..5aa557907 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -199,9 +199,9 @@ namespace storm { template void Model::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; - out << "Model type: \t\t" << this->getType() << " (sparse)" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + out << "Model type: \t" << this->getType() << " (sparse)" << std::endl; + out << "States: \t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t" << this->getNumberOfTransitions() << std::endl; this->getStateLabeling().printLabelingInformationToStream(out); out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; out << "-------------------------------------------------------------- " << std::endl; @@ -286,6 +286,11 @@ namespace storm { this->transitionMatrix = std::move(transitionMatrix); } + template + bool Model::isSparseModel() const { + return true; + } + template class Model; #ifdef STORM_HAVE_CARL diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index 55658935d..2459bbd89 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -252,6 +252,8 @@ namespace storm { */ std::set getLabelsOfState(storm::storage::sparse::state_type state) const; + virtual bool isSparseModel() const override; + protected: /*! * Sets the transition matrix of the model. diff --git a/src/models/sparse/StateLabeling.cpp b/src/models/sparse/StateLabeling.cpp index 6514eb5b0..e23fd7b4c 100644 --- a/src/models/sparse/StateLabeling.cpp +++ b/src/models/sparse/StateLabeling.cpp @@ -102,9 +102,9 @@ namespace storm { } void StateLabeling::printLabelingInformationToStream(std::ostream& out) const { - out << "Labels:" << this->getNumberOfLabels() << std::endl; + out << "Labels: \t" << this->getNumberOfLabels() << std::endl; for (auto const& labelIndexPair : this->nameToLabelingIndexMap) { - out << "\t * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " state(s)" << std::endl; + out << " * " << labelIndexPair.first << " -> " << this->labelings[labelIndexPair.second].getNumberOfSetBits() << " state(s)" << std::endl; } } } diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 1af5c2b6a..64303f487 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -119,17 +119,23 @@ namespace storm { template void Model::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; - out << "Model type: \t\t" << this->getType() << " (symbolic)" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)" << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)" << std::endl; - out << "Variables: \t\t" << "rows:" << this->rowVariables.size() << ", columns: " << this->columnVariables.size() << std::endl; + out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl; + out << "States: \t" << this->getNumberOfStates() << " (" << reachableStates.getNodeCount() << " nodes)" << std::endl; + out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << transitionMatrix.getNodeCount() << " nodes)" << std::endl; + out << "Variables: \t" << "rows: " << this->rowVariables.size() << ", columns: " << this->columnVariables.size() << std::endl; + out << "Labels: \t" << this->labelToExpressionMap.size() << std::endl; for (auto const& label : labelToExpressionMap) { - out << "\t" << label.first << std::endl; + out << " * " << label.first << std::endl; } out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; out << "-------------------------------------------------------------- " << std::endl; } + template + bool Model::isSymbolicModel() const { + return true; + } + // Explicitly instantiate the template class. template class Model; } // namespace symbolic diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 0f8a91c64..9422bde79 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -176,6 +176,8 @@ namespace storm { virtual void printModelInformationToStream(std::ostream& out) const override; + virtual bool isSymbolicModel() const override; + protected: /*! diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index ad2db49d9..0dcd8ad25 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -28,7 +28,7 @@ namespace storm { std::set rowAndNondeterminsmVariables; std::set_union(this->getNondeterminismVariables().begin(), this->getNondeterminismVariables().end(), this->getRowVariables().begin(), this->getRowVariables().end(), std::inserter(rowAndNondeterminsmVariables, rowAndNondeterminsmVariables.begin())); - storm::dd::Dd tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).sumAbstract(rowAndNondeterminsmVariables); + storm::dd::Dd tmp = this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables()).toMtbdd().sumAbstract(rowAndNondeterminsmVariables); return static_cast(tmp.getValue()); } @@ -40,13 +40,14 @@ namespace storm { template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { out << "-------------------------------------------------------------- " << std::endl; - out << "Model type: \t\t" << this->getType() << " (symbolic)" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << " (" << this->getReachableStates().getNodeCount() << " nodes)" << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << " (" << this->getTransitionMatrix().getNodeCount() << " nodes)" << std::endl; - out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; - out << "Variables: \t\t" << "rows:" << this->getRowVariables().size() << ", columns: " << this->getColumnVariables().size() << ", nondeterminism: " << this->getNondeterminismVariables().size() << std::endl; + out << "Model type: \t" << this->getType() << " (symbolic)" << std::endl; + out << "States: \t" << this->getNumberOfStates() << " (" << this->getReachableStates().getNodeCount() << " nodes)" << std::endl; + out << "Transitions: \t" << this->getNumberOfTransitions() << " (" << this->getTransitionMatrix().getNodeCount() << " nodes)" << std::endl; + out << "Choices: \t" << this->getNumberOfChoices() << std::endl; + out << "Variables: \t" << "rows: " << this->getRowVariables().size() << ", columns: " << this->getColumnVariables().size() << ", nondeterminism: " << this->getNondeterminismVariables().size() << std::endl; + out << "Labels: \t" << this->getLabelToExpressionMap().size() << std::endl; for (auto const& label : this->getLabelToExpressionMap()) { - out << "\t" << label.first << std::endl; + out << " * " << label.first << std::endl; } out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl; out << "-------------------------------------------------------------- " << std::endl; diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index cea8e9dfd..effea029f 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -671,7 +671,7 @@ namespace storm { Dd value = *this && valueEncoding; return value.isZero() ? 0 : 1; } else { - Dd value = *this * valueEncoding; + Dd value = *this * valueEncoding.toMtbdd(); value = value.sumAbstract(this->getContainedMetaVariables()); return static_cast(Cudd_V(value.getCuddMtbdd().getNode())); } diff --git a/src/utility/cli.h b/src/utility/cli.h index 622db9aa4..b51ec8b10 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -47,16 +47,14 @@ log4cplus::Logger printer; #include "src/logic/Formulas.h" // Model headers. -#include "src/models/sparse/Model.h" #include "src/models/ModelBase.h" +#include "src/models/sparse/Model.h" +#include "src/models/symbolic/Model.h" // Headers of builders. #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h" -// Headers for DD-related classes. -#include "src/storage/dd/CuddDd.h" - // Headers for model processing. #include "src/storage/DeterministicModelBisimulationDecomposition.h" @@ -88,9 +86,9 @@ namespace storm { consoleLogAppender->setName("mainConsoleAppender"); consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); logger.addAppender(consoleLogAppender); - auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; + auto loglevel = storm::settings::debugSettings().isTraceSet() ? log4cplus::TRACE_LOG_LEVEL : storm::settings::debugSettings().isDebugSet() ? log4cplus::DEBUG_LOG_LEVEL : log4cplus::WARN_LOG_LEVEL; logger.setLogLevel(loglevel); - consoleLogAppender->setThreshold(loglevel); + consoleLogAppender->setThreshold(loglevel); } /*! @@ -134,9 +132,9 @@ namespace storm { void printHeader(const int argc, const char* argv[]) { std::cout << "StoRM" << std::endl; std::cout << "--------" << std::endl << std::endl; - - -// std::cout << storm::utility::StormVersion::longVersionString() << std::endl; + + + // std::cout << storm::utility::StormVersion::longVersionString() << 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 @@ -231,11 +229,11 @@ namespace storm { storm::settings::manager().printHelp(storm::settings::generalSettings().getHelpModuleName()); return false; } - - if (storm::settings::generalSettings().isVersionSet()) { - storm::settings::manager().printVersion(); - return false; - } + + if (storm::settings::generalSettings().isVersionSet()) { + storm::settings::manager().printVersion(); + return false; + } if (storm::settings::generalSettings().isVerboseSet()) { logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); @@ -263,11 +261,11 @@ namespace storm { } template - std::shared_ptr> buildSymbolicModel(storm::prism::Program const& program, boost::optional> const& formula) { - std::shared_ptr> result(nullptr); + std::shared_ptr buildSymbolicModel(storm::prism::Program const& program, boost::optional> const& formula) { + std::shared_ptr result(nullptr); storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); - + // Get the string that assigns values to the unknown currently undefined constants in the model. std::string constants = settings.getConstantDefinitionString(); @@ -276,7 +274,7 @@ namespace storm { buildRewards = formula.get()->isRewardOperatorFormula() || formula.get()->isRewardPathFormula(); } - // Customize model-building. + // Customize and perform model-building. if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) { typename storm::builder::ExplicitPrismModelBuilder::Options options; if (formula) { @@ -284,7 +282,6 @@ namespace storm { } options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); - // Then, build the model from the symbolic description. result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd) { typename storm::builder::DdPrismModelBuilder::Options options; @@ -293,17 +290,19 @@ namespace storm { } options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); - storm::builder::DdPrismModelBuilder::translateProgram(program, options); + result = storm::builder::DdPrismModelBuilder::translateProgram(program, options); } return result; } template - std::shared_ptr> preprocessModel(std::shared_ptr> model, boost::optional> const& formula) { + std::shared_ptr preprocessModel(std::shared_ptr model, boost::optional> const& formula) { if (storm::settings::generalSettings().isBisimulationSet()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); + std::shared_ptr> sparseModel = model->template as>(); STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs."); - std::shared_ptr> dtmc = model->template as>(); + std::shared_ptr> dtmc = sparseModel->template as>(); if (dtmc->hasTransitionRewards()) { dtmc->convertTransitionRewardsToStateRewards(); @@ -312,7 +311,7 @@ namespace storm { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (formula) { - options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, *formula.get()); + options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*sparseModel, *formula.get()); } if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { options.weak = true; @@ -333,16 +332,16 @@ namespace storm { 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->template as>(); - + // 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, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula); } - + } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); } @@ -356,18 +355,20 @@ namespace storm { #endif template - void verifyModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); // If we were requested to generate a counterexample, we now do so. if (settings.isCounterexampleSet()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Counterexample generation is only available for sparse models."); STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model."); generateCounterexample(program.get(), model, formula); } else { + std::shared_ptr> sparseModel = model->template as>(); std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { - std::shared_ptr> dtmc = model->template as>(); + std::shared_ptr> dtmc = sparseModel->template as>(); storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { result = modelchecker.check(*formula.get()); @@ -378,7 +379,7 @@ namespace storm { } } } else if (model->getType() == storm::models::ModelType::Mdp) { - std::shared_ptr> mdp = model->template as>(); + std::shared_ptr> mdp = sparseModel->template as>(); storm::modelchecker::SparseMdpPrctlModelChecker modelchecker(*mdp); result = modelchecker.check(*formula.get()); } @@ -386,32 +387,33 @@ namespace storm { if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; - result->writeToStream(std::cout, model->getInitialStates()); + result->writeToStream(std::cout, sparseModel->getInitialStates()); std::cout << std::endl << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } + } } #ifdef STORM_HAVE_CARL template<> - void verifyModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { + void verifySparseModel(boost::optional const& program, std::shared_ptr> model, std::shared_ptr formula) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); std::shared_ptr> dtmc = model->template as>(); - + std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::unique_ptr result; - + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); if (modelchecker.canHandle(*formula.get())) { result = modelchecker.check(*formula.get()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property."); } - + if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; @@ -427,28 +429,32 @@ namespace storm { void buildAndCheckSymbolicModel(boost::optional const& program, boost::optional> formula) { // Now we are ready to actually build the model. STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed."); - std::shared_ptr> model = buildSymbolicModel(program.get(), formula); + std::shared_ptr model = buildSymbolicModel(program.get(), formula); STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); // Preprocess the model if needed. model = preprocessModel(model, formula); - + // Print some information about the model. model->printModelInformationToStream(std::cout); - + // Verify the model, if a formula was given. if (formula) { - verifyModel(program, model, formula.get()); + if (model->isSparseModel()) { + verifySparseModel(program, model->as>(), formula.get()); + } else { + // Not handled yet. + } } } template void buildAndCheckExplicitModel(boost::optional> formula) { storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); - + STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); - std::shared_ptr> model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); + std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional()); // Preprocess the model if needed. model = preprocessModel(model, formula); @@ -458,7 +464,8 @@ namespace storm { // Verify the model, if a formula was given. if (formula) { - verifyModel(boost::optional(), model, formula.get()); + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); + verifySparseModel(boost::optional(), model->as>(), formula.get()); } }