diff --git a/src/logic/ConditionalFormula.cpp b/src/logic/ConditionalFormula.cpp index 2b63fd941..af3e1d95b 100644 --- a/src/logic/ConditionalFormula.cpp +++ b/src/logic/ConditionalFormula.cpp @@ -1,11 +1,13 @@ #include "src/logic/ConditionalFormula.h" - #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - ConditionalFormula::ConditionalFormula(std::shared_ptr const& subformula, std::shared_ptr const& conditionFormula, Context context) : subformula(subformula), conditionFormula(conditionFormula), context(context) { - // Intentionally left empty. + ConditionalFormula::ConditionalFormula(std::shared_ptr const& subformula, std::shared_ptr const& conditionFormula, FormulaContext context) : subformula(subformula), conditionFormula(conditionFormula), context(context) { + STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward, storm::exceptions::InvalidPropertyException, "Invalid context for formula."); } Formula const& ConditionalFormula::getSubformula() const { @@ -17,11 +19,11 @@ namespace storm { } bool ConditionalFormula::isConditionalProbabilityFormula() const { - return context == Context::Probability; + return context == FormulaContext::Probability; } bool ConditionalFormula::isConditionalRewardFormula() const { - return context == Context::Reward; + return context == FormulaContext::Reward; } boost::any ConditionalFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { @@ -29,7 +31,22 @@ namespace storm { } std::shared_ptr ConditionalFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution)); + return std::make_shared(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution), context); + } + + void ConditionalFormula::gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const { + this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); + this->getConditionFormula().gatherAtomicExpressionFormulas(atomicExpressionFormulas); + } + + void ConditionalFormula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { + this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas); + this->getConditionFormula().gatherAtomicLabelFormulas(atomicLabelFormulas); + } + + void ConditionalFormula::gatherReferencedRewardModels(std::set& referencedRewardModels) const { + this->getSubformula().gatherReferencedRewardModels(referencedRewardModels); + this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels); } std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/ConditionalFormula.h b/src/logic/ConditionalFormula.h index d7b4dc7cd..fc6b61655 100644 --- a/src/logic/ConditionalFormula.h +++ b/src/logic/ConditionalFormula.h @@ -2,6 +2,7 @@ #define STORM_LOGIC_CONDITIONALFORMULA_H_ #include "src/logic/BinaryPathFormula.h" +#include "src/logic/FormulaContext.h" namespace storm { namespace logic { @@ -9,7 +10,7 @@ namespace storm { public: enum class Context { Probability, Reward }; - ConditionalFormula(std::shared_ptr const& subformula, std::shared_ptr const& conditionFormula, Context context = Context::Probability); + ConditionalFormula(std::shared_ptr const& subformula, std::shared_ptr const& conditionFormula, FormulaContext context = FormulaContext::Probability); virtual ~ConditionalFormula() { // Intentionally left empty. @@ -27,10 +28,14 @@ namespace storm { virtual std::shared_ptr substitute(std::map const& substitution) const override; + virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; + virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const override; + virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const override; + private: std::shared_ptr subformula; std::shared_ptr conditionFormula; - Context context; + FormulaContext context; }; } } diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp index 3d2e6fb57..71ff4ac54 100644 --- a/src/logic/EventuallyFormula.cpp +++ b/src/logic/EventuallyFormula.cpp @@ -1,23 +1,25 @@ #include "src/logic/EventuallyFormula.h" - #include "src/logic/FormulaVisitor.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidPropertyException.h" + namespace storm { namespace logic { - EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, Context context) : UnaryPathFormula(subformula), context(context) { - // Intentionally left empty. + EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) { + STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::ExpectedTime, storm::exceptions::InvalidPropertyException, "Invalid context for formula."); } bool EventuallyFormula::isEventuallyFormula() const { - return context == Context::Probability; + return context == FormulaContext::Probability; } bool EventuallyFormula::isReachabilityRewardFormula() const { - return context == Context::Reward; + return context == FormulaContext::Reward; } bool EventuallyFormula::isReachbilityExpectedTimeFormula() const { - return context == Context::ExpectedTime; + return context == FormulaContext::ExpectedTime; } bool EventuallyFormula::isProbabilityPathFormula() const { @@ -37,7 +39,7 @@ namespace storm { } std::shared_ptr EventuallyFormula::substitute(std::map const& substitution) const { - return std::make_shared(this->getSubformula().substitute(substitution)); + return std::make_shared(this->getSubformula().substitute(substitution), context); } std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const { diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h index d7a81fa83..5a0070a16 100644 --- a/src/logic/EventuallyFormula.h +++ b/src/logic/EventuallyFormula.h @@ -2,14 +2,13 @@ #define STORM_LOGIC_EVENTUALLYFORMULA_H_ #include "src/logic/UnaryPathFormula.h" +#include "src/logic/FormulaContext.h" namespace storm { namespace logic { class EventuallyFormula : public UnaryPathFormula { - public: - enum class Context { Probability, Reward, ExpectedTime }; - - EventuallyFormula(std::shared_ptr const& subformula, Context context = Context::Probability); + public: + EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context = FormulaContext::Probability); virtual ~EventuallyFormula() { // Intentionally left empty. @@ -29,7 +28,7 @@ namespace storm { virtual std::shared_ptr substitute(std::map const& substitution) const override; private: - Context context; + FormulaContext context; }; } } diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index d682d02aa..6c7084f53 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -256,6 +256,14 @@ namespace storm { return dynamic_cast(*this); } + EventuallyFormula& Formula::asReachabilityRewardFormula() { + return dynamic_cast(*this); + } + + EventuallyFormula const& Formula::asReachabilityRewardFormula() const { + return dynamic_cast(*this); + } + GloballyFormula& Formula::asGloballyFormula() { return dynamic_cast(*this); } @@ -382,7 +390,7 @@ namespace storm { return; } - void Formula::gatherAtomicLabelFormulas(std::vector>& atomicExpressionFormulas) const { + void Formula::gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const { return; } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index f2e06bc0b..7d77de7b3 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -126,6 +126,9 @@ namespace storm { EventuallyFormula& asEventuallyFormula(); EventuallyFormula const& asEventuallyFormula() const; + EventuallyFormula& asReachabilityRewardFormula(); + EventuallyFormula const& asReachabilityRewardFormula() const; + GloballyFormula& asGloballyFormula(); GloballyFormula const& asGloballyFormula() const; @@ -178,7 +181,7 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const = 0; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const; - virtual void gatherAtomicLabelFormulas(std::vector>& atomicExpressionFormulas) const; + virtual void gatherAtomicLabelFormulas(std::vector>& atomicLabelFormulas) const; virtual void gatherReferencedRewardModels(std::set& referencedRewardModels) const; private: diff --git a/src/logic/FormulaContext.h b/src/logic/FormulaContext.h new file mode 100644 index 000000000..41113cb8d --- /dev/null +++ b/src/logic/FormulaContext.h @@ -0,0 +1,12 @@ +#ifndef STORM_LOGIC_FORMULACONTEXT_H_ +#define STORM_LOGIC_FORMULACONTEXT_H_ + +namespace storm { + namespace logic { + + enum class FormulaContext { Undefined, Probability, Reward, LongRunAverage, ExpectedTime }; + + } +} + +#endif /* STORM_LOGIC_FORMULACONTEXT_H_ */ \ No newline at end of file diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index 8e701cedd..6bf03ddb7 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -68,11 +68,15 @@ namespace storm { bool result = true; if (f.isConditionalProbabilityFormula()) { result = result && inherited.getSpecification().areConditionalProbabilityFormulasAllowed(); - } else if (f.Formula::isConditionalRewardFormula()) { + } else if (f.isConditionalRewardFormula()) { result = result && inherited.getSpecification().areConditionalRewardFormulasFormulasAllowed(); } if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) { - result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula(); + if (f.isConditionalProbabilityFormula()) { + result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula(); + } else if (f.isConditionalRewardFormula()) { + result = result && f.getSubformula().isReachabilityRewardFormula() && f.getConditionFormula().isEventuallyFormula(); + } } result = result && boost::any_cast(f.getSubformula().accept(*this, data)); result = result && boost::any_cast(f.getConditionFormula().accept(*this, data)); @@ -172,7 +176,7 @@ namespace storm { boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areRewardOperatorsAllowed(); - result = result && f.getSubformula().isRewardPathFormula(); + result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula()); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 8f7a7b2f5..ebd760d2e 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -20,7 +20,7 @@ namespace storm { if (formula.isProbabilityPathFormula()) { return this->computeProbabilities(checkTask); } else if (formula.isRewardPathFormula()) { - return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula())); + return this->computeRewards(checkTask); } } else if (formula.isConditionalProbabilityFormula()) { return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula())); @@ -74,18 +74,20 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } - std::unique_ptr AbstractModelChecker::computeRewards(CheckTask const& checkTask) { - storm::logic::PathFormula const& rewardPathFormula = checkTask.getFormula(); - if (rewardPathFormula.isCumulativeRewardFormula()) { - return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula())); - } else if (rewardPathFormula.isInstantaneousRewardFormula()) { - return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula())); - } else if (rewardPathFormula.isReachabilityRewardFormula()) { - return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula())); - } else if (rewardPathFormula.isLongRunAverageRewardFormula()) { - return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula())); + std::unique_ptr AbstractModelChecker::computeRewards(CheckTask const& checkTask) { + storm::logic::Formula const& rewardFormula = checkTask.getFormula(); + if (rewardFormula.isCumulativeRewardFormula()) { + return this->computeCumulativeRewards(checkTask.substituteFormula(rewardFormula.asCumulativeRewardFormula())); + } else if (rewardFormula.isInstantaneousRewardFormula()) { + return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula())); + } else if (rewardFormula.isReachabilityRewardFormula()) { + return this->computeReachabilityRewards(checkTask.substituteFormula(rewardFormula.asEventuallyFormula())); + } else if (rewardFormula.isLongRunAverageRewardFormula()) { + return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula())); + } else if (rewardFormula.isConditionalRewardFormula()) { + return this->computeConditionalRewards(checkTask.substituteFormula(rewardFormula.asConditionalFormula())); } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardFormula << "' is invalid."); } std::unique_ptr AbstractModelChecker::computeConditionalRewards(CheckTask const& checkTask) { @@ -191,7 +193,7 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkRewardOperatorFormula(CheckTask const& checkTask) { storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula(); - std::unique_ptr result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula())); + std::unique_ptr result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula())); if (checkTask.isBoundSet()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index fc7fe2fdd..90562659b 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -44,7 +44,7 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask); // The methods to compute the rewards for path formulas. - virtual std::unique_ptr computeRewards(CheckTask const& checkTask); + virtual std::unique_ptr computeRewards(CheckTask const& checkTask); virtual std::unique_ptr computeConditionalRewards(CheckTask const& checkTask); virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask); virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index df7f1ee9a..b21d509ec 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -36,7 +36,7 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true)); } template @@ -130,6 +130,21 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalRewards(CheckTask const& checkTask) { + storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); + STORM_LOG_THROW(conditionalFormula.getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula."); + + std::unique_ptr leftResultPointer = this->check(conditionalFormula.getSubformula().asReachabilityRewardFormula().getSubformula()); + std::unique_ptr rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula()); + ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); + + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template class SparseDtmcPrctlModelChecker>; } } \ No newline at end of file diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 264f1725d..bdfbe5509 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -25,11 +25,13 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeCumulativeRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - + virtual std::unique_ptr computeConditionalRewards(CheckTask const& checkTask) override; + private: // An object that is used for retrieving linear equation solvers. std::unique_ptr> linearEquationSolverFactory; diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index b1401cd8a..2be798889 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -46,7 +46,7 @@ namespace storm { return result; } - + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. @@ -154,7 +154,7 @@ namespace storm { return result; } - + template std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory); @@ -170,7 +170,7 @@ namespace storm { }, targetStates, qualitative, linearEquationSolverFactory); } - + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { @@ -222,23 +222,26 @@ namespace storm { return result; } - + template std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, qualitative, linearEquationSolverFactory); } template - std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - std::vector probabilitiesToReachConditionStates = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory); + typename SparseDtmcPrctlHelper::BaierTransformedModel SparseDtmcPrctlHelper::computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + BaierTransformedModel result; // Start by computing all 'before' states, i.e. the states for which the conditional probability is defined. - storm::storage::BitVector beforeStates(targetStates.size(), true); + std::vector probabilitiesToReachConditionStates = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory); + + result.beforeStates = storm::storage::BitVector(targetStates.size(), true); uint_fast64_t state = 0; uint_fast64_t beforeStateIndex = 0; for (auto const& value : probabilitiesToReachConditionStates) { if (value == storm::utility::zero()) { - beforeStates.set(state, false); + result.beforeStates.set(state, false); } else { probabilitiesToReachConditionStates[beforeStateIndex] = value; ++beforeStateIndex; @@ -246,35 +249,33 @@ namespace storm { ++state; } probabilitiesToReachConditionStates.resize(beforeStateIndex); - - // If there were any before states, we can compute their conditional probabilities. If not, the result - // is undefined for all states. - std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); + if (targetStates.empty()) { - storm::utility::vector::setVectorValues(result, beforeStates, storm::utility::zero()); - } else if (!beforeStates.empty()) { + result.noTargetStates = true; + return result; + } else if (!result.beforeStates.empty()) { // If there are some states for which the conditional probability is defined and there are some // states that can reach the target states without visiting condition states first, we need to // do more work. - + // First, compute the relevant states and some offsets. storm::storage::BitVector allStates(targetStates.size(), true); - std::vector numberOfBeforeStatesUpToState = beforeStates.getNumberOfSetBitsBeforeIndices(); + std::vector numberOfBeforeStatesUpToState = result.beforeStates.getNumberOfSetBitsBeforeIndices(); storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, allStates, targetStates); statesWithProbabilityGreater0 &= storm::utility::graph::getReachableStates(transitionMatrix, conditionStates, allStates, targetStates); - uint_fast64_t normalStatesOffset = beforeStates.getNumberOfSetBits(); + uint_fast64_t normalStatesOffset = result.beforeStates.getNumberOfSetBits(); std::vector numberOfNormalStatesUpToState = statesWithProbabilityGreater0.getNumberOfSetBitsBeforeIndices(); // All transitions going to states with probability zero, need to be redirected to a deadlock state. bool addDeadlockState = false; uint_fast64_t deadlockState = normalStatesOffset + statesWithProbabilityGreater0.getNumberOfSetBits(); - + // Now, we create the matrix of 'before' and 'normal' states. storm::storage::SparseMatrixBuilder builder; // Start by creating the transitions of the 'before' states. uint_fast64_t currentRow = 0; - for (auto beforeState : beforeStates) { + for (auto beforeState : result.beforeStates) { if (conditionStates.get(beforeState)) { // For condition states, we move to the 'normal' states. ValueType zeroProbability = storm::utility::zero(); @@ -291,7 +292,7 @@ namespace storm { } else { // For non-condition states, we scale the probabilities going to other before states. for (auto const& successorEntry : transitionMatrix.getRow(beforeState)) { - if (beforeStates.get(successorEntry.getColumn())) { + if (result.beforeStates.get(successorEntry.getColumn())) { builder.addNextValue(currentRow, numberOfBeforeStatesUpToState[successorEntry.getColumn()], successorEntry.getValue() * probabilitiesToReachConditionStates[numberOfBeforeStatesUpToState[successorEntry.getColumn()]] / probabilitiesToReachConditionStates[currentRow]); } } @@ -320,21 +321,84 @@ namespace storm { } // Build the new transition matrix and the new targets. - storm::storage::SparseMatrix newTransitionMatrix = builder.build(); - storm::storage::BitVector newTargetStates = targetStates % beforeStates; - newTargetStates.resize(newTransitionMatrix.getRowCount()); + result.transitionMatrix = builder.build(); + storm::storage::BitVector newTargetStates = targetStates % result.beforeStates; + newTargetStates.resize(result.transitionMatrix.get().getRowCount()); for (auto state : targetStates % statesWithProbabilityGreater0) { newTargetStates.set(normalStatesOffset + state, true); } + result.targetStates = std::move(newTargetStates); + + // If a reward model was given, we need to compute the rewards for the transformed model. + if (stateRewards) { + std::vector newStateRewards(result.beforeStates.getNumberOfSetBits()); + storm::utility::vector::selectVectorValues(newStateRewards, result.beforeStates, stateRewards.get()); + + newStateRewards.reserve(newStateRewards.size() + statesWithProbabilityGreater0.getNumberOfSetBits() + 1); + for (auto state : statesWithProbabilityGreater0) { + newStateRewards.push_back(stateRewards.get()[state]); + } + // Add a zero reward to the deadlock state. + newStateRewards.push_back(storm::utility::zero()); + result.stateRewards = std::move(newStateRewards); + } - // Finally, compute the conditional probabiltities by a reachability query. - std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), newTargetStates, qualitative, linearEquationSolverFactory); - storm::utility::vector::setVectorValues(result, beforeStates, conditionalProbabilities); } - + return result; } - + + template + std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + // Prepare result vector. + std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); + + if (!conditionStates.empty()) { + BaierTransformedModel transformedModel = computeBaierTransformation(transitionMatrix, backwardTransitions, targetStates, conditionStates, boost::none, linearEquationSolverFactory); + + if (transformedModel.noTargetStates) { + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); + } else { + // At this point, we do not need to check whether there are 'before' states, since the condition + // states were non-empty so there is at least one state with a positive probability of satisfying + // the condition. + + // Now compute reachability probabilities in the transformed model. + storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); + } + } + + return result; + } + + template + std::vector SparseDtmcPrctlHelper::computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Prepare result vector. + std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); + + if (!conditionStates.empty()) { + BaierTransformedModel transformedModel = computeBaierTransformation(transitionMatrix, backwardTransitions, targetStates, conditionStates, rewardModel.getTotalRewardVector(transitionMatrix), linearEquationSolverFactory); + + if (transformedModel.noTargetStates) { + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, storm::utility::zero()); + } else { + // At this point, we do not need to check whether there are 'before' states, since the condition + // states were non-empty so there is at least one state with a positive probability of satisfying + // the condition. + + // Now compute reachability probabilities in the transformed model. + storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); + std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); + } + } + + return result; + } + template class SparseDtmcPrctlHelper; } } diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index d1414dbce..637c30cb5 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -39,8 +39,20 @@ namespace storm { static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + private: static std::vector 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + struct BaierTransformedModel { + storm::storage::BitVector beforeStates; + boost::optional> transitionMatrix; + boost::optional targetStates; + boost::optional> stateRewards; + bool noTargetStates; + }; + + static BaierTransformedModel computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index ae7d8e0f7..d8fa100c8 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -105,8 +105,8 @@ namespace storm { qi::rule(), Skipper> simpleFormula; qi::rule(), Skipper> stateFormula; - qi::rule(), Skipper> pathFormula; - qi::rule(), Skipper> pathFormulaWithoutUntil; + qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; + qi::rule(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil; qi::rule(), Skipper> simplePathFormula; qi::rule(), Skipper> atomicStateFormula; qi::rule(), Skipper> operatorFormula; @@ -120,11 +120,11 @@ namespace storm { qi::rule(), Skipper> expressionFormula; qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - qi::rule(storm::logic::ConditionalFormula::Context), Skipper> conditionalFormula; - qi::rule(storm::logic::EventuallyFormula::Context), Skipper> eventuallyFormula; - qi::rule(), Skipper> nextFormula; - qi::rule(), Skipper> globallyFormula; - qi::rule(), Skipper> untilFormula; + qi::rule(storm::logic::FormulaContext), Skipper> conditionalFormula; + qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; + qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; + qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; + qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; qi::rule, uint_fast64_t>(), Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; @@ -142,11 +142,11 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::ConditionalFormula::Context context) const; + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; std::pair, boost::optional>> createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardModelName, std::pair, boost::optional>> const& operatorInformation, std::shared_ptr const& subformula) const; @@ -253,7 +253,7 @@ namespace storm { cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); - rewardPathFormula = eventuallyFormula(storm::logic::EventuallyFormula::Context::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(storm::logic::ConditionalFormula::Context::Reward); + rewardPathFormula = conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula; rewardPathFormula.name("reward path formula"); expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; @@ -277,28 +277,28 @@ namespace storm { notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; notStateFormula.name("negation formula"); - eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; + eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; eventuallyFormula.name("eventually formula"); - globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; globallyFormula.name("globally formula"); - nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; + nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; nextFormula.name("next formula"); - pathFormulaWithoutUntil = eventuallyFormula(storm::logic::EventuallyFormula::Context::Probability) | globallyFormula | nextFormula | stateFormula; + pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula; pathFormulaWithoutUntil.name("path formula"); - untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula.name("until formula"); - conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; + conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; conditionalFormula.name("conditional formula"); timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; timeBound.name("time bound"); - pathFormula = conditionalFormula(storm::logic::ConditionalFormula::Context::Probability); + pathFormula = conditionalFormula(qi::_r1); pathFormula.name("path formula"); operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; @@ -313,10 +313,10 @@ namespace storm { rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; rewardOperator.name("reward operator"); - expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::EventuallyFormula::Context::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; expectedTimeOperator.name("expected time operator"); - probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; probabilityOperator.name("probability operator"); andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; @@ -342,10 +342,10 @@ namespace storm { debug(longRunAverageOperator); debug(pathFormulaWithoutUntil); debug(pathFormula); - debug(conditionalFormula); +// debug(conditionalFormula); debug(nextFormula); debug(globallyFormula); - debug(eventuallyFormula); +// debug(eventuallyFormula); debug(atomicStateFormula); debug(booleanLiteralFormula); debug(labelFormula); @@ -421,7 +421,7 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { if (timeBound.get().which() == 0) { std::pair const& bounds = boost::get>(timeBound.get()); @@ -455,7 +455,7 @@ namespace storm { } } - std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::ConditionalFormula::Context context) const { + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const { return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); }