extended eliminator interface, merged model checking part

Former-commit-id: 5e0028c937

src/adapters/Smt2ExpressionAdapter.h

@@ -24,7 +24,8 @@ namespace storm {
              * @param manager The manager that can be used to build expressions.
              * @param useReadableVarNames sets whether the expressions should use human readable names for the variables or the internal representation
              */
-            Smt2ExpressionAdapter(storm::expressions::ExpressionManager& manager, bool useReadableVarNames) : manager(manager), useReadableVarNames(useReadableVarNames) {
+            Smt2ExpressionAdapter(storm::expressions::ExpressionManager& manager, bool useReadableVarNames)
+            : useReadableVarNames(useReadableVarNames) {
                 declaredVariables.emplace_back(std::set<std::string>());
             }
             

src/modelchecker/region/SparseDtmcRegionModelChecker.cpp

@@ -14,6 +14,7 @@
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/RegionSettings.h"
 #include "src/solver/OptimizationDirection.h"
+#include "src/solver/stateelimination/MultiValueStateEliminator.h"
 #include "src/storage/sparse/StateType.h"
 #include "src/storage/FlexibleSparseMatrix.h"
 #include "src/utility/constants.h"
@@ -114,6 +115,8 @@ namespace storm {
                 //The states that we consider to eliminate
                 storm::storage::BitVector considerToEliminate(submatrix.getRowCount(), true);
                 considerToEliminate.set(initialState, false);
+
+                std::vector<storm::storage::sparse::state_type> statesToEliminate;
                 for (auto const& state : considerToEliminate) {
                     bool eliminateThisState=true;
                     for(auto const& entry : flexibleTransitions.getRow(state)){
@@ -145,9 +148,17 @@ namespace storm {
                         }
                     }
                     if(eliminateThisState){
-                        storm::storage::FlexibleSparseMatrix<ParametricType>::eliminateState(flexibleTransitions, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
                         subsystem.set(state,false);
+                        statesToEliminate.push_back(state);
                     }
+
+                }
+                if(stateRewards) {
+                    storm::solver::stateelimination::MultiValueStateEliminator<ParametricType> eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities, stateRewards.get());
+                    eliminator.eliminateAll();
+                } else {
+                    storm::solver::stateelimination::PrioritizedStateEliminator<ParametricType> eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities);
+                    eliminator.eliminateAll();
                 }
                 STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions.");
 

src/modelchecker/region/SparseMdpRegionModelChecker.cpp

@@ -127,7 +127,8 @@ namespace storm {
                         statesToEliminate.push_back(state);
                     }
                 }
-                storm::solver::stateelimination::PrioritizedStateEliminator<ParametricType>(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities);
+                storm::solver::stateelimination::PrioritizedStateEliminator<ParametricType> eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities);
+                eliminator.eliminateAll();
                 STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions.");
 
                 //Build the simple model

src/solver/stateelimination/MultiValueStateEliminator.cpp

@@ -10,7 +10,12 @@ namespace storm {
             MultiValueStateEliminator<ValueType>::MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValuesVector) : PrioritizedStateEliminator<ValueType>(transitionMatrix, backwardTransitions, priorityQueue, stateValues), additionalStateValues({std::ref(additionalStateValuesVector)}) {
 
             }
-            
+
+            template<typename ValueType>
+            MultiValueStateEliminator<ValueType>::MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<storm::storage::sparse::state_type> const& statesToEliminate, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValuesVector) : PrioritizedStateEliminator<ValueType>(transitionMatrix, backwardTransitions, statesToEliminate, stateValues), additionalStateValues({std::ref(additionalStateValuesVector)}) {
+
+            }
+
             template<typename ValueType>
             void MultiValueStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
                 this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
@@ -26,6 +31,14 @@ namespace storm {
                     additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify(additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify(probability * additionalStateValueVectorRef.get()[state]));
                 }
             }
+
+            template<typename ValueType>
+            void MultiValueStateEliminator<ValueType>::clearStateValues(storm::storage::sparse::state_type const& state) {
+                super::clearStateValues(state);
+                for(auto additionStateValueVectorRef : additionalStateValues) {
+                    additionStateValueVectorRef.get()[state] = storm::utility::zero<ValueType>();
+                }
+            }
             
             template class MultiValueStateEliminator<double>;
 

src/solver/stateelimination/MultiValueStateEliminator.h

@@ -9,16 +9,23 @@ namespace storm {
 
             template<typename ValueType>
             class MultiValueStateEliminator : public PrioritizedStateEliminator<ValueType> {
+            private:
+                typedef PrioritizedStateEliminator<ValueType> super;
             public:
                 typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer;
                 typedef typename std::vector<ValueType> ValueTypeVector;
 
-                MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValues);
-                
+                MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions,
+                                          PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValues);
+                MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix,storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions,
+                                          std::vector<storm::storage::sparse::state_type> const& statesToEliminate, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValues);
+
                 // Instantiaton of virtual methods.
                 void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override;
                 void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override;
-                
+
+                virtual void clearStateValues(storm::storage::sparse::state_type const& state) override;
+
             private:
                 std::vector<std::reference_wrapper<ValueTypeVector>>additionalStateValues;
             };

src/solver/stateelimination/PrioritizedStateEliminator.cpp

@@ -34,6 +34,25 @@ namespace storm {
             void PrioritizedStateEliminator<ValueType>::updatePriority(storm::storage::sparse::state_type const& state) {
                 priorityQueue->update(state);
             }
+
+            template<typename ValueType>
+            void PrioritizedStateEliminator<ValueType>::eliminateAll(bool removeForwardTransitions) {
+                while (priorityQueue->hasNext()) {
+                    storm::storage::sparse::state_type state = priorityQueue->pop();
+                    this->eliminateState(priorityQueue->pop(), removeForwardTransitions);
+                    if (removeForwardTransitions) {
+                        clearStateValues(state);
+                    }
+#ifdef STORM_DEV
+                    STORM_LOG_ASSERT(checkConsistent(transitionMatrix, backwardTransitions), "The forward and backward transition matrices became inconsistent.");
+#endif
+                }
+            }
+
+            template<typename ValueType>
+            void PrioritizedStateEliminator<ValueType>::clearStateValues(storm::storage::sparse::state_type const &state) {
+                stateValues[state] = storm::utility::zero<ValueType>();
+            }
             
             template class PrioritizedStateEliminator<double>;
 

src/solver/stateelimination/PrioritizedStateEliminator.h

@@ -18,10 +18,12 @@ namespace storm {
                 PrioritizedStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<storm::storage::sparse::state_type> const& statesToEliminate, std::vector<ValueType>& stateValues);
 
                 // Instantiaton of virtual methods.
-                void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override;
-                void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override;
-                void updatePriority(storm::storage::sparse::state_type const& state) override;
-                
+                virtual void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override;
+                virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override;
+                virtual void updatePriority(storm::storage::sparse::state_type const& state) override;
+
+                virtual void eliminateAll(bool eliminateForwardTransitions = true);
+                virtual void clearStateValues(storm::storage::sparse::state_type const& state);
             protected:
                 PriorityQueuePointer priorityQueue;
                 std::vector<ValueType>& stateValues;