Merge branch 'future' into merge-pla

Former-commit-id: 4208a88a7b

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -18,7 +18,7 @@
 
 #include "src/logic/FragmentSpecification.h"
 
-#include "src/solver/stateelimination/LongRunAverageEliminator.h"
+#include "src/solver/stateelimination/MultiValueStateEliminator.h"
 #include "src/solver/stateelimination/ConditionalStateEliminator.h"
 #include "src/solver/stateelimination/PrioritizedStateEliminator.h"
 #include "src/solver/stateelimination/StaticStatePriorityQueue.h"
@@ -226,7 +226,7 @@ namespace storm {
             
             // First, we eliminate all states in BSCCs (except for the representative states).
             std::shared_ptr<StatePriorityQueue> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs);
-            storm::solver::stateelimination::LongRunAverageEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates);
+            storm::solver::stateelimination::MultiValueStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates);
             
             while (priorityQueue->hasNext()) {
                 storm::storage::sparse::state_type state = priorityQueue->pop();

src/solver/stateelimination/LongRunAverageEliminator.cpp

@@ -1,33 +0,0 @@
-#include "src/solver/stateelimination/LongRunAverageEliminator.h"
-
-#include "src/utility/constants.h"
-
-namespace storm {
-    namespace solver {
-        namespace stateelimination {
-            
-            template<typename ValueType>
-            LongRunAverageEliminator<ValueType>::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates) : PrioritizedStateEliminator<ValueType>(transitionMatrix, backwardTransitions, priorityQueue, stateValues), averageTimeInStates(averageTimeInStates) {
-            }
-            
-            template<typename ValueType>
-            void LongRunAverageEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
-                averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]);
-            }
-       
-            template<typename ValueType>
-            void LongRunAverageEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
-                averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state]));
-            }
-            
-            template class LongRunAverageEliminator<double>;
-
-#ifdef STORM_HAVE_CARL
-            template class LongRunAverageEliminator<storm::RationalNumber>;
-            template class LongRunAverageEliminator<storm::RationalFunction>;
-#endif
-        } // namespace stateelimination
-    } // namespace storage
-} // namespace storm

src/solver/stateelimination/MultiValueStateEliminator.cpp

@@ -0,0 +1,38 @@
+#include "src/solver/stateelimination/MultiValueStateEliminator.h"
+
+#include "src/utility/constants.h"
+
+namespace storm {
+    namespace solver {
+        namespace stateelimination {
+            
+            template<typename ValueType>
+            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>
+            void MultiValueStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
+                this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
+                for(auto additionalStateValueVectorRef : additionalStateValues) {
+                    additionalStateValueVectorRef.get()[state] = storm::utility::simplify(loopProbability * additionalStateValueVectorRef.get()[state]);
+                }
+            }
+       
+            template<typename ValueType>
+            void MultiValueStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
+                this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
+                for(auto additionalStateValueVectorRef : additionalStateValues) {
+                    additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify(additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify(probability * additionalStateValueVectorRef.get()[state]));
+                }
+            }
+            
+            template class MultiValueStateEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
+            template class MultiValueStateEliminator<storm::RationalNumber>;
+            template class MultiValueStateEliminator<storm::RationalFunction>;
+#endif
+        } // namespace stateelimination
+    } // namespace storage
+} // namespace storm

src/solver/stateelimination/LongRunAverageEliminator.h → src/solver/stateelimination/MultiValueStateEliminator.h

@@ -1,6 +1,4 @@
-#ifndef STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_
-#define STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_
-
+#pragma once
 #include "src/solver/stateelimination/PrioritizedStateEliminator.h"
 
 namespace storm {
@@ -10,22 +8,22 @@ namespace storm {
             class StatePriorityQueue;
 
             template<typename ValueType>
-            class LongRunAverageEliminator : public PrioritizedStateEliminator<ValueType> {
+            class MultiValueStateEliminator : public PrioritizedStateEliminator<ValueType> {
             public:
                 typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer;
+                typedef typename std::vector<ValueType> ValueTypeVector;
 
-                LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates);
+                MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, 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;
                 
             private:
-                std::vector<ValueType>& averageTimeInStates;
+                std::vector<std::reference_wrapper<ValueTypeVector>>additionalStateValues;
             };
             
         } // namespace stateelimination
     } // namespace storage
 } // namespace storm
 
-#endif // STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_