From 25a7b6c71a652b067af212cd2cecde7e1748e1ee Mon Sep 17 00:00:00 2001 From: Timo Philipp Gros Date: Sun, 19 Nov 2017 12:20:54 +0100 Subject: [PATCH 1/2] implemented trajans alg to identify prob Cycles --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 74 ++++++++++++++++++- .../helper/SparseMarkovAutomatonCslHelper.h | 15 ++++ 2 files changed, 88 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 8c3d33fc2..88d470dce 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -337,10 +337,82 @@ namespace storm { logfile << " res = " << res << "\n"; } + template ::SupportsExponential, int>::type=0> + int SparseMarkovAutomatonCslHelper::trajans(storm::storage::SparseMatrix const& transitionMatrix, uint64_t node, std::vector& disc, std::vector& finish, uint64_t* counter) { + auto const &rowGroupIndice = transitionMatrix.getRowGroupIndices(); + + disc[node] = *counter; + finish[node] = *counter; + (*counter)+=1; + + auto from = rowGroupIndice[node]; + auto to = rowGroupIndice[node+1]; + + for(uint64_t i =from; i::SupportsExponential, int>::type=0> + storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCycles(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ + + storm::storage::BitVector const& probabilisticStates = ~markovianStates; + storm::storage::BitVector const& probabilisticNonGoalStates = ~markovianStates & ~psiStates; + + storm::storage::SparseMatrix const& probMatrix = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, probabilisticNonGoalStates); + uint64_t probSize = probMatrix.getRowGroupCount(); + std::vector disc(probSize, 0), finish(probSize, 0); + + uint64_t counter =1; + + for (uint64_t i =0; i::SupportsExponential, int>::type> std::vector SparseMarkovAutomatonCslHelper::unifPlus( std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); - + + storm::storage::BitVector const& probabilisticNonGoalStates = ~markovianStates & ~psiStates; + auto cycleStates = identifyProbCycles(transitionMatrix, markovianStates, psiStates); + + for (int i=0 ; i < cycleStates.size() ; i++ ){ + std::cout << cycleStates[i] << "\t" << probabilisticNonGoalStates[i] <<"\n"; + } std::ofstream logfile("U+logfile.txt", std::ios::app); ValueType maxNorm = 0; diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index ff27180bd..559912c2e 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -56,7 +56,20 @@ namespace storm { static std::vector computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: + static uint64_t transformIndice(storm::storage::BitVector const& subset, uint64_t fakeId){ + uint64_t id =0; + uint64_t counter =0; + while(counter<=fakeId){ + if(subset[id]){ + counter++; + } + id++; + } + return id-1; + } + template ::SupportsExponential, int>::type=0> + static storm::storage::BitVector identifyProbCycles(storm::storage::SparseMatrix const& TransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates); /*! * Computes the poission-distribution * @@ -69,6 +82,8 @@ namespace storm { template static ValueType poisson(ValueType lambda, uint64_t i); + template ::SupportsExponential, int>::type=0> + static int trajans(storm::storage::SparseMatrix const& TransitionMatrix, uint64_t node, std::vector& disc, std::vector& finish, uint64_t * counter); /*! * Computes vd vector according to UnifPlus From fe863679bfae91277c45e09b947027508b086882 Mon Sep 17 00:00:00 2001 From: Timo Philipp Gros Date: Sun, 19 Nov 2017 15:26:30 +0100 Subject: [PATCH 2/2] identify probCycles outgoing states --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 47 +++++++++++++++---- .../helper/SparseMarkovAutomatonCslHelper.h | 6 ++- 2 files changed, 43 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 88d470dce..54abee155 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -136,7 +136,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - void SparseMarkovAutomatonCslHelper::printTransitions(std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, std::vector>& vd, std::vector>& vu, std::vector>& wu){ + void SparseMarkovAutomatonCslHelper::printTransitions(std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector>& vd, std::vector>& vu, std::vector>& wu){ std::ofstream logfile("U+logfile.txt", std::ios::app); auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); @@ -160,6 +160,13 @@ namespace storm { } logfile << "\n"; + logfile << "probStates\tmarkovianStates\tgoalStates\tcycleStates\tcycleGoalStates\n"; + for (int i =0 ; i< markovianStates.size() ; i++){ + logfile << (~markovianStates)[i] << "\t" << markovianStates[i] << "\t" << psiStates[i] << "\t" << cycleStates[i] << "\t" << cycleGoalStates[i] << "\n"; + } + + + logfile << "vd: \n"; for (uint_fast64_t i =0 ; i::SupportsExponential, int>::type=0> int SparseMarkovAutomatonCslHelper::trajans(storm::storage::SparseMatrix const& transitionMatrix, uint64_t node, std::vector& disc, std::vector& finish, uint64_t* counter) { - auto const &rowGroupIndice = transitionMatrix.getRowGroupIndices(); + auto const& rowGroupIndice = transitionMatrix.getRowGroupIndices(); disc[node] = *counter; finish[node] = *counter; @@ -362,8 +369,31 @@ namespace storm { return finish[node]; } - template ::SupportsExponential, int>::type=0> + storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCyclesGoalStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& cycleStates) { + + storm::storage::BitVector goalStates(cycleStates.size(), false); + auto const& rowGroupIndices = transitionMatrix.getRowGroupIndices(); + + for (uint64_t i = 0 ; i < transitionMatrix.getRowGroupCount() ; i++){ + if (!cycleStates[i]){ + continue; + } + auto from = rowGroupIndices[i]; + auto to = rowGroupIndices[i+1]; + for (auto j = from ; j::SupportsExponential, int>::type=0> storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCycles(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ storm::storage::BitVector const& probabilisticStates = ~markovianStates; @@ -392,7 +422,6 @@ namespace storm { auto f = finish[i]; for (int j =i; j SparseMarkovAutomatonCslHelper::unifPlus( std::pair const& boundsPair, std::vector const& exitRateVector, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){ STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); + storm::storage::BitVector const& probabilisticNonGoalStates = ~markovianStates & ~psiStates; auto cycleStates = identifyProbCycles(transitionMatrix, markovianStates, psiStates); + auto cycleGoals = identifyProbCyclesGoalStates(transitionMatrix, cycleStates); + - for (int i=0 ; i < cycleStates.size() ; i++ ){ - std::cout << cycleStates[i] << "\t" << probabilisticNonGoalStates[i] <<"\n"; - } std::ofstream logfile("U+logfile.txt", std::ios::app); ValueType maxNorm = 0; @@ -423,6 +452,7 @@ namespace storm { //vectors to save calculation std::vector> vd,vu,wu; + printTransitions(exitRateVector, transitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished //transition matrix with diagonal entries. The values can be changed during uniformisation std::vector exitRate{exitRateVector}; @@ -508,7 +538,6 @@ namespace storm { vu = std::vector> (N + 1, init); wu = std::vector> (N + 1, init); - printTransitions(exitRate, fullTransitionMatrix, markovianStates,vd,vu,wu); // TODO: delete when develepmont is finished // (5) calculate vectors and maxNorm for (uint64_t i = 0; i < numberOfStates; i++) { @@ -521,7 +550,7 @@ namespace storm { maxNorm = std::max(maxNorm, diff); } } - printTransitions(exitRate, fullTransitionMatrix, markovianStates,vd,vu,wu); // TODO: delete when development is finished + //printTransitions(exitRate, fullTransitionMatrix, markovianStates,vd,vu,wu); // TODO: delete when development is finished // (6) double lambda diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 559912c2e..421a1e21a 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -69,6 +69,10 @@ namespace storm { } template ::SupportsExponential, int>::type=0> + static storm::storage::BitVector identifyProbCyclesGoalStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& cycleStates); + + + template ::SupportsExponential, int>::type=0> static storm::storage::BitVector identifyProbCycles(storm::storage::SparseMatrix const& TransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates); /*! * Computes the poission-distribution @@ -114,7 +118,7 @@ namespace storm { */ template ::SupportsExponential, int>::type=0> - static void printTransitions(std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates,std::vector>& vd, std::vector>& vu, std::vector>& wu); + static void printTransitions(std::vector const& exitRateVector, storm::storage::SparseMatrix const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& cycleStates, storm::storage::BitVector const& cycleGoalStates, std::vector>& vd, std::vector>& vu, std::vector>& wu); 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);