diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 47d33c0a1..6613030a2 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -371,7 +371,14 @@ namespace storm { result.second = true; } - if (ioSettings.isToNondeterministicModelSet()) { + if (transformationSettings.isToDiscreteTimeModelSet()) { + // TODO: we should also transform the properties at this point. + STORM_LOG_WARN_COND(!model->hasRewardModel("_time"), "Scheduled transformation to discrete time model, but a reward model named '_time' is already present in this model. We might take the wrong reward model later."); + result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first), storm::api::extractFormulasFromProperties(input.properties)).first; + result.second = true; + } + + if (transformationSettings.isToNondeterministicModelSet()) { result.first = storm::api::transformToNondeterministicModel(std::move(*result.first)); result.second = true; } @@ -658,6 +665,14 @@ namespace storm { !storm::transformer::NonMarkovianChainTransformer::preservesFormula(*rawFormula)) { STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states."); ignored = true; + } else if (transformationSettings.isToDiscreteTimeModelSet()) { + auto propertyFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula(*property.getRawFormula()); + auto filterFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula(*property.getFilter().getStatesFormula()); + if (propertyFormula && filterFormula) { + result = verificationCallback(propertyFormula, filterFormula); + } else { + ignored = true; + } } else { result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula()); diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 4dcaf7f61..521aecb75 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -89,6 +89,18 @@ namespace storm { } + template + std::shared_ptr checkAndTransformContinuousToDiscreteTimeFormula(storm::logic::Formula const& formula, std::string const& timeRewardName = "_time") { + storm::transformer::ContinuousToDiscreteTimeModelTransformer transformer; + if (transformer.preservesFormula(formula)) { + return transformer.checkAndTransformFormulas({formula.asSharedPointer()}, timeRewardName).front(); + } else { + STORM_LOG_ERROR("Unable to transform formula " << formula << " to discrete time."); + } + return nullptr; + } + + /*! * Transforms the given symbolic model to a sparse model. */ diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 04c7d4256..583f37c7f 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -44,7 +44,6 @@ 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"; const std::string IOSettings::qvbsInputOptionName = "qvbs"; const std::string IOSettings::qvbsInputOptionShortName = "qvbs"; @@ -90,7 +89,6 @@ 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.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("model", "The short model name as in the benchmark set.").build()) @@ -266,10 +264,6 @@ namespace storm { return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); } - bool IOSettings::isToNondeterministicModelSet() const { - return this->getOption(toNondetOptionName).getHasOptionBeenSet(); - } - bool IOSettings::isQvbsInputSet() const { return this->getOption(qvbsInputOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 96b419b67..9731a272c 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -290,11 +290,6 @@ 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; /*! * Retrieves whether the input model is to be read from the quantitative verification benchmark set (QVBS) @@ -354,7 +349,6 @@ namespace storm { static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; static const std::string propertyOptionShortName; - static const std::string toNondetOptionName; static const std::string qvbsInputOptionName; static const std::string qvbsInputOptionShortName; static const std::string qvbsRootOptionName; diff --git a/src/storm/settings/modules/TransformationSettings.cpp b/src/storm/settings/modules/TransformationSettings.cpp index 75b1c3daf..d948a48d9 100644 --- a/src/storm/settings/modules/TransformationSettings.cpp +++ b/src/storm/settings/modules/TransformationSettings.cpp @@ -12,6 +12,8 @@ namespace storm { const std::string TransformationSettings::chainEliminationOptionName = "eliminate-chains"; const std::string TransformationSettings::ignoreLabelingOptionName = "ec-ignore-labeling"; + const std::string TransformationSettings::toNondetOptionName = "to-nondet"; + const std::string TransformationSettings::toDiscreteTimeOptionName = "to-discrete"; TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { @@ -19,6 +21,8 @@ namespace storm { "If set, chains of non-Markovian states are eliminated if the resulting model is a Markov Automaton.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, ignoreLabelingOptionName, false, "If set, the elimination of chains ignores the labels for all non-Markovian states. This may cause wrong results.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, toNondetOptionName, false, "If set, DTMCs/CTMCs are converted to MDPs/MAs (without actual nondeterminism) before model checking.").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, toDiscreteTimeOptionName, false, "If set, CTMCs/MAs are converted to DTMCs/MDPs (which might or might not preserve the provided properties).").setIsAdvanced().build()); } bool TransformationSettings::isChainEliminationSet() const { @@ -29,6 +33,13 @@ namespace storm { return this->getOption(ignoreLabelingOptionName).getHasOptionBeenSet(); } + bool TransformationSettings::isToNondeterministicModelSet() const { + return this->getOption(toNondetOptionName).getHasOptionBeenSet(); + } + + bool TransformationSettings::isToDiscreteTimeModelSet() const { + return this->getOption(toDiscreteTimeOptionName).getHasOptionBeenSet(); + } bool TransformationSettings::check() const { // Ensure that labeling preservation is only set if chain elimination is set diff --git a/src/storm/settings/modules/TransformationSettings.h b/src/storm/settings/modules/TransformationSettings.h index ba646c763..00642e5fb 100644 --- a/src/storm/settings/modules/TransformationSettings.h +++ b/src/storm/settings/modules/TransformationSettings.h @@ -34,6 +34,15 @@ namespace storm { */ bool isIgnoreLabelingSet() const; + /*! + * Retrieves whether a DTMC/CTMC should be converted to an MDP/MA + */ + bool isToNondeterministicModelSet() const; + + /*! + * Retrieves whether a CTMC/MA should be converted to a DTMC/MDP + */ + bool isToDiscreteTimeModelSet() const; bool check() const override; @@ -46,6 +55,8 @@ namespace storm { // Define the string names of the options as constants. static const std::string chainEliminationOptionName; static const std::string ignoreLabelingOptionName; + static const std::string toNondetOptionName; + static const std::string toDiscreteTimeOptionName; };