diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index 546c7d83c..45e9ab425 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -101,33 +101,44 @@ 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::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> untilFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - std::shared_ptr> phiStateFormula; - std::shared_ptr> psiStateFormula; - if (untilFormula.get() != nullptr) { - phiStateFormula = untilFormula->getLeft(); - psiStateFormula = untilFormula->getRight(); - } else { - std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - STORM_LOG_THROW(eventuallyFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *untilFormula << " for parametric model checking. Note that only unbounded reachability properties are admitted."); - - 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."); - + ValueType SparseSccModelChecker::computeReachabilityProbability(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 = phiStateFormulaApFormula->getAp() != "true" ? dtmc.getLabeledStates(phiStateFormulaApFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true); - storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiStateFormulaApFormula->getAp()); + 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.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index fbb83d48b..eb0dbb40e 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -37,7 +37,8 @@ namespace storm { template class SparseSccModelChecker { public: - static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, std::shared_ptr> const& filterFormula); + 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 = {}); diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 4d9272203..9aa415c85 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -155,7 +155,11 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(storm::settings::generalSettings().isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property."); std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); - + std::cout << "Checking formula " << *filterFormula << " / " << typeid(*filterFormula).name() << std::endl; + + bool keepRewards = false; + std::shared_ptr> phiStateFormulaApFormula; + std::shared_ptr> psiStateFormulaApFormula; // Perform bisimulation minimization if requested. if (storm::settings::generalSettings().isBisimulationSet()) { @@ -164,20 +168,28 @@ int main(const int argc, const char** argv) { std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); std::shared_ptr> phiStateFormula; std::shared_ptr> psiStateFormula; - if (untilFormula.get() != nullptr) { + if (untilFormula != nullptr) { phiStateFormula = untilFormula->getLeft(); psiStateFormula = untilFormula->getRight(); } else { std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); - STORM_LOG_THROW(eventuallyFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *untilFormula << " for parametric model checking. Note that only unbounded reachability properties are admitted."); + if (eventuallyFormula != nullptr) { - phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); - psiStateFormula = eventuallyFormula->getChild(); + phiStateFormula = std::shared_ptr>(new storm::properties::prctl::Ap("true")); + psiStateFormula = eventuallyFormula->getChild(); + } else { + std::shared_ptr> reachabilityRewardFormula = std::dynamic_pointer_cast>(filterFormula->getChild()); + + STORM_LOG_THROW(reachabilityRewardFormula != nullptr, 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; + } } // 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); + phiStateFormulaApFormula = std::dynamic_pointer_cast>(phiStateFormula); + 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."); @@ -193,7 +205,7 @@ int main(const int argc, const char** argv) { storm::modelchecker::reachability::SparseSccModelChecker modelchecker; - storm::RationalFunction valueFunction = modelchecker.computeReachabilityProbability(*dtmc, filterFormula); + storm::RationalFunction valueFunction = 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);