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

fixed bugs, runnig now

main
Timo Philipp Gros 8 years ago
parent
253b34ce09
commit
286fc8aec7
2 changed files with 24 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 27
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  2. 8
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h

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

@ -357,7 +357,7 @@ namespace storm {
} }
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0> 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) {
uint64_t 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; disc[node] = *counter;
@ -430,7 +430,7 @@ namespace storm {
storm::storage::BitVector cycleStates(markovianStates.size(), false); storm::storage::BitVector cycleStates(markovianStates.size(), false);
for (int i = 0 ; i< finish.size() ; i++){ for (int i = 0 ; i< finish.size() ; i++){
auto f = finish[i]; auto f = finish[i];
for (int j =i; j<finish.size() ; j++){
for (int j =i+1; j<finish.size() ; j++){
if (finish[j]==f){ if (finish[j]==f){
cycleStates.set(transformIndice(probabilisticNonGoalStates,i),true); cycleStates.set(transformIndice(probabilisticNonGoalStates,i),true);
cycleStates.set(transformIndice(probabilisticNonGoalStates,j),true); cycleStates.set(transformIndice(probabilisticNonGoalStates,j),true);
@ -441,9 +441,9 @@ namespace storm {
return cycleStates; return cycleStates;
} }
template <typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper::deleteProbDiagonalEntries(storm::storage::SparseMatrix<ValueType>& transitionMatrix, storm::storage::BitVector const& markovianStates){
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
void SparseMarkovAutomatonCslHelper::deleteProbDiagonals(storm::storage::SparseMatrix<ValueType>& transitionMatrix, storm::storage::BitVector const& markovianStates){
auto const& rowGroupIndices = transitionMatrix.getRowGroupIndices(); auto const& rowGroupIndices = transitionMatrix.getRowGroupIndices();
for (uint64_t i =0; i<transitionMatrix.getRowGroupCount(); i++) { for (uint64_t i =0; i<transitionMatrix.getRowGroupCount(); i++) {
@ -459,6 +459,7 @@ namespace storm {
selfLoop = element.getValue(); selfLoop = element.getValue();
} }
} }
if (selfLoop==0){ if (selfLoop==0){
continue; continue;
} }
@ -467,10 +468,17 @@ namespace storm {
element.setValue(element.getValue()/(1-selfLoop)); element.setValue(element.getValue()/(1-selfLoop));
} else { } else {
element.setValue(0); element.setValue(0);
} }
} }
} }
} }
}
template <typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper::deleteProbDiagonalEntries(storm::storage::SparseMatrix<ValueType>& transitionMatrix, storm::storage::BitVector const& markovianStates){
} }
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type> template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
@ -494,11 +502,14 @@ namespace storm {
//delete prob-diagonal entries //delete prob-diagonal entries
deleteProbDiagonalEntries(fullTransitionMatrix, markovianStates);
//deleteProbDiagonalEntries(fullTransitionMatrix, markovianStates);
deleteProbDiagonals(fullTransitionMatrix, markovianStates);
//identify cycles and cycleGoals //identify cycles and cycleGoals
auto cycleStates = identifyProbCycles(transitionMatrix, markovianStates, psiStates);
auto cycleGoals = identifyProbCyclesGoalStates(transitionMatrix, cycleStates);
auto cycleStates = identifyProbCycles(fullTransitionMatrix, markovianStates, psiStates);
auto cycleGoals = identifyProbCyclesGoalStates(fullTransitionMatrix, cycleStates);
printTransitions(exitRateVector, fullTransitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished
//(1) define horizon, epsilon, kappa , N, lambda, //(1) define horizon, epsilon, kappa , N, lambda,
@ -552,7 +563,6 @@ namespace storm {
vu = std::vector<std::vector<ValueType>> (N + 1, init); vu = std::vector<std::vector<ValueType>> (N + 1, init);
wu = std::vector<std::vector<ValueType>> (N + 1, init); wu = std::vector<std::vector<ValueType>> (N + 1, init);
printTransitions(exitRateVector, transitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished
// (5) calculate vectors and maxNorm // (5) calculate vectors and maxNorm
for (uint64_t i = 0; i < numberOfStates; i++) { for (uint64_t i = 0; i < numberOfStates; i++) {
@ -565,7 +575,6 @@ namespace storm {
maxNorm = std::max(maxNorm, diff); maxNorm = std::max(maxNorm, diff);
} }
} }
printTransitions(exitRateVector, transitionMatrix, markovianStates, psiStates, cycleStates, cycleGoals, vd,vu,wu); // TODO: delete when develepmont is finished
// (6) double lambda // (6) double lambda

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

@ -56,6 +56,10 @@ 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); 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: private:
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
static void deleteProbDiagonals(storm::storage::SparseMatrix<ValueType>& transitionMatrix, storm::storage::BitVector const& markovianStates);
static uint64_t transformIndice(storm::storage::BitVector const& subset, uint64_t fakeId){ static uint64_t transformIndice(storm::storage::BitVector const& subset, uint64_t fakeId){
uint64_t id =0; uint64_t id =0;
uint64_t counter =0; uint64_t counter =0;
@ -84,14 +88,14 @@ namespace storm {
* *
* @param parameter lambda to use * @param parameter lambda to use
* @param point i * @param point i
* TODO: replace with Fox-Lynn
* TODO: replace with Fox-glynn
* @return the probability * @return the probability
*/ */
template <typename ValueType> template <typename ValueType>
static ValueType poisson(ValueType lambda, uint64_t i); static ValueType poisson(ValueType lambda, uint64_t i);
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0> 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);
static uint64_t 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 * Computes vd vector according to UnifPlus

Write Preview
Loading…
Cancel
Save