From 19f353591f1709c713c9f3e7fd940d601074cdfa Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 3 Dec 2018 12:08:45 +0100 Subject: [PATCH] Added an option to transform CTMCs to MAs and DTMCs to MDPs. --- src/storm-cli-utilities/model-handling.h | 6 ++++++ src/storm/api/transformation.h | 18 ++++++++++++++++++ src/storm/settings/modules/IOSettings.cpp | 9 +++++++-- src/storm/settings/modules/IOSettings.h | 7 +++++++ 4 files changed, 38 insertions(+), 2 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 08b4a6e30..7a5b6d13d 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -41,6 +41,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/AbstractionSettings.h" #include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/utility/Stopwatch.h" @@ -322,6 +323,11 @@ namespace storm { result.second = true; } + if (ioSettings.isToNondeterministicModelSet()) { + result.first = storm::api::transformToNondeterministicModel(std::move(*result.first)); + result.second = true; + } + return result; } diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index d26f32ea1..c501c10cf 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -4,6 +4,7 @@ #include "storm/transformer/SymbolicToSparseTransformer.h" #include "storm/utility/macros.h" +#include "storm/utility/builder.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/NotSupportedException.h" @@ -76,5 +77,22 @@ namespace storm { return nullptr; } + template + std::shared_ptr> transformToNondeterministicModel(storm::models::sparse::Model&& model) { + storm::storage::sparse::ModelComponents components(std::move(model.getTransitionMatrix()), std::move(model.getStateLabeling()), std::move(model.getRewardModels())); + components.choiceLabeling = std::move(model.getOptionalChoiceLabeling()); + components.stateValuations = std::move(model.getOptionalStateValuations()); + components.choiceOrigins = std::move(model.getOptionalChoiceOrigins()); + if (model.isOfType(storm::models::ModelType::Dtmc)) { + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Mdp, std::move(components)); + } else if (model.isOfType(storm::models::ModelType::Ctmc)) { + components.rateTransitions = true; + components.markovianStates = storm::storage::BitVector(components.transitionMatrix.getRowGroupCount(), true); + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, std::move(components)); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model of type " << model.getType() << " to a nondeterministic model."); + } + } + } } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 2dabdbdb9..e943b2219 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -42,7 +42,7 @@ namespace storm { const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; const std::string IOSettings::propertyOptionShortName = "prop"; - + const std::string IOSettings::toNondetOptionName = "to-nondet"; IOSettings::IOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") @@ -81,6 +81,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").build()); } bool IOSettings::isExportDotSet() const { @@ -226,7 +227,11 @@ namespace storm { std::string IOSettings::getPropertyFilter() const { return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); } - + + bool IOSettings::isToNondeterministicModelSet() const { + return this->getOption(toNondetOptionName).getHasOptionBeenSet(); + } + void IOSettings::finalize() { // Intentionally left empty. } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 232368cc1..b812fd936 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -264,6 +264,11 @@ namespace storm { * @return The property filter. */ std::string getPropertyFilter() const; + + /*! + * Retrieves whether a DTMC/CTMC should be converted to an MDP/MA + */ + bool isToNondeterministicModelSet() const; bool check() const override; void finalize() override; @@ -296,6 +301,8 @@ namespace storm { static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; static const std::string propertyOptionShortName; + static const std::string toNondetOptionName; + }; } // namespace modules