sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

identify probCycles outgoing states

main
Timo Philipp Gros 7 years ago
parent
25a7b6c71a
commit
fe863679bf
2 changed files with 43 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 47
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  2. 6
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h

47
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -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, std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu){
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){
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<vd.size(); i++){
for(uint_fast64_t j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
@ -339,7 +346,7 @@ namespace storm {
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
int SparseMarkovAutomatonCslHelper::trajans(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, uint64_t node, std::vector<uint64_t >& disc, std::vector<uint64_t >& 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 <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCyclesGoalStates(storm::storage::SparseMatrix<ValueType> 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<to; j++){
for (auto element: transitionMatrix.getRow(j)) {
if (!cycleStates[element.getColumn()]){
goalStates.set(element.getColumn(),true);
}
}
}
}
return goalStates;
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
storm::storage::BitVector SparseMarkovAutomatonCslHelper::identifyProbCycles(storm::storage::SparseMatrix<ValueType> 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<finish.size() ; j++){
if (finish[j]==f){
cycleStates.set(transformIndice(probabilisticNonGoalStates,i),true);
cycleStates.set(transformIndice(probabilisticNonGoalStates,j),true);
}
@ -407,12 +436,12 @@ namespace storm {
std::vector<ValueType> SparseMarkovAutomatonCslHelper::unifPlus( std::pair<double, double> const& boundsPair, std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> 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<std::vector<ValueType>> 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<ValueType> exitRate{exitRateVector};
@ -508,7 +538,6 @@ namespace storm {
vu = std::vector<std::vector<ValueType>> (N + 1, init);
wu = std::vector<std::vector<ValueType>> (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

6
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
View File

@ -69,6 +69,10 @@ namespace storm {
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
static storm::storage::BitVector identifyProbCyclesGoalStates(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& cycleStates);
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
static storm::storage::BitVector identifyProbCycles(storm::storage::SparseMatrix<ValueType> const& TransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates);
/*!
* Computes the poission-distribution
@ -114,7 +118,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,std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu);
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);
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);

Write Preview
Loading…
Cancel
Save