Added an option to transform CTMCs to MAs and DTMCs to MDPs.

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<ValueType>(std::move(*result.first));
+                result.second = true;
+            }
+            
             return result;
         }
         

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 <typename ValueType>
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformToNondeterministicModel(storm::models::sparse::Model<ValueType>&& model) {
+            storm::storage::sparse::ModelComponents<ValueType> 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.");
+            }
+        }
+        
     }
 }

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

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