Enabled bisimulation quotienting.

Former-commit-id: 588827ec8d

src/models/Dtmc.h

@@ -45,8 +45,9 @@ public:
 	 * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state.
 	 */
 	Dtmc(storm::storage::SparseMatrix<T> const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
-				boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
-                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+				boost::optional<std::vector<T>> const& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+                boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
 			: AbstractDeterministicModel<T>(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
@@ -72,8 +73,9 @@ public:
 	 * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state.
 	 */
 	Dtmc(storm::storage::SparseMatrix<T>&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
-				boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
-                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+				boost::optional<std::vector<T>>&& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+                boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
 				// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
 			: AbstractDeterministicModel<T>(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
                                             std::move(optionalChoiceLabeling)) {

src/storage/DeterministicModelBisimulationDecomposition.cpp

@@ -475,6 +475,7 @@ namespace storm {
         
         template<typename ValueType>
         DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak, bool buildQuotient) {
+            STORM_LOG_THROW(!dtmc.hasStateRewards() && !dtmc.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
             computeBisimulationEquivalenceClasses(dtmc, weak, buildQuotient);
         }
         
@@ -492,7 +493,7 @@ namespace storm {
             // (c) the new reward structures.
             
             // Prepare a matrix builder for (a).
-            storm::storage::SparseMatrixBuilder<ValueType> builder;
+            storm::storage::SparseMatrixBuilder<ValueType> builder(this->size(), this->size());
             
             // Prepare the new state labeling for (b).
             storm::models::AtomicPropositionsLabeling newLabeling(this->size(), dtmc.getStateLabeling().getNumberOfAtomicPropositions());
@@ -509,7 +510,22 @@ namespace storm {
                 // Pick one representative state. It doesn't matter which state it is, because they all behave equally.
                 storm::storage::sparse::state_type representativeState = *block.begin();
                 
-                // Add the outgoing transitions
+                // Compute the outgoing transitions of the block.
+                std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
+                for (auto const& entry : dtmc.getTransitionMatrix().getRow(representativeState)) {
+                    storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId();
+                    auto probIterator = blockProbability.find(targetBlock);
+                    if (probIterator != blockProbability.end()) {
+                        probIterator->second += entry.getValue();
+                    } else {
+                        blockProbability[targetBlock] = entry.getValue();
+                    }
+                }
+                
+                // Now add them to the actual matrix.
+                for (auto const& probabilityEntry : blockProbability) {
+                    builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
+                }
                 
                 // Add all atomic propositions to the equivalence class that the representative state satisfies.
                 for (auto const& ap : atomicPropositions) {
@@ -525,7 +541,11 @@ namespace storm {
                 newLabeling.addAtomicPropositionToState("init", initialBlock.getId());
             }
             
-            this->quotient = nullptr;
+            // FIXME:
+            // If reward structures are allowed, the quotient structures need to be built here.
+            
+            // Finally construct the quotient model.
+            this->quotient = std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>>(new storm::models::Dtmc<ValueType>(builder.build(), std::move(newLabeling)));
         }
         
         template<typename ValueType>
@@ -555,16 +575,16 @@ namespace storm {
                 splitterQueue.pop_front();
             }
             
-            // If we are required to build the quotient model, do so now.
-            if (buildQuotient) {
-                this->buildQuotient(dtmc, partition);
-            }
-
             // Now move the states from the internal partition into their final place in the decomposition. We do so in
             // a way that maintains the block IDs as indices.
             this->blocks.resize(partition.size());
             for (auto const& block : partition.getBlocks()) {
-                this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block));
+                this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block), true);
+            }
+
+            // If we are required to build the quotient model, do so now.
+            if (buildQuotient) {
+                this->buildQuotient(dtmc, partition);
             }
             
             std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;

src/storage/StateBlock.h

@@ -2,6 +2,7 @@
 #define STORM_STORAGE_BLOCK_H_
 
 #include <boost/container/flat_set.hpp>
+#include <boost/container/container_fwd.hpp>
 
 #include "src/utility/OsDetection.h"
 #include "src/storage/sparse/StateType.h"
@@ -35,10 +36,15 @@ namespace storm {
              *
              * @param first The first element of the range to insert.
              * @param last The last element of the range (that is itself not inserted).
+             * @param sortedAndUnique If set to true, the input range is assumed to be sorted and duplicate-free.
              */
             template <typename InputIterator>
-            StateBlock(InputIterator first, InputIterator last) : states(first, last) {
-                // Intentionally left empty.
+            StateBlock(InputIterator first, InputIterator last, bool sortedAndUnique = false) {
+                if (sortedAndUnique) {
+                    this->states = container_type(boost::container::ordered_unique_range_t(), first, last);
+                } else {
+                    this->states = container_type(first, last);
+                }
             }
             
             /*!

src/utility/cli.h

@@ -258,11 +258,20 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
                 }
                 
+                // Print some information about the model.
+                result->printModelInformationToStream(std::cout);
+                
                 if (settings.isBisimulationSet()) {
                     STORM_LOG_THROW(result->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only compatible with DTMCs.");
                     std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
-                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc);
-                    return bisimulationDecomposition.getQuotient();
+                    
+                    STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
+                    storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, false, true);
+                    
+                    result = bisimulationDecomposition.getQuotient();
+                    
+                    STORM_PRINT_AND_LOG(std::endl << "Model after minimization:" << std::endl);
+                    result->printModelInformationToStream(std::cout);
                 }
                 
                 return result;
@@ -300,9 +309,6 @@ namespace storm {
                 // Start by parsing/building the model.
                 std::shared_ptr<storm::models::AbstractModel<double>> model = buildModel<double>();
                 
-                // Print some information about the model.
-                model->printModelInformationToStream(std::cout);
-                
                 // If we were requested to generate a counterexample, we now do so.
                 if (settings.isCounterexampleSet()) {
                     STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");

src/utility/constants.h

@@ -202,6 +202,7 @@ inline storm::storage::LabeledValues<double> constantInfinity() {
     
 /*! @endcond */
 
+    
 } //namespace utility
 
 } //namespace storm