new bisimulation-based abstraction-refinement model checker that uses the new abstraction-refinement framework

src/storm/api/verification.h

@@ -12,7 +12,7 @@
 #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
-#include "storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h"
+#include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h"
 #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
 #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 
@@ -68,12 +68,12 @@ namespace storm {
         typename std::enable_if<std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithAbstractionRefinementEngine(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
             std::unique_ptr<storm::modelchecker::CheckResult> result;
             if (model->getType() == storm::models::ModelType::Dtmc) {
-                storm::modelchecker::PartialBisimulationMdpModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*model->template as<storm::models::symbolic::Dtmc<DdType, double>>());
+                storm::modelchecker::BisimulationAbstractionRefinementModelChecker<storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(*model->template as<storm::models::symbolic::Dtmc<DdType, double>>());
                 if (modelchecker.canHandle(task)) {
                     result = modelchecker.check(task);
                 }
             } else if (model->getType() == storm::models::ModelType::Mdp) {
-                storm::modelchecker::PartialBisimulationMdpModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*model->template as<storm::models::symbolic::Mdp<DdType, double>>());
+                storm::modelchecker::BisimulationAbstractionRefinementModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> modelchecker(*model->template as<storm::models::symbolic::Mdp<DdType, double>>());
                 if (modelchecker.canHandle(task)) {
                     result = modelchecker.check(task);
                 }

src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp

@@ -168,6 +168,7 @@ namespace storm {
             // Phase (2): solve quantitatively.
             if (!doSkipQuantitativeSolution) {
                 lastBounds = computeQuantitativeResult(abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second, *lastQualitativeResults);
+                STORM_LOG_ASSERT(lastBounds.first && lastBounds.second, "Expected both bounds.");
                 
                 result = std::make_pair(lastBounds.first->clone(), lastBounds.second->clone());
                 filterInitialStates(abstractModel, result);
@@ -176,8 +177,7 @@ namespace storm {
                 // Check whether the answer can be given after the quantitative solution.
                 if (checkForResultAfterQuantitativeCheck(abstractModel, true, result.first->asQuantitativeCheckResult<ValueType>())) {
                     result.second = nullptr;
-                }
-                if (checkForResultAfterQuantitativeCheck(abstractModel, false, result.second->asQuantitativeCheckResult<ValueType>())) {
+                } else if (checkForResultAfterQuantitativeCheck(abstractModel, false, result.second->asQuantitativeCheckResult<ValueType>())) {
                     result.first = nullptr;
                 }
             } else {
@@ -193,27 +193,37 @@ namespace storm {
         }
         
         template<typename ModelType>
-        bool AbstractAbstractionRefinementModelChecker<ModelType>::checkForResultAfterQuantitativeCheck(storm::models::Model<ValueType> const& abstractModel, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result) {
+        bool AbstractAbstractionRefinementModelChecker<ModelType>::checkForResultAfterQuantitativeCheck(storm::models::Model<ValueType> const& abstractModel, bool lowerBounds, QuantitativeCheckResult<ValueType> const& quantitativeResult) {
+            
+            bool result = false;
+            if (checkTask->isBoundSet()) {
                 storm::logic::ComparisonType comparisonType = checkTask->getBoundComparisonType();
                 ValueType threshold = checkTask->getBoundThreshold();
                 
                 if (lowerBounds) {
                     if (storm::logic::isLowerBound(comparisonType)) {
-                    ValueType minimalLowerBound = result.getMin();
-                    return (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold);
+                        ValueType minimalLowerBound = quantitativeResult.getMin();
+                        result = (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold);
                     } else {
-                    ValueType maximalLowerBound = result.getMax();
-                    return (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold);
+                        ValueType maximalLowerBound = quantitativeResult.getMax();
+                        result = (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold);
                     }
                 } else {
                     if (storm::logic::isLowerBound(comparisonType)) {
-                    ValueType minimalUpperBound = result.getMin();
-                    return (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold);
+                        ValueType minimalUpperBound = quantitativeResult.getMin();
+                        result = (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold);
                     } else {
-                    ValueType maximalUpperBound = result.getMax();
-                    return (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold);
+                        ValueType maximalUpperBound = quantitativeResult.getMax();
+                        result = (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold);
                     }
                 }
+                
+                if (result) {
+                    STORM_LOG_TRACE("Check for result after quantiative check positive.");
+                }
+            }
+            
+            return result;
         }
 
         template<typename ModelType>
@@ -458,7 +468,7 @@ namespace storm {
                     states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()));
                     result->prob1Max = storm::abstraction::QualitativeMdpResult<DdType>(states);
 
-                    states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates() : targetStates.getStates(), states);
+                    states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates() : targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()));
                     result->prob1Min = storm::abstraction::QualitativeMdpResult<DdType>(states);
 
                     states = storm::utility::graph::performProb0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
@@ -482,6 +492,13 @@ namespace storm {
             auto end = std::chrono::high_resolution_clock::now();
             
             auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
+            if (isRewardFormula) {
+                STORM_LOG_TRACE("Min: " << result->getProb1Min().getStates().getNonZeroCount() << " states with probability 1.");
+                STORM_LOG_TRACE("Max: " << result->getProb1Max().getStates().getNonZeroCount() << " states with probability 1.");
+            } else {
+                STORM_LOG_TRACE("Min: " << result->getProb0Min().getStates().getNonZeroCount() << " states with probability 0, " << result->getProb1Min().getStates().getNonZeroCount() << " states with probability 1.");
+                STORM_LOG_TRACE("Max: " << result->getProb0Max().getStates().getNonZeroCount() << " states with probability 0, " << result->getProb1Max().getStates().getNonZeroCount() << " states with probability 1.");
+            }
             STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms.");
             
             return result;
@@ -617,6 +634,10 @@ namespace storm {
                 }
             }
             
+            if (result) {
+                STORM_LOG_TRACE("Check for result after qualitative check positive.");
+            }
+            
             return result;
         }
         

src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp

@@ -2,6 +2,17 @@
 
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
+
+#include "storm/abstraction/SymbolicStateSet.h"
+
+#include "storm/storage/dd/BisimulationDecomposition.h"
+
+#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace modelchecker {
@@ -19,45 +30,98 @@ namespace storm {
             // Intentionally left empty.
         }
         
-//        template<typename ModelType>
-//        bool BisimulationAbstractionRefinementModelChecker<ModelType>::supportsReachabilityRewards() const {
-//            return true;
-//        }
-//        
-//        template<typename ModelType>
-//        std::string const& BisimulationAbstractionRefinementModelChecker<ModelType>::getName() const {
-//            return name;
-//        }
-//        
-//        template<typename ModelType>
-//        void BisimulationAbstractionRefinementModelChecker<ModelType>::initializeAbstractionRefinement() {
-//            
-//        }
-//        
-//        template<typename ModelType>
-//        std::shared_ptr<storm::models::Model<typename BisimulationAbstractionRefinementModelChecker<ModelType>::ValueType>> BisimulationAbstractionRefinementModelChecker<ModelType>::getAbstractModel() {
-//            
-//        }
-//        
-//        template<typename ModelType>
-//        std::pair<std::unique_ptr<storm::abstraction::StateSet>, std::unique_ptr<storm::abstraction::StateSet>> BisimulationAbstractionRefinementModelChecker<ModelType>::getConstraintAndTargetStates(storm::models::Model<ValueType> const& abstractModel) {
-//            
-//        }
-//        
-//        template<typename ModelType>
-//        uint64_t BisimulationAbstractionRefinementModelChecker<ModelType>::getAbstractionPlayer() const {
-//            return 1;
-//        }
-//        
-//        template<typename ModelType>
-//        bool BisimulationAbstractionRefinementModelChecker<ModelType>::requiresSchedulerSynthesis() const {
-//            return false;
-//        }
-//        
-//        template<typename ModelType>
-//        void BisimulationAbstractionRefinementModelChecker<ModelType>::refineAbstractModel() {
-//            
-//        }
+        template<typename ModelType>
+        bool BisimulationAbstractionRefinementModelChecker<ModelType>::supportsReachabilityRewards() const {
+            return true;
+        }
+        
+        template<typename ModelType>
+        std::string const& BisimulationAbstractionRefinementModelChecker<ModelType>::getName() const {
+            return name;
+        }
+        
+        template<typename ModelType>
+        void BisimulationAbstractionRefinementModelChecker<ModelType>::initializeAbstractionRefinement() {
+            // Create the appropriate preservation information.
+            auto const& checkTask = this->getCheckTask();
+            storm::dd::bisimulation::PreservationInformation<DdType, ValueType> preservationInformation(model, {checkTask.getFormula().asSharedPointer()});
+            if (checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward) {
+                if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) {
+                    preservationInformation.addRewardModel(model.getUniqueRewardModelName());
+                } else if (checkTask.isRewardModelSet()) {
+                    preservationInformation.addRewardModel(checkTask.getRewardModel());
+                }
+            }
+
+            // Create the bisimulation object.
+            this->bisimulation = std::make_unique<storm::dd::BisimulationDecomposition<DdType, ValueType>>(this->model, storm::storage::BisimulationType::Strong, preservationInformation);
+        }
+        
+        template<typename ModelType>
+        std::shared_ptr<storm::models::Model<typename BisimulationAbstractionRefinementModelChecker<ModelType>::ValueType>> BisimulationAbstractionRefinementModelChecker<ModelType>::getAbstractModel() {
+            lastAbstractModel = this->bisimulation->getQuotient();
+            return lastAbstractModel;
+        }
+        
+        template<typename ModelType>
+        std::pair<std::unique_ptr<storm::abstraction::StateSet>, std::unique_ptr<storm::abstraction::StateSet>> BisimulationAbstractionRefinementModelChecker<ModelType>::getConstraintAndTargetStates(storm::models::Model<ValueType> const& abstractModel) {
+            
+            STORM_LOG_ASSERT(lastAbstractModel, "Expected abstract model.");
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> ddResult;
+            if (lastAbstractModel->isOfType(storm::models::ModelType::Dtmc)) {
+                ddResult = this->getConstraintAndTargetStates(*lastAbstractModel->template as<storm::models::symbolic::Dtmc<DdType, ValueType>>());
+            } else if (lastAbstractModel->isOfType(storm::models::ModelType::Mdp)) {
+                ddResult = this->getConstraintAndTargetStates(*lastAbstractModel->template as<storm::models::symbolic::Mdp<DdType, ValueType>>());
+            } else {
+                ddResult = this->getConstraintAndTargetStates(*lastAbstractModel->template as<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>());
+            }
+
+            std::pair<std::unique_ptr<storm::abstraction::StateSet>, std::unique_ptr<storm::abstraction::StateSet>> result;
+            result.first = std::make_unique<storm::abstraction::SymbolicStateSet<DdType>>(ddResult.first);
+            result.second = std::make_unique<storm::abstraction::SymbolicStateSet<DdType>>(ddResult.second);
+            return result;
+        }
+        
+        template<typename ModelType>
+        template<typename QuotientModelType>
+        std::pair<storm::dd::Bdd<BisimulationAbstractionRefinementModelChecker<ModelType>::DdType>, storm::dd::Bdd<BisimulationAbstractionRefinementModelChecker<ModelType>::DdType>> BisimulationAbstractionRefinementModelChecker<ModelType>::getConstraintAndTargetStates(QuotientModelType const& quotient) {
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> result;
+            
+            auto const& checkTask = this->getCheckTask();
+            
+            SymbolicPropositionalModelChecker<QuotientModelType> checker(quotient);
+            if (checkTask.getFormula().isUntilFormula()) {
+                std::unique_ptr<CheckResult> subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula());
+                result.first = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
+                subresult = checker.check(checkTask.getFormula().asUntilFormula().getRightSubformula());
+                result.second = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
+            } else if (checkTask.getFormula().isEventuallyFormula()) {
+                storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula().asEventuallyFormula();
+                result.first = quotient.getReachableStates();
+                std::unique_ptr<CheckResult> subresult = checker.check(eventuallyFormula.getSubformula());
+                result.second = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The given formula is not supported by this model checker.");
+            }
+            
+            return result;
+        }
+        
+        template<typename ModelType>
+        uint64_t BisimulationAbstractionRefinementModelChecker<ModelType>::getAbstractionPlayer() const {
+            return 1;
+        }
+        
+        template<typename ModelType>
+        bool BisimulationAbstractionRefinementModelChecker<ModelType>::requiresSchedulerSynthesis() const {
+            return false;
+        }
+        
+        template<typename ModelType>
+        void BisimulationAbstractionRefinementModelChecker<ModelType>::refineAbstractModel() {
+            STORM_LOG_ASSERT(bisimulation, "Bisimulation object required.");
+            this->bisimulation->compute(10);
+        }
         
         template class BisimulationAbstractionRefinementModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
         template class BisimulationAbstractionRefinementModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;

src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h

@@ -31,16 +31,19 @@ namespace storm {
             virtual ~BisimulationAbstractionRefinementModelChecker();
             
         protected:
-//            virtual bool supportsReachabilityRewards() const override;
-//            virtual std::string const& getName() const override;
-//            virtual void initializeAbstractionRefinement() override;
-//            virtual std::shared_ptr<storm::models::Model<ValueType>> getAbstractModel() override;
-//            virtual std::pair<std::unique_ptr<storm::abstraction::StateSet>, std::unique_ptr<storm::abstraction::StateSet>> getConstraintAndTargetStates(storm::models::Model<ValueType> const& abstractModel) override;
-//            virtual uint64_t getAbstractionPlayer() const override;
-//            virtual bool requiresSchedulerSynthesis() const override;
-//            virtual void refineAbstractModel() override;
+            virtual bool supportsReachabilityRewards() const override;
+            virtual std::string const& getName() const override;
+            virtual void initializeAbstractionRefinement() override;
+            virtual std::shared_ptr<storm::models::Model<ValueType>> getAbstractModel() override;
+            virtual std::pair<std::unique_ptr<storm::abstraction::StateSet>, std::unique_ptr<storm::abstraction::StateSet>> getConstraintAndTargetStates(storm::models::Model<ValueType> const& abstractModel) override;
+            virtual uint64_t getAbstractionPlayer() const override;
+            virtual bool requiresSchedulerSynthesis() const override;
+            virtual void refineAbstractModel() override;
             
         private:
+            template<typename QuotientModelType>
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> getConstraintAndTargetStates(QuotientModelType const& quotient);
+            
             ModelType const& model;
 
             /// The bisimulation object that maintains and refines the model.

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp

@@ -122,7 +122,7 @@ namespace storm {
                         
                     if (!converged) {
                         STORM_LOG_TRACE("Performing bisimulation step.");
-                        bisimulation.compute(1);
+                        bisimulation.compute(10);
                     }
                 }