From 8421ff5c654b7eedbcbc2610964ecd57e68ecb23 Mon Sep 17 00:00:00 2001
From: Timo Philipp Gros <timopgros@gmail.com>
Date: Tue, 21 Nov 2017 09:55:04 +0100
Subject: [PATCH] first try, cmake not building

---
 .../helper/SparseMarkovAutomatonCslHelper.cpp | 36 +++++++++++++------
 .../helper/SparseMarkovAutomatonCslHelper.h   |  2 +-
 2 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index fd1ae1161..67eec89ee 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -136,7 +136,7 @@ namespace storm {
             }
             
             template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
-            void SparseMarkovAutomatonCslHelper::printTransitions(std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu){
+            void SparseMarkovAutomatonCslHelper::printTransitions(std::vector<std::vector<ValueType>> relReachability, std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu){
                 std::ofstream logfile("U+logfile.txt", std::ios::app);
                 
                 auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
@@ -165,6 +165,12 @@ namespace storm {
                     logfile << (~markovianStates)[i] << "\t\t" << markovianStates[i] << "\t\t" << psiStates[i] << "\t\t" << cycleStates[i] << "\t\t" << cycleGoalStates[i] << "\n";
                 }
 
+                for (int i =0; i<relReachability.size(); i++){
+                    for (int j=0; j<relReachability[i].size(); j++){
+                        logfile << relReachability[i][j] << "\n";
+                    }
+                    logfile << "\n";
+                }
 
 
                 logfile << "vd: \n";
@@ -495,15 +501,7 @@ namespace storm {
                 auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
 
 
-                //delete prob-diagonal entries
-                //deleteProbDiagonalEntries(fullTransitionMatrix, markovianStates);
-                    deleteProbDiagonals(fullTransitionMatrix, markovianStates);
 
-                //identify cycles and cycleGoals
-                 auto cycleStates = identifyProbCycles(fullTransitionMatrix, markovianStates, psiStates);
-                 auto cycleGoals = identifyProbCyclesGoalStates(fullTransitionMatrix, cycleStates);
-
-                 printTransitions(exitRateVector, fullTransitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished
 
 
                 //(1) define horizon, epsilon, kappa , N, lambda,
@@ -517,8 +515,26 @@ namespace storm {
                 }
                 uint64_t N;
 
+                //calculate relative ReachabilityVectors
+                std::vector<ValueType> in(fullTransitionMatrix.getRowCount(), 0);
+                std::vector<std::vector<ValueType>> relReachability(numberOfStates,in);
+
+                printTransitions(relReachability, exitRateVector, fullTransitionMatrix, markovianStates, psiStates, psiStates, psiStates, vd,vu,wu); // TODO: delete when develepmont is finished
+                for(int i=0 ; i<numberOfStates; i++){
+                     auto from = rowGroupIndices[i];
+                     auto to = rowGroupIndices[i+1];
+                     for (auto j=from ; j,to; j++){
+                         std::vector<ValueType>& act = relReachability[j];
+                         for(auto element: fullTransitionMatrix.getRow(j)){
+                             if (markovianStates[element.getColumn()]){
+                                 act[element.getColumn]=element.getValue();
+                             }
+                         }
+
+                     }
+                }
 
-                // while not close enough to precision:
+                    // while not close enough to precision:
                 do {
                     // (2) update parameter
                     N = ceil(lambda*T*exp(2)-log(kappa*epsilon));
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
index 1cee6364d..376b4e88a 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
@@ -122,7 +122,7 @@ namespace storm {
                  */
 
                 template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
-                static void printTransitions(std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates,  storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu);
+                static void printTransitions(std::vector<std::vector<ValueType>> relReachability, std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates,  storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu);
 
                 template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
                 static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);