added cli option for transforming continuous time models to discrete time.

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<ValueType>(std::move(*result.first));
                 result.second = true;
             }
@@ -658,6 +665,14 @@ namespace storm {
                         !storm::transformer::NonMarkovianChainTransformer<ValueType>::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<ValueType>(*property.getRawFormula());
+                        auto filterFormula = storm::api::checkAndTransformContinuousToDiscreteTimeFormula<ValueType>(*property.getFilter().getStatesFormula());
+                        if (propertyFormula && filterFormula) {
+                            result = verificationCallback(propertyFormula, filterFormula);
+                        } else {
+                            ignored = true;
+                        }
                     } else {
                         result = verificationCallback(property.getRawFormula(),
                                                       property.getFilter().getStatesFormula());

src/storm/api/transformation.h

@@ -89,6 +89,18 @@ namespace storm {
             
         }
         
+        template <typename ValueType>
+        std::shared_ptr<storm::logic::Formula const> checkAndTransformContinuousToDiscreteTimeFormula(storm::logic::Formula const& formula, std::string const& timeRewardName = "_time") {
+            storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> 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.
          */

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();
             }

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;

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

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;
 
             };