diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 43be5d163..32063b293 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -218,11 +218,8 @@ namespace storm { /*! * sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ - void setHint(ModelCheckerHint const& hint) { - this->hint = std::make_shared(hint); - } - void setHint(ModelCheckerHint&& hint){ - this->hint = std::make_shared(hint); + void setHint(std::shared_ptr const& hint) { + this->hint = hint; } /*! diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp index 0b99ca27d..8ad0015b4 100644 --- a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp @@ -1,21 +1,15 @@ #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/adapters/CarlAdapter.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace modelchecker { - template - ExplicitModelCheckerHint::ExplicitModelCheckerHint(boost::optional> const& resultHint, boost::optional const& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint), forceApplicationOfHints(false) { - // Intentionally left empty - } - - template - ExplicitModelCheckerHint::ExplicitModelCheckerHint(boost::optional>&& resultHint, boost::optional&& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint), forceApplicationOfHints(false) { - // Intentionally left empty - } - template bool ExplicitModelCheckerHint::isEmpty() const { - return !resultHint.is_initialized() && !schedulerHint.is_initialized(); + return !hasResultHint() && !hasSchedulerHint() && !hasMaybeStates(); } template @@ -48,6 +42,43 @@ namespace storm { this->resultHint = resultHint; } + template + bool ExplicitModelCheckerHint::getComputeOnlyMaybeStates() const { + STORM_LOG_THROW(!computeOnlyMaybeStates || (hasMaybeStates() && hasResultHint()), storm::exceptions::InvalidOperationException, "Computing only maybestates is activated but no maybestates or no result hint is specified."); + return computeOnlyMaybeStates; + } + + template + void ExplicitModelCheckerHint::setComputeOnlyMaybeStates(bool value) { + STORM_LOG_THROW(!value || (hasMaybeStates() && hasResultHint()), storm::exceptions::InvalidOperationException, "Tried to activate that only maybestates need to be computed, but no maybestates or no result hint was given before."); + this->computeOnlyMaybeStates = value; + } + + template + bool ExplicitModelCheckerHint::hasMaybeStates() const { + return maybeStates.is_initialized(); + } + + template + storm::storage::BitVector const& ExplicitModelCheckerHint::getMaybeStates() const { + return maybeStates.get(); + } + + template + storm::storage::BitVector& ExplicitModelCheckerHint::getMaybeStates() { + return maybeStates.get(); + } + + template + void ExplicitModelCheckerHint::setMaybeStates(storm::storage::BitVector const& newMaybeStates) { + this->maybeStates = newMaybeStates; + } + + template + void ExplicitModelCheckerHint::setMaybeStates(storm::storage::BitVector&& newMaybeStates) { + this->maybeStates = std::move(newMaybeStates); + } + template bool ExplicitModelCheckerHint::hasSchedulerHint() const { return schedulerHint.is_initialized(); @@ -74,13 +105,13 @@ namespace storm { } template - bool ExplicitModelCheckerHint::getForceApplicationOfHints() const { - return forceApplicationOfHints; + bool ExplicitModelCheckerHint::getNoEndComponentsInMaybeStates() const { + return noEndComponentsInMaybeStates; } template - void ExplicitModelCheckerHint::setForceApplicationOfHints(bool value) { - forceApplicationOfHints = value; + void ExplicitModelCheckerHint::setNoEndComponentsInMaybeStates(bool value) { + noEndComponentsInMaybeStates = value; } template class ExplicitModelCheckerHint; diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h index 0a514711e..33acd89ce 100644 --- a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h @@ -18,10 +18,9 @@ namespace storm { class ExplicitModelCheckerHint : public ModelCheckerHint { public: + ExplicitModelCheckerHint() = default; ExplicitModelCheckerHint(ExplicitModelCheckerHint const& other) = default; ExplicitModelCheckerHint(ExplicitModelCheckerHint&& other) = default; - ExplicitModelCheckerHint(boost::optional> const& resultHint = boost::none, boost::optional const& schedulerHint = boost::none); - ExplicitModelCheckerHint(boost::optional>&& resultHint, boost::optional&& schedulerHint = boost::none); // Returns true iff this hint does not contain any information virtual bool isEmpty() const override; @@ -35,22 +34,35 @@ namespace storm { void setResultHint(boost::optional> const& resultHint); void setResultHint(boost::optional>&& resultHint); + // Set whether only the maybestates need to be computed, i.e., skips the qualitative check. + // The result for non-maybe states is taken from the result hint. + // Hence, this option may only be enabled iff a resultHint and a set of maybestates are given. + bool getComputeOnlyMaybeStates() const; + void setComputeOnlyMaybeStates(bool value); + bool hasMaybeStates() const; + storm::storage::BitVector const& getMaybeStates() const; + storm::storage::BitVector& getMaybeStates(); + void setMaybeStates(storm::storage::BitVector const& maybeStates); + void setMaybeStates(storm::storage::BitVector&& maybeStates); + bool hasSchedulerHint() const; storm::storage::TotalScheduler const& getSchedulerHint() const; storm::storage::TotalScheduler& getSchedulerHint(); void setSchedulerHint(boost::optional const& schedulerHint); void setSchedulerHint(boost::optional&& schedulerHint); - // If set, this option forces the application of the specified hints. This means that the model checker may skip some checks to increase performance. - // This might yield wrong results on certain models, e.g., when computing maximal probabilities on an MDP that has an end component consisting only of maybestates. - bool getForceApplicationOfHints() const; - void setForceApplicationOfHints(bool value); + // If set, it is assumed that there are no end components that consist only of maybestates. + // May only be enabled iff maybestates are given. + bool getNoEndComponentsInMaybeStates() const; + void setNoEndComponentsInMaybeStates(bool value); private: boost::optional> resultHint; boost::optional schedulerHint; - bool forceApplicationOfHints; + bool computeOnlyMaybeStates; + boost::optional maybeStates; + bool noEndComponentsInMaybeStates; }; } diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp index 1fd16ebd1..190914458 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -23,37 +24,140 @@ namespace storm { storm::modelchecker::SparseDtmcPrctlModelChecker> modelChecker(instantiatedModel); // Check if there are some optimizations implemented for the specified property - if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) { - return checkWithHint(modelChecker); + if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) { + return checkReachabilityProbabilityFormula(modelChecker); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkReachabilityRewardFormula(modelChecker); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkBoundedUntilFormula(modelChecker); } else { return modelChecker.check(*this->currentCheckTask); } } template - std::unique_ptr SparseDtmcInstantiationModelChecker::checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelchecker) { + std::unique_ptr SparseDtmcInstantiationModelChecker::checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula - if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - std::unique_ptr result = modelchecker.check(*this->currentCheckTask); - this->currentCheckTask->setHint(ExplicitModelCheckerHint(result->template asExplicitQuantitativeCheckResult().getValueVector())); - return result; + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); } else { - std::unique_ptr quantitativeResult; auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - if(this->currentCheckTask->getFormula().isProbabilityOperatorFormula()) { - quantitativeResult = modelchecker.computeProbabilities(newCheckTask); - } else if (this->currentCheckTask->getFormula().isRewardOperatorFormula()) { - quantitativeResult = modelchecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with result hint is only implemented for probability or reward operator formulas"); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + } + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); + uint_fast64_t stateIndex = 0; + for (auto const& value : hint.getResultHint()) { + if (storm::utility::isZero(value) || storm::utility::isOne(value)) { + maybeStates.set(stateIndex, false); + } + ++stateIndex; + } + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } + + return result; + } + + template + std::unique_ptr SparseDtmcInstantiationModelChecker::checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + + // Check the formula and store the result as a hint for the next call. + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + this->currentCheckTask->getHint().template asExplicitModelCheckerHint().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + } + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); + uint_fast64_t stateIndex = 0; + for (auto const& value : hint.getResultHint()) { + if (storm::utility::isInfinity(value)) { + maybeStates.set(stateIndex, false); + } + ++stateIndex; } - std::unique_ptr qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - this->currentCheckTask->setHint(ExplicitModelCheckerHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()))); - return qualitativeResult; + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with reward zero since a valuation might set a reward to zero + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); } + + return result; } + template + std::unique_ptr SparseDtmcInstantiationModelChecker::checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + std::unique_ptr result; + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // We extract the maybestates from the quantitative result + // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + } + storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); + uint_fast64_t stateIndex = 0; + for (auto const& value : hint.getResultHint()) { + if (storm::utility::isZero(value)) { + maybeStates.set(stateIndex, false); + } + ++stateIndex; + } + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } else { + result = modelChecker.check(*this->currentCheckTask); + } + + return result; + } template class SparseDtmcInstantiationModelChecker, double>; template class SparseDtmcInstantiationModelChecker, storm::RationalNumber>; diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h index 4253ea65e..511253107 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h @@ -25,8 +25,10 @@ namespace storm { protected: - // Considers the result of the last check as a hint for the current check - std::unique_ptr checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); + // Optimizations for the different formula types + std::unique_ptr checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); + std::unique_ptr checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); + std::unique_ptr checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); storm::utility::ModelInstantiator> modelInstantiator; }; diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp index 021bbdd59..d1b35d374 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLifting.cpp @@ -40,6 +40,7 @@ namespace storm { } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); + this->instantiationChecker->setInstantiationsAreGraphPreserving(true); } template diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp index b8efac24d..9b8991689 100644 --- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp @@ -12,7 +12,7 @@ namespace storm { namespace parametric { template - SparseInstantiationModelChecker::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) { + SparseInstantiationModelChecker::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), instantiationsAreGraphPreserving(false) { //Intentionally left empty } @@ -24,16 +24,15 @@ namespace storm { } template - storm::modelchecker::ModelCheckerHint& SparseInstantiationModelChecker::getHint() { - return currentCheckTask->getHint(); + void SparseInstantiationModelChecker::setInstantiationsAreGraphPreserving(bool value) { + instantiationsAreGraphPreserving = value; } template - storm::modelchecker::ModelCheckerHint const& SparseInstantiationModelChecker::getHint() const { - return currentCheckTask->getHint(); + bool SparseInstantiationModelChecker::getInstantiationsAreGraphPreserving() const { + return instantiationsAreGraphPreserving; } - template class SparseInstantiationModelChecker, double>; template class SparseInstantiationModelChecker, double>; diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h index 7d5788728..d654e76f9 100644 --- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h @@ -22,8 +22,10 @@ namespace storm { virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) = 0; - storm::modelchecker::ModelCheckerHint& getHint(); - storm::modelchecker::ModelCheckerHint const& getHint() const; + // If set, it is assumed that all considered model instantiations have the same underlying graph structure. + // This bypasses the graph analysis for the different instantiations. + void setInstantiationsAreGraphPreserving(bool value); + bool getInstantiationsAreGraphPreserving() const; protected: @@ -34,6 +36,7 @@ namespace storm { // store the current formula. Note that currentCheckTask only stores a reference to the formula. std::shared_ptr currentFormula; + bool instantiationsAreGraphPreserving; }; } } diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp index dcaa88335..e7a8a1cd8 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp @@ -1,8 +1,10 @@ #include "SparseMdpInstantiationModelChecker.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/modelChecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelChecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelChecker/hints/ExplicitModelCheckerHint.h" +#include "storm/utility/graph.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" @@ -24,42 +26,162 @@ namespace storm { storm::modelchecker::SparseMdpPrctlModelChecker> modelChecker(instantiatedModel); // Check if there are some optimizations implemented for the specified property - if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) { - return checkWithResultHint(modelChecker); + if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) { + return checkReachabilityProbabilityFormula(modelChecker, instantiatedModel); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkReachabilityRewardFormula(modelChecker, instantiatedModel); + } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) { + return checkBoundedUntilFormula(modelChecker); } else { return modelChecker.check(*this->currentCheckTask); } } template - std::unique_ptr SparseMdpInstantiationModelChecker::checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker>& modelchecker) { + std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { this->currentCheckTask->setProduceSchedulers(true); + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + // Check the formula and store the result as a hint for the next call. // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { - std::unique_ptr result = modelchecker.check(*this->currentCheckTask); + result = modelChecker.check(*this->currentCheckTask); storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); - this->currentCheckTask->setHint(ExplicitModelCheckerHint(result->template asExplicitQuantitativeCheckResult().getValueVector(), - dynamic_cast(scheduler))); - return result; + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + hint.setSchedulerHint(dynamic_cast(scheduler)); } else { - std::unique_ptr quantitativeResult; auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); - if(this->currentCheckTask->getFormula().isProbabilityOperatorFormula()) { - quantitativeResult = modelchecker.computeProbabilities(newCheckTask); - } else if (this->currentCheckTask->getFormula().isRewardOperatorFormula()) { - quantitativeResult = modelchecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with hint is only implemented for probability or reward operator formulas"); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + hint.setSchedulerHint(std::move(dynamic_cast(scheduler))); + } + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); + uint_fast64_t stateIndex = 0; + for (auto const& value : hint.getResultHint()) { + if (storm::utility::isZero(value) || storm::utility::isOne(value)) { + maybeStates.set(stateIndex, false); + } + ++stateIndex; + } + + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + + // Check if there can be end components within the maybestates + if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) || + storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { + hint.setNoEndComponentsInMaybeStates(true); } - std::unique_ptr qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + } + + return result; + } + + template + std::unique_ptr SparseMdpInstantiationModelChecker::checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel) { + + this->currentCheckTask->setProduceSchedulers(true); + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + std::unique_ptr result; + + // Check the formula and store the result as a hint for the next call. + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula + if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + std::unique_ptr result = modelChecker.check(*this->currentCheckTask); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + hint.setSchedulerHint(dynamic_cast(scheduler)); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); storm::storage::Scheduler& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); - this->currentCheckTask->setHint(ExplicitModelCheckerHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()), - std::move(dynamic_cast(scheduler)))); - return qualitativeResult; + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + hint.setSchedulerHint(std::move(dynamic_cast(scheduler))); + } + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // Extract the maybe states from the current result. + assert(hint.hasResultHint()); + storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); + uint_fast64_t stateIndex = 0; + for (auto const& value : hint.getResultHint()) { + if (storm::utility::isInfinity(value)) { + maybeStates.set(stateIndex, false); + } + ++stateIndex; + } + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with reward zero since a valuation might set a reward to zero + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + + // Check if there can be end components within the maybestates + if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) || + storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) { + hint.setNoEndComponentsInMaybeStates(true); + } + } + return result; + } + + template + std::unique_ptr SparseMdpInstantiationModelChecker::checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker) { + + if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) { + this->currentCheckTask->setHint(std::make_shared>()); + } + std::unique_ptr result; + ExplicitModelCheckerHint& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint(); + + if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { + // We extract the maybestates from the quantitative result + // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula + if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { + result = modelChecker.check(*this->currentCheckTask); + hint.setResultHint(result->template asExplicitQuantitativeCheckResult().getValueVector()); + } else { + auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false); + std::unique_ptr quantitativeResult = modelChecker.computeProbabilities(newCheckTask); + result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); + hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); + } + storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); + uint_fast64_t stateIndex = 0; + for (auto const& value : hint.getResultHint()) { + if (storm::utility::isZero(value)) { + maybeStates.set(stateIndex, false); + } + ++stateIndex; + } + // We need to exclude the target states from the maybe states. + // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps + std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); + maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + hint.setMaybeStates(std::move(maybeStates)); + hint.setComputeOnlyMaybeStates(true); + } else { + result = modelChecker.check(*this->currentCheckTask); } + return result; } template class SparseMdpInstantiationModelChecker, double>; diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h index ad3b97e67..f9fc7e4ec 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h @@ -25,8 +25,10 @@ namespace storm { virtual std::unique_ptr check(storm::utility::parametric::Valuation const& valuation) override; protected: - // Considers the result of the last check as a hint for the current check - std::unique_ptr checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker); + // Optimizations for the different formula types + std::unique_ptr checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel); + std::unique_ptr checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker, storm::models::sparse::Mdp const& instantiatedModel); + std::unique_ptr checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker); storm::utility::ModelInstantiator> modelInstantiator; }; diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp index 43c6db29a..67fa06d25 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLifting.cpp @@ -40,6 +40,7 @@ namespace storm { } this->parameterLiftingChecker = std::make_unique>(this->getConsideredParametricModel()); this->instantiationChecker = std::make_unique>(this->getConsideredParametricModel()); + this->instantiationChecker->setInstantiationsAreGraphPreserving(true); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index a6a68522e..9fde067e9 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -48,7 +48,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 08de02dc8..44db5e635 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -64,7 +64,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index a812806eb..6d219bda6 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -13,18 +13,27 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis. - storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, stepBound); - maybeStates &= ~psiStates; - STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + storm::storage::BitVector maybeStates; + + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + } else { + maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, stepBound); + maybeStates &= ~psiStates; + STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + } + + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); if (!maybeStates.empty()) { // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. @@ -43,7 +52,6 @@ namespace storm { // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); } - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); return result; } @@ -51,20 +59,44 @@ namespace storm { template std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { - // We need to identify the states which have to be taken out of the matrix, i.e. - // all states that have probability 0 and 1 of satisfying the until-formula. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); - storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); - storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - - // Perform some logging. - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); - STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); - STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - // Create resulting vector. - std::vector result(transitionMatrix.getRowCount()); + std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + + // We need to identify the maybe states (states which have a probability for satisfying the until formula + // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1. + storm::storage::BitVector maybeStates, statesWithProbability1; + + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + + // Treat the states with probability one + std::vector const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint().getResultHint(); + statesWithProbability1 = storm::storage::BitVector(maybeStates.size(), false); + storm::storage::BitVector nonMaybeStates = ~maybeStates; + for (auto const& state : nonMaybeStates) { + if (storm::utility::isOne(resultsForNonMaybeStates[state])) { + statesWithProbability1.set(state, true); + result[state] = storm::utility::one(); + } else { + STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException, "Expected that the result hint specifies probabilities in {0,1} for non-maybe states"); + } + } + } else { + + // Get all states that have probability 0 and 1 of satisfying the until-formula. + std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); + storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); + statesWithProbability1 = std::move(statesWithProbability01.second); + maybeStates = ~(statesWithProbability0 | statesWithProbability1); + + STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); + STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); + STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Set values of resulting vector that are known exactly. + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); + } // Check whether we need to compute exact probabilities for some states. if (qualitative) { @@ -84,9 +116,11 @@ namespace storm { // Initialize the x vector with the hint (if available) or with 0.5 for each element. // This is the initial guess for the iterative solvers. It should be safe as for all // 'maybe' states we know that the probability is strictly larger than 0. - std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); + std::vector x; if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { - storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint().getResultHint()); + x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } else { + x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); } // Prepare the right-hand side of the equation system. For entry i this corresponds to @@ -102,11 +136,6 @@ namespace storm { storm::utility::vector::setVectorValues(result, maybeStates, x); } } - - // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); - storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - return result; } @@ -180,18 +209,27 @@ namespace storm { template std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { - // Determine which states have a reward of infinity by definition. - storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); - storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates); - infinityStates.complement(); - storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; - STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); - STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states."); - STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - // Create resulting vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + // Determine which states have a reward that is less than infinity. + storm::storage::BitVector maybeStates; + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + storm::utility::vector::setVectorValues(result, ~(maybeStates | targetStates), storm::utility::infinity()); + } else { + storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates); + infinityStates.complement(); + maybeStates = ~(targetStates | infinityStates); + + STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); + STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states."); + STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); + } + // Check whether we need to compute exact rewards for some states. if (qualitative) { // Set the values for all maybe-states to 1 to indicate that their reward values @@ -209,9 +247,11 @@ namespace storm { // Initialize the x vector with the hint (if available) or with 1 for each element. // This is the initial guess for the iterative solvers. - std::vector x(submatrix.getColumnCount(), storm::utility::one()); + std::vector x; if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { - storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint().getResultHint()); + x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } else { + x = std::vector(submatrix.getColumnCount(), storm::utility::one()); } // Prepare the right-hand side of the equation system. @@ -226,10 +266,6 @@ namespace storm { storm::utility::vector::setVectorValues(result, maybeStates, x); } } - - // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); - return result; } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 2dfaac693..12f545d00 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -22,7 +22,7 @@ namespace storm { template > class SparseDtmcPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 5c79cd3c5..73fa080c0 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -22,24 +22,29 @@ #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/IllegalFunctionCallException.h" +#include "storm/exceptions/IllegalArgumentException.h" namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. storm::storage::BitVector maybeStates; - if (dir == OptimizationDirection::Minimize) { - maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); } else { - maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, stepBound); + if (dir == OptimizationDirection::Minimize) { + maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); + } else { + maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, stepBound); + } + maybeStates &= ~psiStates; + STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); } - maybeStates &= ~psiStates; - STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); if (!maybeStates.empty()) { // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. @@ -77,28 +82,49 @@ namespace storm { MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only."); - // We need to identify the states which have to be taken out of the matrix, i.e. - // all states that have probability 0 and 1 of satisfying the until-formula. - std::pair statesWithProbability01; - if (goal.minimize()) { - statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + + // We need to identify the maybe states (states which have a probability for satisfying the until formula + // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively. + storm::storage::BitVector maybeStates, statesWithProbability1, statesWithProbability0; + + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + + // Treat the states with probability one + std::vector const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint().getResultHint(); + statesWithProbability1 = storm::storage::BitVector(maybeStates.size(), false); + statesWithProbability0 = storm::storage::BitVector(maybeStates.size(), false); + storm::storage::BitVector nonMaybeStates = ~maybeStates; + for (auto const& state : nonMaybeStates) { + if (storm::utility::isOne(resultsForNonMaybeStates[state])) { + statesWithProbability1.set(state, true); + result[state] = storm::utility::one(); + } else { + STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException, "Expected that the result hint specifies probabilities in {0,1} for non-maybe states"); + statesWithProbability0.set(state, true); + } + } } else { - statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); + // Get all states that have probability 0 and 1 of satisfying the until-formula. + std::pair statesWithProbability01; + if (goal.minimize()) { + statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); + } else { + statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); + } + statesWithProbability0 = std::move(statesWithProbability01.first); + statesWithProbability1 = std::move(statesWithProbability01.second); + maybeStates = ~(statesWithProbability0 | statesWithProbability1); + STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); + STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); + STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Set values of resulting vector that are known exactly. + storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); + storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); } - storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); - storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); - STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); - STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector. - std::vector result(transitionMatrix.getRowGroupCount()); - // Set values of resulting vector that are known exactly. - storm::utility::vector::setVectorValues(result, statesWithProbability0, storm::utility::zero()); - storm::utility::vector::setVectorValues(result, statesWithProbability1, storm::utility::one()); - // If requested, we will produce a scheduler. std::unique_ptr scheduler; if (produceScheduler) { @@ -122,7 +148,8 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); // Now compute the results for the maybeStates - MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, goal.minimize(), storm::utility::zero(), storm::utility::one()); + bool skipEcWithinMaybeStatesCheck = goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); + MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, skipEcWithinMaybeStatesCheck, storm::utility::zero(), storm::utility::one()); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); @@ -167,8 +194,8 @@ namespace storm { solver->setUpperBound(upperResultBound.get()); } // the scheduler hint is only applicable if it induces no BSCC consisting of maybestates - if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint() && - (hint.template asExplicitModelCheckerHint().getForceApplicationOfHints() || skipECWithinMaybeStatesCheck || + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint() && + (skipECWithinMaybeStatesCheck || storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hint.template asExplicitModelCheckerHint().getSchedulerHint().getChoices()), maybeStates, ~maybeStates).full())) { solver->setSchedulerHint(hint.template asExplicitModelCheckerHint().getSchedulerHint().getSchedulerForSubsystem(maybeStates)); } @@ -177,8 +204,8 @@ namespace storm { // Create the solution vector. std::vector x; // The result hint is only applicable if there are no End Components consisting of maybestates - if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && - (hint.template asExplicitModelCheckerHint().getForceApplicationOfHints() || skipECWithinMaybeStatesCheck || solver->hasSchedulerHint() || + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && + (skipECWithinMaybeStatesCheck || solver->hasSchedulerHint() || storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) { x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); } else { @@ -309,27 +336,30 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); - // Determine which states have a reward of infinity by definition. - storm::storage::BitVector infinityStates; - storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); - if (goal.minimize()) { - STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops."); - infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates); + + // Determine which states have a reward that is infinity or less than infinity. + storm::storage::BitVector maybeStates, infinityStates; + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + infinityStates = ~(maybeStates | targetStates); } else { - infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates); + storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); + if (goal.minimize()) { + STORM_LOG_WARN("Results of reward computation may be too low, because of zero-reward loops."); + infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates); + } else { + infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates); + } + infinityStates.complement(); + maybeStates = ~(targetStates | infinityStates); + STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); + STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states."); + STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); } - infinityStates.complement(); - storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; - STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); - STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states."); - STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector. - std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - - // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity()); // If requested, we will produce a scheduler. @@ -369,8 +399,9 @@ namespace storm { } } + bool skipEcWithinMaybeStatesCheck = !goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); // Now compute the results for the maybeStates - MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, !goal.minimize(), storm::utility::zero()); + MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeValuesOnlyMaybeStates(goal, transitionMatrix, backwardTransitions, maybeStates, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hint, skipEcWithinMaybeStatesCheck, storm::utility::zero()); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 2eb4ae3ae..0d4e603d5 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -33,7 +33,7 @@ namespace storm { template class SparseMdpPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/storm/utility/parameterlifting.h b/src/storm/utility/parameterlifting.h index 11ae11962..3c8cdbf73 100644 --- a/src/storm/utility/parameterlifting.h +++ b/src/storm/utility/parameterlifting.h @@ -45,7 +45,7 @@ namespace storm { } } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { // Markov Automata store the probability matrix and the exit rate vector. However, we need to considert the rate matrix. - if (model->template as>()->isClosed()) { + if (!model->template as>()->isClosed()) { STORM_LOG_ERROR("parameter lifting requires a closed Markov automaton."); return false; } @@ -56,7 +56,7 @@ namespace storm { auto const& exitRate = rateVector[state]; for (auto const& entry : model->getTransitionMatrix().getRowGroup(state)) { if (!storm::utility::parametric::isMultiLinearPolynomial(storm::utility::simplify(entry.getValue() * exitRate))) { - STORM_LOG_WARN("The input model contains a non-linear polynomial as transition: '" << entry.getValue() << "'. Can not validate that parameter lifting is sound on this model."); + STORM_LOG_WARN("The input model contains a non-linear polynomial as transition rate: '" << storm::utility::simplify(entry.getValue() * exitRate) << "'. Can not validate that parameter lifting is sound on this model."); return false; } } diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 77932dab6..9cbbc4da4 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -482,6 +482,17 @@ namespace storm { storm::storage::BitVector filterZero(std::vector const& values) { return filter(values, storm::utility::isZero); } + + /*! + * Retrieves a bit vector containing all the indices for which the value at this position is equal to one + * + * @param values The vector of values. + * @return The resulting bit vector. + */ + template + storm::storage::BitVector filterOne(std::vector const& values) { + return filter(values, storm::utility::isOne); + } /** * Sum the entries from values that are set to one in the filter vector.