diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 8c64b83a7..85a432b12 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -304,8 +304,8 @@ namespace storm { std::vector averageTimeInStates(stateValues.size(), storm::utility::one()); // First, we eliminate all states in BSCCs (except for the representative states). - std::unique_ptr> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); - storm::solver::stateelimination::LongRunAverageEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, *priorityQueue, stateValues, averageTimeInStates); + std::shared_ptr> priorityQueue = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, stateValues, regularStatesInBsccs); + storm::solver::stateelimination::LongRunAverageEliminator 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 flexibleBackwardTransitions(submatrixTransposed, true); std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now(); - std::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate); + std::shared_ptr> 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 - std::unique_ptr> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { + std::shared_ptr> SparseDtmcEliminationModelChecker::createStatePriorityQueue(boost::optional> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states) { STORM_LOG_TRACE("Creating state priority queue for states " << states); @@ -915,15 +915,15 @@ namespace storm { } template - std::unique_ptr> SparseDtmcEliminationModelChecker::createNaivePriorityQueue(storm::storage::BitVector const& states) { + std::shared_ptr> SparseDtmcEliminationModelChecker::createNaivePriorityQueue(storm::storage::BitVector const& states) { std::vector sortedStates(states.begin(), states.end()); - return std::unique_ptr>(new StaticStatePriorityQueue(sortedStates)); + return std::shared_ptr>(new StaticStatePriorityQueue(sortedStates)); } template - void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::unique_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { + void SparseDtmcEliminationModelChecker::performPrioritizedStateElimination(std::shared_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly) { - storm::solver::stateelimination::PrioritizedEliminator stateEliminator(transitionMatrix, backwardTransitions, *priorityQueue, values); + storm::solver::stateelimination::PrioritizedEliminator stateEliminator(transitionMatrix, backwardTransitions, priorityQueue, values); while (priorityQueue->hasNextState()) { storm::storage::sparse::state_type state = priorityQueue->popNextState(); @@ -938,7 +938,7 @@ namespace storm { template void SparseDtmcEliminationModelChecker::performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional> const& distanceBasedPriorities) { - std::unique_ptr> statePriorities = createStatePriorityQueue(distanceBasedPriorities, transitionMatrix, backwardTransitions, values, subsystem); + std::shared_ptr> 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 sortedStates(entryStateQueue.begin(), entryStateQueue.end()); - std::unique_ptr> queuePriorities = std::unique_ptr>(new StaticStatePriorityQueue(sortedStates)); + std::shared_ptr> queuePriorities = std::shared_ptr>(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> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, statesInTrivialSccs); + std::shared_ptr> 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> statePriorities = createStatePriorityQueue(distanceBasedPriorities, matrix, backwardTransitions, values, scc & ~entryStates); + std::shared_ptr> 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> naivePriorities = createNaivePriorityQueue(entryStates); + std::shared_ptr> naivePriorities = createNaivePriorityQueue(entryStates); performPrioritizedStateElimination(naivePriorities, matrix, backwardTransitions, values, initialStates, computeResultsForInitialStatesOnly); STORM_LOG_TRACE("Eliminated/added entry states."); } else { diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h index 005b20b35..76e939d66 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h @@ -93,11 +93,11 @@ namespace storm { static std::vector computeReachabilityValues(storm::storage::SparseMatrix const& transitionMatrix, std::vector& values, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& oneStepProbabilitiesToTarget); - static std::unique_ptr> createStatePriorityQueue(boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); + static std::shared_ptr> createStatePriorityQueue(boost::optional> const& stateDistances, storm::storage::FlexibleSparseMatrix const& transitionMatrix, storm::storage::FlexibleSparseMatrix const& backwardTransitions, std::vector& oneStepProbabilities, storm::storage::BitVector const& states); - static std::unique_ptr> createNaivePriorityQueue(storm::storage::BitVector const& states); + static std::shared_ptr> createNaivePriorityQueue(storm::storage::BitVector const& states); - static void performPrioritizedStateElimination(std::unique_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); + static void performPrioritizedStateElimination(std::shared_ptr>& priorityQueue, storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& values, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly); static void performOrdinaryStateElimination(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& initialStates, bool computeResultsForInitialStatesOnly, std::vector& values, boost::optional>& additionalStateValues, boost::optional> const& distanceBasedPriorities); diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp index 250030c54..ec59dd1b1 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.cpp +++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp @@ -5,7 +5,7 @@ namespace storm { namespace stateelimination { template - LongRunAverageEliminator::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue& priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) { + LongRunAverageEliminator::LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues), averageTimeInStates(averageTimeInStates) { } template @@ -22,7 +22,7 @@ namespace storm { template void LongRunAverageEliminator::updatePriority(storm::storage::sparse::state_type const& state) { - priorityQueue.update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); + priorityQueue->update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); } template diff --git a/src/solver/stateelimination/LongRunAverageEliminator.h b/src/solver/stateelimination/LongRunAverageEliminator.h index 0e5522fef..f9b1e9cce 100644 --- a/src/solver/stateelimination/LongRunAverageEliminator.h +++ b/src/solver/stateelimination/LongRunAverageEliminator.h @@ -11,9 +11,10 @@ namespace storm { class LongRunAverageEliminator : public StateEliminator { typedef typename SparseModelType::ValueType ValueType; + typedef typename std::shared_ptr> PriorityQueuePointer; public: - LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue& priorityQueue, std::vector& stateValues, std::vector& averageTimeInStates); + LongRunAverageEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues, std::vector& 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& priorityQueue; + PriorityQueuePointer priorityQueue; std::vector& stateValues; std::vector& averageTimeInStates; }; diff --git a/src/solver/stateelimination/PrioritizedEliminator.cpp b/src/solver/stateelimination/PrioritizedEliminator.cpp index de760e66b..567d07df9 100644 --- a/src/solver/stateelimination/PrioritizedEliminator.cpp +++ b/src/solver/stateelimination/PrioritizedEliminator.cpp @@ -5,7 +5,7 @@ namespace storm { namespace stateelimination { template - PrioritizedEliminator::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue priorityQueue, std::vector& stateValues) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { + PrioritizedEliminator::PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& stateValues) : StateEliminator(transitionMatrix, backwardTransitions), priorityQueue(priorityQueue), stateValues(stateValues) { } template @@ -20,7 +20,7 @@ namespace storm { template void PrioritizedEliminator::updatePriority(storm::storage::sparse::state_type const& state) { - priorityQueue.update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); + priorityQueue->update(state, StateEliminator::transitionMatrix, StateEliminator::backwardTransitions, stateValues); } template diff --git a/src/solver/stateelimination/PrioritizedEliminator.h b/src/solver/stateelimination/PrioritizedEliminator.h index 7a242ebdf..1180fad09 100644 --- a/src/solver/stateelimination/PrioritizedEliminator.h +++ b/src/solver/stateelimination/PrioritizedEliminator.h @@ -11,9 +11,10 @@ namespace storm { class PrioritizedEliminator : public StateEliminator { typedef typename SparseModelType::ValueType ValueType; + typedef typename std::shared_ptr> PriorityQueuePointer; public: - PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, storm::modelchecker::StatePriorityQueue priorityQueue, std::vector& stateValues); + PrioritizedEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, PriorityQueuePointer priorityQueue, std::vector& 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& priorityQueue; + PriorityQueuePointer priorityQueue; std::vector& stateValues; }; diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index 5ab573057..163a25aa4 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -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;