Started work on sparse bisimulation decomposition.

Former-commit-id: 56840e4705

src/settings/modules/GeneralSettings.cpp

@@ -42,6 +42,8 @@ namespace storm {
             const std::string GeneralSettings::constantsOptionShortName = "const";
             const std::string GeneralSettings::statisticsOptionName = "statistics";
             const std::string GeneralSettings::statisticsOptionShortName = "stats";
+            const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
+            const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
 
             GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
@@ -72,7 +74,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build());
-                
+                this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, true, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
@@ -91,7 +93,6 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
-
             }
             
             bool GeneralSettings::isHelpSet() const {
@@ -278,6 +279,10 @@ namespace storm {
                 return true;
             }
             
+            bool GeneralSettings::isBisimulationSet() const {
+                return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
+            }
+            
         } // namespace modules
     } // namespace settings
 } // namespace storm

src/settings/modules/GeneralSettings.h

@@ -314,6 +314,13 @@ namespace storm {
                  */
                 bool isShowStatisticsSet() const;
                 
+                /*!
+                 * Retrieves whether the option to perform bisimulation minimization is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isBisimulationSet() const;
+                
                 bool check() const override;
 
                 // The name of the module.
@@ -354,6 +361,8 @@ namespace storm {
                 static const std::string constantsOptionShortName;
                 static const std::string statisticsOptionName;
                 static const std::string statisticsOptionShortName;
+                static const std::string bisimulationOptionName;
+                static const std::string bisimulationOptionShortName;
             };
             
         } // namespace modules

src/storage/BisimulationDecomposition.cpp

@@ -0,0 +1,50 @@
+#include "src/storage/BisimulationDecomposition.h"
+
+#include <queue>
+
+namespace storm {
+    namespace storage {
+        
+        template<typename ValueType>
+        BisimulationDecomposition<ValueType>::BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak) {
+            computeBisimulationEquivalenceClasses(model, weak);
+        }
+        
+        template<typename ValueType>
+        void BisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak) {
+            // We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks.
+            std::vector<std::size_t> stateToBlockMapping(model.getNumberOfStates());
+            storm::storage::BitVector labeledStates = model.getLabeledStates("one");
+            this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
+            std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } );
+            labeledStates.complement();
+            this->blocks.emplace_back(labeledStates.begin(), labeledStates.end());
+            std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 1; } );
+            
+            // Retrieve the backward transitions to allow for better checking of states that need to be re-examined.
+            storm::storage::SparseMatrix<ValueType> const& backwardTransitions = model.getBackwardTransitions();
+            
+            // Initially, both blocks are potential splitters.
+            std::queue<std::size_t> splitterQueue;
+            splitterQueue.push(0);
+            splitterQueue.push(1);
+
+            // As long as there is a splitter, we keep refining the current partition.
+            while (!splitterQueue.empty()) {
+                
+            }
+            
+            // While there is a splitter...
+            //
+            // check the predecessors of the splitter:
+            // * if they still have the same signature as before, then they remain unsplit
+            // * otherwise, split off the states that now behave differently
+            //   and mark the smaller block as a splitter
+            
+            //
+            
+        }
+        
+        template class BisimulationDecomposition<double>;
+    }
+}

src/storage/BisimulationDecomposition.h

@@ -0,0 +1,28 @@
+#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_
+
+#include "src/storage/Decomposition.h"
+#include "src/models/Dtmc.h"
+
+namespace storm {
+    namespace storage {
+        
+        /*!
+         * This class represents the decomposition model into its bisimulation quotient.
+         */
+        template <typename ValueType>
+        class BisimulationDecomposition : public Decomposition<StateBlock> {
+        public:
+            /*!
+             * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
+             */
+            BisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak);
+            
+        private:
+            void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak);
+        };
+        
+    }
+}
+
+#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */

src/storage/Distribution.cpp

@@ -0,0 +1,35 @@
+#include "src/storage/Distribution.h"
+
+#include <algorithm>
+
+namespace storm {
+    namespace storage {
+        template<typename ValueType>
+        void Distribution<ValueType>::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) {
+            this->distribution[state] += probability;
+            this->hash += static_cast<std::size_t>(state);
+        }
+        
+        template<typename ValueType>
+        typename Distribution<ValueType>::iterator Distribution<ValueType>::begin() {
+            return this->distribution.begin();
+        }
+
+        template<typename ValueType>
+        typename Distribution<ValueType>::const_iterator Distribution<ValueType>::begin() const {
+            return this->distribution.begin();
+        }
+        
+        template<typename ValueType>
+        typename Distribution<ValueType>::iterator Distribution<ValueType>::end() {
+            return this->distribution.end();
+        }
+        
+        template<typename ValueType>
+        typename Distribution<ValueType>::const_iterator Distribution<ValueType>::end() const {
+            return this->distribution.end();
+        }
+        
+        template class Distribution<double>;
+    }
+}

src/storage/Distribution.h

@@ -0,0 +1,71 @@
+#ifndef STORM_STORAGE_DISTRIBUTION_H_
+#define STORM_STORAGE_DISTRIBUTION_H_
+
+#include <vector>
+#include <boost/container/flat_map.hpp>
+
+#include "src/storage/sparse/StateType.h"
+
+namespace storm {
+    namespace storage {
+        
+        template<typename ValueType>
+        class Distribution {
+        public:
+            typedef boost::container::flat_map<storm::storage::sparse::state_type, ValueType> container_type;
+            typedef typename container_type::iterator iterator;
+            typedef typename container_type::const_iterator const_iterator;
+            
+            /*!
+             * Creates an empty distribution.
+             */
+            Distribution() = default;
+            
+            /*!
+             * Assigns the given state the given probability under this distribution.
+             *
+             * @param state The state to which to assign the probability.
+             * @param probability The probability to assign.
+             */
+            void addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability);
+            
+            /*!
+             * Retrieves an iterator to the elements in this distribution.
+             *
+             * @return The iterator to the elements in this distribution.
+             */
+            iterator begin();
+
+            /*!
+             * Retrieves an iterator to the elements in this distribution.
+             *
+             * @return The iterator to the elements in this distribution.
+             */
+            const_iterator begin() const;
+            
+            /*!
+             * Retrieves an iterator past the elements in this distribution.
+             *
+             * @return The iterator past the elements in this distribution.
+             */
+            iterator end();
+
+            /*!
+             * Retrieves an iterator past the elements in this distribution.
+             *
+             * @return The iterator past the elements in this distribution.
+             */
+            const_iterator end() const;
+            
+        private:
+            // A list of states and the probabilities that are assigned to them.
+            container_type distribution;
+            
+            // A hash value that is maintained to allow for quicker equality comparison between distribution.s
+            std::size_t hash;
+        };
+        
+    }
+}
+
+#endif /* STORM_STORAGE_DISTRIBUTION_H_ */