From c54ce9fea5620803e0ded448dcc96731634e2afe Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 14 Aug 2026 22:56:11 +0200 Subject: [PATCH 1/2] merging of equivalent states as preprocessing * extends the GoalStateMerger so that it can now merge states based on an input formula (e.g. all prob0/prob1 states * adds a CLI option --merge-equivalent-states to invoke that as a preprocessing * Simplifies SparseParametricModelSimplifier by calling the new GoalStateMerger --- src/storm-cli-utilities/model-handling.h | 15 + src/storm-pars-cli/sampling.h | 2 - src/storm-pars-cli/storm-pars.cpp | 7 +- ...SparseDtmcParameterLiftingModelChecker.cpp | 4 +- .../SparseMdpParameterLiftingModelChecker.cpp | 4 +- ...tingSparseParameterLiftingModelChecker.cpp | 18 +- .../SparseParametricDtmcSimplifier.cpp | 242 -------- .../SparseParametricDtmcSimplifier.h | 27 - .../SparseParametricMdpSimplifier.cpp | 354 ------------ .../SparseParametricMdpSimplifier.h | 40 -- .../SparseParametricModelSimplifier.cpp | 317 +++++++--- .../SparseParametricModelSimplifier.h | 26 +- src/storm/api/transformation.h | 24 + .../constraintbased/SparseCbQuery.cpp | 4 +- .../pcaa/StandardPcaaWeightVectorChecker.cpp | 4 +- .../modules/TransformationSettings.cpp | 10 + .../settings/modules/TransformationSettings.h | 6 + src/storm/transformer/GoalStateMerger.cpp | 541 ++++++++++++++---- src/storm/transformer/GoalStateMerger.h | 89 ++- src/storm/utility/graph.cpp | 4 + ...adientDescentInstantiationSearcherTest.cpp | 6 +- ...erivativeInstantiationModelCheckerTest.cpp | 8 +- ...seDtmcParameterLiftingMonotonicityTest.cpp | 4 +- .../monotonicity/AssumptionCheckerTest.cpp | 12 +- .../monotonicity/AssumptionMakerTest.cpp | 8 +- .../monotonicity/MonotonicityCheckerTest.cpp | 12 +- .../monotonicity/MonotonicityHelperTest.cpp | 18 +- .../region/monotonicity/OrderExtenderTest.cpp | 20 +- .../storm/transformer/GoalStateMergerTest.cpp | 119 ++++ 29 files changed, 955 insertions(+), 990 deletions(-) delete mode 100644 src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp delete mode 100644 src/storm-pars/transformer/SparseParametricDtmcSimplifier.h delete mode 100644 src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp delete mode 100644 src/storm-pars/transformer/SparseParametricMdpSimplifier.h create mode 100644 src/test/storm/transformer/GoalStateMergerTest.cpp diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 32eaf1c900..cc4b07eeb8 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -735,6 +735,21 @@ std::pair, bool> preprocessModel(std:: STORM_PRINT_AND_LOG("Transition matrix hash after permuting: " << result.first->getTransitionMatrix().hash() << ".\n"); } + // Merging of states should be done before applying bisimulation as this order leads to the smallest quotient + if (transformationSettings.isMergeEquivalentStatesSet()) { + auto formulas = createFormulasToRespect(input.properties); + if (formulas.size() != 1) { + STORM_LOG_WARN("Skipping merging of equivalent states as it requires exactly one input property. " << formulas.size() + << " properties given instead."); + } else if (auto mergedModel = storm::api::mergeEquivalentStatesForFormula(result.first, *formulas.front())) { + STORM_LOG_INFO("Merged target/sink states relevant for the considered property '" << *formulas.front() << "'."); + result.first = mergedModel; + result.second = true; + } else { + STORM_LOG_INFO("Merging equivalent states is not applicable for the considered property '" << *formulas.front() << "'."); + } + } + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); result.second = true; diff --git a/src/storm-pars-cli/sampling.h b/src/storm-pars-cli/sampling.h index 0b6362455b..6475c873ee 100644 --- a/src/storm-pars-cli/sampling.h +++ b/src/storm-pars-cli/sampling.h @@ -24,8 +24,6 @@ #include "storm-pars/settings/modules/RegionSettings.h" #include "storm-pars/derivative/GradientDescentMethod.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" -#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" #include "storm-pars/utility/parametric.h" diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index c35a87c389..9aa9d42b8c 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -19,8 +19,7 @@ #include "storm-pars/settings/modules/SamplingSettings.h" #include "storm-pars/transformer/BigStep.h" #include "storm-pars/transformer/BinaryDtmcTransformer.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" -#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-pars/utility/parametric.h" #include "storm/api/storm.h" #include "storm/exceptions/BaseException.h" @@ -159,7 +158,7 @@ std::shared_ptr simplifyModel(std::shared_ptr result; if (model->isOfType(storm::models::ModelType::Dtmc)) { - storm::transformer::SparseParametricDtmcSimplifier> simplifier( + storm::transformer::SparseParametricModelSimplifier> simplifier( *(model->template as>())); std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); @@ -168,7 +167,7 @@ std::shared_ptr simplifyModel(std::shared_ptrisOfType(storm::models::ModelType::Mdp)) { - storm::transformer::SparseParametricMdpSimplifier> simplifier( + storm::transformer::SparseParametricModelSimplifier> simplifier( *(model->template as>())); std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 1db115b690..b54771e002 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -9,7 +9,7 @@ #include "storm-pars/modelchecker/region/monotonicity/OrderBasedMonotonicityBackend.h" #include "storm-pars/transformer/BigStep.h" #include "storm-pars/transformer/IntervalEndComponentPreserver.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/RationalFunctionForward.h" #include "storm/environment/Environment.h" @@ -93,7 +93,7 @@ void SparseDtmcParameterLiftingModelChecker(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier(*dtmc); simplifier.setPreserveParametricTransitions(true); STORM_LOG_THROW(simplifier.simplify(checkTask.getFormula()), storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); this->parametricModel = simplifier.getSimplifiedModel(); diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp index 9947da01e3..d7f077f636 100644 --- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp @@ -2,7 +2,7 @@ #include "storm-pars/modelchecker/region/AnnotatedRegion.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityBackend.h" -#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotImplementedException.h" @@ -68,7 +68,7 @@ void SparseMdpParameterLiftingModelChecker::speci reset(); if (allowModelSimplifications) { - auto simplifier = storm::transformer::SparseParametricMdpSimplifier(*mdp); + auto simplifier = storm::transformer::SparseParametricModelSimplifier(*mdp); STORM_LOG_THROW(simplifier.simplify(checkTask.getFormula()), storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); this->parametricModel = simplifier.getSimplifiedModel(); this->specifyFormula(env, checkTask.substituteFormula(*simplifier.getSimplifiedFormula())); diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp index d9425b0cb1..0bad553c5b 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp @@ -2,8 +2,7 @@ #include "storm-pars/modelchecker/region/AnnotatedRegion.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityBackend.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" -#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -50,17 +49,10 @@ void ValidatingSparseParameterLiftingModelCheckertemplate as(); - if constexpr (IsMDP) { - auto simplifier = storm::transformer::SparseParametricMdpSimplifier(*dtmcOrMdp); - STORM_LOG_THROW(simplifier.simplify(checkTask.getFormula()), storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); - auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); - specifyUnderlyingCheckers(simplifier.getSimplifiedModel(), simplifiedTask); - } else { - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier(*dtmcOrMdp); - STORM_LOG_THROW(simplifier.simplify(checkTask.getFormula()), storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); - auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); - specifyUnderlyingCheckers(simplifier.getSimplifiedModel(), simplifiedTask); - } + auto simplifier = storm::transformer::SparseParametricModelSimplifier(*dtmcOrMdp); + STORM_LOG_THROW(simplifier.simplify(checkTask.getFormula()), storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula()); + specifyUnderlyingCheckers(simplifier.getSimplifiedModel(), simplifiedTask); } else { specifyUnderlyingCheckers(parametricModel, checkTask); } diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp deleted file mode 100644 index 8ddebc5dca..0000000000 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.cpp +++ /dev/null @@ -1,242 +0,0 @@ -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" - -#include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/UnexpectedException.h" -#include "storm/logic/CloneVisitor.h" -#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/models/sparse/Dtmc.h" -#include "storm/transformer/GoalStateMerger.h" -#include "storm/utility/graph.h" - -namespace storm { -namespace transformer { - -template -SparseParametricDtmcSimplifier::SparseParametricDtmcSimplifier(SparseModelType const& model) - : SparseParametricModelSimplifier(model) { - // intentionally left empty -} - -template -bool SparseParametricDtmcSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // Get the prob0, prob1 and the maybeStates - storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); - if (!propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getLeftSubformula()) || - !propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getRightSubformula())) { - STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); - return false; - } - storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - std::pair statesWithProbability01 = - storm::utility::graph::performProb01(this->originalModel, phiStates, psiStates); - // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state - storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates( - this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, - statesWithProbability01.second); - storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second; - - // obtain the resulting subsystem - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); - this->simplifiedModel = mergerResult.model; - statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.targetState) { - statesWithProbability01.second.set(mergerResult.targetState.get(), true); - } - std::string targetLabel = "target"; - while (this->simplifiedModel->hasLabel(targetLabel)) { - targetLabel = "_" + targetLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(statesWithProbability01.second)); - - // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared(targetLabel); - auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); - this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); - - // Eliminate all states for which all outgoing transitions are constant - storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); - if (mergerResult.targetState) { - considerForElimination.set(*mergerResult.targetState, false); - } - if (mergerResult.sinkState) { - considerForElimination.set(*mergerResult.sinkState, false); - } - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination); - - return true; -} - -template -bool SparseParametricDtmcSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - STORM_LOG_THROW(!formula.getSubformula().asBoundedUntilFormula().hasLowerBound(), storm::exceptions::NotSupportedException, - "Lower step bounds are not supported."); - STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().hasUpperBound(), storm::exceptions::UnexpectedException, - "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().getUpperBound().getBaseExpression().isIntegerLiteralExpression(), - storm::exceptions::UnexpectedException, "Expected a bounded until formula with integral bounds."); - - uint_fast64_t upperStepBound = formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt(); - if (formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict()) { - STORM_LOG_THROW(upperStepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero."); - --upperStepBound; - } - - // Get the prob0, target, and the maybeStates - storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); - if (!propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) || - !propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())) { - STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); - return false; - } - storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - storm::storage::BitVector probGreater0States = - storm::utility::graph::performProbGreater0(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound); - - // Only consider the maybestates that are reachable from one initial probGreater0 state within the given amount of steps and without hopping over a target - // state - storm::storage::BitVector reachableGreater0States = - storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & probGreater0States, - probGreater0States, psiStates, true, upperStepBound); - storm::storage::BitVector maybeStates = reachableGreater0States & ~psiStates; - storm::storage::BitVector prob0States = ~reachableGreater0States & ~psiStates; - - // obtain the resulting subsystem - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States); - this->simplifiedModel = mergerResult.model; - psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.targetState) { - psiStates.set(mergerResult.targetState.get(), true); - } - std::string targetLabel = "target"; - while (this->simplifiedModel->hasLabel(targetLabel)) { - targetLabel = "_" + targetLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates)); - - // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared(targetLabel); - auto boundedUntilFormula = - std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, - storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), - formula.getSubformula().asBoundedUntilFormula().getUpperBound()), - storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); - this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); - - return true; -} - -template -bool SparseParametricDtmcSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { - typename SparseModelType::RewardModelType const& originalRewardModel = - formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel(); - - // Get the prob1 and the maybeStates - storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); - if (!propositionalChecker.canHandle(formula.getSubformula().asEventuallyFormula().getSubformula())) { - STORM_LOG_DEBUG("Can not simplify when reachability reward formula has non-propositional subformula(s). Formula: " << formula); - return false; - } - storm::storage::BitVector targetStates = std::move(propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward - targetStates = storm::utility::graph::performProb1(this->originalModel.getBackwardTransitions(), - originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates); - storm::storage::BitVector statesWithProb1 = storm::utility::graph::performProb1( - this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates); - storm::storage::BitVector infinityStates = ~statesWithProb1; - // Only consider the states that are reachable from an initial state without hopping over a target state - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates( - this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates); - storm::storage::BitVector maybeStates = reachableStates & ~targetStates; - - // obtain the resulting subsystem - std::vector rewardModelNameAsVector( - 1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); - this->simplifiedModel = mergerResult.model; - targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.targetState) { - targetStates.set(mergerResult.targetState.get(), true); - } - std::string targetLabel = "target"; - while (this->simplifiedModel->hasLabel(targetLabel)) { - targetLabel = "_" + targetLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates)); - - // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared(targetLabel); - auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); - this->simplifiedFormula = - std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation()); - - // Eliminate all states for which all outgoing transitions are constant - storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); - if (mergerResult.targetState) { - considerForElimination.set(*mergerResult.targetState, false); - } - if (mergerResult.sinkState) { - considerForElimination.set(*mergerResult.sinkState, false); - } - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front()); - - return true; -} - -template -bool SparseParametricDtmcSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { - STORM_LOG_THROW(formula.getSubformula().asCumulativeRewardFormula().getBound().getBaseExpression().isIntegerLiteralExpression(), - storm::exceptions::UnexpectedException, "Expected a cumulative reward formula with integral bound."); - - typename SparseModelType::RewardModelType const& originalRewardModel = - formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel(); - - uint_fast64_t stepBound = formula.getSubformula().asCumulativeRewardFormula().getBound().evaluateAsInt(); - if (formula.getSubformula().asCumulativeRewardFormula().isBoundStrict()) { - STORM_LOG_THROW(stepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero."); - --stepBound; - } - - // Get the states with non-zero reward - storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0( - this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), - ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound); - storm::storage::BitVector zeroRewardStates = ~maybeStates; - storm::storage::BitVector noStates(this->originalModel.getNumberOfStates(), false); - - // obtain the resulting subsystem - std::vector rewardModelNameAsVector( - 1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); - this->simplifiedModel = mergerResult.model; - - // obtain the simplified formula for the simplified model - this->simplifiedFormula = storm::logic::CloneVisitor().clone(formula); - - return true; -} - -template class SparseParametricDtmcSimplifier>; -} // namespace transformer -} // namespace storm diff --git a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h b/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h deleted file mode 100644 index 2c788fc902..0000000000 --- a/src/storm-pars/transformer/SparseParametricDtmcSimplifier.h +++ /dev/null @@ -1,27 +0,0 @@ -#pragma once - -#include "storm-pars/transformer/SparseParametricModelSimplifier.h" - -namespace storm { -namespace transformer { - -/*! - * This class performs different steps to simplify the given (parametric) model. - * Checking the obtained simplified formula on the simplified model yields the same result as checking the original formula on the original model (wrt. to the - * initial states of the two models) End Components of nondeterministic models are removed whenever this is valid for the corresponding formula. This allows us - * to apply, e.g., value iteration that does not start from the 0,...,0 vector. - */ -template -class SparseParametricDtmcSimplifier : public SparseParametricModelSimplifier { - public: - SparseParametricDtmcSimplifier(SparseModelType const& model); - - protected: - // Perform the simplification for the corresponding formula type - virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override; - virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override; - virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) override; - virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) override; -}; -} // namespace transformer -} // namespace storm diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp b/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp deleted file mode 100644 index ab40622cfc..0000000000 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.cpp +++ /dev/null @@ -1,354 +0,0 @@ -#include "storm-pars/transformer/SparseParametricMdpSimplifier.h" - -#include "storm/adapters/RationalFunctionAdapter.h" -#include "storm/exceptions/NotSupportedException.h" -#include "storm/exceptions/UnexpectedException.h" -#include "storm/logic/CloneVisitor.h" -#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/models/sparse/Mdp.h" -#include "storm/transformer/EndComponentEliminator.h" -#include "storm/transformer/GoalStateMerger.h" -#include "storm/utility/graph.h" -#include "storm/utility/vector.h" - -namespace storm { -namespace transformer { - -template -SparseParametricMdpSimplifier::SparseParametricMdpSimplifier(SparseModelType const& model) - : SparseParametricModelSimplifier(model) { - // intentionally left empty -} - -template -bool SparseParametricMdpSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - bool minimizing = - formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); - - // Get the prob0, prob1 and the maybeStates - storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); - if (!propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getLeftSubformula()) || - !propositionalChecker.canHandle(formula.getSubformula().asUntilFormula().getRightSubformula())) { - STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); - return false; - } - storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getLeftSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asUntilFormula().getRightSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - std::pair statesWithProbability01 = - minimizing ? storm::utility::graph::performProb01Min(this->originalModel, phiStates, psiStates) - : storm::utility::graph::performProb01Max(this->originalModel, phiStates, psiStates); - - // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state - storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates( - this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, - statesWithProbability01.second); - storm::storage::BitVector maybeStates = reachableGreater0States & ~statesWithProbability01.second; - - // obtain the resulting subsystem - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); - this->simplifiedModel = mergerResult.model; - statesWithProbability01.first = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.sinkState) { - statesWithProbability01.first.set(mergerResult.sinkState.get(), true); - } - std::string sinkLabel = "sink"; - while (this->simplifiedModel->hasLabel(sinkLabel)) { - sinkLabel = "_" + sinkLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(statesWithProbability01.first)); - statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.targetState) { - statesWithProbability01.second.set(mergerResult.targetState.get(), true); - } - std::string targetLabel = "target"; - while (this->simplifiedModel->hasLabel(targetLabel)) { - targetLabel = "_" + targetLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(statesWithProbability01.second)); - - // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared(targetLabel); - auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); - this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); - - // Eliminate all states for which all outgoing transitions are constant - storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); - if (mergerResult.targetState) { - considerForElimination.set(*mergerResult.targetState, false); - } - if (mergerResult.sinkState) { - considerForElimination.set(*mergerResult.sinkState, false); - } - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination); - - // Eliminate the end components that do not contain a target or a sink state (only required if the probability is maximized) - if (!minimizing) { - this->simplifiedModel = this->eliminateNeutralEndComponents( - *this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel)); - } - - return true; -} - -template -bool SparseParametricMdpSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - STORM_LOG_THROW(!formula.getSubformula().asBoundedUntilFormula().hasLowerBound(), storm::exceptions::NotSupportedException, - "Lower step bounds are not supported."); - STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().hasUpperBound(), storm::exceptions::UnexpectedException, - "Expected a bounded until formula with an upper bound."); - STORM_LOG_THROW(formula.getSubformula().asBoundedUntilFormula().getUpperBound().getBaseExpression().isIntegerLiteralExpression(), - storm::exceptions::UnexpectedException, "Expected a bounded until formula with integral bounds."); - - bool minimizing = - formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); - uint_fast64_t upperStepBound = formula.getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt(); - if (formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict()) { - STORM_LOG_THROW(upperStepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero."); - --upperStepBound; - } - - // Get the prob0, target, and the maybeStates - storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); - if (!propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) || - !propositionalChecker.canHandle(formula.getSubformula().asBoundedUntilFormula().getRightSubformula())) { - STORM_LOG_DEBUG("Can not simplify when Until-formula has non-propositional subformula(s). Formula: " << formula); - return false; - } - storm::storage::BitVector phiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getLeftSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - storm::storage::BitVector psiStates = std::move(propositionalChecker.check(formula.getSubformula().asBoundedUntilFormula().getRightSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - storm::storage::BitVector probGreater0States = - minimizing ? storm::utility::graph::performProbGreater0A(this->originalModel.getTransitionMatrix(), - this->originalModel.getTransitionMatrix().getRowGroupIndices(), - this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound) - : storm::utility::graph::performProbGreater0E(this->originalModel.getBackwardTransitions(), phiStates, psiStates, true, upperStepBound); - - // Only consider the maybestates that are reachable from one initial probGreater0 state within the given amount of steps and without hopping over a target - // state - storm::storage::BitVector reachableGreater0States = - storm::utility::graph::getReachableStates(this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & probGreater0States, - probGreater0States, psiStates, true, upperStepBound); - storm::storage::BitVector maybeStates = reachableGreater0States & ~psiStates; - storm::storage::BitVector prob0States = ~reachableGreater0States & ~psiStates; - - // obtain the resulting subsystem - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States); - this->simplifiedModel = mergerResult.model; - psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.targetState) { - psiStates.set(mergerResult.targetState.get(), true); - } - std::string targetLabel = "target"; - while (this->simplifiedModel->hasLabel(targetLabel)) { - targetLabel = "_" + targetLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates)); - - // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared(targetLabel); - auto boundedUntilFormula = - std::make_shared(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, - storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), - formula.getSubformula().asBoundedUntilFormula().getUpperBound()), - storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); - this->simplifiedFormula = std::make_shared(boundedUntilFormula, formula.getOperatorInformation()); - - return true; -} - -template -bool SparseParametricMdpSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { - typename SparseModelType::RewardModelType const& originalRewardModel = - formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel(); - - bool minimizing = - formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); - - // Get the prob1 and the maybeStates - storm::modelchecker::SparsePropositionalModelChecker propositionalChecker(this->originalModel); - if (!propositionalChecker.canHandle(formula.getSubformula().asEventuallyFormula().getSubformula())) { - STORM_LOG_DEBUG("Can not simplify when reachability reward formula has non-propositional subformula(s). Formula: " << formula); - return false; - } - storm::storage::BitVector targetStates = std::move(propositionalChecker.check(formula.getSubformula().asEventuallyFormula().getSubformula()) - ->template asExplicitQualitativeCheckResult() - .getTruthValuesVector()); - // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward - // TODO for the call of Prob1E we could restrict the analysis to actions with zero reward instead of states with zero reward - targetStates = - minimizing ? storm::utility::graph::performProb1E(this->originalModel, this->originalModel.getBackwardTransitions(), - originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates) - : storm::utility::graph::performProb1A(this->originalModel, this->originalModel.getBackwardTransitions(), - originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), targetStates); - storm::storage::BitVector statesWithProb1 = - minimizing ? storm::utility::graph::performProb1E(this->originalModel, this->originalModel.getBackwardTransitions(), - storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates) - : storm::utility::graph::performProb1A(this->originalModel, this->originalModel.getBackwardTransitions(), - storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), targetStates); - storm::storage::BitVector infinityStates = ~statesWithProb1; - // Only consider the states that are reachable from an initial state without hopping over a target state - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates( - this->originalModel.getTransitionMatrix(), this->originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates); - storm::storage::BitVector maybeStates = reachableStates & ~targetStates; - - // obtain the resulting subsystem - std::vector rewardModelNameAsVector( - 1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); - this->simplifiedModel = mergerResult.model; - infinityStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.sinkState) { - infinityStates.set(mergerResult.sinkState.get(), true); - } - std::string sinkLabel = "sink"; - while (this->simplifiedModel->hasLabel(sinkLabel)) { - sinkLabel = "_" + sinkLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(infinityStates)); - - targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); - if (mergerResult.targetState) { - targetStates.set(mergerResult.targetState.get(), true); - } - std::string targetLabel = "target"; - while (this->simplifiedModel->hasLabel(targetLabel)) { - targetLabel = "_" + targetLabel; - } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates)); - - // obtain the simplified formula for the simplified model - auto labelFormula = std::make_shared(targetLabel); - auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); - this->simplifiedFormula = - std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation()); - - // Eliminate all states for which all outgoing transitions are constant - storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); - if (mergerResult.targetState) { - considerForElimination.set(*mergerResult.targetState, false); - } - if (mergerResult.sinkState) { - considerForElimination.set(*mergerResult.sinkState, false); - } - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front()); - - // Eliminate the end components in which no reward is collected (only required if rewards are minimized) - if (minimizing) { - this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, - this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel), - rewardModelNameAsVector.front()); - } - return true; -} - -template -bool SparseParametricMdpSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { - STORM_LOG_THROW(formula.getSubformula().asCumulativeRewardFormula().getBound().getBaseExpression().isIntegerLiteralExpression(), - storm::exceptions::UnexpectedException, "Expected a cumulative reward formula with integral bound."); - - typename SparseModelType::RewardModelType const& originalRewardModel = - formula.hasRewardModelName() ? this->originalModel.getRewardModel(formula.getRewardModelName()) : this->originalModel.getUniqueRewardModel(); - - bool minimizing = - formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); - uint_fast64_t stepBound = formula.getSubformula().asCumulativeRewardFormula().getBound().evaluateAsInt(); - if (formula.getSubformula().asCumulativeRewardFormula().isBoundStrict()) { - STORM_LOG_THROW(stepBound > 0, storm::exceptions::UnexpectedException, "Expected a strict upper bound that is greater than zero."); - --stepBound; - } - - // Get the states with non-zero reward - storm::storage::BitVector maybeStates = - minimizing ? storm::utility::graph::performProbGreater0A( - this->originalModel.getTransitionMatrix(), this->originalModel.getTransitionMatrix().getRowGroupIndices(), - this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), - ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound) - : storm::utility::graph::performProbGreater0E( - this->originalModel.getBackwardTransitions(), storm::storage::BitVector(this->originalModel.getNumberOfStates(), true), - ~originalRewardModel.getStatesWithZeroReward(this->originalModel.getTransitionMatrix()), true, stepBound); - storm::storage::BitVector zeroRewardStates = ~maybeStates; - storm::storage::BitVector noStates(this->originalModel.getNumberOfStates(), false); - - // obtain the resulting subsystem - std::vector rewardModelNameAsVector( - 1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); - storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = - goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); - this->simplifiedModel = mergerResult.model; - - // obtain the simplified formula for the simplified model - this->simplifiedFormula = storm::logic::CloneVisitor().clone(formula); - - return true; -} - -template -std::shared_ptr SparseParametricMdpSimplifier::eliminateNeutralEndComponents( - SparseModelType const& model, storm::storage::BitVector const& ignoredStates, boost::optional const& rewardModelName) { - // Get the actions that can be part of an EC - storm::storage::BitVector possibleECActions(model.getNumberOfChoices(), true); - for (auto state : ignoredStates) { - for (uint_fast64_t actionIndex = model.getTransitionMatrix().getRowGroupIndices()[state]; - actionIndex < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++actionIndex) { - possibleECActions.set(actionIndex, false); - } - } - - // Get the action-based reward values and unselect non-zero reward actions - std::vector actionRewards; - if (rewardModelName) { - actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(model.getTransitionMatrix()); - uint_fast64_t actionIndex = 0; - for (auto const& actionReward : actionRewards) { - if (!storm::utility::isZero(actionReward)) { - possibleECActions.set(actionIndex, false); - } - ++actionIndex; - } - } - - // Invoke EC Elimination - auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform( - model.getTransitionMatrix(), storm::storage::BitVector(model.getNumberOfStates(), true), possibleECActions, - storm::storage::BitVector(model.getNumberOfStates(), false)); - - // obtain the reward model for the resulting system - std::unordered_map rewardModels; - if (rewardModelName) { - std::vector newActionRewards(ecEliminatorResult.matrix.getRowCount()); - storm::utility::vector::selectVectorValues(newActionRewards, ecEliminatorResult.newToOldRowMapping, actionRewards); - rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(std::nullopt, std::move(actionRewards)))); - } - - // the new labeling - storm::models::sparse::StateLabeling labeling(ecEliminatorResult.matrix.getRowGroupCount()); - for (auto const& label : model.getStateLabeling().getLabels()) { - auto const& origStatesWithLabel = model.getStates(label); - storm::storage::BitVector newStatesWithLabel(ecEliminatorResult.matrix.getRowGroupCount(), false); - for (auto const& origState : origStatesWithLabel) { - newStatesWithLabel.set(ecEliminatorResult.oldToNewStateMapping[origState], true); - } - labeling.addLabel(label, std::move(newStatesWithLabel)); - } - - return std::make_shared(std::move(ecEliminatorResult.matrix), std::move(labeling), std::move(rewardModels)); -} - -template class SparseParametricMdpSimplifier>; -} // namespace transformer -} // namespace storm diff --git a/src/storm-pars/transformer/SparseParametricMdpSimplifier.h b/src/storm-pars/transformer/SparseParametricMdpSimplifier.h deleted file mode 100644 index bca6af0d52..0000000000 --- a/src/storm-pars/transformer/SparseParametricMdpSimplifier.h +++ /dev/null @@ -1,40 +0,0 @@ -#pragma once - -#include "storm-pars/transformer/SparseParametricModelSimplifier.h" - -namespace storm { -namespace transformer { - -/*! - * This class performs different steps to simplify the given (parametric) model. - * Checking the obtained simplified formula on the simplified model yields the same result as checking the original formula on the original model (wrt. to the - * initial states of the two models) End Components of nondeterministic models are removed whenever this is valid for the corresponding formula. This allows us - * to apply, e.g., value iteration that does not start from the 0,...,0 vector. - */ -template -class SparseParametricMdpSimplifier : public SparseParametricModelSimplifier { - public: - SparseParametricMdpSimplifier(SparseModelType const& model); - - protected: - // Perform the simplification for the corresponding formula type - virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override; - virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override; - virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) override; - virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) override; - - /*! - * Eliminates all end components of the model satisfying - * * ignoredStates is false for all states of the EC - * * (if rewardModelName is given) there is no reward collected while staying inside the EC. - * - * Eliminating an EC means that it is replaced by a single state whose incoming and outgoing tansitions correspond to the incoming and outgoing transitions - * of the EC - * - * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given) - */ - static std::shared_ptr eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates, - boost::optional const& rewardModelName = boost::none); -}; -} // namespace transformer -} // namespace storm diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp index 16dbe56742..ec6a484245 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp @@ -8,99 +8,29 @@ #include "storm/models/sparse/Mdp.h" #include "storm/solver/stateelimination/NondeterministicModelStateEliminator.h" #include "storm/storage/FlexibleSparseMatrix.h" +#include "storm/transformer/EndComponentEliminator.h" +#include "storm/transformer/GoalStateMerger.h" #include "storm/utility/vector.h" namespace storm { namespace transformer { -template -SparseParametricModelSimplifier::SparseParametricModelSimplifier(SparseModelType const& model) : originalModel(model) { - // intentionally left empty -} +namespace { +/*! + * Eliminates all states that satisfy + * * there is only one enabled action (i.e., there is no nondeterministic choice at the state), + * * all outgoing transitions are constant, + * * there is no statelabel defined, and + * * (if rewardModelName is given) the reward collected at the state is constant. + * + * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given). + * Labelings of eliminated states will be lost + */ template -bool SparseParametricModelSimplifier::simplify(storm::logic::Formula const& formula) { - // Make sure that there is no old result from a previous call - simplifiedModel = nullptr; - simplifiedFormula = nullptr; - if (formula.isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const& probOpForm = formula.asProbabilityOperatorFormula(); - if (probOpForm.getSubformula().isUntilFormula()) { - return simplifyForUntilProbabilities(probOpForm); - } else if (probOpForm.getSubformula().isReachabilityProbabilityFormula()) { - return simplifyForReachabilityProbabilities(probOpForm); - } else if (probOpForm.getSubformula().isBoundedUntilFormula()) { - return simplifyForBoundedUntilProbabilities(probOpForm); - } - } else if (formula.isRewardOperatorFormula()) { - storm::logic::RewardOperatorFormula rewOpForm = formula.asRewardOperatorFormula(); - STORM_LOG_THROW((rewOpForm.hasRewardModelName() && originalModel.hasRewardModel(rewOpForm.getRewardModelName())) || - (!rewOpForm.hasRewardModelName() && originalModel.hasUniqueRewardModel()), - storm::exceptions::InvalidPropertyException, - "The reward model specified by formula " << formula << " is not available in the given model."); - if (rewOpForm.getSubformula().isReachabilityRewardFormula()) { - return simplifyForReachabilityRewards(rewOpForm); - } else if (rewOpForm.getSubformula().isCumulativeRewardFormula()) { - return simplifyForCumulativeRewards(rewOpForm); - } - } - // reaching this point means that the provided formula is not supported. Thus, no simplification is possible. - STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); - return false; -} - -template -std::shared_ptr SparseParametricModelSimplifier::getSimplifiedModel() const { - STORM_LOG_THROW(simplifiedModel, storm::exceptions::InvalidStateException, "Tried to get the simplified model but simplification was not invoked before."); - return simplifiedModel; -} - -template -std::shared_ptr SparseParametricModelSimplifier::getSimplifiedFormula() const { - STORM_LOG_THROW(simplifiedFormula, storm::exceptions::InvalidStateException, - "Tried to get the simplified formula but simplification was not invoked before."); - return simplifiedFormula; -} - -template -bool SparseParametricModelSimplifier::simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // If this method was not overridden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); - return false; -} - -template -bool SparseParametricModelSimplifier::simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // transform to until formula - auto untilFormula = std::make_shared(storm::logic::Formula::getTrueFormula(), - formula.getSubformula().asEventuallyFormula().getSubformula().asSharedPointer()); - return simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula(untilFormula, formula.getOperatorInformation())); -} - -template -bool SparseParametricModelSimplifier::simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) { - // If this method was not overridden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); - return false; -} - -template -bool SparseParametricModelSimplifier::simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) { - // If this method was not overridden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); - return false; -} - -template -bool SparseParametricModelSimplifier::simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) { - // If this method was not overridden by any subclass, simplification is not possible - STORM_LOG_DEBUG("Simplification not possible because the formula is not supported. Formula: " << formula); - return false; -} - -template -std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates( - SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName) { +std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, bool preserveParametricTransitions, + storm::storage::BitVector const& consideredStates, + std::optional const& rewardModelName) { storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); auto backwardsSparseMatrix = sparseMatrix.transpose(); @@ -117,14 +47,14 @@ std::shared_ptr SparseParametricModelSimplifierpreserveParametricTransitions) { + if (state && preserveParametricTransitions) { for (auto const& entry : backwardsSparseMatrix.getRowGroup(state)) { if (!storm::utility::isConstant(entry.getValue())) { selectedStates.set(state, false); @@ -159,6 +89,217 @@ std::shared_ptr SparseParametricModelSimplifier(std::move(newTransitionMatrix), model.getStateLabeling().getSubLabeling(selectedStates), std::move(rewardModels)); } +/*! + * Eliminates all end components of the model satisfying + * * ignoredStates is false for all states of the EC + * * (if rewardModelName is given) there is no reward collected while staying inside the EC. + * + * Eliminating an EC means that it is replaced by a single state whose incoming and outgoing tansitions correspond to the incoming and outgoing transitions + * of the EC. Only applicable to nondeterministic models. + * + * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given) + */ +template +std::shared_ptr eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates, + std::optional const& rewardModelName) { + // Get the actions that can be part of an EC + storm::storage::BitVector possibleECActions(model.getNumberOfChoices(), true); + for (auto state : ignoredStates) { + for (uint_fast64_t actionIndex = model.getTransitionMatrix().getRowGroupIndices()[state]; + actionIndex < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++actionIndex) { + possibleECActions.set(actionIndex, false); + } + } + + // Get the action-based reward values and unselect non-zero reward actions + std::vector actionRewards; + if (rewardModelName) { + actionRewards = model.getRewardModel(*rewardModelName).getTotalRewardVector(model.getTransitionMatrix()); + uint_fast64_t actionIndex = 0; + for (auto const& actionReward : actionRewards) { + if (!storm::utility::isZero(actionReward)) { + possibleECActions.set(actionIndex, false); + } + ++actionIndex; + } + } + + // Invoke EC Elimination + auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform( + model.getTransitionMatrix(), storm::storage::BitVector(model.getNumberOfStates(), true), possibleECActions, + storm::storage::BitVector(model.getNumberOfStates(), false)); + + // obtain the reward model for the resulting system + std::unordered_map rewardModels; + if (rewardModelName) { + std::vector newActionRewards(ecEliminatorResult.matrix.getRowCount()); + storm::utility::vector::selectVectorValues(newActionRewards, ecEliminatorResult.newToOldRowMapping, actionRewards); + rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(std::nullopt, std::move(actionRewards)))); + } + + // the new labeling + storm::models::sparse::StateLabeling labeling(ecEliminatorResult.matrix.getRowGroupCount()); + for (auto const& label : model.getStateLabeling().getLabels()) { + auto const& origStatesWithLabel = model.getStates(label); + storm::storage::BitVector newStatesWithLabel(ecEliminatorResult.matrix.getRowGroupCount(), false); + for (auto const& origState : origStatesWithLabel) { + newStatesWithLabel.set(ecEliminatorResult.oldToNewStateMapping[origState], true); + } + labeling.addLabel(label, std::move(newStatesWithLabel)); + } + + return std::make_shared(std::move(ecEliminatorResult.matrix), std::move(labeling), std::move(rewardModels)); +} + +} // namespace + +template +SparseParametricModelSimplifier::SparseParametricModelSimplifier(SparseModelType const& model) : originalModel(model) { + // intentionally left empty +} + +template +bool SparseParametricModelSimplifier::simplify(storm::logic::Formula const& formula) { + // Make sure that there is no old result from a previous call + simplifiedModel = nullptr; + simplifiedFormula = nullptr; + + // Go through various cases for the formula, simplify if possible, and decide if state elimination and end component elimination preserves the formula. + auto const& operatorFormula = formula.asOperatorFormula(); + STORM_LOG_THROW(!originalModel.isNondeterministicModel() || operatorFormula.hasOptimalityType() || operatorFormula.hasBound(), + storm::exceptions::InvalidPropertyException, + "The formula " << formula << " is not supported for nondeterministic models. It must either have an optimality type or a bound."); + bool const minimizing = originalModel.isNondeterministicModel() && + (operatorFormula.hasOptimalityType() ? storm::solver::minimize(operatorFormula.getOptimalityType()) + : storm::logic::isLowerBound(operatorFormula.getBound().comparisonType)); + bool enableStateElimination = false; + bool enableEndComponentElimination = false; + std::optional rewardModelName; + if (operatorFormula.isProbabilityOperatorFormula()) { + if (operatorFormula.getSubformula().isUntilFormula()) { + // GoalStateMerger merges all states violating the left subformula (if any) into the sink state, so it can safely be dropped here. Note that the + // subformula may either be an until formula (phi U psi) or a plain reachability-probability formula (F psi, i.e. implicitly true U psi). + auto eventuallyFormula = std::make_shared( + operatorFormula.getSubformula().asUntilFormula().getRightSubformula().asSharedPointer(), storm::logic::FormulaContext::Probability); + simplifiedFormula = std::make_shared(eventuallyFormula, operatorFormula.getOperatorInformation()); + enableStateElimination = true; + enableEndComponentElimination = originalModel.isNondeterministicModel() && !minimizing; // end components can only exist for Pmax queries. + } else if (operatorFormula.getSubformula().isReachabilityProbabilityFormula()) { + enableStateElimination = true; + enableEndComponentElimination = originalModel.isNondeterministicModel() && !minimizing; // end components can only exist for Pmax queries. + } else if (operatorFormula.getSubformula().isBoundedUntilFormula()) { + // multidimensional or reward bounded until formulas are not considered in this simplifier. + if (auto const& boundedUntilFormula = operatorFormula.getSubformula().asBoundedUntilFormula(); + !boundedUntilFormula.isMultiDimensional() && !boundedUntilFormula.getTimeBoundReference().isRewardBound()) { + // Since we have a discrete-time model, we may assume a step bound. + // Similar to (unbounded) until above, we can also drop the left subformula. + boost::optional lowerBound, upperBound; + if (boundedUntilFormula.hasLowerBound()) { + lowerBound.emplace(boundedUntilFormula.isLowerBoundStrict(), boundedUntilFormula.getLowerBound()); + } + if (boundedUntilFormula.hasUpperBound()) { + upperBound.emplace(boundedUntilFormula.isUpperBoundStrict(), boundedUntilFormula.getUpperBound()); + } + auto newBoundedUntilFormula = std::make_shared( + storm::logic::Formula::getTrueFormula(), boundedUntilFormula.getRightSubformula().asSharedPointer(), lowerBound, upperBound, + storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)); + simplifiedFormula = + std::make_shared(newBoundedUntilFormula, operatorFormula.getOperatorInformation()); + // neither state elimination nor end component elimination preserve step-bounded formulas. + } + } + } else if (operatorFormula.isRewardOperatorFormula()) { + if (operatorFormula.asRewardOperatorFormula().hasRewardModelName()) { + rewardModelName = operatorFormula.asRewardOperatorFormula().getRewardModelName(); + STORM_LOG_THROW(originalModel.hasRewardModel(*rewardModelName), storm::exceptions::InvalidPropertyException, + "The reward model specified by formula " << formula << " is not available in the given model."); + } else { + STORM_LOG_THROW(originalModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, + "The formula " << formula << " does not specify a reward model and the reward model is not unique."); + rewardModelName = originalModel.getUniqueRewardModelName(); + } + if (operatorFormula.getSubformula().isReachabilityRewardFormula()) { + enableStateElimination = true; + enableEndComponentElimination = originalModel.isNondeterministicModel() && minimizing; // end components can only exist for Rmin queries. + } else if (operatorFormula.getSubformula().isCumulativeRewardFormula()) { + // multidimensional or reward bounded cumulative reward formulas are not considered in this simplifier + if (auto const& cumulativeRewardFormula = operatorFormula.getSubformula().asCumulativeRewardFormula(); + !cumulativeRewardFormula.isMultiDimensional() && !cumulativeRewardFormula.getTimeBoundReference().isRewardBound()) { + // Since we have a discrete-time model, we may assume a step bound. + boost::optional rewAcc; + if (cumulativeRewardFormula.hasRewardAccumulation()) { + rewAcc = cumulativeRewardFormula.getRewardAccumulation(); + } + storm::logic::TimeBound timeBound(cumulativeRewardFormula.isBoundStrict(), cumulativeRewardFormula.getBound()); + auto newCumulativeRewardFormula = + std::make_shared(timeBound, cumulativeRewardFormula.getTimeBoundReference(), rewAcc); + simplifiedFormula = std::make_shared(newCumulativeRewardFormula, rewardModelName.value(), + operatorFormula.getOperatorInformation()); + // neither state elimination nor end component elimination preserve step-bounded formulas. + } + } + } + + // If we have not set a simplified formula yet, we do so now by taking the original formula. + if (!simplifiedFormula) { + simplifiedFormula = formula.clone(); + } + + // Perform the actual simplifications. + // First merge equivalent states based on the formula (e.g. prob0/1 states for until probabilities) + storm::transformer::GoalStateMerger goalStateMerger(originalModel); + auto mergerResult = goalStateMerger.mergeForFormula(formula, true); + if (!mergerResult) { + STORM_LOG_DEBUG("Simplification not possible because the goal state merger does not support it."); + return false; + } + simplifiedModel = mergerResult->model->template as(); + + // Next do state elimination and end component elimination. + std::string bottomLabel = ""; + if (enableEndComponentElimination) { + // Insert a bottom label *before* doing state elimination. This is so that we still know what the sink/target states are after elimination. + storm::storage::BitVector bottomStates(simplifiedModel->getNumberOfStates(), false); + if (mergerResult->targetState) { + bottomStates.set(*mergerResult->targetState, true); + } + if (mergerResult->sinkState) { + bottomStates.set(*mergerResult->sinkState, true); + } + bottomLabel = simplifiedModel->getStateLabeling().addUniqueLabel("bottom", std::move(bottomStates)); + } + if (enableStateElimination) { + // Eliminate all states for which all outgoing transitions are constant + storm::storage::BitVector considerForElimination = ~simplifiedModel->getInitialStates(); + if (mergerResult->targetState) { + considerForElimination.set(*mergerResult->targetState, false); + } + if (mergerResult->sinkState) { + considerForElimination.set(*mergerResult->sinkState, false); + } + simplifiedModel = eliminateConstantDeterministicStates(*simplifiedModel, preserveParametricTransitions, considerForElimination, rewardModelName); + } + if (enableEndComponentElimination) { + // Eliminate the end components that do not contain a target or a sink state + simplifiedModel = eliminateNeutralEndComponents(*simplifiedModel, simplifiedModel->getStates(bottomLabel), rewardModelName); + } + + return true; // simplification successful +} + +template +std::shared_ptr SparseParametricModelSimplifier::getSimplifiedModel() const { + STORM_LOG_THROW(simplifiedModel, storm::exceptions::InvalidStateException, "Tried to get the simplified model but simplification was not invoked before."); + return simplifiedModel; +} + +template +std::shared_ptr SparseParametricModelSimplifier::getSimplifiedFormula() const { + STORM_LOG_THROW(simplifiedFormula, storm::exceptions::InvalidStateException, + "Tried to get the simplified formula but simplification was not invoked before."); + return simplifiedFormula; +} + template void SparseParametricModelSimplifier::setPreserveParametricTransitions(bool preserveParametricTransitions) { this->preserveParametricTransitions = preserveParametricTransitions; diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.h b/src/storm-pars/transformer/SparseParametricModelSimplifier.h index d1ffe408b1..9ca3985b9f 100644 --- a/src/storm-pars/transformer/SparseParametricModelSimplifier.h +++ b/src/storm-pars/transformer/SparseParametricModelSimplifier.h @@ -2,6 +2,7 @@ #include #include +#include #include #include "storm/logic/Formulas.h" @@ -20,7 +21,6 @@ template class SparseParametricModelSimplifier { public: SparseParametricModelSimplifier(SparseModelType const& model); - virtual ~SparseParametricModelSimplifier() = default; /* * Invokes the simplification of the model w.r.t. the given formula. @@ -48,31 +48,11 @@ class SparseParametricModelSimplifier { void setPreserveParametricTransitions(bool preserveParametricTransitions); /** - * Whether this SparseParametricDtmcSimplifier preserves parametric transitions. + * Whether this SparseParametricModelSimplifier preserves parametric transitions. */ bool isPreserveParametricTransitionsSet() const; - protected: - // Perform the simplification for the corresponding formula type - virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula); - virtual bool simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula); - virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula); - virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula); - virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula); - - /*! - * Eliminates all states that satisfy - * * there is only one enabled action (i.e., there is no nondeterministic choice at the state), - * * all outgoing transitions are constant, - * * there is no statelabel defined, and - * * (if rewardModelName is given) the reward collected at the state is constant. - * - * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given). - * Labelings of eliminated states will be lost - */ - std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, - boost::optional const& rewardModelName = boost::none); - + private: SparseModelType const& originalModel; std::shared_ptr simplifiedModel; diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h index 26c48cba7a..3b2344622d 100644 --- a/src/storm/api/transformation.h +++ b/src/storm/api/transformation.h @@ -1,6 +1,8 @@ #pragma once +#include "storm/adapters/RationalFunctionForward.h" #include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h" +#include "storm/transformer/GoalStateMerger.h" #include "storm/transformer/NonMarkovianChainTransformer.h" #include "storm/transformer/StatePermuter.h" #include "storm/transformer/SymbolicToSparseTransformer.h" @@ -146,6 +148,28 @@ std::shared_ptr> transformToNondetermini } } +/*! + * Identifies states of the given model and formula that are equivalent and merges them into a single state, yielding a (potentially smaller) model on which the + * given formula can still be checked. + * @note depending on the formula, this merges, e.g., states with probability 0/1 or reward 0/infty based on graph-based analysis. + * @return the resulting model, or nullptr if merging is not applicable (e.g. because the model type or the formula is not supported). + */ +template +std::shared_ptr> mergeEquivalentStatesForFormula(std::shared_ptr> const& model, + storm::logic::Formula const& formula) { + // storm::transformer::GoalStateMerger is only instantiated for double, rational number, and rational function value types. + if constexpr (std::is_same_v || std::is_same_v || std::is_same_v) { + if (model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || + model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + storm::transformer::GoalStateMerger merger(*model); + if (auto result = merger.mergeForFormula(formula, false)) { + return result->model; + } + } + } + return nullptr; +} + /*! * Permutes the order of the states of the model according to the given order. * The order of the available choices at a state (of a nondeterministic model) is not changed. diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp index 3741b761b2..c19657a759 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp @@ -37,11 +37,11 @@ SparseCbQuery::SparseCbQuery(preprocessing::SparseMultiObjectiv for (auto const& obj : this->objectives) { obj.formula->gatherReferencedRewardModels(relevantRewardModels); } - storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); + storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); - preprocessedModel = mergerResult.model; + preprocessedModel = mergerResult.model->template as(); reward0EStates = rewardAnalysis.totalReward0EStates % maybeStates; if (mergerResult.targetState) { // There is an additional state in the result diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index c2c7139864..b11650f243 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -62,14 +62,14 @@ void StandardPcaaWeightVectorChecker::initialize( for (auto const& obj : this->objectives) { obj.formula->gatherReferencedRewardModels(relevantRewardModels); } - storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); + storm::transformer::GoalStateMerger merger(*preprocessorResult.preprocessedModel); auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices); goalStateMergerInputToReducedStateIndexMapping = std::move(mergerResult.oldToNewStateIndexMapping); goalStateMergerReducedToInputChoiceMapping = mergerResult.keptChoices.getNumberOfSetBitsBeforeIndices(); // Initialize data specific for the considered model type - initializeModelTypeSpecificData(*mergerResult.model); + initializeModelTypeSpecificData(*mergerResult.model->template as()); // Initilize general data of the model transitionMatrix = std::move(mergerResult.model->getTransitionMatrix()); diff --git a/src/storm/settings/modules/TransformationSettings.cpp b/src/storm/settings/modules/TransformationSettings.cpp index 8d4bb6f490..cbf8846c3b 100644 --- a/src/storm/settings/modules/TransformationSettings.cpp +++ b/src/storm/settings/modules/TransformationSettings.cpp @@ -17,6 +17,7 @@ const std::string TransformationSettings::chainEliminationOptionName = "eliminat const std::string TransformationSettings::labelBehaviorOptionName = "ec-label-behavior"; const std::string TransformationSettings::toNondetOptionName = "to-nondet"; const std::string TransformationSettings::toDiscreteTimeOptionName = "to-discrete"; +const std::string TransformationSettings::mergeEquivalentStatesOptionName = "merge-equivalent-states"; const std::string TransformationSettings::permuteModelOptionName = "permute"; TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { @@ -48,6 +49,11 @@ TransformationSettings::TransformationSettings() : ModuleSettings(moduleName) { "If set, CTMCs/MAs are converted to DTMCs/MDPs (which might or might not preserve the provided properties).") .setIsAdvanced() .build()); + this->addOption( + storm::settings::OptionBuilder(moduleName, mergeEquivalentStatesOptionName, false, + "If set, merges states that are equivalent w.r.t. the considered property into a single state before model checking.") + .setIsAdvanced() + .build()); this->addOption( storm::settings::OptionBuilder(moduleName, permuteModelOptionName, false, "Permutes the build model w.r.t. the given order.") @@ -88,6 +94,10 @@ bool TransformationSettings::isToDiscreteTimeModelSet() const { return this->getOption(toDiscreteTimeOptionName).getHasOptionBeenSet(); } +bool TransformationSettings::isMergeEquivalentStatesSet() const { + return this->getOption(mergeEquivalentStatesOptionName).getHasOptionBeenSet(); +} + std::optional TransformationSettings::getModelPermutation() const { if (this->getOption(permuteModelOptionName).getHasOptionBeenSet()) { return storm::utility::permutation::orderKindFromString(this->getOption(permuteModelOptionName).getArgumentByName("order").getValueAsString()); diff --git a/src/storm/settings/modules/TransformationSettings.h b/src/storm/settings/modules/TransformationSettings.h index 72edae40cc..240f6a74ff 100644 --- a/src/storm/settings/modules/TransformationSettings.h +++ b/src/storm/settings/modules/TransformationSettings.h @@ -48,6 +48,11 @@ class TransformationSettings : public ModuleSettings { */ bool isToDiscreteTimeModelSet() const; + /*! + * Retrieves whether the target/sink states relevant for the considered properties should be merged into single states before model checking. + */ + bool isMergeEquivalentStatesSet() const; + /*! * If the returned value is not empty, the model should be permuted according to the given order. */ @@ -71,6 +76,7 @@ class TransformationSettings : public ModuleSettings { static const std::string labelBehaviorOptionName; static const std::string toNondetOptionName; static const std::string toDiscreteTimeOptionName; + static const std::string mergeEquivalentStatesOptionName; static const std::string permuteModelOptionName; }; diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 0ca7c8d326..8107fc7233 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -2,57 +2,403 @@ #include #include +#include #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/logic/Formulas.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/DeterministicModel.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/NondeterministicModel.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/solver/OptimizationDirection.h" +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/utility/builder.h" #include "storm/utility/constants.h" +#include "storm/utility/graph.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" namespace storm { namespace transformer { -template -GoalStateMerger::GoalStateMerger(SparseModelType const& model) : originalModel(model) { - // Intentionally left empty +namespace { +// Whether the given operator formula asks for the minimizing (as opposed to maximizing) value. +bool isMinimizing(storm::logic::OperatorFormula const& formula) { + return formula.hasOptimalityType() ? storm::solver::minimize(formula.getOptimalityType()) : storm::logic::isLowerBound(formula.getBound().comparisonType); } +// Checks the given (propositional) subformula and returns the truth values vector, or std::nullopt if the subformula is not propositional. template -typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates( +std::optional const checkPropositional(storm::modelchecker::SparsePropositionalModelChecker& checker, + storm::logic::Formula const& subformula) { + if (!checker.canHandle(subformula)) { + return std::nullopt; + } + return std::move(checker.check(subformula)->template asExplicitQualitativeCheckResult().getTruthValuesVector()); +} + +std::optional representative(storm::storage::BitVector const& b) { + if (auto it = b.begin(); it != b.end()) { + return *it; + } + return std::nullopt; +} + +} // namespace + +template +GoalStateMerger::GoalStateMerger(storm::models::sparse::Model const& model) : originalModel(model) { + STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Ctmc) || + model.isOfType(storm::models::ModelType::Mdp) || model.isOfType(storm::models::ModelType::MarkovAutomaton), + storm::exceptions::NotSupportedException, "GoalStateMerger does not support models of type " << model.getType() << "."); +} + +template +typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates( storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, - std::vector const& selectedRewardModels, boost::optional const& choiceFilter) const { + std::vector const& selectedRewardModels, std::optional const& choiceFilter, + std::optional const representativeTargetState, std::optional const representativeSinkState) const { STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "Maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case."); auto result = initialize(maybeStates, targetStates, sinkStates, choiceFilter); + // Initialize model components auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second); - auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first); + auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first, representativeTargetState, representativeSinkState); auto rewardModels = buildRewardModels(maybeStates, result.first, selectedRewardModels); + storm::storage::sparse::ModelComponents modelComponents(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + + uint64_t const newStateCount = modelComponents.transitionMatrix.getRowGroupCount(); + uint64_t const newChoiceCount = modelComponents.transitionMatrix.getRowCount(); + + // Obtain model type-specific data + using enum storm::models::ModelType; + if (originalModel.isOfType(Ctmc)) { + // The transition matrix entries are rates (as opposed to probabilities that would need to be scaled by the exit rate). + modelComponents.rateTransitions = true; + } else if (originalModel.isOfType(MarkovAutomaton)) { + auto const& ma = *originalModel.template as>(); + modelComponents.markovianStates = ma.getMarkovianStates() % maybeStates; + modelComponents.markovianStates->resize(newStateCount, true); + modelComponents.exitRates = storm::utility::vector::filterVector(ma.getExitRates(), maybeStates); + modelComponents.exitRates->resize(newStateCount, storm::utility::one()); + } else { + STORM_LOG_ASSERT(originalModel.isOfType(Dtmc) || originalModel.isOfType(Mdp), "Unhandled model type: " << originalModel.getType()); + } - result.first.model = buildOutputModel(maybeStates, result.first, std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + // Reapply state valuations, choice labeling, choice origins if available + if (originalModel.hasStateValuations()) { + std::vector newToOldStateIndices = maybeStates.getNumberOfSetBitsBeforeIndices(); + if (result.first.targetState.has_value()) { + STORM_LOG_ASSERT(result.first.targetState.value() == newToOldStateIndices.size(), "unexpected position of target state."); + newToOldStateIndices.push_back(representativeTargetState.value_or(*targetStates.begin())); + } + if (result.first.sinkState.has_value()) { + STORM_LOG_ASSERT(result.first.sinkState.value() == newToOldStateIndices.size(), "unexpected position of sink state."); + newToOldStateIndices.push_back(representativeSinkState.value_or(*sinkStates.begin())); + } + modelComponents.stateValuations = originalModel.getStateValuations().selectEntities(newToOldStateIndices); + } + if (originalModel.hasChoiceLabeling()) { + modelComponents.choiceLabeling.emplace(newChoiceCount); + for (auto const& label : originalModel.getChoiceLabeling().getLabels()) { + storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label); + storm::storage::BitVector choiceLabes = originalModel.getChoiceLabeling().getChoices(label) % result.first.keptChoices; + choiceLabes.resize(newChoiceCount, false); // no label for the choice at target/sink states + modelComponents.choiceLabeling->addLabel(label, std::move(choiceLabes)); + } + } + if (originalModel.hasChoiceOrigins()) { + std::vector newToOldChoiceIndices = maybeStates.getNumberOfSetBitsBeforeIndices(); + newToOldChoiceIndices.resize(newChoiceCount, std::numeric_limits::max()); // target/sink choices will not have an origin + modelComponents.choiceOrigins = originalModel.getChoiceOrigins()->selectChoices(newToOldChoiceIndices); + } + // Finalize result + result.first.model = storm::utility::builder::buildModelFromComponents(originalModel.getType(), std::move(modelComponents)); return result.first; } -template -std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize( +template +std::optional::ReturnType> GoalStateMerger::mergeForFormula(storm::logic::Formula const& formula, + bool const dropUnreachableFromInit) const { + if (formula.isProbabilityOperatorFormula()) { + auto const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); + if (probabilityOperatorFormula.getSubformula().isUntilFormula()) { + return mergeForUntilProbabilities(probabilityOperatorFormula, dropUnreachableFromInit); + } else if (probabilityOperatorFormula.getSubformula().isEventuallyFormula()) { + return mergeForUntilProbabilities(probabilityOperatorFormula, dropUnreachableFromInit); + } else if (probabilityOperatorFormula.getSubformula().isBoundedUntilFormula()) { + return mergeForBoundedUntilProbabilities(probabilityOperatorFormula, dropUnreachableFromInit); + } + } else if (formula.isRewardOperatorFormula()) { + auto const& rewardOperatorFormula = formula.asRewardOperatorFormula(); + if (rewardOperatorFormula.getSubformula().isReachabilityRewardFormula()) { + return mergeForReachabilityRewards(rewardOperatorFormula, dropUnreachableFromInit); + } else if (rewardOperatorFormula.getSubformula().isCumulativeRewardFormula()) { + return mergeForCumulativeRewards(rewardOperatorFormula); + } + } + return std::nullopt; +} + +template +std::optional::ReturnType> GoalStateMerger::mergeForUntilProbabilities( + storm::logic::ProbabilityOperatorFormula const& formula, bool const dropUnreachableFromInit) const { + std::optional phiStates, psiStates; + if (formula.getSubformula().isUntilFormula()) { + auto const& untilFormula = formula.getSubformula().asUntilFormula(); + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(originalModel); + phiStates = checkPropositional(propositionalChecker, untilFormula.getLeftSubformula()); + psiStates = checkPropositional(propositionalChecker, untilFormula.getRightSubformula()); + } else { + STORM_LOG_ASSERT(formula.getSubformula().isEventuallyFormula(), "Unexpected formula type: " << formula.getSubformula()); + auto const eventuallyFormula = formula.getSubformula().asEventuallyFormula(); + STORM_LOG_ASSERT(eventuallyFormula.isReachabilityProbabilityFormula(), "Unexpected formula context"); + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(originalModel); + phiStates.emplace(originalModel.getNumberOfStates(), true); + psiStates = checkPropositional(propositionalChecker, eventuallyFormula.getSubformula()); + } + if (!phiStates || !psiStates) { + return std::nullopt; + } + + auto const& transitions = originalModel.getTransitionMatrix(); + storm::storage::SparseMatrix const backwardTransitions = originalModel.getBackwardTransitions(); + std::pair statesWithProbability01; + if (originalModel.isNondeterministicModel()) { + statesWithProbability01 = + isMinimizing(formula) + ? storm::utility::graph::performProb01Min(transitions, transitions.getRowGroupIndices(), backwardTransitions, *phiStates, *psiStates) + : storm::utility::graph::performProb01Max(transitions, transitions.getRowGroupIndices(), backwardTransitions, *phiStates, *psiStates); + } else { + statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, *phiStates, *psiStates); + } + + storm::storage::BitVector maybeStates; + if (dropUnreachableFromInit) { + // Only consider the maybestates that are reachable from one initial state without hopping over a target (i.e., prob1) state + storm::storage::BitVector reachableGreater0States = storm::utility::graph::getReachableStates( + transitions, originalModel.getInitialStates() & ~statesWithProbability01.first, ~statesWithProbability01.first, statesWithProbability01.second); + maybeStates = reachableGreater0States & ~statesWithProbability01.second; + } else { + // Equivalent to the above with all states considered initial: every non-prob0, non-prob1 state is a maybestate. + maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); + } + + // Ensure that we pick an actual psiState as representative for the target and an actual sink (prob0) state as representative for the sink. Note that a + // phi-violating state is not necessarily a sink state, as it might coincide with a psi (target) state, so we can not take a shortcut via phiStates here. + std::optional const representativeTarget = representative(*psiStates); + std::optional const representativeSink = representative(statesWithProbability01.first); + return mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first, std::vector(), std::nullopt, + representativeTarget, representativeSink); +} + +template +std::optional::ReturnType> GoalStateMerger::mergeForBoundedUntilProbabilities( + storm::logic::ProbabilityOperatorFormula const& formula, bool const dropUnreachableFromInit) const { + auto const& boundedUntilFormula = formula.getSubformula().asBoundedUntilFormula(); + if (boundedUntilFormula.isMultiDimensional() || boundedUntilFormula.hasLowerBound()) { + // we can not make the psiStates absorbing or we have to deal with multi-dimensionality. We don't consider these here. + return std::nullopt; + } + + std::optional upperStepBound; + if (originalModel.isDiscreteTimeModel() && boundedUntilFormula.hasUpperBound() && !boundedUntilFormula.getTimeBoundReference().isRewardBound() && + boundedUntilFormula.getUpperBound().getBaseExpression().isIntegerLiteralExpression()) { + upperStepBound = boundedUntilFormula.getUpperBound().evaluateAsInt(); + if (boundedUntilFormula.isUpperBoundStrict()) { + if (upperStepBound.value() == 0) { + // The formula has the form `phi U<0 psi`. Not a case we want to treat here. + return std::nullopt; + } + --upperStepBound.value(); + } + } + + // Get the prob0, prob1 and the maybeStates + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(originalModel); + auto phiStates = checkPropositional(propositionalChecker, boundedUntilFormula.getLeftSubformula()); + auto psiStates = checkPropositional(propositionalChecker, boundedUntilFormula.getRightSubformula()); + if (!phiStates || !psiStates) { + return std::nullopt; + } + + auto const& transitions = originalModel.getTransitionMatrix(); + storm::storage::SparseMatrix const backwardTransitions = originalModel.getBackwardTransitions(); + storm::storage::BitVector probGreater0States; + if (originalModel.isNondeterministicModel()) { + probGreater0States = isMinimizing(formula) + ? storm::utility::graph::performProbGreater0A(transitions, transitions.getRowGroupIndices(), backwardTransitions, *phiStates, + *psiStates, upperStepBound.has_value(), upperStepBound.value_or(0)) + : storm::utility::graph::performProbGreater0E(backwardTransitions, *phiStates, *psiStates, upperStepBound.has_value(), + upperStepBound.value_or(0)); + } else { + probGreater0States = + storm::utility::graph::performProbGreater0(backwardTransitions, *phiStates, *psiStates, upperStepBound.has_value(), upperStepBound.value_or(0)); + } + + storm::storage::BitVector maybeStates; + storm::storage::BitVector prob0States; + if (dropUnreachableFromInit) { + // Only consider the maybestates that are reachable from one initial probGreater0 state within the given amount of steps and without hopping over a + // target state + storm::storage::BitVector reachableGreater0States = + storm::utility::graph::getReachableStates(transitions, originalModel.getInitialStates() & probGreater0States, probGreater0States, *psiStates, + upperStepBound.has_value(), upperStepBound.value_or(0)); + maybeStates = reachableGreater0States & ~*psiStates; + prob0States = ~reachableGreater0States & ~*psiStates; + } else { + // Equivalent to the above with all states considered initial. + maybeStates = probGreater0States & ~*psiStates; + prob0States = ~probGreater0States & ~*psiStates; + } + + // For a reward-bounded formula we must preserve that reward model. + std::vector rewardModels; + if (boundedUntilFormula.getTimeBoundReference().isRewardBound()) { + auto rewName = boundedUntilFormula.getTimeBoundReference().getOptionalRewardModelName(); + if (!rewName) { + rewName = originalModel.getUniqueRewardModelName(); + } + rewardModels.push_back(rewName.value()); + } + // Ensure that we pick an actual psiState as representative for the target and an actual sink (prob0) state as representative for the sink. Note that a + // phi-violating state is not necessarily a sink state, as it might coincide with a psi (target) state, so we can not take a shortcut via phiStates here. + std::optional const representativeTarget = representative(*psiStates); + std::optional const representativeSink = representative(prob0States); + return mergeTargetAndSinkStates(maybeStates, psiStates.value(), prob0States, rewardModels, std::nullopt, representativeTarget, representativeSink); +} + +template +std::optional::ReturnType> GoalStateMerger::mergeForReachabilityRewards( + storm::logic::RewardOperatorFormula const& formula, bool const dropUnreachableFromInit) const { + auto const& originalRewardModel = + formula.hasRewardModelName() ? originalModel.getRewardModel(formula.getRewardModelName()) : originalModel.getUniqueRewardModel(); + + // Get the prob1 and the maybeStates + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(originalModel); + auto const& eventuallyFormula = formula.getSubformula().asEventuallyFormula(); + auto checkedTargetStates = checkPropositional(propositionalChecker, eventuallyFormula.getSubformula()); + if (!checkedTargetStates) { + return std::nullopt; + } + storm::storage::BitVector targetStates = std::move(*checkedTargetStates); + // we extend the target states below, so we must pick our representative here already. + auto representativeTargetState = representative(targetStates); + + auto const& transitions = originalModel.getTransitionMatrix(); + auto const backwardTransitions = originalModel.getBackwardTransitions(); + storm::storage::BitVector statesWithProb1; + if (originalModel.isNondeterministicModel()) { + // The set of target states can be extended by the states that reach target with probability 1 without collecting any reward + targetStates = + isMinimizing(formula) + ? storm::utility::graph::performProb1E(transitions, transitions.getRowGroupIndices(), backwardTransitions, + originalRewardModel.getStatesWithZeroReward(originalModel.getTransitionMatrix()), targetStates) + : storm::utility::graph::performProb1A(transitions, transitions.getRowGroupIndices(), backwardTransitions, + originalRewardModel.getStatesWithZeroReward(originalModel.getTransitionMatrix()), targetStates); + statesWithProb1 = isMinimizing(formula) + ? storm::utility::graph::performProb1E(transitions, transitions.getRowGroupIndices(), backwardTransitions, + storm::storage::BitVector(originalModel.getNumberOfStates(), true), targetStates) + : storm::utility::graph::performProb1A(transitions, transitions.getRowGroupIndices(), backwardTransitions, + storm::storage::BitVector(originalModel.getNumberOfStates(), true), targetStates); + } else { + targetStates = storm::utility::graph::performProb1(backwardTransitions, + originalRewardModel.getStatesWithZeroReward(originalModel.getTransitionMatrix()), targetStates); + statesWithProb1 = + storm::utility::graph::performProb1(backwardTransitions, storm::storage::BitVector(originalModel.getNumberOfStates(), true), targetStates); + } + storm::storage::BitVector infinityStates = ~statesWithProb1; + storm::storage::BitVector maybeStates; + if (dropUnreachableFromInit) { + // Only consider the states that are reachable from an initial state without hopping over a target state + storm::storage::BitVector reachableStates = + storm::utility::graph::getReachableStates(transitions, originalModel.getInitialStates() & statesWithProb1, statesWithProb1, targetStates); + maybeStates = reachableStates & ~targetStates; + } else { + // Equivalent to the above with all states considered initial. + maybeStates = statesWithProb1 & ~targetStates; + } + + std::vector rewardModelNameAsVector( + 1, formula.hasRewardModelName() ? formula.getRewardModelName() : originalModel.getRewardModels().begin()->first); + return mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector, std::nullopt, representativeTargetState, + representative(infinityStates)); +} + +template +std::optional::ReturnType> GoalStateMerger::mergeForCumulativeRewards( + storm::logic::RewardOperatorFormula const& formula) const { + auto const& cumulativeRewardFormula = formula.getSubformula().asCumulativeRewardFormula(); + if (cumulativeRewardFormula.isMultiDimensional()) { + return std::nullopt; // we don't handle those more sophisticated formulas here. + } + + std::optional stepBound; + if (originalModel.isDiscreteTimeModel() && !cumulativeRewardFormula.getTimeBoundReference().isRewardBound() && + cumulativeRewardFormula.getBound().getBaseExpression().isIntegerLiteralExpression()) { + stepBound = cumulativeRewardFormula.getBound().evaluateAsInt(); + if (cumulativeRewardFormula.isBoundStrict()) { + if (stepBound.value() == 0) { + return std::nullopt; // Don't treat formulas of the form C<0 here. + } + --stepBound.value(); + } + } + + auto const& originalRewardModel = + formula.hasRewardModelName() ? originalModel.getRewardModel(formula.getRewardModelName()) : originalModel.getUniqueRewardModel(); + + // Get the states for which no reward is reachable (within the step bound) + auto const& transitions = originalModel.getTransitionMatrix(); + auto const backwardTransitions = originalModel.getBackwardTransitions(); + storm::storage::BitVector maybeStates; + storm::storage::BitVector const statesWithNonZeroRewards = ~originalRewardModel.getStatesWithZeroReward(transitions); + storm::storage::BitVector const allStates(originalModel.getNumberOfStates(), true); + if (originalModel.isNondeterministicModel()) { + maybeStates = isMinimizing(formula) + ? storm::utility::graph::performProbGreater0A(transitions, transitions.getRowGroupIndices(), backwardTransitions, allStates, + statesWithNonZeroRewards, stepBound.has_value(), stepBound.value_or(0)) + : storm::utility::graph::performProbGreater0E(backwardTransitions, allStates, statesWithNonZeroRewards, stepBound.has_value(), + stepBound.value_or(0)); + } else { + maybeStates = + storm::utility::graph::performProbGreater0(backwardTransitions, allStates, statesWithNonZeroRewards, stepBound.has_value(), stepBound.value_or(0)); + } + auto const zeroExpectedRewardStates = ~maybeStates; + auto const noStates = ~allStates; + + auto rewardModels = formula.getReferencedRewardModels(); + if (originalModel.hasUniqueRewardModel()) { + rewardModels.emplace(originalModel.getUniqueRewardModelName()); + } + std::vector rewardModelNameAsVector(rewardModels.begin(), rewardModels.end()); + return mergeTargetAndSinkStates(maybeStates, noStates, zeroExpectedRewardStates, rewardModelNameAsVector, std::nullopt, std::nullopt, + representative(zeroExpectedRewardStates)); +} + +template +std::pair::ReturnType, uint64_t> GoalStateMerger::initialize( storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, - boost::optional const& choiceFilter) const { - storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); + std::optional const& choiceFilter) const { + storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); ReturnType result; result.keptChoices = storm::storage::BitVector(origMatrix.getRowCount(), false); - result.oldToNewStateIndexMapping = - std::vector(maybeStates.size(), std::numeric_limits::max()); // init with some invalid state + result.oldToNewStateIndexMapping = std::vector(maybeStates.size(), std::numeric_limits::max()); // init with some invalid state - uint_fast64_t transitionCount(0), stateCount(0); + uint64_t transitionCount(0), stateCount(0); bool targetStateRequired = !originalModel.getInitialStates().isDisjointFrom(targetStates); bool sinkStateRequired = !originalModel.getInitialStates().isDisjointFrom(sinkStates); for (auto state : maybeStates) { @@ -60,10 +406,10 @@ std::pair::ReturnType, uint_fast64_t> auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state + 1]; bool stateIsDeadlock = true; - for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { - uint_fast64_t transitionsToMaybeStates = 0; + for (uint64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { + uint64_t transitionsToMaybeStates = 0; bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false); - if (!choiceFilter || choiceFilter.get().get(row)) { + if (!choiceFilter || choiceFilter->get(row)) { for (auto const& entry : origMatrix.getRow(row)) { if (maybeStates.get(entry.getColumn())) { ++transitionsToMaybeStates; @@ -113,34 +459,34 @@ std::pair::ReturnType, uint_fast64_t> return std::make_pair(std::move(result), std::move(transitionCount)); } -template -storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix( - storm::storage::BitVector const& maybeStates, ReturnType const& resultData, uint_fast64_t transitionCount) const { - storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); +template +storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, + ReturnType const& resultData, uint64_t transitionCount) const { + storm::storage::SparseMatrix const& origMatrix = originalModel.getTransitionMatrix(); - uint_fast64_t rowCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits(); - uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - storm::storage::SparseMatrixBuilder builder( - rowCount, stateCount, transitionCount, true, !origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount); + uint64_t rowCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + uint64_t maybeStateCount = maybeStates.getNumberOfSetBits(); + uint64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + storm::storage::SparseMatrixBuilder builder(rowCount, stateCount, transitionCount, true, !origMatrix.hasTrivialRowGrouping(), + origMatrix.hasTrivialRowGrouping() ? 0 : stateCount); - uint_fast64_t currRow = 0; + uint64_t currRow = 0; for (auto state : maybeStates) { if (!origMatrix.hasTrivialRowGrouping()) { builder.newRowGroup(currRow); } auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state + 1]; - for (uint_fast64_t row = resultData.keptChoices.getNextSetIndex(origMatrix.getRowGroupIndices()[state]); row < endOfRowGroup; + for (uint64_t row = resultData.keptChoices.getNextSetIndex(origMatrix.getRowGroupIndices()[state]); row < endOfRowGroup; row = resultData.keptChoices.getNextSetIndex(row + 1)) { - boost::optional targetValue, sinkValue; + std::optional targetValue, sinkValue; for (auto const& entry : origMatrix.getRow(row)) { - uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; + uint64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; if (newColumn < maybeStateCount) { builder.addNextValue(currRow, newColumn, entry.getValue()); - } else if (resultData.targetState && newColumn == resultData.targetState.get()) { - targetValue = targetValue.is_initialized() ? *targetValue + entry.getValue() : entry.getValue(); - } else if (resultData.sinkState && newColumn == resultData.sinkState.get()) { - sinkValue = sinkValue.is_initialized() ? *sinkValue + entry.getValue() : entry.getValue(); + } else if (resultData.targetState && newColumn == resultData.targetState.value()) { + targetValue = targetValue.has_value() ? *targetValue + entry.getValue() : entry.getValue(); + } else if (resultData.sinkState && newColumn == resultData.sinkState.value()) { + sinkValue = sinkValue.has_value() ? *sinkValue + entry.getValue() : entry.getValue(); } else { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); @@ -161,36 +507,48 @@ storm::storage::SparseMatrix GoalStateMerge if (!origMatrix.hasTrivialRowGrouping()) { builder.newRowGroup(currRow); } - builder.addNextValue(currRow, *resultData.targetState, storm::utility::one()); + builder.addNextValue(currRow, *resultData.targetState, storm::utility::one()); ++currRow; } if (resultData.sinkState) { if (!origMatrix.hasTrivialRowGrouping()) { builder.newRowGroup(currRow); } - builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one()); + builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one()); ++currRow; } return builder.build(); } -template -storm::models::sparse::StateLabeling GoalStateMerger::buildStateLabeling(storm::storage::BitVector const& maybeStates, - storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& sinkStates, - ReturnType const& resultData) const { - uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); +template +storm::models::sparse::StateLabeling GoalStateMerger::buildStateLabeling(storm::storage::BitVector const& maybeStates, + storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& sinkStates, ReturnType const& resultData, + std::optional const representativeTargetState, + std::optional const representativeSinkState) const { + uint64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); storm::models::sparse::StateLabeling labeling(stateCount); for (auto const& label : originalModel.getStateLabeling().getLabels()) { storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label); storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates; newStatesWithLabel.resize(stateCount, false); - if (!oldStatesWithLabel.isDisjointFrom(targetStates) && resultData.targetState.is_initialized()) { + + // decide whether to mark the target/sink state with that label. + // There are two cases where we would do so: + // - either a representative target (or sink) state is given and contains label or + // - it is not given but one of the target (or sink) states has that label + // The init label is special: there we always assign the label if one of the targets/sinks is init. + bool const isInitialStatesLabel = label == "init"; + bool const markTarget = (representativeTargetState && !isInitialStatesLabel) ? oldStatesWithLabel.get(representativeTargetState.value()) + : !oldStatesWithLabel.isDisjointFrom(targetStates); + if (markTarget && resultData.targetState.has_value()) { newStatesWithLabel.set(*resultData.targetState, true); } - if (!oldStatesWithLabel.isDisjointFrom(sinkStates) && resultData.sinkState.is_initialized()) { + bool const markSink = (representativeSinkState && !isInitialStatesLabel) ? oldStatesWithLabel.get(representativeSinkState.value()) + : !oldStatesWithLabel.isDisjointFrom(sinkStates); + if (markSink && resultData.sinkState.has_value()) { newStatesWithLabel.set(*resultData.sinkState, true); } labeling.addLabel(label, std::move(newStatesWithLabel)); @@ -199,44 +557,42 @@ storm::models::sparse::StateLabeling GoalStateMerger::buildStat return labeling; } -template -std::unordered_map GoalStateMerger::buildRewardModels( +template +std::unordered_map> GoalStateMerger::buildRewardModels( storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector const& selectedRewardModels) const { - typedef typename SparseModelType::RewardModelType::ValueType RewardValueType; - - uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits(); - uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - uint_fast64_t choiceCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + uint64_t maybeStateCount = maybeStates.getNumberOfSetBits(); + uint64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); + uint64_t choiceCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - std::unordered_map rewardModels; + std::unordered_map> rewardModels; for (auto rewardModelName : selectedRewardModels) { auto origRewardModel = originalModel.getRewardModel(rewardModelName); - std::optional> stateRewards; + std::optional> stateRewards; if (origRewardModel.hasStateRewards()) { stateRewards = storm::utility::vector::filterVector(origRewardModel.getStateRewardVector(), maybeStates); - stateRewards->resize(stateCount, storm::utility::zero()); + stateRewards->resize(stateCount, storm::utility::zero()); } - std::optional> stateActionRewards; + std::optional> stateActionRewards; if (origRewardModel.hasStateActionRewards()) { stateActionRewards = storm::utility::vector::filterVector(origRewardModel.getStateActionRewardVector(), resultData.keptChoices); - stateActionRewards->resize(choiceCount, storm::utility::zero()); + stateActionRewards->resize(choiceCount, storm::utility::zero()); } - std::optional> transitionRewards; + std::optional> transitionRewards; if (origRewardModel.hasTransitionRewards()) { - storm::storage::SparseMatrixBuilder builder(choiceCount, stateCount, 0, true); + storm::storage::SparseMatrixBuilder builder(choiceCount, stateCount, 0, true); for (auto row : resultData.keptChoices) { - boost::optional targetValue, sinkValue; + std::optional targetValue, sinkValue; for (auto const& entry : origRewardModel.getTransitionRewardMatrix().getRow(row)) { - uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; + uint64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()]; if (newColumn < maybeStateCount) { builder.addNextValue(row, newColumn, entry.getValue()); - } else if (resultData.targetState && newColumn == resultData.targetState.get()) { - targetValue = targetValue.is_initialized() ? *targetValue + entry.getValue() : entry.getValue(); - } else if (resultData.sinkState && newColumn == resultData.sinkState.get()) { - sinkValue = sinkValue.is_initialized() ? *sinkValue + entry.getValue() : entry.getValue(); + } else if (resultData.targetState && newColumn == resultData.targetState.value()) { + targetValue = targetValue.has_value() ? *targetValue + entry.getValue() : entry.getValue(); + } else if (resultData.sinkState && newColumn == resultData.sinkState.value()) { + sinkValue = sinkValue.has_value() ? *sinkValue + entry.getValue() : entry.getValue(); } else { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition reward originating from a maybestate that does not lead to a maybe-, target-, or sinkstate."); @@ -252,62 +608,15 @@ std::unordered_map GoalS transitionRewards = builder.build(); } - rewardModels.insert(std::make_pair( - rewardModelName, typename SparseModelType::RewardModelType(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); + rewardModels.emplace(rewardModelName, models::sparse::StandardRewardModel(std::move(stateRewards), std::move(stateActionRewards), + std::move(transitionRewards))); } return rewardModels; } -template<> -std::shared_ptr> GoalStateMerger>::buildOutputModel( - storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& labeling, - std::unordered_map::RewardModelType>&& rewardModels) const { - storm::storage::sparse::ModelComponents modelComponents(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); - uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - - modelComponents.markovianStates = originalModel.getMarkovianStates() % maybeStates; - modelComponents.markovianStates->resize(stateCount, true); - - modelComponents.exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); - modelComponents.exitRates->resize(stateCount, storm::utility::one()); - - return std::make_shared>(std::move(modelComponents)); -} - -template<> -std::shared_ptr> -GoalStateMerger>::buildOutputModel( - storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& labeling, - std::unordered_map::RewardModelType>&& rewardModels) const { - storm::storage::sparse::ModelComponents modelComponents(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); - uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - - modelComponents.markovianStates = originalModel.getMarkovianStates() % maybeStates; - modelComponents.markovianStates->resize(stateCount, true); - - modelComponents.exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); - modelComponents.exitRates->resize(stateCount, storm::utility::one()); - - return std::make_shared>(std::move(modelComponents)); -} - -template -std::shared_ptr GoalStateMerger::buildOutputModel( - storm::storage::BitVector const&, GoalStateMerger::ReturnType const&, storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels) const { - return std::make_shared(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); -} - -template class GoalStateMerger>; -template class GoalStateMerger>; -template class GoalStateMerger>; -template class GoalStateMerger>; -template class GoalStateMerger>; -template class GoalStateMerger>; -template class GoalStateMerger>; -template class GoalStateMerger>; +template class GoalStateMerger; +template class GoalStateMerger; +template class GoalStateMerger; } // namespace transformer } // namespace storm diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h index 2fe803eeb5..ed749d02e5 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -1,36 +1,48 @@ #pragma once -#include +#include #include +#include +#include #include #include #include +#include "storm/models/sparse/ModelForward.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" namespace storm { +namespace logic { +class Formula; +class ProbabilityOperatorFormula; +class RewardOperatorFormula; +} // namespace logic namespace transformer { /* - * Merges the given target and sink states into single states with a selfloop + * Merges the given target and sink states into single states with a selfloop. + * Supports Dtmc, Ctmc, Mdp, and MarkovAutomaton models. */ -template +template class GoalStateMerger { public: struct ReturnType { - std::shared_ptr model; // The output model - boost::optional targetState; // The target state of the output model (if reachable) - boost::optional sinkState; // The sink state of the output model (if reachable) - std::vector oldToNewStateIndexMapping; // maps a state from the input model to the corresponding state of the output model. Invalid - // index if the state does not exist - storm::storage::BitVector keptChoices; // The choices of the input model that are still present in the output model + std::shared_ptr> model; // The output model + std::optional targetState; // The target state of the output model (if reachable) + std::optional sinkState; // The sink state of the output model (if reachable) + std::vector oldToNewStateIndexMapping; // maps a state from the input model to the corresponding state of the output model. Invalid + // index if the state does not exist + storm::storage::BitVector keptChoices; // The choices of the input model that are still present in the output model }; - GoalStateMerger(SparseModelType const& model); + /*! + * @throws storm::exceptions::NotSupportedException if the given model is not supported by this transformer. + */ + GoalStateMerger(storm::models::sparse::Model const& model); - /* Computes a submodel of the specified model that only considers the states given by maybeStates as well as + /*! Computes a submodel of the specified model that only considers the states given by maybeStates as well as * * one target state to which all transitions to a state selected by targetStates are redirected and * * one sink state to which all transitions to a state selected by sinkStates are redirected. * @@ -38,43 +50,62 @@ class GoalStateMerger { * * Notes: * * the target (or sink) state is not created, if it is not reachable - * * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label. + * * by default, the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have + * that label. If a representative target (sink) state is given, this default behaviour is overridden: the target (sink) state will then get exactly the + * labels of the representative state instead. This assumes that the provided label names are already known labels of the input model. * * Only the selected reward models will be kept. The target and sink states will not get any reward. - * * Choices that lead from a maybeState to a ~(target | sink) state will be removed. An exception is thrown if this leads to deadlocks. - * * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown. + * * Choices that lead from a maybeState to a ~(maybeState | target | sink) state will be removed. An exception is thrown if this leads to deadlocks. + * * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise, an exception is thrown. * * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model). */ ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector(), - boost::optional const& choiceFilter = boost::none) const; + std::optional const& choiceFilter = std::nullopt, + std::optional representativeTargetState = std::nullopt, + std::optional representativeSinkState = std::nullopt) const; + + /*! + * Identifies the maybeStates, targetStates, sinkStates (and, if applicable, the reward model and choice filter) that correspond to the + * given formula and invokes mergeTargetAndSinkStates accordingly. + * + * @param dropUnreachableFromInit if true, maybeStates that are not reachable from the initial states (without hopping over a target/sink state) are + * dropped. If false, this reachability analysis is skipped, i.e., the result is as if every state of the input model was an initial state. + * + * @return the result of the corresponding call to mergeTargetAndSinkStates, or std::nullopt if the given formula is not supported + * (e.g. because it has non-propositional subformulas or is not one of the supported formula types). + */ + std::optional mergeForFormula(storm::logic::Formula const& formula, bool const dropUnreachableFromInit) const; private: - SparseModelType const& originalModel; + std::optional mergeForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula, bool const dropUnreachableFromInit) const; + std::optional mergeForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula, + bool const dropUnreachableFromInit) const; + std::optional mergeForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula, bool const dropUnreachableFromInit) const; + std::optional mergeForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) const; + + storm::models::sparse::Model const& originalModel; /*! * Initializes the data required to build the result model * * @return The initialized result and the number of transitions of the result model */ - std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& sinkStates, - boost::optional const& choiceFilter = boost::none) const; + std::pair initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, + storm::storage::BitVector const& sinkStates, + std::optional const& choiceFilter = std::nullopt) const; /*! * Builds the transition matrix of the resulting model */ - storm::storage::SparseMatrix buildTransitionMatrix(storm::storage::BitVector const& maybeStates, - ReturnType const& resultData, uint_fast64_t transitionCount) const; + storm::storage::SparseMatrix buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, + uint64_t transitionCount) const; storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, - storm::storage::BitVector const& sinkStates, ReturnType const& resultData) const; - std::unordered_map buildRewardModels(storm::storage::BitVector const& maybeStates, - ReturnType const& resultData, - std::vector const& selectedRewardModels) const; - std::shared_ptr buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& labeling, - std::unordered_map&& rewardModels) const; + storm::storage::BitVector const& sinkStates, ReturnType const& resultData, + std::optional const representativeTargetState = std::nullopt, + std::optional const representativeSinkState = std::nullopt) const; + std::unordered_map> buildRewardModels( + storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector const& selectedRewardModels) const; }; } // namespace transformer } // namespace storm diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 5cc3154d78..6d89a3a5d8 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1974,6 +1974,10 @@ template storm::storage::BitVector performProb1A( template storm::storage::BitVector performProb1A( storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); +template storm::storage::BitVector performProb1A( + storm::models::sparse::NondeterministicModel> const& model, + storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, + storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb1A( storm::models::sparse::NondeterministicModel> const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, diff --git a/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp b/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp index 5ec9d78cff..6cfe3d5e26 100644 --- a/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp +++ b/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp @@ -2,7 +2,7 @@ #include "test/storm_gtest.h" #include "storm-pars/derivative/GradientDescentInstantiationSearcher.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-pars/utility/FeasibilitySynthesisTask.h" #include "storm-parsers/api/storm-parsers.h" #include "storm-parsers/parser/PrismParser.h" @@ -115,7 +115,7 @@ TYPED_TEST(GradientDescentInstantiationSearcherTest, Simple) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*formulas[0])); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); @@ -147,7 +147,7 @@ TYPED_TEST(GradientDescentInstantiationSearcherTest, Crowds) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*formulas[0])); model = simplifier.getSimplifiedModel(); diff --git a/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp b/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp index 9b80ac846f..4033358cc0 100644 --- a/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp +++ b/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp @@ -3,7 +3,7 @@ #include "storm-pars/api/storm-pars.h" #include "storm-pars/derivative/SparseDerivativeInstantiationModelChecker.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-parsers/api/storm-parsers.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/api/builder.h" @@ -172,7 +172,7 @@ TYPED_TEST(SparseDerivativeInstantiationModelCheckerTest, Simple) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); @@ -200,7 +200,7 @@ TYPED_TEST(SparseDerivativeInstantiationModelCheckerTest, Simple2) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); @@ -230,7 +230,7 @@ TYPED_TEST(SparseDerivativeInstantiationModelCheckerTest, Brp162) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp index 7bcb38dc62..3982cbd70f 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp @@ -3,7 +3,7 @@ #include "storm-pars/api/region.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -79,7 +79,7 @@ void buildMonotonicityModel(std::string const& programFile, std::string const& f if (simplifyAndBisimulate) { // Simplify model - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel()->as>(); formulas[0] = simplifier.getSimplifiedFormula(); diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp index 6e6aa753ec..2c9f8be6fd 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp @@ -9,7 +9,7 @@ #include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" #include "storm-pars/modelchecker/region/monotonicity/Order.h" #include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" #include "storm-parsers/parser/AutoParser.h" @@ -45,7 +45,7 @@ TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -119,7 +119,7 @@ TEST_F(AssumptionCheckerTest, Simple1) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); @@ -193,7 +193,7 @@ TEST_F(AssumptionCheckerTest, Casestudy1) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); @@ -268,7 +268,7 @@ TEST_F(AssumptionCheckerTest, Casestudy2) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); @@ -328,7 +328,7 @@ TEST_F(AssumptionCheckerTest, Casestudy3) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); dtmc = model->as>(); diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp index d6d68716cc..3d4b33c8c9 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp @@ -9,7 +9,7 @@ #include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" #include "storm-pars/modelchecker/region/monotonicity/Order.h" #include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" #include "storm-parsers/parser/AutoParser.h" @@ -43,7 +43,7 @@ TEST_F(AssumptionMakerTest, Brp_without_bisimulation) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); model = model->as>(); @@ -94,7 +94,7 @@ TEST_F(AssumptionMakerTest, Simple1) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -147,7 +147,7 @@ TEST_F(AssumptionMakerTest, Casestudy1) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); model = model->as>(); diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp index f435a7bde2..2b03de99e4 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp @@ -5,7 +5,7 @@ #include "storm-pars/modelchecker/region/monotonicity/MonotonicityChecker.h" #include "storm-pars/modelchecker/region/monotonicity/Order.h" #include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" #include "storm-parsers/parser/PrismParser.h" @@ -40,7 +40,7 @@ TEST_F(MonotonicityCheckerTest, Simple1_larger_region) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -89,7 +89,7 @@ TEST_F(MonotonicityCheckerTest, Simple1_small_region) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -139,7 +139,7 @@ TEST_F(MonotonicityCheckerTest, Casestudy1) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -193,7 +193,7 @@ TEST_F(MonotonicityCheckerTest, Casestudy2) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -248,7 +248,7 @@ TEST_F(MonotonicityCheckerTest, Casestudy3) { std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); std::shared_ptr> dtmc = model->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*dtmc); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp index eab67945de..7cef664cc3 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp @@ -10,7 +10,7 @@ #include "storm-pars/api/region.h" #include "storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-pars/utility/parametric.h" #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" @@ -127,7 +127,7 @@ TEST_F(MonotonicityHelperTest, Brp_with_bisimulation_no_samples) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -179,7 +179,7 @@ TEST_F(MonotonicityHelperTest, Brp_with_bisimulation_samples) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -231,7 +231,7 @@ TEST_F(MonotonicityHelperTest, zeroconf) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -282,7 +282,7 @@ TEST_F(MonotonicityHelperTest, Simple1) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); ASSERT_EQ(5ul, model->getNumberOfStates()); @@ -328,7 +328,7 @@ TEST_F(MonotonicityHelperTest, Casestudy1) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -370,7 +370,7 @@ TEST_F(MonotonicityHelperTest, CaseStudy2) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -403,7 +403,7 @@ TEST_F(MonotonicityHelperTest, Casestudy3_not_monotone) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -446,7 +446,7 @@ TEST_F(MonotonicityHelperTest, Casestudy3_monotone) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp index fa3b73dcb5..40e80adf03 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp @@ -8,7 +8,7 @@ #include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h" #include "storm-pars/modelchecker/region/monotonicity/Order.h" #include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h" -#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" +#include "storm-pars/transformer/SparseParametricModelSimplifier.h" #include "storm-parsers/api/model_descriptions.h" #include "storm-parsers/api/properties.h" #include "storm-parsers/parser/AutoParser.h" @@ -43,7 +43,7 @@ TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_model) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -92,7 +92,7 @@ TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_model) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -123,7 +123,7 @@ TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_matrix) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -177,7 +177,7 @@ TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -217,7 +217,7 @@ TEST_F(OrderExtenderTest, simple1_on_model) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -255,7 +255,7 @@ TEST_F(OrderExtenderTest, simple1_on_matrix) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -309,7 +309,7 @@ TEST_F(OrderExtenderTest, casestudy1_on_model) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -347,7 +347,7 @@ TEST_F(OrderExtenderTest, casestudy1_on_matrix) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); @@ -401,7 +401,7 @@ TEST_F(OrderExtenderTest, casestudy2_on_matrix) { storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*model); + auto simplifier = storm::transformer::SparseParametricModelSimplifier>(*model); ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); model = simplifier.getSimplifiedModel(); diff --git a/src/test/storm/transformer/GoalStateMergerTest.cpp b/src/test/storm/transformer/GoalStateMergerTest.cpp new file mode 100644 index 0000000000..c205e3082d --- /dev/null +++ b/src/test/storm/transformer/GoalStateMergerTest.cpp @@ -0,0 +1,119 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/api/storm-parsers.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/api/storm.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/transformer/GoalStateMerger.h" + +namespace { + +class GoalStateMergerTest : public ::testing::Test { + protected: + void SetUp() override { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + } +}; + +void testGoalStateMerger(std::string const& prismModelFile, std::string const& formulaString) { + storm::prism::Program program = storm::parser::PrismParser::parse(prismModelFile, true); + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program)); + auto model = storm::api::buildSparseModel(program, formulas); + auto task = storm::api::createTask(formulas.front(), false); + ASSERT_EQ(1ull, model->getInitialStates().getNumberOfSetBits()) << "For model " << prismModelFile << "."; + + auto computeValue = [&task](auto const& m) { + auto result = storm::api::verifyWithSparseEngine(m, task); + return result->template asExplicitQuantitativeCheckResult()[*m->getInitialStates().begin()]; + }; + auto const modelVal = computeValue(model); + + storm::transformer::GoalStateMerger merger(*model); + for (bool dropUnreachableFromInit : {true, false}) { + auto mergerResult = merger.mergeForFormula(*formulas.front(), dropUnreachableFromInit); + ASSERT_TRUE(mergerResult.has_value()) << "Merging goal states failed for model " << prismModelFile << " and formula " << *formulas.front() + << " (dropUnreachableFromInit=" << dropUnreachableFromInit << ")."; + ASSERT_EQ(1ull, mergerResult->model->getInitialStates().getNumberOfSetBits()) + << "For merged model of " << prismModelFile << " (dropUnreachableFromInit=" << dropUnreachableFromInit << ")."; + + // The original (unmodified) formula must still be valid on the merged model and induce the same value at the initial state. + auto const mergedVal = computeValue(mergerResult->model); + EXPECT_LE(std::abs(mergedVal - modelVal) / modelVal, 1e-6) + << "Relative difference between original model result (" << modelVal << ") and merged model result (" << mergedVal + << ") is too high.\nFailed for model " << prismModelFile << " and formula " << *formulas.front() + << " (dropUnreachableFromInit=" << dropUnreachableFromInit << ")."; + } +} + +TEST_F(GoalStateMergerTest, BrpUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm", "P=? [ true U \"target\"]"); +} + +TEST_F(GoalStateMergerTest, BrpBoundedUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm", "P=? [ true U<=100 \"target\"]"); +} + +TEST_F(GoalStateMergerTest, DieUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", "P=? [ !\"done\" U \"one\"]"); +} + +TEST_F(GoalStateMergerTest, LeaderUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", "P=? [ true U \"elected\"]"); +} + +TEST_F(GoalStateMergerTest, CrowdsUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", "P=? [ true U \"observeIGreater1\"]"); +} + +TEST_F(GoalStateMergerTest, LeaderBoundedUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", "P=? [F<=5 \"elected\"]"); +} + +TEST_F(GoalStateMergerTest, DieReachabilityRewardTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", "R=? [F \"done\"]"); +} + +TEST_F(GoalStateMergerTest, TwoDiceUntilMinTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", "Pmin=? [ true U \"two\"]"); +} + +TEST_F(GoalStateMergerTest, TwoDiceUntilMaxTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", "Pmax=? [ true U \"two\"]"); +} + +TEST_F(GoalStateMergerTest, LeaderMdpBoundedUntilMinTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", "Pmin=? [F<=25 \"elected\"]"); +} + +TEST_F(GoalStateMergerTest, LeaderMdpBoundedUntilMaxTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", "Pmax=? [F<=25 \"elected\"]"); +} + +TEST_F(GoalStateMergerTest, ChainBoundedUntilTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/chain.nm", "Pmax=? [ x<3 U<=4 x=5]"); +} + +TEST_F(GoalStateMergerTest, TinyRewardsCumulativeRewardTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", "Rmax=? [C<=2]"); +} + +TEST_F(GoalStateMergerTest, Coin22ReachabilityRewardTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Rmax=? [ F \"finished\"]"); +} + +TEST_F(GoalStateMergerTest, TandemReachabilityRewardTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm", "R=? [F \"first_queue_full\"&\"second_queue_full\"]"); +} + +TEST_F(GoalStateMergerTest, ClusterCumulativeRewardTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm", "R{\"num_repairs\"}=? [C<=200]"); +} + +TEST_F(GoalStateMergerTest, StreamReachabilityRewardTest) { + testGoalStateMerger(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma", "R{\"buffering\"}max=? [ F \"done\"]"); +} + +} // namespace From 588933cdd29c79997776a2d6beba351265a3dd54 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 14 Aug 2026 23:19:22 +0200 Subject: [PATCH 2/2] Fix unused variable. --- src/storm/transformer/GoalStateMerger.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 8107fc7233..842e596c3e 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -112,7 +112,6 @@ typename GoalStateMerger::ReturnType GoalStateMerger::merg if (originalModel.hasChoiceLabeling()) { modelComponents.choiceLabeling.emplace(newChoiceCount); for (auto const& label : originalModel.getChoiceLabeling().getLabels()) { - storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label); storm::storage::BitVector choiceLabes = originalModel.getChoiceLabeling().getChoices(label) % result.first.keptChoices; choiceLabes.resize(newChoiceCount, false); // no label for the choice at target/sink states modelComponents.choiceLabeling->addLabel(label, std::move(choiceLabes));