From 3a18d609251fc89c0a3cc59368182b55db478d7a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 14 Dec 2014 22:30:29 +0100 Subject: [PATCH] Working towards reachability reward properties for parametric DTMCs. Former-commit-id: addf59ca34cffd1824c68d7d4c46ee245abd4695 --- .../reachability/SparseSccModelChecker.cpp | 207 +++++++----------- .../reachability/SparseSccModelChecker.h | 15 +- src/stormParametric.cpp | 8 +- 3 files changed, 91 insertions(+), 139 deletions(-) diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 45e9ab425..99622b0b9 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -17,7 +17,7 @@ namespace storm { namespace reachability { template - ValueType SparseSccModelChecker::computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& statePriorities) { + ValueType SparseSccModelChecker::computeReachabilityValue(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards, boost::optional> const& statePriorities) { std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now(); @@ -45,7 +45,7 @@ namespace storm { STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl); for (auto const& state : states) { - eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); } STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl); } else if (storm::settings::parametricSettings().getEliminationMethod() == storm::settings::modules::ParametricSettings::EliminationMethod::Hybrid) { @@ -53,13 +53,13 @@ namespace storm { storm::utility::ConstantsComparator comparator; std::vector entryStateQueue; STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl); - maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, statePriorities); + maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue, comparator, stateRewards, statePriorities); // If the entry states were to be eliminated last, we need to do so now. STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step."); if (storm::settings::parametricSettings().isEliminateEntryStatesLastSet()) { for (auto const& state : entryStateQueue) { - eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions); + eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards); } } STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states." << std::endl); @@ -67,7 +67,7 @@ namespace storm { // Finally eliminate initial state. STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << "." << std::endl); - eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions); + eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards); // Make sure that we have eliminated all transitions from the initial state. STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty."); @@ -101,38 +101,59 @@ namespace storm { return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]); } -// template -// ValueType SparseSccModelChecker::computeReachabilityReward(storm::models::Dtmc const& dtmc, std::shared_ptr> const& phiFormula, std::shared_ptr> const& psiFormula) { -// // Now retrieve the appropriate bitvectors from the atomic propositions. -// storm::storage::BitVector phiStates = phiFormula->getAp() != "true" ? dtmc.getLabeledStates(phiFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); -// storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiFormula->getAp()); -// -// // Do some sanity checks to establish some required properties. -// STORM_LOG_THROW(!dtmc.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported."); -// STORM_LOG_THROW(dtmc.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model."); -// STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); -// -// // Then, compute the subset of states that has a reachability reward less than infinity. -// storm::storage::BitVector trueStates(dtmc.getNumberOfStates(), true); -// storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(dtmc.getBackwardTransitions(), trueStates, psiStates); -// infinityStates.complement(); -// storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; -// -// // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result. -// STORM_LOG_THROW(dtmc.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward."); -// if (!dtmc.getInitialStates().isDisjointFrom(psiStates)) { -// STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); -// return storm::utility::constantZero(); -// } -// -// // Determine the set of states that is reachable from the initial state without jumping over a target state. -// storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, psiStates); -// -// // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). -// maybeStates &= reachableStates; -// -// -// } + template + ValueType SparseSccModelChecker::computeReachabilityReward(storm::models::Dtmc const& dtmc, std::shared_ptr> const& phiFormula, std::shared_ptr> const& psiFormula) { + // Now retrieve the appropriate bitvectors from the atomic propositions. + storm::storage::BitVector phiStates = phiFormula->getAp() != "true" ? dtmc.getLabeledStates(phiFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); + storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiFormula->getAp()); + + // Do some sanity checks to establish some required properties. + STORM_LOG_THROW(!dtmc.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported."); + STORM_LOG_THROW(dtmc.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model."); + STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); + + // Then, compute the subset of states that has a reachability reward less than infinity. + storm::storage::BitVector trueStates(dtmc.getNumberOfStates(), true); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(dtmc.getBackwardTransitions(), trueStates, psiStates); + infinityStates.complement(); + storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates; + + // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result. + STORM_LOG_THROW(dtmc.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward."); + if (!dtmc.getInitialStates().isDisjointFrom(psiStates)) { + STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step."); + return storm::utility::constantZero(); + } + + // Determine the set of states that is reachable from the initial state without jumping over a target state. + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, psiStates); + + // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). + maybeStates &= reachableStates; + + // Create a vector for the probabilities to go to a state with probability 1 in one step. + std::vector oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates); + + // Create a vector that holds the one-step rewards. + std::vector oneStepRewards = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + + // Project the state reward vector to all maybe-states. + boost::optional> stateRewards(maybeStates.getNumberOfSetBits()); + storm::utility::vector::selectVectorValues(stateRewards.get(), maybeStates, dtmc.getStateRewardVector()); + + // Determine the set of initial states of the sub-DTMC. + storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates; + + // We then build the submatrix that only has the transitions of the maybe states. + storm::storage::SparseMatrix submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrixTransposed = submatrix.transpose(); + + // Before starting the model checking process, we assign priorities to states so we can use them to + // impose ordering constraints later. + std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); + + return computeReachabilityValue(submatrix, oneStepRewards, submatrixTransposed, newInitialStates, phiStates, psiStates, stateRewards, statePriorities); + } template ValueType SparseSccModelChecker::computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& phiFormula, std::shared_ptr> const& psiFormula) { @@ -173,8 +194,16 @@ namespace storm { // Before starting the model checking process, we assign priorities to states so we can use them to // impose ordering constraints later. - std::vector statePriorities(submatrix.getRowCount()); - std::vector states(submatrix.getRowCount()); + std::vector statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities); + + boost::optional> missingStateRewards; + return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities); + } + + template + std::vector SparseSccModelChecker::getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities) { + std::vector statePriorities(transitionMatrix.getRowCount()); + std::vector states(transitionMatrix.getRowCount()); for (std::size_t index = 0; index < states.size(); ++index) { states[index] = index; } @@ -183,19 +212,19 @@ namespace storm { } else { std::vector distances; if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Forward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::ForwardReversed) { - distances = storm::utility::graph::getDistances(submatrix, newInitialStates); + distances = storm::utility::graph::getDistances(transitionMatrix, initialStates); } else if (storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::Backward || storm::settings::parametricSettings().getEliminationOrder() == storm::settings::modules::ParametricSettings::EliminationOrder::BackwardReversed) { // Since the target states were eliminated from the matrix already, we construct a replacement by // treating all states that have some non-zero probability to go to a target state in one step. storm::utility::ConstantsComparator comparator; - storm::storage::BitVector pseudoTargetStates(submatrix.getRowCount()); + storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount()); for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) { if (!comparator.isZero(oneStepProbabilities[index])) { pseudoTargetStates.set(index); } } - distances = storm::utility::graph::getDistances(submatrixTransposed, pseudoTargetStates); + distances = storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates); } else { STORM_LOG_ASSERT(false, "Illegal sorting order selected."); } @@ -214,7 +243,7 @@ namespace storm { statePriorities[states[index]] = index; } - return computeReachabilityProbability(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, statePriorities); + return statePriorities; } template @@ -232,7 +261,7 @@ namespace storm { } template - uint_fast64_t SparseSccModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& statePriorities) { + uint_fast64_t SparseSccModelChecker::treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional>& stateRewards, boost::optional> const& statePriorities) { uint_fast64_t maximalDepth = level; // If the SCCs are large enough, we try to split them further. @@ -264,7 +293,7 @@ namespace storm { STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs."); for (auto const& stateIndexPair : trivialSccs) { - eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions); + eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards); remainingSccs.set(stateIndexPair.second, false); } STORM_LOG_DEBUG("Eliminated all trivial SCCs."); @@ -288,7 +317,7 @@ namespace storm { } // Recursively descend in SCC-hierarchy. - uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, statePriorities); + uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, stateRewards, statePriorities); maximalDepth = std::max(maximalDepth, depth); } @@ -307,7 +336,7 @@ namespace storm { // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified) // transition probability matrix. for (auto const& state : states) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); } STORM_LOG_DEBUG("Eliminated all states of SCC."); @@ -317,7 +346,7 @@ namespace storm { if (eliminateEntryStates) { STORM_LOG_DEBUG("Finally, eliminating/adding entry states."); for (auto state : entryStates) { - eliminateState(matrix, oneStepProbabilities, state, backwardTransitions); + eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards); } STORM_LOG_DEBUG("Eliminated/added entry states."); } else { @@ -335,7 +364,7 @@ namespace storm { } template - void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions) { + void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards) { auto eliminationStart = std::chrono::high_resolution_clock::now(); ++counter; @@ -513,86 +542,6 @@ namespace storm { auto eliminationTime = eliminationEnd - eliminationStart; } - template - bool SparseSccModelChecker::eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions) { - typename storm::storage::SparseMatrix::iterator forwardElement = matrix.getRow(state).begin(); - typename storm::storage::SparseMatrix::iterator backwardElement = backwardTransitions.getRow(state).begin(); - - if (forwardElement->getValue() != storm::utility::constantOne() || backwardElement->getValue() != storm::utility::constantOne()) { - return false; - } - - std::cout << "eliminating " << state << std::endl; - std::cout << "fwd element: " << *forwardElement << " and bwd element: " << *backwardElement << std::endl; - - // Find the element of the predecessor that moves to the state that we want to eliminate. - typename storm::storage::SparseMatrix::rows forwardRow = matrix.getRow(backwardElement->getColumn()); - typename storm::storage::SparseMatrix::iterator multiplyElement = std::find_if(forwardRow.begin(), forwardRow.end(), [&](storm::storage::MatrixEntry::index_type, typename storm::storage::SparseMatrix::value_type> const& a) { return a.getColumn() == state; }); - - std::cout << "before fwd: " << std::endl; - for (auto element : matrix.getRow(backwardElement->getColumn())) { - std::cout << element << ", " << std::endl; - } - - // Modify the forward probability entry of the predecessor. - multiplyElement->setValue(multiplyElement->getValue() * forwardElement->getValue()); - multiplyElement->setColumn(forwardElement->getColumn()); - - // Modify the one-step probability for the predecessor if necessary. - if (oneStepProbabilities[state] != storm::utility::constantZero()) { - oneStepProbabilities[backwardElement->getColumn()] += multiplyElement->getValue() * oneStepProbabilities[state]; - } - - // If the forward entry is not at the right position, we need to move it there. - if (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) { - while (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) { - std::swap(*multiplyElement, *(multiplyElement - 1)); - --multiplyElement; - } - } else if ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) { - while ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) { - std::swap(*multiplyElement, *(multiplyElement + 1)); - ++multiplyElement; - } - } - - std::cout << "after fwd: " << std::endl; - for (auto element : matrix.getRow(backwardElement->getColumn())) { - std::cout << element << ", " << std::endl; - } - - // Find the backward element of the successor that moves to the state that we want to eliminate. - typename storm::storage::SparseMatrix::rows backwardRow = backwardTransitions.getRow(forwardElement->getColumn()); - typename storm::storage::SparseMatrix::iterator backwardEntry = std::find_if(backwardRow.begin(), backwardRow.end(), [&](storm::storage::MatrixEntry::index_type, typename storm::storage::SparseMatrix::value_type> const& a) { return a.getColumn() == state; }); - - std::cout << "before bwd" << std::endl; - for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) { - std::cout << element << ", " << std::endl; - } - - // Modify the predecessor list of the successor and add the predecessor of the state we eliminate. - backwardEntry->setColumn(backwardElement->getColumn()); - - // If the backward entry is not at the right position, we need to move it there. - if (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) { - while (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) { - std::swap(*backwardEntry, *(backwardEntry - 1)); - --backwardEntry; - } - } else if ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) { - while ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) { - std::swap(*backwardEntry, *(backwardEntry + 1)); - ++backwardEntry; - } - } - - std::cout << "after bwd" << std::endl; - for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) { - std::cout << element << ", " << std::endl; - } - return true; - } - template FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) { // Intentionally left empty. diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index eb0dbb40e..f234abb8b 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -38,15 +38,18 @@ namespace storm { class SparseSccModelChecker { public: static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& phiFormula, std::shared_ptr> const& psiFormula); -// static ValueType computeReachabilityReward(storm::models::Dtmc const& dtmc, std::shared_ptr> const& phiFormula, std::shared_ptr> const& psiFormula); - - static ValueType computeReachabilityProbability(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional> const& statePriorities = {}); + static ValueType computeReachabilityReward(storm::models::Dtmc const& dtmc, std::shared_ptr> const& phiFormula, std::shared_ptr> const& psiFormula); private: - static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional> const& distances = {}); + static ValueType computeReachabilityValue(storm::storage::SparseMatrix const& transitionMatrix, std::vector& oneStepProbabilities, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional>& stateRewards, boost::optional> const& statePriorities = {}); + + static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector& entryStateQueue, storm::utility::ConstantsComparator const& comparator, boost::optional>& stateRewards, boost::optional> const& statePriorities = {}); + static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); - static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions); - static bool eliminateStateInPlace(storm::storage::SparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix& backwardTransitions); + + static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional>& stateRewards); + + static std::vector getStatePriorities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector const& oneStepProbabilities); }; } // namespace reachability diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index ad0a41933..d8d9d4f78 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -157,7 +157,7 @@ int main(const int argc, const char** argv) { std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); std::cout << "Checking formula " << *filterFormula << std::endl; - bool keepRewards = false; + bool checkRewards = false; std::shared_ptr> phiStateFormulaApFormula = nullptr; std::shared_ptr> psiStateFormulaApFormula = nullptr; @@ -180,7 +180,7 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(reachabilityRewardFormula, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties (probabilities/rewards) are admitted."); phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); psiStateFormula = reachabilityRewardFormula->getChild(); - keepRewards = true; + checkRewards = true; } } @@ -192,7 +192,7 @@ int main(const int argc, const char** argv) { // Perform bisimulation minimization if requested. if (storm::settings::generalSettings().isBisimulationSet()) { - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), keepRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), checkRewards, storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); dtmc = bisimulationDecomposition.getQuotient()->as>(); dtmc->printModelInformationToStream(std::cout); @@ -204,7 +204,7 @@ int main(const int argc, const char** argv) { storm::modelchecker::reachability::SparseSccModelChecker modelchecker; - storm::RationalFunction valueFunction = modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); + storm::RationalFunction valueFunction = checkRewards ? modelchecker.computeReachabilityReward(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula) : modelchecker.computeReachabilityProbability(*dtmc, phiStateFormulaApFormula, psiStateFormulaApFormula); // STORM_PRINT_AND_LOG(std::endl << "Result: (" << carl::computePolynomial(valueFunction.nominator()) << ") / (" << carl::computePolynomial(valueFunction.denominator()) << ")" << std::endl); // STORM_PRINT_AND_LOG(std::endl << "Result: (" << valueFunction.nominator() << ") / (" << valueFunction.denominator() << ")" << std::endl); STORM_PRINT_AND_LOG(std::endl << "Result: " << valueFunction << std::endl);