From 4b43a1c42c9cbe69f193deddb8da3fe59afaaef5 Mon Sep 17 00:00:00 2001 From: Timo Philipp Gros Date: Sun, 26 Nov 2017 18:15:22 +0100 Subject: [PATCH] catching case psiStates=probStates, logprints still included --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 67 ++++++++++--------- .../helper/SparseMarkovAutomatonCslHelper.h | 6 +- 2 files changed, 40 insertions(+), 33 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 8bd2ba44c..3d12a0cbe 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -141,11 +141,7 @@ namespace storm { std::vector const &exitRateVector, storm::storage::BitVector const &markovianStates, storm::storage::BitVector const &psiStates, std::vector> relReachability, const storage::BitVector &cycleStates, const storage::BitVector &cycleGoalStates, - std::vector>> &unifVectors) { - - - - std::ofstream logfile("U+logfile.txt", std::ios::app); + std::vector>> &unifVectors, std::ofstream& logfile) { auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); auto numberOfStates = fullTransitionMatrix.getRowGroupCount(); @@ -169,12 +165,12 @@ namespace storm { } logfile << "\n"; - /*logfile << "probStates\tmarkovianStates\tgoalStates\tcycleStates\tcycleGoalStates\n"; + logfile << "probStates\tmarkovianStates\tgoalStates\tcycleStates\tcycleGoalStates\n"; for (int i =0 ; i< markovianStates.size() ; i++){ logfile << (~markovianStates)[i] << "\t\t" << markovianStates[i] << "\t\t" << psiStates[i] << "\t\t" << cycleStates[i] << "\t\t" << cycleGoalStates[i] << "\n"; - } */ + } - logfile << "Iteration for N = " << N << "maximal difference was " << " diff\n"; + logfile << "Iteration for N = " << N << "maximal difference was " << diff << "\n"; logfile << "vd: \n"; for (uint64_t i =0 ; i @@ -217,7 +211,7 @@ namespace storm { template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver){ + void SparseMarkovAutomatonCslHelper::calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile){ if (unifVectors[1][k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation. uint64_t N = unifVectors[1].size()-1; auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); @@ -225,7 +219,7 @@ namespace storm { ValueType res =0; for (uint64_t i = k ; i < N ; i++ ){ if (unifVectors[2][N-1-(i-k)][node]==-1){ - calculateUnifPlusVector(N-1-(i-k),node,2,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix, markovianStates,psiStates,solver); + calculateUnifPlusVector(N-1-(i-k),node,2,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix, markovianStates,psiStates,solver, logfile); //old: relativeReachability, dir, (N-1-(i-k)),node,lambda,wu,fullTransitionMatrix,markovianStates,psiStates, solver); } res+=poisson(lambda, i)*unifVectors[2][N-1-(i-k)][node]; @@ -244,11 +238,14 @@ namespace storm { storm::storage::SparseMatrix const &fullTransitionMatrix, storm::storage::BitVector const &markovianStates, storm::storage::BitVector const &psiStates, - std::unique_ptr> const &solver) { + std::unique_ptr> const &solver, std::ofstream& logfile) { - if (unifVectors[kind][k][node]!=-1){return;} - //std::ofstream logfile("U+logfile.txt", std::ios::app); - //logfile << "calculating vector " << kind << " for k = " << k << " node "<< node << " \t"; + + if (unifVectors[kind][k][node]!=-1){ + logfile << "already calculated for k = " << k << " node = " << node << "\n"; + return; + } + std::string print = std::string("calculating vector ") + std::to_string(kind) + " for k = " + std::to_string(k) + " node " + std::to_string(node) +" \t"; auto probabilisticStates = ~markovianStates; auto numberOfProbStates = probabilisticStates.getNumberOfSetBits(); @@ -259,7 +256,7 @@ namespace storm { // First Case, k==N, independent from kind of state if (k==N){ - //logfile << "k == N! res = 0\n"; + logfile << print << "k == N! res = 0\n"; unifVectors[kind][k][node]=0; return; } @@ -278,31 +275,29 @@ namespace storm { // WU unifVectors[kind][k][node]=1; } - //logfile << "goal state node " << node << " res = " << res << "\n"; + logfile << print << "goal state node " << node << " res = " << res << "\n"; return; } //markovian non-goal State if (markovianStates[node]){ - //logfile << "markovian state: "; res = 0; auto line = fullTransitionMatrix.getRow(rowGroupIndices[node]); for (auto &element : line){ uint64_t to = element.getColumn(); if (unifVectors[kind][k+1][to]==-1){ - calculateUnifPlusVector(k+1,to,kind,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); + calculateUnifPlusVector(k+1,to,kind,lambda,probSize,relativeReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver, logfile); } res+=element.getValue()*unifVectors[kind][k+1][to]; } unifVectors[kind][k][node]=res; - //logfile << " res = " << res << "\n"; + logfile << print << "markovian state: " << " res = " << res << "\n"; return; } //probabilistic non-goal State if (probabilisticStates[node]){ - //logfile << "probabilistic state: "; std::vector b(probSize, 0), x(numberOfProbStates,0); //calculate b uint64_t lineCounter=0; @@ -322,7 +317,7 @@ namespace storm { if (unifVectors[kind][k][to] == -1) { calculateUnifPlusVector(k, to, kind, lambda, probSize, relativeReachability, dir, unifVectors, fullTransitionMatrix, markovianStates, - psiStates, solver); + psiStates, solver, logfile); } res = res + relativeReachability[j][to] * unifVectors[kind][k][to]; } @@ -340,7 +335,7 @@ namespace storm { unifVectors[kind][k][trueI]=x[i]; } - //logfile << " res = " << unifVectors[kind][k][node] << " but calculated more \n"; + logfile << print << "probabilistic state: "<< " res = " << unifVectors[kind][k][node] << " but calculated more \n"; } //end probabilistic states } @@ -467,12 +462,16 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseMarkovAutomatonCslHelper::unifPlus(OptimizationDirection dir, std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory){ + std::vector SparseMarkovAutomatonCslHelper::unifPlus(OptimizationDirection dir, std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory){ STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); + + + std::ofstream logfile("U+logfile.txt", std::ios::app); ValueType maxNorm = storm::utility::zero(); //bitvectors to identify different kind of states + storm::storage::BitVector markovianStates = markovStates; storm::storage::BitVector allStates(markovianStates.size(), true); storm::storage::BitVector probabilisticStates = ~markovianStates; @@ -482,6 +481,14 @@ namespace storm { std::vector>> unifVectors{}; + //transitions from goalStates will be ignored. still: they are not allowed to be probabilistic! + for (uint64_t i =0 ; i exitRate{exitRateVector}; typename storm::storage::SparseMatrix fullTransitionMatrix = transitionMatrix.getSubmatrix(true, allStates , allStates , true); @@ -595,22 +602,22 @@ namespace storm { // (5) calculate vectors and maxNorm for (uint64_t i = 0; i < numberOfStates; i++) { for (uint64_t k = N; k <= N; k--) { - calculateUnifPlusVector(k,i,0,lambda,probSize,relReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); - calculateUnifPlusVector(k,i,2,lambda,probSize,relReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); - calculateVu(relReachability,dir,k,i,1,lambda,probSize,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver); + calculateUnifPlusVector(k,i,0,lambda,probSize,relReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver, logfile); + calculateUnifPlusVector(k,i,2,lambda,probSize,relReachability,dir,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver, logfile); + calculateVu(relReachability,dir,k,i,1,lambda,probSize,unifVectors,fullTransitionMatrix,markovianStates,psiStates,solver, logfile); //also use iteration to keep maxNorm of vd and vup to date, so the loop-condition is easy to prove ValueType diff = std::abs(unifVectors[0][k][i]-unifVectors[1][k][i]); maxNorm = std::max(maxNorm, diff); } } - printTransitions(N, maxNorm, fullTransitionMatrix,exitRate,markovianStates,psiStates,relReachability,psiStates, psiStates,unifVectors); //TODO remove - + printTransitions(N, maxNorm, fullTransitionMatrix,exitRate,markovianStates,psiStates,relReachability,psiStates, psiStates,unifVectors, logfile); //TODO remove // (6) double lambda lambda=2*lambda; } while (maxNorm>epsilon*(1-kappa)); + logfile.close(); return unifVectors[0][0]; } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 49970334b..b2ad305a1 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -57,7 +57,7 @@ namespace storm { private: template ::SupportsExponential, int>::type=0> - static void calculateUnifPlusVector(uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector> const& relativeReachability, OptimizationDirection dir, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); + static void calculateUnifPlusVector(uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector> const& relativeReachability, OptimizationDirection dir, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile); template ::SupportsExponential, int>::type=0> static void deleteProbDiagonals(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates); @@ -100,7 +100,7 @@ namespace storm { * */ template ::SupportsExponential, int>::type=0> - static void calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver); + static void calculateVu(std::vector> const& relativeReachability, OptimizationDirection dir, uint64_t k, uint64_t node, uint64_t const kind, ValueType lambda, uint64_t probSize, std::vector>>& unifVectors, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::unique_ptr> const& solver, std::ofstream& logfile); @@ -114,7 +114,7 @@ namespace storm { template ::SupportsExponential, int>::type=0> static void printTransitions(const uint64_t N, ValueType const diff, storm::storage::SparseMatrix const& fullTransitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::vector> relReachability, - storm::storage::BitVector const& cycleStates , storm::storage::BitVector const& cycleGoalStates ,std::vector>>& unifVectors); + storm::storage::BitVector const& cycleStates , storm::storage::BitVector const& cycleGoalStates ,std::vector>>& unifVectors, std::ofstream& logfile); template ::SupportsExponential, int>::type = 0> static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory);