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

lra into multivalueeliminator 

Former-commit-id: 981aebe161
main
sjunges 9 years ago
parent
979c90fac2
commit
ee4cb38d43
4 changed files with 45 additions and 42 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. 4
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 33
      src/solver/stateelimination/LongRunAverageEliminator.cpp
  3. 38
      src/solver/stateelimination/MultiValueStateEliminator.cpp
  4. 12
      src/solver/stateelimination/MultiValueStateEliminator.h

4
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -18,7 +18,7 @@
#include "src/logic/FragmentSpecification.h"
#include "src/solver/stateelimination/LongRunAverageEliminator.h"
#include "src/solver/stateelimination/MultiValueStateEliminator.h"
#include "src/solver/stateelimination/ConditionalStateEliminator.h"
#include "src/solver/stateelimination/PrioritizedStateEliminator.h"
#include "src/solver/stateelimination/StaticStatePriorityQueue.h"
@ -226,7 +226,7 @@ namespace storm {
// First, we eliminate all states in BSCCs (except for the representative states).
std::shared_ptr<StatePriorityQueue> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs);
storm::solver::stateelimination::LongRunAverageEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates);
storm::solver::stateelimination::MultiValueStateEliminator<ValueType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates);
while (priorityQueue->hasNext()) {
storm::storage::sparse::state_type state = priorityQueue->pop();

33
src/solver/stateelimination/LongRunAverageEliminator.cpp
View File

@ -1,33 +0,0 @@
#include "src/solver/stateelimination/LongRunAverageEliminator.h"
#include "src/utility/constants.h"
namespace storm {
namespace solver {
namespace stateelimination {
template<typename ValueType>
LongRunAverageEliminator<ValueType>::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates) : PrioritizedStateEliminator<ValueType>(transitionMatrix, backwardTransitions, priorityQueue, stateValues), averageTimeInStates(averageTimeInStates) {
}
template<typename ValueType>
void LongRunAverageEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
averageTimeInStates[state] = storm::utility::simplify(loopProbability * averageTimeInStates[state]);
}
template<typename ValueType>
void LongRunAverageEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
averageTimeInStates[predecessor] = storm::utility::simplify(averageTimeInStates[predecessor] + storm::utility::simplify(probability * averageTimeInStates[state]));
}
template class LongRunAverageEliminator<double>;
#ifdef STORM_HAVE_CARL
template class LongRunAverageEliminator<storm::RationalNumber>;
template class LongRunAverageEliminator<storm::RationalFunction>;
#endif
} // namespace stateelimination
} // namespace storage
} // namespace storm

38
src/solver/stateelimination/MultiValueStateEliminator.cpp
View File

@ -0,0 +1,38 @@
#include "src/solver/stateelimination/MultiValueStateEliminator.h"
#include "src/utility/constants.h"
namespace storm {
namespace solver {
namespace stateelimination {
template<typename ValueType>
MultiValueStateEliminator<ValueType>::MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValuesVector) : PrioritizedStateEliminator<ValueType>(transitionMatrix, backwardTransitions, priorityQueue, stateValues), additionalStateValues({std::ref(additionalStateValuesVector)}) {
}
template<typename ValueType>
void MultiValueStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
for(auto additionalStateValueVectorRef : additionalStateValues) {
additionalStateValueVectorRef.get()[state] = storm::utility::simplify(loopProbability * additionalStateValueVectorRef.get()[state]);
}
}
template<typename ValueType>
void MultiValueStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
for(auto additionalStateValueVectorRef : additionalStateValues) {
additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify(additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify(probability * additionalStateValueVectorRef.get()[state]));
}
}
template class MultiValueStateEliminator<double>;
#ifdef STORM_HAVE_CARL
template class MultiValueStateEliminator<storm::RationalNumber>;
template class MultiValueStateEliminator<storm::RationalFunction>;
#endif
} // namespace stateelimination
} // namespace storage
} // namespace storm

12
src/solver/stateelimination/LongRunAverageEliminator.h → src/solver/stateelimination/MultiValueStateEliminator.h
View File

@ -1,6 +1,4 @@
#ifndef STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_
#define STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_
#pragma once
#include "src/solver/stateelimination/PrioritizedStateEliminator.h"
namespace storm {
@ -10,22 +8,22 @@ namespace storm {
class StatePriorityQueue;
template<typename ValueType>
class LongRunAverageEliminator : public PrioritizedStateEliminator<ValueType> {
class MultiValueStateEliminator : public PrioritizedStateEliminator<ValueType> {
public:
typedef typename std::shared_ptr<StatePriorityQueue> PriorityQueuePointer;
typedef typename std::vector<ValueType> ValueTypeVector;
LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates);
MultiValueStateEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& additionalStateValues);
// Instantiaton of virtual methods.
void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override;
void updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) override;
private:
std::vector<ValueType>& averageTimeInStates;
std::vector<std::reference_wrapper<ValueTypeVector>>additionalStateValues;
};
} // namespace stateelimination
} // namespace storage
} // namespace storm
#endif // STORM_SOLVER_STATEELIMINATION_LONGRUNAVERAGEELIMINATOR_H_
Write Preview
Loading…
Cancel
Save