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

Merge branch 'exact_equation_solver' into monolithic-dft 

Former-commit-id: aebbb68f38
main
Mavo 9 years ago
parent
f1bf0f5469 56bcdcc807
commit
cd638e6908
7 changed files with 27 additions and 27 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. 26
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 6
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  3. 4
      src/solver/stateelimination/LongRunAverageEliminator.cpp
  4. 5
      src/solver/stateelimination/LongRunAverageEliminator.h
  5. 4
      src/solver/stateelimination/PrioritizedEliminator.cpp
  6. 5
      src/solver/stateelimination/PrioritizedEliminator.h
  7. 4
      src/storage/FlexibleSparseMatrix.h

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

@ -304,8 +304,8 @@ namespace storm {
std::vector<ValueType> averageTimeInStates(stateValues.size(), storm::utility::one<ValueType>());
// First, we eliminate all states in BSCCs (except for the representative states).
std::unique_ptr<StatePriorityQueue<ValueType>> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs);
storm::solver::stateelimination::LongRunAverageEliminator<SparseDtmcModelType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, *priorityQueue, stateValues, averageTimeInStates);
std::shared_ptr<StatePriorityQueue<ValueType>> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs);
storm::solver::stateelimination::LongRunAverageEliminator<SparseDtmcModelType> stateEliminator(flexibleMatrix, flexibleBackwardTransitions, priorityQueue, stateValues, averageTimeInStates);
while (priorityQueue->hasNextState()) {
storm::storage::sparse::state_type state = priorityQueue->popNextState();
@ -744,7 +744,7 @@ namespace storm {
storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(submatrixTransposed, true);
std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now();
std::unique_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
STORM_LOG_INFO("Computing conditional probilities." << std::endl);
std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
@ -871,7 +871,7 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<StatePriorityQueue<typename SparseDtmcModelType::ValueType>> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states) {
std::shared_ptr<StatePriorityQueue<typename SparseDtmcModelType::ValueType>> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states) {
STORM_LOG_TRACE("Creating state priority queue for states " << states);
@ -915,15 +915,15 @@ namespace storm {
}
template<typename SparseDtmcModelType>
std::unique_ptr<StatePriorityQueue<typename SparseDtmcModelType::ValueType>> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createNaivePriorityQueue(storm::storage::BitVector const& states) {
std::shared_ptr<StatePriorityQueue<typename SparseDtmcModelType::ValueType>> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::createNaivePriorityQueue(storm::storage::BitVector const& states) {
std::vector<storm::storage::sparse::state_type> sortedStates(states.begin(), states.end());
return std::unique_ptr<StatePriorityQueue<ValueType>>(new StaticStatePriorityQueue(sortedStates));
return std::shared_ptr<StatePriorityQueue<ValueType>>(new StaticStatePriorityQueue(sortedStates));
}
template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performPrioritizedStateElimination(std::unique_ptr<StatePriorityQueue<ValueType>>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) {
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performPrioritizedStateElimination(std::shared_ptr<StatePriorityQueue<ValueType>>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) {
storm::solver::stateelimination::PrioritizedEliminator<SparseDtmcModelType> stateEliminator(transitionMatrix, backwardTransitions, *priorityQueue, values);
storm::solver::stateelimination::PrioritizedEliminator<SparseDtmcModelType> stateEliminator(transitionMatrix, backwardTransitions, priorityQueue, values);
while (priorityQueue->hasNextState()) {
storm::storage::sparse::state_type state = priorityQueue->popNextState();
@ -938,7 +938,7 @@ namespace storm {
template<typename SparseDtmcModelType>
void SparseDtmcEliminationModelChecker<SparseDtmcModelType>::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities) {
std::unique_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem);
std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem);
std::size_t numberOfStatesToEliminate = statePriorities->size();
STORM_LOG_DEBUG("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl);
@ -957,7 +957,7 @@ namespace storm {
if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) {
STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
std::vector<storm::storage::sparse::state_type> sortedStates(entryStateQueue.begin(), entryStateQueue.end());
std::unique_ptr<StatePriorityQueue<ValueType>> queuePriorities = std::unique_ptr<StatePriorityQueue<ValueType>>(new StaticStatePriorityQueue(sortedStates));
std::shared_ptr<StatePriorityQueue<ValueType>> queuePriorities = std::shared_ptr<StatePriorityQueue<ValueType>>(new StaticStatePriorityQueue(sortedStates));
performPrioritizedStateElimination(queuePriorities, transitionMatrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly);
}
STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl);
@ -1028,7 +1028,7 @@ namespace storm {
}
}
std::unique_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs);
std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs);
STORM_LOG_TRACE("Eliminating " << statePriorities->size() << " trivial SCCs.");
performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly);
STORM_LOG_TRACE("Eliminated all trivial SCCs.");
@ -1058,7 +1058,7 @@ namespace storm {
} else {
// In this case, we perform simple state elimination in the current SCC.
STORM_LOG_TRACE("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly.");
std::unique_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates);
std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates);
performPrioritizedStateElimination(statePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly);
STORM_LOG_TRACE("Eliminated all states of SCC.");
}
@ -1066,7 +1066,7 @@ namespace storm {
// Finally, eliminate the entry states (if we are required to do so).
if (eliminateEntryStates) {
STORM_LOG_TRACE("Finally, eliminating entry states.");
std::unique_ptr<StatePriorityQueue<ValueType>> naivePriorities = createNaivePriorityQueue(entryStates);
std::shared_ptr<StatePriorityQueue<ValueType>> naivePriorities = createNaivePriorityQueue(entryStates);
performPrioritizedStateElimination(naivePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly);
STORM_LOG_TRACE("Eliminated/added entry states.");
} else {

6
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -93,11 +93,11 @@ namespace storm {
static std::vector<ValueType> computeReachabilityValues(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& values, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& oneStepProbabilitiesToTarget);
static std::unique_ptr<StatePriorityQueue<ValueType>> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& stateDistances, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states);
static std::shared_ptr<StatePriorityQueue<ValueType>> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& stateDistances, storm::storage::FlexibleSparseMatrix<ValueType> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& states);
static std::unique_ptr<StatePriorityQueue<ValueType>> createNaivePriorityQueue(storm::storage::BitVector const& states);
static std::shared_ptr<StatePriorityQueue<ValueType>> createNaivePriorityQueue(storm::storage::BitVector const& states);
static void performPrioritizedStateElimination(std::unique_ptr<StatePriorityQueue<ValueType>>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly);
static void performPrioritizedStateElimination(std::shared_ptr<StatePriorityQueue<ValueType>>& priorityQueue, storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, std::vector<ValueType>& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly);
static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector<ValueType>& values, boost::optional<std::vector<ValueType>>& additionalStateValues, boost::optional<std::vector<uint_fast64_t>> const& distanceBasedPriorities);

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

@ -5,7 +5,7 @@ namespace storm {
namespace stateelimination {
template<typename SparseModelType>
LongRunAverageEliminator<SparseModelType>::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::modelchecker::StatePriorityQueue<ValueType>& priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) {
LongRunAverageEliminator<SparseModelType>::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) {
}
template<typename SparseModelType>
@ -22,7 +22,7 @@ namespace storm {
template<typename SparseModelType>
void LongRunAverageEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
priorityQueue.update(state, StateEliminator<SparseModelType>::transitionMatrix, StateEliminator<SparseModelType>::backwardTransitions, stateValues);
priorityQueue->update(state, StateEliminator<SparseModelType>::transitionMatrix, StateEliminator<SparseModelType>::backwardTransitions, stateValues);
}
template<typename SparseModelType>

5
src/solver/stateelimination/LongRunAverageEliminator.h
View File

@ -11,9 +11,10 @@ namespace storm {
class LongRunAverageEliminator : public StateEliminator<SparseModelType> {
typedef typename SparseModelType::ValueType ValueType;
typedef typename std::shared_ptr<storm::modelchecker::StatePriorityQueue<ValueType>> PriorityQueuePointer;
public:
LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::modelchecker::StatePriorityQueue<ValueType>& priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates);
LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues, std::vector<ValueType>& averageTimeInStates);
// Instantiaton of Virtual methods
void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override;
@ -24,7 +25,7 @@ namespace storm {
private:
storm::modelchecker::StatePriorityQueue<ValueType>& priorityQueue;
PriorityQueuePointer priorityQueue;
std::vector<ValueType>& stateValues;
std::vector<ValueType>& averageTimeInStates;
};

4
src/solver/stateelimination/PrioritizedEliminator.cpp
View File

@ -5,7 +5,7 @@ namespace storm {
namespace stateelimination {
template<typename SparseModelType>
PrioritizedEliminator<SparseModelType>::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::modelchecker::StatePriorityQueue<ValueType> priorityQueue, std::vector<ValueType>& stateValues) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) {
PrioritizedEliminator<SparseModelType>::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues) : StateEliminator<SparseModelType>(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) {
}
template<typename SparseModelType>
@ -20,7 +20,7 @@ namespace storm {
template<typename SparseModelType>
void PrioritizedEliminator<SparseModelType>::updatePriority(storm::storage::sparse::state_type const& state) {
priorityQueue.update(state, StateEliminator<SparseModelType>::transitionMatrix, StateEliminator<SparseModelType>::backwardTransitions, stateValues);
priorityQueue->update(state, StateEliminator<SparseModelType>::transitionMatrix, StateEliminator<SparseModelType>::backwardTransitions, stateValues);
}
template<typename SparseModelType>

5
src/solver/stateelimination/PrioritizedEliminator.h
View File

@ -11,9 +11,10 @@ namespace storm {
class PrioritizedEliminator : public StateEliminator<SparseModelType> {
typedef typename SparseModelType::ValueType ValueType;
typedef typename std::shared_ptr<storm::modelchecker::StatePriorityQueue<ValueType>> PriorityQueuePointer;
public:
PrioritizedEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, storm::modelchecker::StatePriorityQueue<ValueType> priorityQueue, std::vector<ValueType>& stateValues);
PrioritizedEliminator(storm::storage::FlexibleSparseMatrix<ValueType>& transitionMatrix, storm::storage::FlexibleSparseMatrix<ValueType>& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector<ValueType>& stateValues);
// Instantiaton of Virtual methods
void updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) override;
@ -23,7 +24,7 @@ namespace storm {
bool isFilterPredecessor() const override;
private:
storm::modelchecker::StatePriorityQueue<ValueType>& priorityQueue;
PriorityQueuePointer priorityQueue;
std::vector<ValueType>& stateValues;
};

4
src/storage/FlexibleSparseMatrix.h
View File

@ -21,9 +21,7 @@ namespace storm {
class FlexibleSparseMatrix {
public:
// TODO: make this class a bit more consistent with the big sparse matrix and improve it:
// * add output iterator and improve the way the matrix is printed
// * add stuff like clearRow, multiplyRowWithScalar
// * implement row grouping
// * add stuff like iterator, clearRow, multiplyRowWithScalar
typedef uint_fast64_t index_type;
typedef ValueType value_type;

Write Preview
Loading…
Cancel
Save