From 253b34ce094404cc1ddccd23f762c4a285e9cbe3 Mon Sep 17 00:00:00 2001 From: Timo Philipp Gros Date: Mon, 20 Nov 2017 08:51:55 +0100 Subject: [PATCH] modularised diagonal-prob entrie delete and skipped zero loops in cycle identification --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 81 ++++++++++--------- .../helper/SparseMarkovAutomatonCslHelper.h | 6 +- 2 files changed, 47 insertions(+), 40 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 725594d5b..b9aaa221e 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -162,7 +162,7 @@ namespace storm { 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 << (~markovianStates)[i] << "\t\t" << markovianStates[i] << "\t\t" << psiStates[i] << "\t\t" << cycleStates[i] << "\t\t" << cycleGoalStates[i] << "\n"; } @@ -369,6 +369,9 @@ namespace storm { for(uint64_t i =from; i + std::vector SparseMarkovAutomatonCslHelper::deleteProbDiagonalEntries(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates){ - 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_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); - - - std::ofstream logfile("U+logfile.txt", std::ios::app); - ValueType maxNorm = 0; - - //bitvectors to identify different kind of states -// storm::storage::BitVector const &markovianNonGoalStates = markovianStates & ~psiStates; -// storm::storage::BitVector const &probabilisticNonGoalStates = ~markovianStates & ~psiStates; - storm::storage::BitVector allStates(markovianStates.size(), true); - - //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}; - typename storm::storage::SparseMatrix fullTransitionMatrix = transitionMatrix.getSubmatrix(true, allStates , allStates , true); - auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); + auto const& rowGroupIndices = transitionMatrix.getRowGroupIndices(); - //delete prob-diagonal entries - for (uint64_t i =0; i::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_LOG_TRACE("Using UnifPlus to compute bounded until probabilities."); + + std::ofstream logfile("U+logfile.txt", std::ios::app); + ValueType maxNorm = 0; + + //bitvectors to identify different kind of states + storm::storage::BitVector allStates(markovianStates.size(), true); + + //vectors to save calculation + std::vector> vd,vu,wu; + + + //transition matrix with diagonal entries. The values can be changed during uniformisation + std::vector exitRate{exitRateVector}; + typename storm::storage::SparseMatrix fullTransitionMatrix = transitionMatrix.getSubmatrix(true, allStates , allStates , true); + auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices(); + + + //delete prob-diagonal entries + deleteProbDiagonalEntries(fullTransitionMatrix, markovianStates); + + //identify cycles and cycleGoals + auto cycleStates = identifyProbCycles(transitionMatrix, markovianStates, psiStates); + auto cycleGoals = identifyProbCyclesGoalStates(transitionMatrix, cycleStates); //(1) define horizon, epsilon, kappa , N, lambda, @@ -543,13 +545,14 @@ namespace storm { } exitRate[i] = exitNew; } - + // (4) define vectors/matrices std::vector init(numberOfStates, -1); vd = std::vector> (N + 1, init); vu = std::vector> (N + 1, init); wu = std::vector> (N + 1, init); - + + printTransitions(exitRateVector, transitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished // (5) calculate vectors and maxNorm for (uint64_t i = 0; i < numberOfStates; i++) { @@ -562,7 +565,7 @@ namespace storm { maxNorm = std::max(maxNorm, diff); } } - //printTransitions(exitRate, fullTransitionMatrix, markovianStates,vd,vu,wu); // TODO: delete when development is finished + printTransitions(exitRateVector, transitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished // (6) double lambda diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index 908668d2b..363de0867 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -68,7 +68,11 @@ namespace storm { return id-1; } - template ::SupportsExponential, int>::type=0> + template + static std::vector deleteProbDiagonalEntries(storm::storage::SparseMatrix& transitionMatrix, storm::storage::BitVector const& markovianStates); + + + template ::SupportsExponential, int>::type=0> static storm::storage::BitVector identifyProbCyclesGoalStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& cycleStates);