more work on bisimulation-based abstraction-refinement

src/storm/modelchecker/CheckTask.h

@@ -128,6 +128,13 @@ namespace storm {
                 return optimizationDirection.get();
             }
             
+            /*!
+             * Sets the optimization direction.
+             */
+            void setOptimizationDirection(storm::OptimizationDirection const& dir) {
+                optimizationDirection = dir;
+            }
+            
             /*!
              * Retrieves whether a reward model was set.
              */

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp

@@ -2,34 +2,252 @@
 
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 
 #include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 
 #include "storm/logic/FragmentSpecification.h"
 
+#include "storm/storage/dd/Bdd.h"
+#include "storm/storage/dd/BisimulationDecomposition.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/AbstractionSettings.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/InvalidTypeException.h"
+
 namespace storm {
     namespace modelchecker {
         
         template<typename ModelType>
-        PartialBisimulationMdpModelChecker<ModelType>::PartialBisimulationMdpModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker<ModelType>(model) {
+        PartialBisimulationMdpModelChecker<ModelType>::PartialBisimulationMdpModelChecker(ModelType const& model) : AbstractModelChecker<ModelType>(), model(model) {
             // Intentionally left empty.
         }
         
         template<typename ModelType>
         bool PartialBisimulationMdpModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            storm::logic::FragmentSpecification fragment = storm::logic::reachability();
+            storm::logic::FragmentSpecification fragment = storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true);
             return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
         }
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
-            return nullptr;
+            return computeValuesAbstractionRefinement(false, checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
         }
         
         template<typename ModelType>
         std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
-            return nullptr;
+            return computeValuesAbstractionRefinement(false, checkTask.substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
+        }
+
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
+            STORM_LOG_THROW(rewardMeasureType == storm::logic::RewardMeasureType::Expectation, storm::exceptions::InvalidPropertyException, "Can only compute reward expectations.");
+            return computeValuesAbstractionRefinement(true, checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
+        }
+
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeValuesAbstractionRefinement(bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+
+            STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
+            
+            // Create the appropriate preservation information.
+            storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, storm::storage::BisimulationType::Strong);
+            if (checkTask.isRewardModelSet()) {
+                if (checkTask.getRewardModel() != "" || model.hasRewardModel(checkTask.getRewardModel())) {
+                    preservationInformation.addRewardModel(checkTask.getRewardModel());
+                } else if (model.hasUniqueRewardModel()) {
+                    preservationInformation.addRewardModel(model.getUniqueRewardModelName());
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Property refers to illegal reward model '" << checkTask.getRewardModel() << "'.");
+                }
+            }
+            
+            // Create a bisimulation object that is used to obtain (partial) quotients.
+            storm::dd::BisimulationDecomposition<DdType, ValueType> bisimulation(this->model, {checkTask.getFormula().asSharedPointer()}, storm::storage::BisimulationType::Strong);
+            
+            auto start = std::chrono::high_resolution_clock::now();
+            
+            uint64_t iterations = 0;
+            std::unique_ptr<CheckResult> result;
+            while (!result) {
+                bool fullQuotient = bisimulation.getReachedFixedPoint();
+                std::shared_ptr<storm::models::Model<ValueType>> quotient = bisimulation.getQuotient();
+                STORM_LOG_TRACE("Model in iteration " << (iterations + 1) << " has " << quotient->getNumberOfStates() << " states and " << quotient->getNumberOfTransitions() << " transitions.");
+                
+                if (fullQuotient) {
+                    STORM_LOG_TRACE("Reached final quotient.");
+                    quotient->printModelInformationToStream(std::cout);
+                    result = computeResultFullQuotient(*quotient, rewards, checkTask);
+                } else {
+                    // Obtain lower and upper bounds from the partial quotient.
+                    std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> bounds = computeBoundsPartialQuotient(*quotient, rewards, checkTask);
+                    
+                    // Check whether the bounds are sufficiently close.
+                    bool converged = checkBoundsSufficientlyClose(bounds);
+                    if (converged) {
+                        result = getAverageOfBounds(bounds);
+                    } else {
+                        printBoundsInformation(bounds);
+                        
+                        STORM_LOG_TRACE("Performing bisimulation step.");
+                        bisimulation.compute(10);
+                    }
+                }
+                
+                ++iterations;
+            }
+
+            auto end = std::chrono::high_resolution_clock::now();
+            STORM_LOG_TRACE("Completed abstraction-refinement in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+            
+            return result;
+        }
+        
+        template<typename ModelType>
+        void PartialBisimulationMdpModelChecker<ModelType>::printBoundsInformation(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds) {
+            STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+            STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+
+            // If there is exactly one value that we stored, we print the current bounds as an interval.
+            if (lowerBounds.getStates().getNonZeroCount() == 1 && upperBounds.getStates().getNonZeroCount() == 1) {
+                STORM_LOG_TRACE("Obtained bounds [" << lowerBounds.getValueVector().getMax() << ", " << upperBounds.getValueVector().getMax() << "] on actual result.");
+            } else {
+                STORM_LOG_TRACE("Largest difference over initial states is " << getLargestDifference(bounds) << ".");
+            }
+        }
+        
+        template<typename ModelType>
+        typename PartialBisimulationMdpModelChecker<ModelType>::ValueType PartialBisimulationMdpModelChecker<ModelType>::getLargestDifference(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds) {
+            STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+            STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+
+            return (upperBounds.getValueVector() - lowerBounds.getValueVector()).getMax();
+        }
+
+        template<typename ModelType>
+        bool PartialBisimulationMdpModelChecker<ModelType>::checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds) {
+            STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+            STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+
+            return lowerBounds.getValueVector().equalModuloPrecision(upperBounds.getValueVector(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision(), false);
+        }
+        
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::getAverageOfBounds(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds) {
+            STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+            STORM_LOG_THROW(bounds.second->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidTypeException, "Expected symbolic quantitative check result.");
+            storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
+            
+            return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber<ValueType>(std::string("2.0"))));
+        }
+        
+        static int i = 0;
+        
+        template<typename ModelType>
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+            
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
+            
+            CheckTask<storm::logic::Formula> newCheckTask(checkTask);
+            SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
+
+            newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Minimize);
+            if (rewards) {
+                result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation,newCheckTask);
+            } else {
+                result.first = checker.computeProbabilities(newCheckTask);
+            }
+            result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("lower_values" + std::to_string(i) + ".dot");
+            result.first->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+            
+            newCheckTask.setOptimizationDirection(storm::OptimizationDirection::Maximize);
+            if (rewards) {
+                result.first = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, newCheckTask);
+            } else {
+                result.second = checker.computeProbabilities(newCheckTask);
+            }
+            result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector().exportToDot("upper_values" + std::to_string(i++) + ".dot");
+            result.second->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+
+            return result;
+        }
+
+        template<typename ModelType>
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented.");
+        }
+
+        template<typename ModelType>
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+            
+            // Sanity checks.
+            STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient.");
+            storm::models::ModelType modelType = quotient.getType();
+            STORM_LOG_THROW(modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Only MDPs and stochastic games are supported as partial quotients.");
+            
+            if (modelType == storm::models::ModelType::Mdp) {
+                return computeBoundsPartialQuotient(*quotient.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), rewards, checkTask);
+            } else {
+                return computeBoundsPartialQuotient(*quotient.template as<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(), rewards, checkTask);
+            }
+        }
+        
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+            SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> checker(quotient);
+            std::unique_ptr<CheckResult> result;
+            if (rewards) {
+                result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask);
+            } else {
+                result = checker.computeProbabilities(checkTask);
+            }
+            result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+            return result;
+        }
+
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+            SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
+            std::unique_ptr<CheckResult> result;
+            if (rewards) {
+                result = checker.computeRewards(storm::logic::RewardMeasureType::Expectation, checkTask);
+            } else {
+                result = checker.computeProbabilities(checkTask);
+            }
+            result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(quotient.getReachableStates(), quotient.getInitialStates()));
+            return result;
+        }
+
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask) {
+            
+            // Sanity checks.
+            STORM_LOG_THROW(quotient.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expecting symbolic quotient.");
+            storm::models::ModelType modelType = quotient.getType();
+            STORM_LOG_THROW(modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp, storm::exceptions::NotSupportedException, "Only DTMCs and MDPs supported as full quotients.");
+            
+            if (modelType == storm::models::ModelType::Dtmc) {
+                return computeResultFullQuotient(*quotient.template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), rewards, checkTask);
+            } else {
+                return computeResultFullQuotient(*quotient.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), rewards, checkTask);
+            }
         }
         
         template class PartialBisimulationMdpModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h

@@ -1,26 +1,71 @@
 #pragma once
 
-#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
+#include "storm/modelchecker/AbstractModelChecker.h"
 
 #include "storm/storage/dd/DdType.h"
 
 namespace storm {
+    namespace dd {
+        template <storm::dd::DdType DdType>
+        class Bdd;
+    }
+    
+    namespace models {
+        template <typename ValueType>
+        class Model;
+
+        namespace symbolic {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class Dtmc;
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            class Mdp;
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            class StochasticTwoPlayerGame;
+        }
+    }
+    
     namespace modelchecker {
         
         template<typename ModelType>
-        class PartialBisimulationMdpModelChecker : public SymbolicPropositionalModelChecker<ModelType> {
+        class PartialBisimulationMdpModelChecker : public AbstractModelChecker<ModelType> {
         public:
             typedef typename ModelType::ValueType ValueType;
+            static const storm::dd::DdType DdType = ModelType::DdType;
 
             /*!
              * Constructs a model checker for the given model.
              */
             explicit PartialBisimulationMdpModelChecker(ModelType const& model);
             
-//            /// Overridden methods from super class.
+            /// Overridden methods from super class.
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
+
+        private:
+            std::unique_ptr<CheckResult> computeValuesAbstractionRefinement(bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            
+            // Methods to check for convergence and postprocessing the result.
+            bool checkBoundsSufficientlyClose(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
+            std::unique_ptr<CheckResult> getAverageOfBounds(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
+            void printBoundsInformation(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
+            ValueType getLargestDifference(std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> const& bounds);
+
+            // Methods to compute bounds on the partial quotient.
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeBoundsPartialQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            
+            // Methods to solve the query on the full quotient.
+            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Dtmc<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            std::unique_ptr<CheckResult> computeResultFullQuotient(storm::models::Model<ValueType> const& quotient, bool rewards, CheckTask<storm::logic::Formula> const& checkTask);
+            
+            // The non-abstracted model.
+            ModelType const& model;
         };
     }
 }

src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@@ -49,7 +49,7 @@ namespace storm {
                 
                 storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
                 
-                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining).");
+                STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining).");
                 
                 // Check whether we need to compute exact probabilities for some states.
                 if (qualitative) {

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -57,6 +57,16 @@ namespace storm {
             return values;
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> const& SymbolicQuantitativeCheckResult<Type, ValueType>::getStates() const {
+            return states;
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> const& SymbolicQuantitativeCheckResult<Type, ValueType>::getReachableStates() const {
+            return reachableStates;
+        }
+        
         template<typename ValueType>
         void print(std::ostream& out, ValueType const& value) {
             if (value == storm::utility::infinity<ValueType>()) {

src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h

@@ -31,6 +31,8 @@ namespace storm {
             virtual bool isSymbolicQuantitativeCheckResult() const override;
             
             storm::dd::Add<Type, ValueType> const& getValueVector() const;
+            storm::dd::Bdd<Type> const& getStates() const;
+            storm::dd::Bdd<Type> const& getReachableStates() const;
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             

src/storm/models/ModelBase.h

@@ -130,6 +130,16 @@ namespace storm {
              */
             virtual void reduceToStateBasedRewards() = 0;
             
+            /*!
+             * Retrieves whether the model has a reward model with the given name.
+             *
+             * @return True iff the model has a reward model with the given name.
+             */
+            virtual bool hasRewardModel(std::string const& rewardModelName) const = 0;
+            
+            virtual bool hasUniqueRewardModel() const = 0;
+            virtual std::string const& getUniqueRewardModelName() const = 0;
+            
         private:
             // The type of the model.
             ModelType modelType;

src/storm/models/sparse/Model.cpp

@@ -176,6 +176,12 @@ namespace storm {
                 return this->getNumberOfRewardModels() == 1;
             }
             
+            template<typename ValueType, typename RewardModelType>
+            std::string const& Model<ValueType, RewardModelType>::getUniqueRewardModelName() const {
+                STORM_LOG_THROW(this->getNumberOfRewardModels() == 1, storm::exceptions::IllegalFunctionCallException, "The reward model is not unique.");
+                return this->rewardModels.begin()->first;
+            }
+            
             template<typename ValueType, typename RewardModelType>
             bool Model<ValueType, RewardModelType>::hasRewardModel() const {
                 return !this->rewardModels.empty();

src/storm/models/sparse/Model.h

@@ -134,7 +134,7 @@ namespace storm {
                  *
                  * @return True iff the model has a reward model with the given name.
                  */
-                bool hasRewardModel(std::string const& rewardModelName) const;
+                virtual bool hasRewardModel(std::string const& rewardModelName) const override;
                 
                 /*!
                  * Retrieves the reward model with the given name, if one exists. Otherwise, an exception is thrown.
@@ -162,7 +162,14 @@ namespace storm {
                  *
                  * @return True iff the model has a unique reward model.
                  */
-                bool hasUniqueRewardModel() const;
+                virtual bool hasUniqueRewardModel() const override;
+                
+                /*!
+                 * Retrieves the name of the unique reward model, if there exists exactly one. Otherwise, an exception is thrown.
+                 *
+                 * @return The name of the unique reward model.
+                 */
+                virtual std::string const& getUniqueRewardModelName() const override;
                 
                 /*!
                  * Retrieves whether the model has at least one reward model.

src/storm/models/symbolic/Model.h

@@ -261,7 +261,7 @@ namespace storm {
                  *
                  * @return True iff the model has a reward model with the given name.
                  */
-                bool hasRewardModel(std::string const& rewardModelName) const;
+                virtual bool hasRewardModel(std::string const& rewardModelName) const override;
                 
                 /*!
                  * Retrieves the reward model with the given name, if one exists. Otherwise, an exception is thrown.
@@ -282,7 +282,7 @@ namespace storm {
                  *
                  * @return The name of the unique reward model.
                  */
-                std::string const& getUniqueRewardModelName() const;
+                virtual std::string const& getUniqueRewardModelName() const override;
 
                 /*!
                  * Retrieves the unique reward model, if there exists exactly one. Otherwise, an exception is thrown.
@@ -296,7 +296,7 @@ namespace storm {
                  *
                  * @return True iff the model has a unique reward model.
                  */
-                bool hasUniqueRewardModel() const;
+                virtual bool hasUniqueRewardModel() const override;
                 
                 /*!
                  * Retrieves whether the model has at least one reward model.

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -33,32 +33,29 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
-            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            showProgress = generalSettings.isVerboseSet();
-            showProgressDelay = generalSettings.getShowProgressDelay();
-            this->refineWrtRewardModels();
+            this->initialize();
+        }
       
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
-#ifndef NDEBUG
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
-#endif
+        template <storm::dd::DdType DdType, typename ValueType>
+        BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
+            this->initialize();
         }
   
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
-            auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-            showProgress = generalSettings.isVerboseSet();
-            showProgressDelay = generalSettings.getShowProgressDelay();
-            this->refineWrtRewardModels();
-            
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
-#ifndef NDEBUG
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
-#endif
+            this->initialize();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
+            this->initialize();
+        }
+        
+        template <storm::dd::DdType DdType, typename ValueType>
+        BisimulationDecomposition<DdType, ValueType>::~BisimulationDecomposition() = default;
+        
+        template <storm::dd::DdType DdType, typename ValueType>
+        void BisimulationDecomposition<DdType, ValueType>::initialize() {
             auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             showProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
@@ -70,9 +67,6 @@ namespace storm {
 #endif
         }
         
-        template <storm::dd::DdType DdType, typename ValueType>
-        BisimulationDecomposition<DdType, ValueType>::~BisimulationDecomposition() = default;
-        
         template <storm::dd::DdType DdType, typename ValueType>
         void BisimulationDecomposition<DdType, ValueType>::compute(bisimulation::SignatureMode const& mode) {
             STORM_LOG_ASSERT(refiner, "No suitable refiner.");
@@ -132,6 +126,11 @@ namespace storm {
             return !refined;
         }
         
+        template <storm::dd::DdType DdType, typename ValueType>
+        bool BisimulationDecomposition<DdType, ValueType>::getReachedFixedPoint() const {
+            return this->refiner->getStatus() == Status::FixedPoint;
+        }
+        
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
             std::shared_ptr<storm::models::Model<ValueType>> quotient;
@@ -148,7 +147,6 @@ namespace storm {
                 }
 
                 quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
-                STORM_LOG_TRACE("Quotient extraction done.");
             }
 
             STORM_LOG_TRACE("Quotient extraction done.");

src/storm/storage/dd/BisimulationDecomposition.h

@@ -37,6 +37,7 @@ namespace storm {
         class BisimulationDecomposition {
         public:
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
+            BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation);
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType);
             BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, bisimulation::Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation);
             
@@ -54,12 +55,19 @@ namespace storm {
              */
             bool compute(uint64_t steps, bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager);
             
+            /*!
+             * Retrieves whether a fixed point has been reached. Depending on this, extracting a quotient will either
+             * give a full quotient or a partial one.
+             */
+            bool getReachedFixedPoint() const;
+            
             /*!
              * Retrieves the quotient model after the bisimulation decomposition was computed.
              */
             std::shared_ptr<storm::models::Model<ValueType>> getQuotient() const;
             
         private:
+            void initialize();
             void refineWrtRewardModels();
             
             // The model for which to compute the bisimulation decomposition.