diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 2b07436f5..24fb2287a 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -17,111 +17,111 @@ #include "src/models/Dtmc.h" #include "src/properties/prctl/PrctlFilter.h" -std::tuple>, boost::optional>, boost::optional, boost::optional, boost::optional> computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula) { - // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract - // the bitvector representation of the atomic propositions. - - std::shared_ptr> stateFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - std::shared_ptr> pathFormula; - boost::optional threshold; - boost::optional strict; - if (stateFormula != nullptr) { - std::shared_ptr> probabilisticBoundFormula = std::dynamic_pointer_cast>(stateFormula); - STORM_LOG_THROW(probabilisticBoundFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); - STORM_LOG_THROW(probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS_EQUAL || probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties with upper probability bounds are permitted."); - - threshold = probabilisticBoundFormula->getBound(); - strict = probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS; - pathFormula = probabilisticBoundFormula->getChild(); - } else { - pathFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - } - - STORM_LOG_THROW(pathFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); - - std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); - std::shared_ptr> phiStateFormula; - std::shared_ptr> psiStateFormula; - if (untilFormula != nullptr) { - phiStateFormula = untilFormula->getLeft(); - psiStateFormula = untilFormula->getRight(); - } else { - std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); - STORM_LOG_THROW(eventuallyFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); - phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); - psiStateFormula = eventuallyFormula->getChild(); - } - - // Now we need to make sure the formulas defining the phi and psi states are just labels. - std::shared_ptr> phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); - std::shared_ptr> psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); - STORM_LOG_THROW(phiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - STORM_LOG_THROW(psiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - - // Now retrieve the appropriate bitvectors from the atomic propositions. - storm::storage::BitVector phiStates = phiStateFormulaApFormula->getAp() != "true" ? dtmc.getLabeledStates(phiStateFormulaApFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); - storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiStateFormulaApFormula->getAp()); - - // Do some sanity checks to establish some required properties. - 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 probability of 0 or 1, respectively. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates); - storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; - storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - - // If the initial state is known to have either probability 0 or 1, we can directly return the result. - if (dtmc.getInitialStates().isDisjointFrom(maybeStates)) { - STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); - return statesWithProbability0.get(*dtmc.getInitialStates().begin()) ? storm::utility::constantZero() : storm::utility::constantOne(); - } - - // 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, statesWithProbability1); - - // 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, statesWithProbability1); - - // 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); - - // To be able to apply heuristics later, we now determine the distance of each state to the initial state. - std::vector> stateQueue; - stateQueue.reserve(submatrix.getRowCount()); - storm::storage::BitVector statesInQueue(submatrix.getRowCount()); - std::vector distances(submatrix.getRowCount()); - - storm::storage::sparse::state_type currentPosition = 0; - for (auto const& initialState : newInitialStates) { - stateQueue.emplace_back(initialState, 0); - statesInQueue.set(initialState); - } - - // Perform a BFS. - while (currentPosition < stateQueue.size()) { - std::pair const& stateDistancePair = stateQueue[currentPosition]; - distances[stateDistancePair.first] = stateDistancePair.second; - - for (auto const& successorEntry : submatrix.getRow(stateDistancePair.first)) { - if (!statesInQueue.get(successorEntry.getColumn())) { - stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); - statesInQueue.set(successorEntry.getColumn()); - } - } - ++currentPosition; - } - - storm::modelchecker::reachability::SparseSccModelChecker modelchecker; - - return std::make_tuple(modelchecker.computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances),submatrix, oneStepProbabilities, newInitialStates, threshold, strict); -} +//std::tuple>, boost::optional>, boost::optional, boost::optional, boost::optional> computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula) { +// // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract +// // the bitvector representation of the atomic propositions. +// +// std::shared_ptr> stateFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); +// std::shared_ptr> pathFormula; +// boost::optional threshold; +// boost::optional strict; +// if (stateFormula != nullptr) { +// std::shared_ptr> probabilisticBoundFormula = std::dynamic_pointer_cast>(stateFormula); +// STORM_LOG_THROW(probabilisticBoundFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); +// STORM_LOG_THROW(probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS_EQUAL || probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties with upper probability bounds are permitted."); +// +// threshold = probabilisticBoundFormula->getBound(); +// strict = probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS; +// pathFormula = probabilisticBoundFormula->getChild(); +// } else { +// pathFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); +// } +// +// STORM_LOG_THROW(pathFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); +// +// std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); +// std::shared_ptr> phiStateFormula; +// std::shared_ptr> psiStateFormula; +// if (untilFormula != nullptr) { +// phiStateFormula = untilFormula->getLeft(); +// psiStateFormula = untilFormula->getRight(); +// } else { +// std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); +// STORM_LOG_THROW(eventuallyFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted."); +// phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); +// psiStateFormula = eventuallyFormula->getChild(); +// } +// +// // Now we need to make sure the formulas defining the phi and psi states are just labels. +// std::shared_ptr> phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); +// std::shared_ptr> psiStateFormulaApFormula = std::dynamic_pointer_cast>(psiStateFormula); +// STORM_LOG_THROW(phiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); +// STORM_LOG_THROW(psiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); +// +// // Now retrieve the appropriate bitvectors from the atomic propositions. +// storm::storage::BitVector phiStates = phiStateFormulaApFormula->getAp() != "true" ? dtmc.getLabeledStates(phiStateFormulaApFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); +// storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiStateFormulaApFormula->getAp()); +// +// // Do some sanity checks to establish some required properties. +// 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 probability of 0 or 1, respectively. +// std::pair statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates); +// storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first; +// storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second; +// storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); +// +// // If the initial state is known to have either probability 0 or 1, we can directly return the result. +// if (dtmc.getInitialStates().isDisjointFrom(maybeStates)) { +// STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step."); +// return statesWithProbability0.get(*dtmc.getInitialStates().begin()) ? storm::utility::constantZero() : storm::utility::constantOne(); +// } +// +// // 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, statesWithProbability1); +// +// // 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, statesWithProbability1); +// +// // 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); +// +// // To be able to apply heuristics later, we now determine the distance of each state to the initial state. +// std::vector> stateQueue; +// stateQueue.reserve(submatrix.getRowCount()); +// storm::storage::BitVector statesInQueue(submatrix.getRowCount()); +// std::vector distances(submatrix.getRowCount()); +// +// storm::storage::sparse::state_type currentPosition = 0; +// for (auto const& initialState : newInitialStates) { +// stateQueue.emplace_back(initialState, 0); +// statesInQueue.set(initialState); +// } +// +// // Perform a BFS. +// while (currentPosition < stateQueue.size()) { +// std::pair const& stateDistancePair = stateQueue[currentPosition]; +// distances[stateDistancePair.first] = stateDistancePair.second; +// +// for (auto const& successorEntry : submatrix.getRow(stateDistancePair.first)) { +// if (!statesInQueue.get(successorEntry.getColumn())) { +// stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); +// statesInQueue.set(successorEntry.getColumn()); +// } +// } +// ++currentPosition; +// } +// +// storm::modelchecker::reachability::SparseSccModelChecker modelchecker; +// +// return std::make_tuple(modelchecker.computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances),submatrix, oneStepProbabilities, newInitialStates, threshold, strict); +//} /*! * Main entry point of the executable storm.