smg lra debug commit

this should be dropped in the future

src/storm/builder/ExplicitModelBuilder.cpp

@@ -154,6 +154,7 @@ namespace storm {
             while (!statesToExplore.empty()) {
                 // Get the first state in the queue.
                 CompressedState currentState = statesToExplore.front().first;
+                STORM_LOG_DEBUG("Exploring (" << currentRowGroup << ") : " << toString(currentState, this->generator->getVariableInformation()));
                 StateType currentIndex = statesToExplore.front().second;
                 statesToExplore.pop_front();
 

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp

@@ -63,7 +63,10 @@ namespace storm {
                         this->_backwardTransitions = this->_computedBackwardTransitions.get();
                     }
                     this->_computedLongRunComponentDecomposition = std::make_unique<storm::storage::GameMaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions);
+
                     this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get();
+                    //STORM_LOG_DEBUG("\n" << this->_transitionMatrix);
+                    STORM_LOG_DEBUG("GMEC: " << *(this->_longRunComponentDecomposition));
                 }
             }
 

src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp

@@ -24,11 +24,11 @@ namespace storm {
     namespace modelchecker {
         namespace helper {
             namespace internal {
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 LraViHelper<ValueType, ComponentType, TransitionsType>::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector<ValueType> const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) {
                     setComponent(component);
-                    
+
                     // Run through the component and collect some data:
                     // We create two submodels, one consisting of the timed states of the component and one consisting of the instant states of the component.
                     // For this, we create a state index map that point from state indices of the input model to indices of the corresponding submodel of that state.
@@ -141,8 +141,9 @@ namespace storm {
                         _IsTransitions = isTransitionsBuilder.build();
                         _IsToTsTransitions = isToTsTransitionsBuilder.build();
                     }
+                    STORM_LOG_DEBUG(uniformizationFactor << " - " << _uniformizationRate);
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 void LraViHelper<ValueType, ComponentType, TransitionsType>::setComponent(ComponentType component) {
                     _component.clear();
@@ -156,7 +157,7 @@ namespace storm {
                     }
                 }
 
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 ValueType LraViHelper<ValueType, ComponentType, TransitionsType>::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector<uint64_t>* choices) {
                     initializeNewValues(stateValueGetter, actionValueGetter, exitRates);
@@ -166,7 +167,7 @@ namespace storm {
                     if (env.solver().lra().isMaximalIterationCountSet()) {
                         maxIter = env.solver().lra().getMaximalIterationCount();
                     }
-                
+
                     // start the iterations
                     ValueType result = storm::utility::zero<ValueType>();
                     uint64_t iter = 0;
@@ -198,7 +199,7 @@ namespace storm {
 
                         // If there will be a next iteration, we have to prepare it.
                         prepareNextIteration(env);
-                        
+
                     }
                     if (maxIter.is_initialized() && iter == maxIter.get()) {
                         STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations.");
@@ -207,15 +208,23 @@ namespace storm {
                     } else {
                         STORM_LOG_TRACE("LRA computation converged after " << iter << " iterations.");
                     }
-                    
+
                     if (choices) {
                         // We will be doing one more iteration step and track scheduler choices this time.
                         prepareNextIteration(env);
                         performIterationStep(env, dir, choices);
                     }
+                    std::cout << "result (" << iter << " steps):" << std::endl;
+                    for(int i = 0; i < xNew().size() ; i++ ) {
+                        std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl;
+                        //if(i == 50) {std::cout << "only showing top 50 lines"; break; }
+                    for(int i = 0; i < xNew().size() ; i++ ) {
+                        std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl;
+                        //if(i == 50) {std::cout << "only showing top 50 lines"; break; }
+                    }
                     return result;
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 void LraViHelper<ValueType, ComponentType, TransitionsType>::initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates) {
                     // clear potential old values and reserve enough space for new values
@@ -225,7 +234,7 @@ namespace storm {
                         _IsChoiceValues.clear();
                         _IsChoiceValues.reserve(_IsTransitions.getRowCount());
                     }
-                    
+
                     // Set the new choice-based values
                     ValueType actionRewardScalingFactor = storm::utility::one<ValueType>() / _uniformizationRate;
                     for (auto const& element : _component) {
@@ -250,14 +259,14 @@ namespace storm {
                     // Set-up new iteration vectors for timed states
                     _Tsx1.assign(_TsTransitions.getRowGroupCount(), storm::utility::zero<ValueType>());
                     _Tsx2 = _Tsx1;
-                    
+
                     if (_hasInstantStates) {
                         // Set-up vectors for storing intermediate results for instant states.
                         _Isx.resize(_IsTransitions.getRowGroupCount(), storm::utility::zero<ValueType>());
                         _Isb = _IsChoiceValues;
                     }
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 void LraViHelper<ValueType, ComponentType, TransitionsType>::prepareSolversAndMultipliers(const Environment& env, storm::solver::OptimizationDirection const* dir) {
                     _TsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsTransitions);
@@ -315,7 +324,7 @@ namespace storm {
                                 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "The solver requirement " << req.getEnabledRequirementsAsString() << " has not been cleared.");
                             }
                         }
-                        
+
                         // Set up multipliers for transitions connecting timed and instant states
                         _TsToIsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsToIsTransitions);
                         _IsToTsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _IsToTsTransitions);
@@ -324,7 +333,7 @@ namespace storm {
                         _TsMultiplier->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get());
                     }
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 void LraViHelper<ValueType, ComponentType, TransitionsType>::setInputModelChoices(std::vector<uint64_t>& choices, std::vector<uint64_t> const& localMecChoices, bool setChoiceZeroToTimedStates, bool setChoiceZeroToInstantStates) const {
                     // Transform the local choices (within this mec) to choice indices for the input model
@@ -347,7 +356,7 @@ namespace storm {
                     }
                     STORM_LOG_ASSERT(localState == localMecChoices.size(), "Did not traverse all component states.");
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 void LraViHelper<ValueType, ComponentType, TransitionsType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir, std::vector<uint64_t>* choices) {
                     STORM_LOG_ASSERT(!((nondetTs() || nondetIs()) && dir == nullptr), "No optimization direction provided for model with nondeterminism");
@@ -355,13 +364,13 @@ namespace storm {
                     if (!_TsMultiplier) {
                         prepareSolversAndMultipliers(env, dir);
                     }
-                    
+
                     // Compute new x values for the timed states
                     // Flip what is new and what is old
                     _Tsx1IsCurrent = !_Tsx1IsCurrent;
                     // At this point, xOld() points to what has been computed in the most recent call of performIterationStep (initially, this is the 0-vector).
                     // The result of this ongoing computation will be stored in xNew()
-                    
+
                     // Compute the values obtained by a single uniformization step between timed states only
                     if (nondetTs() && !gameNondetTs()) {
                         if (choices == nullptr) {
@@ -425,7 +434,7 @@ namespace storm {
                         _TsToIsMultiplier->multiply(env, _Isx, &xNew(), xNew());
                     }
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 typename LraViHelper<ValueType, ComponentType, TransitionsType>::ConvergenceCheckResult LraViHelper<ValueType, ComponentType, TransitionsType>::checkConvergence(bool relative, ValueType precision) const {
                     STORM_LOG_ASSERT(_TsMultiplier, "tried to check for convergence without doing an iteration first.");
@@ -433,7 +442,7 @@ namespace storm {
                     // We need to 'revert' this scaling when computing the absolute precision.
                     // However, for relative precision, the scaling cancels out.
                     ValueType threshold = relative ? precision : ValueType(precision / _uniformizationRate);
-                    
+
                     ConvergenceCheckResult res = { true, storm::utility::one<ValueType>() };
                     // Now check whether the currently produced results are precise enough
                     STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
@@ -460,15 +469,15 @@ namespace storm {
                             break;
                         }
                     }
-                    
+
                     // Compute the average of the maximal and the minimal difference.
                     ValueType avgDiff = (maxDiff + minDiff) / (storm::utility::convertNumber<ValueType>(2.0));
-                    
+
                     // "Undo" the scaling of the values
                     res.currentValue = avgDiff * _uniformizationRate;
                     return res;
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 void LraViHelper<ValueType, ComponentType, TransitionsType>::prepareNextIteration(Environment const& env) {
                     // To avoid large (and numerically unstable) x-values, we substract a reference value.
@@ -480,39 +489,39 @@ namespace storm {
                         _IsToTsMultiplier->multiply(env, xNew(), &_IsChoiceValues, _Isb);
                     }
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 bool LraViHelper<ValueType, ComponentType, TransitionsType>::isTimedState(uint64_t const& inputModelStateIndex) const {
                     STORM_LOG_ASSERT(!_hasInstantStates || _timedStates != nullptr, "Model has instant states but no partition into timed and instant states is given.");
                     STORM_LOG_ASSERT(!_hasInstantStates || inputModelStateIndex < _timedStates->size(), "Unable to determine whether state " << inputModelStateIndex << " is timed.");
                     return !_hasInstantStates || _timedStates->get(inputModelStateIndex);
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 std::vector<ValueType>& LraViHelper<ValueType, ComponentType, TransitionsType>::xNew() {
                     return _Tsx1IsCurrent ? _Tsx1 : _Tsx2;
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 std::vector<ValueType> const& LraViHelper<ValueType, ComponentType, TransitionsType>::xNew() const {
                     return _Tsx1IsCurrent ? _Tsx1 : _Tsx2;
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 std::vector<ValueType>& LraViHelper<ValueType, ComponentType, TransitionsType>::xOld() {
                     return _Tsx1IsCurrent ? _Tsx2 : _Tsx1;
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 std::vector<ValueType> const& LraViHelper<ValueType, ComponentType, TransitionsType>::xOld() const {
                     return _Tsx1IsCurrent ? _Tsx2 : _Tsx1;
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetTs() const {
                     return TransitionsType == LraViTransitionsType::NondetTsNoIs || gameNondetTs();
                 }
-                
+
                 template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
                 bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetIs() const {
                     return TransitionsType == LraViTransitionsType::DetTsNondetIs;
@@ -529,11 +538,11 @@ namespace storm {
                 template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::GameNondetTsNoIs>;
                 template class LraViHelper<double, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>;
                 template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>;
-                
+
                 template class LraViHelper<double, storm::storage::StronglyConnectedComponent, LraViTransitionsType::DetTsNoIs>;
                 template class LraViHelper<storm::RationalNumber, storm::storage::StronglyConnectedComponent, LraViTransitionsType::DetTsNoIs>;
-                
+
             }
         }
     }
-}
+}

src/storm/solver/GmmxxMultiplier.cpp

@@ -16,25 +16,26 @@
 
 namespace storm {
     namespace solver {
-        
+
         template<typename ValueType>
         GmmxxMultiplier<ValueType>::GmmxxMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : Multiplier<ValueType>(matrix) {
             // Intentionally left empty.
+            //STORM_LOG_DEBUG("\n" << matrix);
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::initialize() const {
             if (gmmMatrix.nrows() == 0) {
                 gmmMatrix = std::move(*storm::adapters::GmmxxAdapter<ValueType>().toGmmxxSparseMatrix(this->matrix));
             }
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::clearCache() const {
             gmmMatrix = gmm::csr_matrix<ValueType>();
             Multiplier<ValueType>::clearCache();
         }
-        
+
         template<typename ValueType>
         bool GmmxxMultiplier<ValueType>::parallelize(Environment const& env) const {
 #ifdef STORM_HAVE_INTELTBB
@@ -43,7 +44,7 @@ namespace storm {
             return false;
 #endif
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
             initialize();
@@ -65,7 +66,7 @@ namespace storm {
                 std::swap(result, *this->cachedVector);
             }
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards) const {
             initialize();
@@ -84,7 +85,7 @@ namespace storm {
                 }
             }
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
             initialize();
@@ -106,13 +107,13 @@ namespace storm {
                 std::swap(result, *this->cachedVector);
             }
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
             initialize();
             multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, backwards);
         }
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const {
             initialize();
@@ -148,14 +149,14 @@ namespace storm {
                 }
             }
         }
-        
+
         template<typename ValueType>
         template<typename Compare, bool backwards>
         void GmmxxMultiplier<ValueType>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
             Compare compare;
             typedef std::vector<ValueType> VectorType;
             typedef gmm::csr_matrix<ValueType> MatrixType;
-            
+
             typename gmm::linalg_traits<VectorType>::const_iterator add_it, add_ite;
             if (b) {
                 add_it = backwards ? gmm::vect_end(*b) - 1 : gmm::vect_begin(*b);
@@ -181,6 +182,7 @@ namespace storm {
             uint64_t currentRowGroup = backwards ? rowGroupIndices.size() - 1 : 0;
             auto row_group_it = backwards ? rowGroupIndices.end() - 2 : rowGroupIndices.begin();
             auto row_group_ite = backwards ? rowGroupIndices.begin() - 1 : rowGroupIndices.end() - 1;
+            //if(choices) STORM_LOG_DEBUG(" ");
             while (row_group_it != row_group_ite) {
                 ValueType currentValue = storm::utility::zero<ValueType>();
 
@@ -199,7 +201,7 @@ namespace storm {
                             oldSelectedChoiceValue = currentValue;
                         }
                     }
-                    
+
                     // move row-based iterators to the next row
                     if (backwards) {
                         --itr;
@@ -213,6 +215,10 @@ namespace storm {
 
                     // Process the (rowGroupSize-1) remaining rows within the current row Group
                     uint64_t rowGroupSize = *(row_group_it + 1) - *row_group_it;
+                    uint choiceforprintout = 0;
+                    //std::cout << currentRowGroup << ": " << currentValue << ", ";
+                    //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
+                    //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
                     for (uint64_t i = 1; i < rowGroupSize; ++i) {
                         ValueType newValue = b ? *add_it : storm::utility::zero<ValueType>();
                         newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
@@ -220,12 +226,13 @@ namespace storm {
                         if (choices && currentRow == *choice_it + *row_group_it) {
                             oldSelectedChoiceValue = newValue;
                         }
-
-                        if(this->isOverridden(currentRowGroup) ? !compare(newValue, currentValue) : compare(newValue, currentValue)) {
+                        //std::cout << newValue << ", ";
+                        //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
                             currentValue = newValue;
                             if (choices) {
                                 selectedChoice = currentRow - *row_group_it;
                             }
+                            choiceforprintout = currentRow - *row_group_it;
                         }
                         // move row-based iterators to the next row
                         if (backwards) {
@@ -238,7 +245,8 @@ namespace storm {
                              ++add_it;
                         }
                     }
-
+                    //STORM_LOG_DEBUG("\t= " << currentValue << "\tchoice: " << choiceforprintout);
+                    //std::cout << std::fixed << std::setprecision(2) << " | v(" << currentRowGroup << ")=" << currentValue << " c: " << choiceforprintout << " |\n" ;
                     // Finally write value to target vector.
                     *target_it = currentValue;
                     if(choices) {
@@ -261,6 +269,7 @@ namespace storm {
                     ++currentRowGroup;
                 }
             }
+                //std::cout << std::endl;
         }
 
         template<>
@@ -286,7 +295,7 @@ namespace storm {
             multAdd(x, b, result);
 #endif
         }
-        
+
 #ifdef STORM_HAVE_INTELTBB
         template<typename ValueType, typename Compare>
         class TbbMultAddReduceFunctor {
@@ -294,14 +303,14 @@ namespace storm {
             TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, gmm::csr_matrix<ValueType> const& matrix, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) {
                 // Intentionally left empty.
             }
-            
+
             void operator()(tbb::blocked_range<unsigned long> const& range) const {
                 typedef std::vector<ValueType> VectorType;
                 typedef gmm::csr_matrix<ValueType> MatrixType;
 
                 auto groupIt = rowGroupIndices.begin() + range.begin();
                 auto groupIte = rowGroupIndices.begin() + range.end();
-                
+
                 auto itr = mat_row_const_begin(matrix) + *groupIt;
                 typename std::vector<ValueType>::const_iterator bIt;
                 if (b) {
@@ -311,40 +320,40 @@ namespace storm {
                 if (choices) {
                     choiceIt = choices->begin() + range.begin();
                 }
-                
+
                 auto resultIt = result.begin() + range.begin();
-                
+
                 // Variables for correctly tracking choices (only update if new choice is strictly better).
                 ValueType oldSelectedChoiceValue;
                 uint64_t selectedChoice;
-                
+
                 uint64_t currentRow = *groupIt;
                 for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) {
                     ValueType currentValue = storm::utility::zero<ValueType>();
-                    
+
                     // Only multiply and reduce if the row group is not empty.
                     if (*groupIt != *(groupIt + 1)) {
                         if (b) {
                             currentValue = *bIt;
                             ++bIt;
                         }
-                        
+
                         currentValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
-                        
+
                         if (choices) {
                             selectedChoice = currentRow - *groupIt;
                             if (*choiceIt == selectedChoice) {
                                 oldSelectedChoiceValue = currentValue;
                             }
                         }
-                        
+
                         ++itr;
                         ++currentRow;
-                        
+
                         for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr, ++bIt, ++currentRow) {
                             ValueType newValue = b ? *bIt : storm::utility::zero<ValueType>();
                             newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
-                            
+
                             if (compare(newValue, currentValue)) {
                                 currentValue = newValue;
                                 if (choices) {
@@ -353,7 +362,7 @@ namespace storm {
                             }
                         }
                     }
-                    
+
                     // Finally write value to target vector.
                     *resultIt = currentValue;
                     if (choices && compare(currentValue, oldSelectedChoiceValue)) {
@@ -361,7 +370,7 @@ namespace storm {
                     }
                 }
             }
-            
+
         private:
             Compare compare;
             std::vector<uint64_t> const& rowGroupIndices;
@@ -372,7 +381,7 @@ namespace storm {
             std::vector<uint64_t>* choices;
         };
 #endif
-        
+
         template<typename ValueType>
         void GmmxxMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
 #ifdef STORM_HAVE_INTELTBB
@@ -386,18 +395,18 @@ namespace storm {
             multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices);
 #endif
         }
-        
+
         template<>
         void GmmxxMultiplier<storm::RationalFunction>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
         }
-        
+
         template class GmmxxMultiplier<double>;
-        
+
 #ifdef STORM_HAVE_CARL
         template class GmmxxMultiplier<storm::RationalNumber>;
         template class GmmxxMultiplier<storm::RationalFunction>;
 #endif
-        
+
     }
 }

src/storm/storage/Decomposition.cpp

@@ -8,84 +8,84 @@
 
 namespace storm {
     namespace storage {
-        
+
         template <typename BlockType>
         Decomposition<BlockType>::Decomposition() : blocks() {
             // Intentionally left empty.
         }
-        
+
         template <typename BlockType>
         Decomposition<BlockType>::Decomposition(Decomposition const& other) : blocks(other.blocks) {
             // Intentionally left empty.
         }
-        
+
         template <typename BlockType>
         Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition const& other) {
             this->blocks = other.blocks;
             return *this;
         }
-        
+
         template <typename BlockType>
         Decomposition<BlockType>::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) {
             // Intentionally left empty.
         }
-        
+
         template <typename BlockType>
         Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition&& other) {
             this->blocks = std::move(other.blocks);
             return *this;
         }
-        
+
         template <typename BlockType>
         std::size_t Decomposition<BlockType>::size() const {
             return blocks.size();
         }
-        
+
         template <typename BlockType>
         bool Decomposition<BlockType>::empty() const {
             return blocks.empty();
         }
-        
+
         template <typename BlockType>
         typename Decomposition<BlockType>::iterator Decomposition<BlockType>::begin() {
             return blocks.begin();
         }
-        
+
         template <typename BlockType>
         typename Decomposition<BlockType>::iterator Decomposition<BlockType>::end() {
             return blocks.end();
         }
-        
+
         template <typename BlockType>
         typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::begin() const {
             return blocks.begin();
         }
-        
+
         template <typename BlockType>
         typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::end() const {
             return blocks.end();
         }
-        
+
         template <typename BlockType>
         BlockType const& Decomposition<BlockType>::getBlock(uint_fast64_t index) const {
             return blocks.at(index);
         }
-        
+
         template <typename BlockType>
         BlockType& Decomposition<BlockType>::getBlock(uint_fast64_t index) {
             return blocks.at(index);
         }
-        
+
         template <typename BlockType>
         BlockType const& Decomposition<BlockType>::operator[](uint_fast64_t index) const {
             return blocks[index];
         }
-        
+
         template <typename BlockType>
         BlockType& Decomposition<BlockType>::operator[](uint_fast64_t index) {
             return blocks[index];
         }
-        
+
         template <typename BlockType>
         template <typename ValueType>
         storm::storage::SparseMatrix<ValueType> Decomposition<BlockType>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<ValueType> const& matrix) const {
@@ -97,49 +97,49 @@ namespace storm {
                     stateToBlockMap[state] = i;
                 }
             }
-            
+
             // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
             storm::storage::SparseMatrixBuilder<ValueType> dependencyGraphBuilder(this->size(), this->size());
-            
+
             for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < this->size(); ++currentBlockIndex) {
                 // Get the next block.
                 block_type const& block = this->getBlock(currentBlockIndex);
-                
+
                 // Now, we determine the blocks which are reachable (in one step) from the current block.
                 storm::storage::FlatSet<uint_fast64_t> allTargetBlocks;
                 for (auto state : block) {
                     for (auto const& transitionEntry : matrix.getRowGroup(state)) {
                         uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.getColumn()];
-                        
+
                         // We only need to consider transitions that are actually leaving the SCC.
                         if (targetBlock != currentBlockIndex) {
                             allTargetBlocks.insert(targetBlock);
                         }
                     }
                 }
-                
+
                 // Now we can just enumerate all the target blocks and insert the corresponding transitions.
                 for (auto const& targetBlock : allTargetBlocks) {
                     dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::one<ValueType>());
                 }
             }
-            
+
             return dependencyGraphBuilder.build();
         }
-        
+
         template <typename BlockType>
         std::ostream& operator<<(std::ostream& out, Decomposition<BlockType> const& decomposition) {
-            out << "[";
+            out << "[ ";
             if (decomposition.size() > 0) {
                 for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) {
-                    out << decomposition.blocks[blockIndex] << ", ";
+                    out << decomposition.blocks[blockIndex] << ", " << std::endl;
                 }
                 out << decomposition.blocks.back();
             }
-            out << "]";
+            out << " ]";
             return out;
         }
-        
+
         template storm::storage::SparseMatrix<double> Decomposition<StateBlock>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<double> const& matrix) const;
         template storm::storage::SparseMatrix<float> Decomposition<StateBlock>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<float> const& matrix) const;
         template class Decomposition<StateBlock>;
@@ -149,7 +149,7 @@ namespace storm {
         template storm::storage::SparseMatrix<float> Decomposition<StronglyConnectedComponent>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<float> const& matrix) const;
         template class Decomposition<StronglyConnectedComponent>;
         template std::ostream& operator<<(std::ostream& out, Decomposition<StronglyConnectedComponent> const& decomposition);
-        
+
         template class Decomposition<MaximalEndComponent>;
         template std::ostream& operator<<(std::ostream& out, Decomposition<MaximalEndComponent> const& decomposition);
     } // namespace storage

src/storm/storage/MaximalEndComponent.cpp

@@ -3,125 +3,125 @@
 
 namespace storm {
     namespace storage {
-        
+
         std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet<uint_fast64_t> const& block);
-        
+
         MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() {
             // Intentionally left empty.
         }
-        
+
         MaximalEndComponent::MaximalEndComponent(MaximalEndComponent const& other) : stateToChoicesMapping(other.stateToChoicesMapping) {
             // Intentionally left empty.
         }
-        
+
         MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent const& other) {
             stateToChoicesMapping = other.stateToChoicesMapping;
             return *this;
         }
-        
+
         MaximalEndComponent::MaximalEndComponent(MaximalEndComponent&& other) : stateToChoicesMapping(std::move(other.stateToChoicesMapping)) {
             // Intentionally left empty.
         }
-        
+
         MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent&& other) {
             stateToChoicesMapping = std::move(other.stateToChoicesMapping);
             return *this;
         }
-        
+
         void MaximalEndComponent::addState(uint_fast64_t state, set_type const& choices) {
             stateToChoicesMapping[state] = choices;
         }
-        
+
         void MaximalEndComponent::addState(uint_fast64_t state, set_type&& choices) {
             stateToChoicesMapping.emplace(state, std::move(choices));
         }
-        
+
         std::size_t MaximalEndComponent::size() const {
             return stateToChoicesMapping.size();
         }
-        
+
         MaximalEndComponent::set_type const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
             auto stateChoicePair = stateToChoicesMapping.find(state);
-            
+
             if (stateChoicePair == stateToChoicesMapping.end()) {
                 throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC.";
             }
-            
+
             return stateChoicePair->second;
         }
-        
+
         MaximalEndComponent::set_type& MaximalEndComponent::getChoicesForState(uint_fast64_t state) {
             auto stateChoicePair = stateToChoicesMapping.find(state);
-            
+
             if (stateChoicePair == stateToChoicesMapping.end()) {
                 throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC.";
             }
-            
+
             return stateChoicePair->second;
         }
-        
+
         bool MaximalEndComponent::containsState(uint_fast64_t state) const {
             auto stateChoicePair = stateToChoicesMapping.find(state);
-            
+
             if (stateChoicePair == stateToChoicesMapping.end()) {
                 return false;
             }
             return true;
         }
-        
+
         void MaximalEndComponent::removeState(uint_fast64_t state) {
             auto stateChoicePair = stateToChoicesMapping.find(state);
-            
+
             if (stateChoicePair == stateToChoicesMapping.end()) {
                 throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::removeState: cannot remove state not contained in MEC.";
             }
-            
+
             stateToChoicesMapping.erase(stateChoicePair);
         }
-        
+
         bool MaximalEndComponent::containsChoice(uint_fast64_t state, uint_fast64_t choice) const {
             auto stateChoicePair = stateToChoicesMapping.find(state);
-            
+
             if (stateChoicePair == stateToChoicesMapping.end()) {
                 throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::containsChoice: cannot obtain choices for state not contained in MEC.";
             }
-            
+
             return stateChoicePair->second.find(choice) != stateChoicePair->second.end();
         }
-        
+
         MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const {
             set_type states;
             states.reserve(stateToChoicesMapping.size());
-            
+
             for (auto const& stateChoicesPair : stateToChoicesMapping) {
                 states.insert(stateChoicesPair.first);
             }
-            
+
             return states;
         }
-        
+
         std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) {
             out << "{";
             for (auto const& stateChoicesPair : component.stateToChoicesMapping) {
-                out << "{" << stateChoicesPair.first << ", " << stateChoicesPair.second << "}";
+                out << "(" << stateChoicesPair.first << ", " << stateChoicesPair.second << ")";
             }
             out << "}";
-            
+
             return out;
         }
-        
+
         MaximalEndComponent::iterator MaximalEndComponent::begin() {
             return stateToChoicesMapping.begin();
         }
-        
+
         MaximalEndComponent::iterator MaximalEndComponent::end() {
             return stateToChoicesMapping.end();
         }
-        
+
         MaximalEndComponent::const_iterator MaximalEndComponent::begin() const {
             return stateToChoicesMapping.begin();
         }
-        
+
         MaximalEndComponent::const_iterator MaximalEndComponent::end() const {
             return stateToChoicesMapping.end();
         }