From 40e125fb85c99929341c6c45331b53f9a473bcad Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 1 Mar 2017 17:19:32 +0100 Subject: [PATCH] Enable parsing of parametric DRN --- src/storm/cli/cli.cpp | 13 ++++++- src/storm/cli/entrypoints.h | 29 +++++++++++++++ src/storm/parser/DirectEncodingParser.cpp | 4 +- src/storm/utility/DirectEncodingExporter.cpp | 39 +++++++++++++++++--- src/storm/utility/DirectEncodingExporter.h | 9 +++++ 5 files changed, 84 insertions(+), 10 deletions(-) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index a524de567..4eafad0f7 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -303,9 +303,18 @@ namespace storm { if (ioSettings.isPropertySet()) { properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter); } - - buildAndCheckExplicitModel(properties, true); + + if (generalSettings.isParametricSet()) { +#ifdef STORM_HAVE_CARL + buildAndCheckExplicitModel(properties, true); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); +#endif + } else { + buildAndCheckExplicitModel(properties, true); + } } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } } diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 38ed1f551..fcf743b14 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -409,6 +409,35 @@ namespace storm { verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); } } + +#ifdef STORM_HAVE_CARL + template<> + void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant) { + storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); + + STORM_LOG_THROW(settings.isExplicitSet() || settings.isExplicitDRNSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); + + storm::utility::Stopwatch modelBuildingWatch(true); + std::shared_ptr model; + STORM_LOG_THROW(!settings.isExplicitSet(), storm::exceptions::NotSupportedException, "Parametric explicit model files are not supported."); + model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); + modelBuildingWatch.stop(); + STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); + + // Preprocess the model if needed. + BRANCH_ON_MODELTYPE(model, model, storm::RationalFunction, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties)); + + // Print some information about the model. + model->printModelInformationToStream(std::cout); + + // Verify the model, if a formula was given. + if (!properties.empty()) { + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); + verifySparseModel(model->as>(), properties, onlyInitialStatesRelevant); + } + } +#endif + } } diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 8c1288ce1..110c9ca32 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -20,8 +20,8 @@ namespace storm { namespace parser { - template<> - void ValueParser::addParameter(std::string const& parameter) { + template + void ValueParser::addParameter(std::string const& parameter) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build."); } diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index f08d979d6..b82957c9c 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -16,7 +16,7 @@ namespace storm { namespace exporter { template - void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { + void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters) { // Notice that for CTMCs we write the rate matrix instead of probabilities @@ -33,8 +33,14 @@ namespace storm { os << "// Original model type: " << sparseModel->getType() << std::endl; os << "@type: " << sparseModel->getType() << std::endl; os << "@parameters" << std::endl; - for (auto const& p : parameters) { - os << p << " "; + if (parameters.empty()) { + for (std::string const& parameter : getParameters(sparseModel)) { + os << parameter << " "; + } + } else { + for (std::string const& parameter : parameters) { + os << parameter << " "; + } } os << std::endl; os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; @@ -119,12 +125,33 @@ namespace storm { } // end matrix iteration } - - - + + template + std::vector getParameters(std::shared_ptr> sparseModel) { + return {}; + } + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); #ifdef STORM_HAVE_CARL + template<> + std::vector getParameters(std::shared_ptr> sparseModel) { + std::vector parameters; + std::set parametersProb = storm::models::sparse::getProbabilityParameters(*sparseModel); + for (auto const& parameter : parametersProb) { + std::stringstream stream; + stream << parameter; + parameters.push_back(stream.str()); + } + std::set parametersReward = storm::models::sparse::getRewardParameters(*sparseModel); + for (auto const& parameter : parametersReward) { + std::stringstream stream; + stream << parameter; + parameters.push_back(stream.str()); + } + return parameters; + } + template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); #endif diff --git a/src/storm/utility/DirectEncodingExporter.h b/src/storm/utility/DirectEncodingExporter.h index 2ebee0092..9728599a6 100644 --- a/src/storm/utility/DirectEncodingExporter.h +++ b/src/storm/utility/DirectEncodingExporter.h @@ -16,6 +16,15 @@ namespace storm { */ template void explicitExportSparseModel(std::ostream& os, std::shared_ptr> sparseModel, std::vector const& parameters); + + /*! + * Accumalate parameters in the model. + * + * @param sparseModel Model. + * @return List of parameters in the model. + */ + template + std::vector getParameters(std::shared_ptr> sparseModel); } }