added option to perform dd-bisimulation using exact arithmetic

src/storm-cli-utilities/model-handling.h

@@ -665,7 +665,7 @@ namespace storm {
             return model;
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
+        template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
         void processInputWithValueTypeAndDdlib(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
@@ -674,19 +674,26 @@ namespace storm {
             storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
             
             if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
-                verifyWithAbstractionRefinementEngine<DdType, ValueType>(input);
+                verifyWithAbstractionRefinementEngine<DdType, VerificationValueType>(input);
             } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
-                verifyWithExplorationEngine<ValueType>(input);
+                verifyWithExplorationEngine<VerificationValueType>(input);
             } else {
-                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, ValueType>(input, engine);
+                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType>(input, engine);
                 
                 if (model) {
+                    if (!std::is_same<BuildValueType, VerificationValueType>::value) {
+                        if (model->isSymbolicModel()) {
+                            auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, BuildValueType>>();
+                            model = symbolicModel->template toValueType<VerificationValueType>();
+                        }
+                    }
+                    
                     if (coreSettings.isCounterexampleSet()) {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-                        generateCounterexamples<ValueType>(model, input);
+                        generateCounterexamples<VerificationValueType>(model, input);
                     } else {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-                        verifyModel<DdType, ValueType>(model, input, coreSettings);
+                        verifyModel<DdType, VerificationValueType>(model, input, coreSettings);
                     }
                 }
             }
@@ -696,10 +703,14 @@ namespace storm {
         void processInputWithValueType(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             
             if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && generalSettings.isExactSet()) {
                 STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
-                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(input);
+            } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD && coreSettings.isDdLibraryTypeSetFromDefaultValue() && std::is_same<ValueType, double>::value && generalSettings.isBisimulationSet() && bisimulationSettings.useExactArithmeticInDdBisimulation()) {
+                STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
+                processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input);
             } else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
                 processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);
             } else {

src/storm/models/Model.h

@@ -16,6 +16,7 @@ namespace storm {
             Model(ModelType const& modelType) : ModelBase(modelType) {
                 // Intentionally left empty.
             }
+            
         };
 
         

src/storm/models/ModelBase.h

@@ -48,7 +48,7 @@ namespace storm {
             std::shared_ptr<ModelType const> as() const {
                 return std::dynamic_pointer_cast<ModelType const>(this->shared_from_this());
             }
-            
+                        
             /*!
              *	@brief Return the actual type of the model.
              *

src/storm/models/symbolic/Ctmc.cpp

@@ -84,11 +84,29 @@ namespace storm {
                 return exitRates.get();
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            std::shared_ptr<Ctmc<Type, NewValueType>> Ctmc<Type, ValueType>::toValueType() const {
+                typedef typename DeterministicModel<Type, NewValueType>::RewardModelType NewRewardModelType;
+                std::unordered_map<std::string, NewRewardModelType> newRewardModels;
+                
+                for (auto const& e : this->getRewardModels()) {
+                    newRewardModels.emplace(e.first, e.second.template toValueType<NewValueType>());
+                }
+                
+                auto newLabelToBddMap = this->getLabelToBddMap();
+                newLabelToBddMap.erase("init");
+                newLabelToBddMap.erase("deadlock");
+                
+                return std::make_shared<Ctmc<Type, NewValueType>>(this->getManagerAsSharedPointer(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), this->getTransitionMatrix().template toValueType<NewValueType>(), this->getExitRateVector().template toValueType<NewValueType>(), this->getRowVariables(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), newLabelToBddMap, newRewardModels);
+            }
+            
             // Explicitly instantiate the template class.
             template class Ctmc<storm::dd::DdType::CUDD, double>;
             template class Ctmc<storm::dd::DdType::Sylvan, double>;
             
             template class Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template std::shared_ptr<Ctmc<storm::dd::DdType::Sylvan, double>> Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
             template class Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction>;
             
         } // namespace symbolic

src/storm/models/symbolic/Ctmc.h

@@ -141,6 +141,9 @@ namespace storm {
                  */
                 storm::dd::Add<Type, ValueType> const& getExitRateVector() const;
                 
+                template<typename NewValueType>
+                std::shared_ptr<Ctmc<Type, NewValueType>> toValueType() const;
+                
             private:
                 mutable boost::optional<storm::dd::Add<Type, ValueType>> exitRates;
             };

src/storm/models/symbolic/Dtmc.cpp

@@ -43,11 +43,29 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            std::shared_ptr<Dtmc<Type, NewValueType>> Dtmc<Type, ValueType>::toValueType() const {
+                typedef typename DeterministicModel<Type, NewValueType>::RewardModelType NewRewardModelType;
+                std::unordered_map<std::string, NewRewardModelType> newRewardModels;
+                
+                for (auto const& e : this->getRewardModels()) {
+                    newRewardModels.emplace(e.first, e.second.template toValueType<NewValueType>());
+                }
+                
+                auto newLabelToBddMap = this->getLabelToBddMap();
+                newLabelToBddMap.erase("init");
+                newLabelToBddMap.erase("deadlock");
+
+                return std::make_shared<Dtmc<Type, NewValueType>>(this->getManagerAsSharedPointer(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), this->getTransitionMatrix().template toValueType<NewValueType>(), this->getRowVariables(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), newLabelToBddMap, newRewardModels);
+            }
+            
             // Explicitly instantiate the template class.
             template class Dtmc<storm::dd::DdType::CUDD, double>;
             template class Dtmc<storm::dd::DdType::Sylvan, double>;
 
             template class Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template std::shared_ptr<Dtmc<storm::dd::DdType::Sylvan, double>> Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
             template class Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 
         } // namespace symbolic

src/storm/models/symbolic/Dtmc.h

@@ -76,6 +76,10 @@ namespace storm {
                      std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
                      std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
                      std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
+                
+                template<typename NewValueType>
+                std::shared_ptr<Dtmc<Type, NewValueType>> toValueType() const;
+
             };
             
         } // namespace symbolic

src/storm/models/symbolic/MarkovAutomaton.cpp

@@ -115,11 +115,29 @@ namespace storm {
                 return this->exitRateVector;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            std::shared_ptr<MarkovAutomaton<Type, NewValueType>> MarkovAutomaton<Type, ValueType>::toValueType() const {
+                typedef typename NondeterministicModel<Type, NewValueType>::RewardModelType NewRewardModelType;
+                std::unordered_map<std::string, NewRewardModelType> newRewardModels;
+                
+                for (auto const& e : this->getRewardModels()) {
+                    newRewardModels.emplace(e.first, e.second.template toValueType<NewValueType>());
+                }
+                
+                auto newLabelToBddMap = this->getLabelToBddMap();
+                newLabelToBddMap.erase("init");
+                newLabelToBddMap.erase("deadlock");
+                
+                return std::make_shared<MarkovAutomaton<Type, NewValueType>>(this->getManagerAsSharedPointer(), this->getMarkovianMarker(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), this->getTransitionMatrix().template toValueType<NewValueType>(), this->getRowVariables(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), this->getNondeterminismVariables(), newLabelToBddMap, newRewardModels);
+            }
+            
             // Explicitly instantiate the template class.
             template class MarkovAutomaton<storm::dd::DdType::CUDD, double>;
             template class MarkovAutomaton<storm::dd::DdType::Sylvan, double>;
             
             template class MarkovAutomaton<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template std::shared_ptr<MarkovAutomaton<storm::dd::DdType::Sylvan, double>> MarkovAutomaton<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
             template class MarkovAutomaton<storm::dd::DdType::Sylvan, storm::RationalFunction>;
             
         } // namespace symbolic

src/storm/models/symbolic/MarkovAutomaton.h

@@ -92,6 +92,9 @@ namespace storm {
                 
                 storm::dd::Add<Type, ValueType> const& getExitRateVector() const;
                 
+                template<typename NewValueType>
+                std::shared_ptr<MarkovAutomaton<Type, NewValueType>> toValueType() const;
+                
             private:
                 /*!
                  * Computes the member data related to Markovian stuff.

src/storm/models/symbolic/Mdp.cpp

@@ -45,11 +45,29 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            std::shared_ptr<Mdp<Type, NewValueType>> Mdp<Type, ValueType>::toValueType() const {
+                typedef typename NondeterministicModel<Type, NewValueType>::RewardModelType NewRewardModelType;
+                std::unordered_map<std::string, NewRewardModelType> newRewardModels;
+                
+                for (auto const& e : this->getRewardModels()) {
+                    newRewardModels.emplace(e.first, e.second.template toValueType<NewValueType>());
+                }
+                
+                auto newLabelToBddMap = this->getLabelToBddMap();
+                newLabelToBddMap.erase("init");
+                newLabelToBddMap.erase("deadlock");
+                
+                return std::make_shared<Mdp<Type, NewValueType>>(this->getManagerAsSharedPointer(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), this->getTransitionMatrix().template toValueType<NewValueType>(), this->getRowVariables(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), this->getNondeterminismVariables(), newLabelToBddMap, newRewardModels);
+            }
+            
             // Explicitly instantiate the template class.
             template class Mdp<storm::dd::DdType::CUDD, double>;
             template class Mdp<storm::dd::DdType::Sylvan, double>;
             
             template class Mdp<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template std::shared_ptr<Mdp<storm::dd::DdType::Sylvan, double>> Mdp<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
             template class Mdp<storm::dd::DdType::Sylvan, storm::RationalFunction>;
             
         } // namespace symbolic

src/storm/models/symbolic/Mdp.h

@@ -83,6 +83,9 @@ namespace storm {
                     std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
                     std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
                 
+                template<typename NewValueType>
+                std::shared_ptr<Mdp<Type, NewValueType>> toValueType() const;
+
             };
             
         } // namespace symbolic

src/storm/models/symbolic/Model.cpp

@@ -2,6 +2,11 @@
 
 #include <boost/algorithm/string/join.hpp>
 
+#include "storm/models/symbolic/Dtmc.h"
+#include "storm/models/symbolic/Ctmc.h"
+#include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/MarkovAutomaton.h"
+
 #include "storm/exceptions/IllegalArgumentException.h"
 #include "storm/exceptions/InvalidOperationException.h"
 
@@ -211,6 +216,11 @@ namespace storm {
                 return labelToExpressionMap;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            std::map<std::string, storm::dd::Bdd<Type>> const& Model<Type, ValueType>::getLabelToBddMap() const {
+                return labelToBddMap;
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             storm::dd::Add<Type, ValueType> Model<Type, ValueType>::getRowColumnIdentity() const {
                 return (storm::utility::dd::getRowColumnDiagonal<Type>(this->getManager(), this->getRowColumnMetaVariablePairs()) && this->getReachableStates()).template toAdd<ValueType>();
@@ -372,11 +382,30 @@ namespace storm {
                 return parameters;
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            std::shared_ptr<Model<Type, NewValueType>> Model<Type, ValueType>::toValueType() const {
+                // Make a huge branching here as we cannot make a templated function virtual.
+                if (this->getType() == storm::models::ModelType::Dtmc) {
+                    return this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>()->template toValueType<NewValueType>();
+                } else if (this->getType() == storm::models::ModelType::Ctmc) {
+                    return this->template as<storm::models::symbolic::Ctmc<Type, ValueType>>()->template toValueType<NewValueType>();
+                } else if (this->getType() == storm::models::ModelType::Mdp) {
+                    return this->template as<storm::models::symbolic::Mdp<Type, ValueType>>()->template toValueType<NewValueType>();
+                } else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
+                    return this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>()->template toValueType<NewValueType>();
+                }
+                
+                STORM_LOG_WARN("Could not convert value type of model.");
+                return nullptr;
+            }
+            
             // Explicitly instantiate the template class.
             template class Model<storm::dd::DdType::CUDD, double>;
             template class Model<storm::dd::DdType::Sylvan, double>;
             
             template class Model<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>> Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
             template class Model<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         } // namespace symbolic
     } // namespace models

src/storm/models/symbolic/Model.h

@@ -327,6 +327,9 @@ namespace storm {
                 
                 std::set<storm::RationalFunctionVariable> const& getParameters() const;
                 
+                template<typename NewValueType>
+                std::shared_ptr<Model<Type, NewValueType>> toValueType() const;
+                
             protected:
                 /*!
                  * Sets the transition matrix of the model.
@@ -342,6 +345,13 @@ namespace storm {
                  */
                 std::map<std::string, storm::expressions::Expression> const& getLabelToExpressionMap() const;
                 
+                /*!
+                 * Retrieves the mapping of labels to their defining expressions.
+                 *
+                 * @returns The mapping of labels to their defining expressions.
+                 */
+                std::map<std::string, storm::dd::Bdd<Type>> const& getLabelToBddMap() const;
+                
                 /*!
                  * Prints the information header (number of states and transitions) of the model to the specified stream.
                  *

src/storm/models/symbolic/StandardRewardModel.cpp

@@ -196,10 +196,17 @@ namespace storm {
                 }
             }
             
+            template <storm::dd::DdType Type, typename ValueType>
+            template<typename NewValueType>
+            StandardRewardModel<Type, NewValueType> StandardRewardModel<Type, ValueType>::toValueType() const {
+                return StandardRewardModel<Type, NewValueType>(this->hasStateRewards() ? boost::make_optional(this->getStateRewardVector().template toValueType<NewValueType>()) : boost::none, this->hasStateActionRewards() ? boost::make_optional(this->getStateActionRewardVector().template toValueType<NewValueType>()) : boost::none, this->hasTransitionRewards() ? boost::make_optional(this->getTransitionRewardMatrix().template toValueType<NewValueType>()) : boost::none);
+            }
+            
             template class StandardRewardModel<storm::dd::DdType::CUDD, double>;
             template class StandardRewardModel<storm::dd::DdType::Sylvan, double>;
 
             template class StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template StandardRewardModel<storm::dd::DdType::Sylvan, double> StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
             template class StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 
         }

src/storm/models/symbolic/StandardRewardModel.h

@@ -212,6 +212,9 @@ namespace storm {
                  */
                 void reduceToStateBasedRewards(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, bool reduceToStateRewards);
                 
+                template<typename NewValueType>
+                StandardRewardModel<Type, NewValueType> toValueType() const;
+
             private:
                 // The state reward vector.
                 boost::optional<storm::dd::Add<Type, ValueType>> optionalStateRewardVector;

src/storm/settings/modules/BisimulationSettings.cpp

@@ -21,6 +21,7 @@ namespace storm {
             const std::string BisimulationSettings::reuseOptionName = "reuse";
             const std::string BisimulationSettings::initialPartitionOptionName = "init";
             const std::string BisimulationSettings::refinementModeOptionName = "refine";
+            const std::string BisimulationSettings::exactArithmeticDdOptionName = "ddexact";
             
             BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> types = { "strong", "weak" };
@@ -31,6 +32,7 @@ namespace storm {
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exactArithmeticDdOptionName, false, "Sets whether to use exact arithmetic in dd-based bisimulation.").build());
 
                 std::vector<std::string> signatureModes = { "eager", "lazy" };
                 this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
@@ -84,6 +86,10 @@ namespace storm {
                 return this->getOption(originalVariablesOptionName).getHasOptionBeenSet();
             }
             
+            bool BisimulationSettings::useExactArithmeticInDdBisimulation() const {
+                return this->getOption(exactArithmeticDdOptionName).getHasOptionBeenSet();
+            }
+            
             storm::dd::bisimulation::SignatureMode BisimulationSettings::getSignatureMode() const {
                 std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString();
                 if (modeAsString == "eager") {

src/storm/settings/modules/BisimulationSettings.h

@@ -63,6 +63,13 @@ namespace storm {
                  */
                 bool isUseOriginalVariablesSet() const;
                 
+                /*!
+                 * Retrieves whether exact arithmetic is to be used in symbolic bisimulation minimization.
+                 *
+                 * @return True iff exact arithmetic is to be used in symbolic bisimulation minimization.
+                 */
+                bool useExactArithmeticInDdBisimulation() const;
+                
                 /*!
                  * Retrieves the mode to compute signatures.
                  */
@@ -99,6 +106,7 @@ namespace storm {
                 static const std::string initialPartitionOptionName;
                 static const std::string refinementModeOptionName;
                 static const std::string parallelismModeOptionName;
+                static const std::string exactArithmeticDdOptionName;
             };
         } // namespace modules
     } // namespace settings