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

implemented trajans alg to identify prob Cycles

main
Timo Philipp Gros 8 years ago
parent
652b69c5b0
commit
25a7b6c71a
2 changed files with 88 additions and 1 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. 74
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  2. 15
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h

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

@ -337,10 +337,82 @@ namespace storm {
logfile << " res = " << res << "\n";
}
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();
disc[node] = *counter;
finish[node] = *counter;
(*counter)+=1;
auto from = rowGroupIndice[node];
auto to = rowGroupIndice[node+1];
for(uint64_t i =from; i<to ; i++ ) {
for(auto element : transitionMatrix.getRow(i)){
if (disc[element.getColumn()]==0){
uint64_t back = trajans(transitionMatrix,element.getColumn(),disc,finish, counter);
finish[node]=std::min(finish[node], back);
} else {
finish[node]=std::min(finish[node], disc[element.getColumn()]);
}
}
}
return finish[node];
}
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;
storm::storage::BitVector const& probabilisticNonGoalStates = ~markovianStates & ~psiStates;
storm::storage::SparseMatrix<ValueType> const& probMatrix = transitionMatrix.getSubmatrix(true, probabilisticNonGoalStates, probabilisticNonGoalStates);
uint64_t probSize = probMatrix.getRowGroupCount();
std::vector<uint64_t> disc(probSize, 0), finish(probSize, 0);
uint64_t counter =1;
for (uint64_t i =0; i<probSize; i++){
if (disc[i]==0) {
trajans(probMatrix, i, disc, finish, &counter);
}
}
std::cout << "giving the circle vectors \n";
for (uint64_t i = 0 ; i<probSize; i++){
std::cout << disc[i] << '\t' << finish[i] << "\n";
}
storm::storage::BitVector cycleStates(markovianStates.size(), false);
for (int i = 0 ; i< finish.size() ; i++){
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);
}
}
}
return cycleStates;
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
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);
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;

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

@ -56,7 +56,20 @@ namespace storm {
static std::vector<ValueType> computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> 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 <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
*
@ -69,6 +82,8 @@ namespace storm {
template <typename ValueType>
static ValueType poisson(ValueType lambda, uint64_t i);
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
static int trajans(storm::storage::SparseMatrix<ValueType> const& TransitionMatrix, uint64_t node, std::vector<uint64_t>& disc, std::vector<uint64_t>& finish, uint64_t * counter);
/*!
* Computes vd vector according to UnifPlus

Write Preview
Loading…
Cancel
Save