started on partial bisimulation model checker

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

@@ -252,23 +252,23 @@ namespace storm {
         
         template <typename ValueType>
         std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
-        auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
-        auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
-        auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+            auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
+            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             
-        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
+            std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
             
-        if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-        result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
-        result.second = true;
-        }
+            if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+                result.second = true;
+            }
             
-        if (generalSettings.isBisimulationSet()) {
-        result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings);
-        result.second = true;
-        }
+            if (generalSettings.isBisimulationSet()) {
+                result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings);
+                result.second = true;
+            }
             
-        return result;
+            return result;
         }
         
         template <typename ValueType>
@@ -474,14 +474,14 @@ namespace storm {
         
         template<typename ValueType>
         void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
-        for (auto const& property : properties) {
-        printModelCheckingProperty(property);
-        storm::utility::Stopwatch watch(true);
-        std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
-        watch.stop();
-        postprocessingCallback(result);
-        printResult<ValueType>(result, property, &watch);
-        }
+            for (auto const& property : properties) {
+                printModelCheckingProperty(property);
+                storm::utility::Stopwatch watch(true);
+                std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
+                watch.stop();
+                postprocessingCallback(result);
+                printResult<ValueType>(result, property, &watch);
+            }
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -571,11 +571,13 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) {
-            bool hybrid = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid;
-            if (hybrid) {
+            storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();;
+            if (engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
                 verifyWithHybridEngine<DdType, ValueType>(model, input);
-            } else {
+            } else if (engine == storm::settings::modules::CoreSettings::Engine::Dd) {
                 verifyWithDdEngine<DdType, ValueType>(model, input);
+            } else {
+                verifyWithAbstractionRefinementEngine<DdType, ValueType>(model, input);
             }
         }
         
@@ -622,10 +624,12 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         void processInputWithValueTypeAndDdlib(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
 
             // For several engines, no model building step is performed, but the verification is started right away.
             storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
-            if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
+            
+            if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
                 verifyWithAbstractionRefinementEngine<DdType, ValueType>(input);
             } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
                 verifyWithExplorationEngine<ValueType>(input);
@@ -660,5 +664,5 @@ namespace storm {
             }
         }
         
-}
+    }
 }

src/storm/api/verification.h

@@ -12,6 +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/exploration/SparseExplorationModelChecker.h"
 #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 
@@ -41,6 +42,7 @@ namespace storm {
             STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::NotSupportedException, "Can only treat DTMCs/MDPs using the abstraction refinement engine.");
             
             std::unique_ptr<storm::modelchecker::CheckResult> result;
+            
             if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) {
                 storm::modelchecker::GameBasedMdpModelChecker<DdType, storm::models::symbolic::Dtmc<DdType, ValueType>> modelchecker(model);
                 if (modelchecker.canHandle(task)) {
@@ -51,6 +53,8 @@ namespace storm {
                 if (modelchecker.canHandle(task)) {
                     result = modelchecker.check(task);
                 }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException);
             }
             return result;
         }
@@ -60,6 +64,30 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type.");
         }
         
+        template<storm::dd::DdType DdType, typename ValueType>
+        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->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->as<storm::models::symbolic::Mdp<DdType, double>>());
+                if (modelchecker.canHandle(task)) {
+                    result = modelchecker.check(task);
+                }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the dd engine.");
+            }
+            return result;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        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) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type.");
+        }
+        
         template<typename ValueType>
         typename std::enable_if<std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
             STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Exploration engine is currently only applicable to PRISM models.");

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp

@@ -0,0 +1,19 @@
+#include "storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h"
+
+#include "storm/models/symbolic/Dtmc.h"
+#include "storm/models/symbolic/Mdp.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<storm::dd::DdType Type, typename ModelType>
+        PartialBisimulationMdpModelChecker<Type, ModelType>::PartialBisimulationMdpModelChecker(ModelType const& model) : model(model) {
+
+        }
+        
+        template class PartialBisimulationMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
+        template class PartialBisimulationMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
+        template class PartialBisimulationMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
+        template class PartialBisimulationMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
+    }
+}

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h

@@ -0,0 +1,29 @@
+#pragma once
+
+#include "storm/modelchecker/AbstractModelChecker.h"
+
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<storm::dd::DdType Type, typename ModelType>
+        class PartialBisimulationMdpModelChecker : public AbstractModelChecker<ModelType> {
+        public:
+            typedef typename ModelType::ValueType ValueType;
+            
+            /*!
+             * Constructs a model checker for the given model.
+             */
+            explicit PartialBisimulationMdpModelChecker(ModelType const& model);
+            
+//            /// 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;
+            
+        private:
+            ModelType const& model;
+        };
+    }
+}

src/storm/models/symbolic/StochasticTwoPlayerGame.cpp

@@ -86,6 +86,7 @@ namespace storm {
 			template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>;
 			template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>;
 #ifdef STORM_HAVE_CARL
+            template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>;
 			template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 #endif
             

src/storm/settings/modules/AbstractionSettings.cpp

@@ -12,6 +12,7 @@ namespace storm {
     namespace settings {
         namespace modules {
             
+            const std::string AbstractionSettings::methodOptionName = "method";
             const std::string AbstractionSettings::moduleName = "abstraction";
             const std::string AbstractionSettings::useDecompositionOptionName = "decomposition";
             const std::string AbstractionSettings::splitModeOptionName = "split";
@@ -22,6 +23,12 @@ namespace storm {
             const std::string AbstractionSettings::reuseResultsOptionName = "reuse";
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
+                std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, methodOptionName, true, "Sets which abstraction-refinement method to use.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of themethod to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods))
+                                             .setDefaultValueString("bisim").build())
+                                .build());
+                
                 std::vector<std::string> onOff = {"on", "off"};
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, useDecompositionOptionName, true, "Sets whether to apply decomposition during the abstraction.")
@@ -59,6 +66,16 @@ namespace storm {
                                 .build());
             }
             
+            AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
+                std::string methodAsString = this->getOption(methodOptionName).getArgumentByName("method").getValueAsString();
+                if (methodAsString == "games") {
+                    return Method::Games;
+                } else if (methodAsString == "bisimulation" || methodAsString == "bism") {
+                    return Method::Bisimulation;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown abstraction-refinement method '" << methodAsString << "'.");
+            }
+            
             bool AbstractionSettings::isUseDecompositionSet() const {
                 return this->getOption(useDecompositionOptionName).getHasOptionBeenSet();
             }

src/storm/settings/modules/AbstractionSettings.h

@@ -11,6 +11,10 @@ namespace storm {
              */
             class AbstractionSettings : public ModuleSettings {
             public:
+                enum class Method {
+                    Games, Bisimulation
+                };
+                
                 enum class PivotSelectionHeuristic {
                     NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation
                 };
@@ -28,6 +32,11 @@ namespace storm {
                  */
                 AbstractionSettings();
                 
+                /*!
+                 * Retrieves the selected abstraction refinement method.
+                 */
+                Method getAbstractionRefinementMethod() const;
+                
                 /*!
                  * Retrieves whether the option to use the decomposition was set.
                  *
@@ -87,6 +96,7 @@ namespace storm {
                 const static std::string moduleName;
                 
             private:
+                const static std::string methodOptionName;
                 const static std::string useDecompositionOptionName;
                 const static std::string splitModeOptionName;
                 const static std::string addAllGuardsOptionName;

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -140,6 +140,8 @@ namespace storm {
                 QuotientExtractor<DdType, ValueType> extractor;
                 quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
             } else {
+                STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models.");
+                
                 STORM_LOG_TRACE("Starting partial quotient extraction.");
                 if (!partialQuotientExtractor) {
                     partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType>>(model);

src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp

@@ -3,6 +3,7 @@
 #include "storm/storage/dd/DdManager.h"
 
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm/settings/SettingsManager.h"
@@ -41,7 +42,7 @@ namespace storm {
             std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> PartialQuotientExtractor<DdType, ValueType>::extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
                 
                 auto modelType = model.getType();
-                if (modelType == storm::models::ModelType::Dtmc) {
+                if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp) {
                     // Sanity checks.
                     STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size.");
                     STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition.");
@@ -84,12 +85,6 @@ namespace storm {
                     storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
                     storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables());
                     
-//                    // Pick a representative from each block.
-//                    auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
-//                    partitionAsBdd &= representatives;
-//                    partitionAsAdd *= partitionAsBdd.template toAdd<ValueType>();
-                    
-//                    quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables());
                     quotientTransitionMatrix = quotientTransitionMatrix * partitionAsAdd;
                     end = std::chrono::high_resolution_clock::now();
                     
@@ -125,11 +120,13 @@ namespace storm {
                     end = std::chrono::high_resolution_clock::now();
                     STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
-                    std::set<storm::expressions::Variable> newNondeterminismVariables = model.getNondeterminismVariables();
-                    newNondeterminismVariables.insert(model.getRowVariables().begin(), model.getRowVariables().end());
-                    
                     if (modelType == storm::models::ModelType::Dtmc) {
-                        return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, newNondeterminismVariables, preservedLabelBdds, quotientRewardModels));
+                        return std::make_shared<storm::models::symbolic::Mdp<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), preservedLabelBdds, quotientRewardModels);
+                    } else if (modelType == storm::models::ModelType::Mdp) {
+                        std::set<storm::expressions::Variable> allNondeterminismVariables;
+                        std::set_union(model.getRowVariables().begin(), model.getRowVariables().end(), model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end(), std::inserter(allNondeterminismVariables, allNondeterminismVariables.begin()));
+                        
+                        return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), model.getNondeterminismVariables(), allNondeterminismVariables, preservedLabelBdds, quotientRewardModels);
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type.");
                     }

src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h

@@ -18,12 +18,12 @@ namespace storm {
             
             template<storm::dd::DdType DdType, typename ValueType>
             class PartialQuotientExtractor {
-                public:
+            public:
                 PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model);
                 
                 std::shared_ptr<storm::models::Model<ValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 
-                private:
+            private:
                 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 
                 // The model for which to compute the partial quotient.