From ee4cb38d43c7514ca426b8ac76b4471e5725bb14 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 4 Aug 2016 17:34:06 +0200
Subject: [PATCH] lra into multivalueeliminator

Former-commit-id: 981aebe161b8f69b0b73049e57f314902d303bb7
---
 .../SparseDtmcEliminationModelChecker.cpp     |  4 +-
 .../LongRunAverageEliminator.cpp              | 33 ----------------
 .../MultiValueStateEliminator.cpp             | 38 +++++++++++++++++++
 ...iminator.h => MultiValueStateEliminator.h} | 12 +++---
 4 files changed, 45 insertions(+), 42 deletions(-)
 delete mode 100644 src/solver/stateelimination/LongRunAverageEliminator.cpp
 create mode 100644 src/solver/stateelimination/MultiValueStateEliminator.cpp
 rename src/solver/stateelimination/{LongRunAverageEliminator.h => MultiValueStateEliminator.h} (57%)

diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 3337fd14a..27667e26d 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/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();
diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp
deleted file mode 100644
index 982342b5a..000000000
--- a/src/solver/stateelimination/LongRunAverageEliminator.cpp
+++ /dev/null
@@ -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
diff --git a/src/solver/stateelimination/MultiValueStateEliminator.cpp b/src/solver/stateelimination/MultiValueStateEliminator.cpp
new file mode 100644
index 000000000..c9e9acbd1
--- /dev/null
+++ b/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
diff --git a/src/solver/stateelimination/LongRunAverageEliminator.h b/src/solver/stateelimination/MultiValueStateEliminator.h
similarity index 57%
rename from src/solver/stateelimination/LongRunAverageEliminator.h
rename to src/solver/stateelimination/MultiValueStateEliminator.h
index d56e53e98..fcd3daaa9 100644
--- a/src/solver/stateelimination/LongRunAverageEliminator.h
+++ b/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_