From 2ccf251923738e141c9d2beee6d17a44e58664cc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 7 Aug 2026 13:05:24 +0200 Subject: [PATCH 1/2] Fix for measure-driven bisimiluation partitions --- src/storm-cli-utilities/model-handling.h | 3 +- src/storm/api/bisimulation.h | 23 ++-- .../settings/modules/BisimulationSettings.cpp | 9 ++ .../settings/modules/BisimulationSettings.h | 7 + .../BisimulationDecomposition.cpp | 54 ++++++-- .../bisimulation/BisimulationDecomposition.h | 36 +++++- .../bisimulation/DeterministicBlockData.cpp | 16 +++ .../bisimulation/DeterministicBlockData.h | 14 ++ ...ministicModelBisimulationDecomposition.cpp | 18 +++ ...ministicModelBisimulationDecomposition.cpp | 57 ++++++++ ...erministicModelBisimulationDecomposition.h | 4 + src/storm/storage/bisimulation/Partition.cpp | 2 + ...sticModelBisimulationDecompositionTest.cpp | 122 ++++++++++++++++++ 13 files changed, 342 insertions(+), 23 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e1ae439c46..eb0d2cd8d6 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -700,7 +700,8 @@ std::shared_ptr> preprocessSparseModelBi } STORM_LOG_INFO("Performing bisimulation minimization..."); - return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType, graphPreserving); + return storm::api::performBisimulationMinimization(model, createFormulasToRespect(input.properties), bisimType, graphPreserving, + !bisimulationSettings.isMeasureDrivenPartitionDisabled()); } template diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h index 102612054a..a2110bdc47 100644 --- a/src/storm/api/bisimulation.h +++ b/src/storm/api/bisimulation.h @@ -16,10 +16,12 @@ namespace api { template std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, - storm::storage::BisimulationType type, bool graphPreserving = true) { + storm::storage::BisimulationType type, bool graphPreserving = true, + bool allowMeasureDrivenInitialPartition = true) { typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; if (!formulas.empty() && graphPreserving) { - options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, formulas); + options = + typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, formulas, allowMeasureDrivenInitialPartition); } // If we cannot use formula-based decomposition because of // non-graph-preserving regions but there are reward models, we need to @@ -29,6 +31,7 @@ std::shared_ptr performDeterministicSparseBisimulationMinimization(st options.setKeepRewards(true); } options.setType(type); + options.setAllowMeasureDrivenInitialPartition(allowMeasureDrivenInitialPartition); storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); @@ -38,10 +41,12 @@ std::shared_ptr performDeterministicSparseBisimulationMinimization(st template std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, - storm::storage::BisimulationType type, bool graphPreserving = true) { + storm::storage::BisimulationType type, bool graphPreserving = true, + bool allowMeasureDrivenInitialPartition = true) { typename storm::storage::NondeterministicModelBisimulationDecomposition::Options options; if (!formulas.empty() && graphPreserving) { - options = typename storm::storage::NondeterministicModelBisimulationDecomposition::Options(*model, formulas); + options = + typename storm::storage::NondeterministicModelBisimulationDecomposition::Options(*model, formulas, allowMeasureDrivenInitialPartition); } // If we cannot use formula-based decomposition because of // non-graph-preserving regions but there are reward models, we need to @@ -51,6 +56,7 @@ std::shared_ptr performNondeterministicSparseBisimulationMinimization options.setKeepRewards(true); } options.setType(type); + options.setAllowMeasureDrivenInitialPartition(allowMeasureDrivenInitialPartition); storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); @@ -60,7 +66,8 @@ std::shared_ptr performNondeterministicSparseBisimulationMinimization template std::shared_ptr> performBisimulationMinimization( std::shared_ptr> const& model, std::vector> const& formulas, - storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong, bool graphPreserving = true) { + storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong, bool graphPreserving = true, + bool allowMeasureDrivenInitialPartition = true) { STORM_LOG_THROW( model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); @@ -70,13 +77,13 @@ std::shared_ptr> performBisimulationMini if (model->isOfType(storm::models::ModelType::Dtmc)) { return performDeterministicSparseBisimulationMinimization>( - model->template as>(), formulas, type, graphPreserving); + model->template as>(), formulas, type, graphPreserving, allowMeasureDrivenInitialPartition); } else if (model->isOfType(storm::models::ModelType::Ctmc)) { return performDeterministicSparseBisimulationMinimization>( - model->template as>(), formulas, type, graphPreserving); + model->template as>(), formulas, type, graphPreserving, allowMeasureDrivenInitialPartition); } else { return performNondeterministicSparseBisimulationMinimization>( - model->template as>(), formulas, type, graphPreserving); + model->template as>(), formulas, type, graphPreserving, allowMeasureDrivenInitialPartition); } } diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp index 8698b7e5cb..75bdf5f93f 100644 --- a/src/storm/settings/modules/BisimulationSettings.cpp +++ b/src/storm/settings/modules/BisimulationSettings.cpp @@ -22,6 +22,7 @@ const std::string BisimulationSettings::reuseOptionName = "reuse"; const std::string BisimulationSettings::initialPartitionOptionName = "init"; const std::string BisimulationSettings::refinementModeOptionName = "refine"; const std::string BisimulationSettings::exactArithmeticDdOptionName = "ddexact"; +const std::string BisimulationSettings::noMeasureDrivenOptionName = "nomeasuredriven"; BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { std::vector types = {"strong", "weak"}; @@ -55,6 +56,10 @@ BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) { storm::settings::OptionBuilder(moduleName, exactArithmeticDdOptionName, false, "Sets whether to use exact arithmetic in dd-based bisimulation.") .setIsAdvanced() .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noMeasureDrivenOptionName, false, + "Disables the measure-driven initial partition for sparse bisimulation minimization.") + .setIsAdvanced() + .build()); std::vector signatureModes = {"eager", "lazy"}; this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.") @@ -173,6 +178,10 @@ BisimulationSettings::RefinementMode BisimulationSettings::getRefinementMode() c return RefinementMode::Full; } +bool BisimulationSettings::isMeasureDrivenPartitionDisabled() const { + return this->getOption(noMeasureDrivenOptionName).getHasOptionBeenSet(); +} + bool BisimulationSettings::check() const { bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet(); STORM_LOG_WARN_COND(storm::settings::getModule().isBisimulationSet() || !optionsSet, diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h index 3519b05b84..73ed1d7807 100644 --- a/src/storm/settings/modules/BisimulationSettings.h +++ b/src/storm/settings/modules/BisimulationSettings.h @@ -95,6 +95,12 @@ class BisimulationSettings : public ModuleSettings { */ RefinementMode getRefinementMode() const; + /*! + * Retrieves whether the measure-driven initial partition is disabled for (sparse) bisimulation minimization. + * NOTE: only applies to sparse-based bisimulation. + */ + bool isMeasureDrivenPartitionDisabled() const; + virtual bool check() const override; // The name of the module. @@ -112,6 +118,7 @@ class BisimulationSettings : public ModuleSettings { static const std::string refinementModeOptionName; static const std::string parallelismModeOptionName; static const std::string exactArithmeticDdOptionName; + static const std::string noMeasureDrivenOptionName; }; } // namespace modules } // namespace settings diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp index f18d33f84d..6b5f1ab868 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp @@ -29,8 +29,10 @@ BisimulationDecomposition::Options::Options(ModelType template BisimulationDecomposition::Options::Options(ModelType const& model, - std::vector> const& formulas) + std::vector> const& formulas, + bool allowMeasureDrivenInitialPartition) : Options() { + this->allowMeasureDrivenInitialPartition = allowMeasureDrivenInitialPartition; if (formulas.empty()) { this->respectedAtomicPropositions = model.getStateLabeling().getLabels(); this->keepRewards = true; @@ -129,21 +131,31 @@ void BisimulationDecomposition::Options::checkAndSetMe optimalityType = OptimizationDirection::Minimize; } } + formulaIsRewardObjective = true; newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer(); } std::shared_ptr leftSubformula = std::make_shared(true); std::shared_ptr rightSubformula; if (newFormula->isUntilFormula()) { - leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer(); - rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer(); - if (leftSubformula->isInFragment(storm::logic::propositional()) && rightSubformula->isInFragment(storm::logic::propositional())) { - measureDrivenInitialPartition = true; + // UntilFormula is only ever probability-reachability; a reward objective can't reach this point. + if (!formulaIsRewardObjective) { + leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer(); + rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer(); + if (leftSubformula->isInFragment(storm::logic::propositional()) && rightSubformula->isInFragment(storm::logic::propositional())) { + measureDrivenInitialPartition = allowMeasureDrivenInitialPartition; + } } } else if (newFormula->isEventuallyFormula()) { - rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); - if (rightSubformula->isInFragment(storm::logic::propositional())) { - measureDrivenInitialPartition = true; + storm::logic::EventuallyFormula const& eventuallyFormula = newFormula->asEventuallyFormula(); + rightSubformula = eventuallyFormula.getSubformula().asSharedPointer(); + + // Only the context matching the unwrapped operator (probability vs. reward) with default reward + // accumulation is supported by getStatesWithInfiniteReward/getStatesWithRewardZero. + bool const contextMatches = + formulaIsRewardObjective ? eventuallyFormula.isReachabilityRewardFormula() : eventuallyFormula.isReachabilityProbabilityFormula(); + if (contextMatches && !eventuallyFormula.hasRewardAccumulation() && rightSubformula->isInFragment(storm::logic::propositional())) { + measureDrivenInitialPartition = allowMeasureDrivenInitialPartition; } } @@ -355,17 +367,33 @@ void BisimulationDecomposition::initializeLabelBasedPa } template -void BisimulationDecomposition::initializeMeasureDrivenPartition() { - std::pair statesWithProbability01 = this->getStatesWithProbability01(); +storm::storage::BitVector BisimulationDecomposition::getStatesWithInfiniteReward() { + return this->getStatesWithProbability01().first; +} + +template +storm::storage::BitVector BisimulationDecomposition::getStatesWithRewardZero() { + return options.psiStates.value(); +} +template +void BisimulationDecomposition::initializeMeasureDrivenPartition() { std::optional representativePsiState; if (!options.psiStates.value().empty()) { representativePsiState = *options.psiStates.value().begin(); } - partition = storm::storage::bisimulation::Partition( - model.getNumberOfStates(), statesWithProbability01.first, - options.getBounded() || options.getKeepRewards() ? options.psiStates.value() : statesWithProbability01.second, representativePsiState); + if (options.formulaIsRewardObjective) { + // No meaningful "probability 1" counterpart for rewards; merge with the reward-zero states instead. + storm::storage::BitVector infinityStates = this->getStatesWithInfiniteReward(); + storm::storage::BitVector rewardZeroStates = this->getStatesWithRewardZero(); + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), infinityStates, rewardZeroStates, representativePsiState); + } else { + std::pair statesWithProbability01 = this->getStatesWithProbability01(); + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, + options.getBounded() ? options.psiStates.value() : statesWithProbability01.second, + representativePsiState); + } // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h index 40fef0b017..fc4f90fe84 100644 --- a/src/storm/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h @@ -65,8 +65,11 @@ class BisimulationDecomposition : public Decomposition { * @param model The model for which the quotient model shall be computed. This needs to be given in order to * derive a suitable initial partition. * @param formulas The formulas that need to be preserved. + * @param allowMeasureDrivenInitialPartition Whether a measure-driven initial partition may be used (if + * applicable for the given formulas). */ - Options(ModelType const& model, std::vector> const& formulas); + Options(ModelType const& model, std::vector> const& formulas, + bool allowMeasureDrivenInitialPartition = true); /*! * Changes the options in a way that the given formula is preserved. @@ -110,6 +113,15 @@ class BisimulationDecomposition : public Decomposition { this->keepRewards = keepRewards; } + bool getAllowMeasureDrivenInitialPartition() const { + return this->allowMeasureDrivenInitialPartition; + } + + // Disables the measure-driven initial partition even if it would otherwise be applicable. + void setAllowMeasureDrivenInitialPartition(bool value) { + this->allowMeasureDrivenInitialPartition = value; + } + bool isOptimizationDirectionSet() const { return static_cast(optimalityType); } @@ -132,6 +144,10 @@ class BisimulationDecomposition : public Decomposition { std::optional phiStates; std::optional psiStates; + // Whether optimalityType refers to a reward objective (Rmin/Rmax) rather than a probability objective + // (Pmin/Pmax). Only meaningful together with measureDrivenInitialPartition. + bool formulaIsRewardObjective = false; + /// An optional set of strings that indicate which of the atomic propositions of the model are to be /// respected and which may be ignored. If not given, all atomic propositions of the model are respected. std::optional> respectedAtomicPropositions; @@ -153,6 +169,9 @@ class BisimulationDecomposition : public Decomposition { /// when computing strong bisimulation equivalence. bool bounded; + /// Whether a measure-driven initial partition may be used (if applicable). + bool allowMeasureDrivenInitialPartition = true; + /// A flag that indicates whether discounted properties are to be preserved. This may only be set to true /// when computing strong bisimulation equivalence. bool discounted; @@ -263,6 +282,21 @@ class BisimulationDecomposition : public Decomposition { */ virtual std::pair getStatesWithProbability01() = 0; + /*! + * Computes the states with infinite expected reward until psi. Used instead of getStatesWithProbability01() + * for the measure-driven initial partition of a reward objective. Default implementation delegates to + * getStatesWithProbability01(); nondeterministic models override this (see + * NondeterministicModelBisimulationDecomposition::getStatesWithInfiniteReward). + */ + virtual storm::storage::BitVector getStatesWithInfiniteReward(); + + /*! + * Computes the states known a priori to have expected reward 0 until psi (a superset of the psi states + * themselves). Default implementation just returns the psi states; nondeterministic models can compute a + * larger set (see NondeterministicModelBisimulationDecomposition::getStatesWithRewardZero). + */ + virtual storm::storage::BitVector getStatesWithRewardZero(); + /*! * Splits the initial partition based on the (unique) reward model of the current model. */ diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.cpp b/src/storm/storage/bisimulation/DeterministicBlockData.cpp index b7e2a8e2b2..9530d6aec9 100644 --- a/src/storm/storage/bisimulation/DeterministicBlockData.cpp +++ b/src/storm/storage/bisimulation/DeterministicBlockData.cpp @@ -93,6 +93,22 @@ storm::storage::sparse::state_type DeterministicBlockData::representativeState() return valRepresentativeState.value(); } +void DeterministicBlockData::setProb0(bool value) { + setFlag(PROB0_FLAG, value); +} + +bool DeterministicBlockData::prob0() const { + return getFlag(PROB0_FLAG); +} + +void DeterministicBlockData::setProb1(bool value) { + setFlag(PROB1_FLAG, value); +} + +bool DeterministicBlockData::prob1() const { + return getFlag(PROB1_FLAG); +} + bool DeterministicBlockData::needsRefinement() const { return getFlag(REFINEMENT_FLAG); } diff --git a/src/storm/storage/bisimulation/DeterministicBlockData.h b/src/storm/storage/bisimulation/DeterministicBlockData.h index 84f274436c..860da9879b 100644 --- a/src/storm/storage/bisimulation/DeterministicBlockData.h +++ b/src/storm/storage/bisimulation/DeterministicBlockData.h @@ -65,6 +65,18 @@ class DeterministicBlockData { // Retrieves the representative state for this block. storm::storage::sparse::state_type representativeState() const; + // Sets whether this is the prob0 block of a measure-driven initial partition. + void setProb0(bool value = true); + + // Retrieves whether this is the prob0 block of a measure-driven initial partition. + bool prob0() const; + + // Sets whether this is the prob1 block of a measure-driven initial partition. + void setProb1(bool value = true); + + // Retrieves whether this is the prob1 block of a measure-driven initial partition. + bool prob1() const; + friend std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data); public: @@ -82,6 +94,8 @@ class DeterministicBlockData { static constexpr uint64_t REFINEMENT_FLAG = 1ull << 1; static constexpr uint64_t ABSORBING_FLAG = 1ull << 2; static constexpr uint64_t REWARD_FLAG = 1ull << 3; + static constexpr uint64_t PROB0_FLAG = 1ull << 4; + static constexpr uint64_t PROB1_FLAG = 1ull << 5; uint8_t flags; // An optional representative state for the block. If this is set, this state is used to derive the diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 9e2559cc2d..402b195440 100644 --- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -602,6 +602,16 @@ void DeterministicModelBisimulationDecomposition::buildQuotient() { newLabeling.addLabel(ap); } + // Mark synthetic blocks produced by a measure-driven initial partition, so they're distinguishable from + // blocks that correspond to a single original state. + bool const addMeasureDrivenLabels = this->options.measureDrivenInitialPartition; + std::string const firstBlockLabel = this->options.formulaIsRewardObjective ? "__rewinf__" : "__prob0__"; + std::string const secondBlockLabel = this->options.formulaIsRewardObjective ? "__rew0__" : "__prob1__"; + if (addMeasureDrivenLabels) { + newLabeling.addLabel(firstBlockLabel); + newLabeling.addLabel(secondBlockLabel); + } + // If the model had state rewards, we need to build the state rewards for the quotient as well. std::optional> stateRewards; if (this->options.getKeepRewards() && this->model.hasRewardModel()) { @@ -645,6 +655,14 @@ void DeterministicModelBisimulationDecomposition::buildQuotient() { newLabeling.addLabelToState(ap, blockIndex); } } + + if (addMeasureDrivenLabels) { + if (oldBlock.data().prob0()) { + newLabeling.addLabelToState(firstBlockLabel, blockIndex); + } else if (oldBlock.data().prob1()) { + newLabeling.addLabelToState(secondBlockLabel, blockIndex); + } + } } else { // Compute the outgoing transitions of the block. std::map blockProbability; diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index e70eabdda6..a76e34bcbf 100644 --- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -37,6 +37,45 @@ std::pair Nondeterministic } } +template +storm::storage::BitVector NondeterministicModelBisimulationDecomposition::getStatesWithInfiniteReward() { + STORM_LOG_THROW(this->options.isOptimizationDirectionSet(), storm::exceptions::IllegalFunctionCallException, + "Can only compute states with infinite reward with an optimization direction (min/max)."); + // Rmin is infinite iff no scheduler reaches psi a.s. (not in the existential Prob1E set); Rmax is infinite + // iff not every scheduler does (not in the universal Prob1A set) - the opposite of the reward's own + // direction. Cf. SparseMdpPrctlHelper::computeQualitativeStateSetsReachabilityRewards. + if (this->options.getOptimizationDirection() == OptimizationDirection::Minimize) { + return ~storm::utility::graph::performProb1E(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), + this->model.getBackwardTransitions(), this->options.phiStates.value(), this->options.psiStates.value()); + } else { + return ~storm::utility::graph::performProb1A(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), + this->model.getBackwardTransitions(), this->options.phiStates.value(), this->options.psiStates.value()); + } +} + +template +storm::storage::BitVector NondeterministicModelBisimulationDecomposition::getStatesWithRewardZero() { + if (!this->model.hasRewardModel()) { + return this->options.psiStates.value(); + } + STORM_LOG_THROW(this->options.isOptimizationDirectionSet(), storm::exceptions::IllegalFunctionCallException, + "Can only compute states with reward zero with an optimization direction (min/max)."); + auto const& rewardModel = this->model.getUniqueRewardModel(); + storm::storage::BitVector trueStates(this->model.getNumberOfStates(), true); + + // For Rmin: reward 0 if some scheduler reaches psi using only zero-reward choices (existential). For Rmax: + // reward 0 only if every scheduler staying within zero-reward states reaches psi (universal). + if (this->options.getOptimizationDirection() == OptimizationDirection::Minimize) { + storm::storage::BitVector zeroRewardChoices = rewardModel.getChoicesWithZeroReward(this->model.getTransitionMatrix()); + return storm::utility::graph::performProb1E(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), + this->model.getBackwardTransitions(), trueStates, this->options.psiStates.value(), zeroRewardChoices); + } else { + storm::storage::BitVector zeroRewardStates = rewardModel.getStatesWithZeroReward(this->model.getTransitionMatrix()); + return storm::utility::graph::performProb1A(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), + this->model.getBackwardTransitions(), zeroRewardStates, this->options.psiStates.value()); + } +} + template void NondeterministicModelBisimulationDecomposition::initialize() { this->createChoiceToStateMapping(); @@ -121,6 +160,16 @@ void NondeterministicModelBisimulationDecomposition::buildQuotient() newLabeling.addLabel(ap); } + // Mark synthetic blocks produced by a measure-driven initial partition, so they're distinguishable from + // blocks that correspond to a single original state. + bool const addMeasureDrivenLabels = this->options.measureDrivenInitialPartition; + std::string const firstBlockLabel = this->options.formulaIsRewardObjective ? "__rewinf__" : "__prob0__"; + std::string const secondBlockLabel = this->options.formulaIsRewardObjective ? "__rew0__" : "__prob1__"; + if (addMeasureDrivenLabels) { + newLabeling.addLabel(firstBlockLabel); + newLabeling.addLabel(secondBlockLabel); + } + // If the model had state (action) rewards, we need to build the state rewards for the quotient as well. std::optional> stateRewards; std::optional> stateActionRewards; @@ -169,6 +218,14 @@ void NondeterministicModelBisimulationDecomposition::buildQuotient() newLabeling.addLabelToState(ap, blockIndex); } } + + if (addMeasureDrivenLabels) { + if (oldBlock.data().prob0()) { + newLabeling.addLabelToState(firstBlockLabel, blockIndex); + } else if (oldBlock.data().prob1()) { + newLabeling.addLabelToState(secondBlockLabel, blockIndex); + } + } } else { // Add the outgoing choices of the block. for (uint_fast64_t choice = nondeterministicChoiceIndices[representativeState]; choice < nondeterministicChoiceIndices[representativeState + 1]; diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index 089265f353..4c124039e6 100644 --- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -31,6 +31,10 @@ class NondeterministicModelBisimulationDecomposition : public BisimulationDecomp protected: virtual std::pair getStatesWithProbability01() override; + virtual storm::storage::BitVector getStatesWithInfiniteReward() override; + + virtual storm::storage::BitVector getStatesWithRewardZero() override; + virtual void buildQuotient() override; virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, diff --git a/src/storm/storage/bisimulation/Partition.cpp b/src/storm/storage/bisimulation/Partition.cpp index 798168562c..08324cbb6a 100644 --- a/src/storm/storage/bisimulation/Partition.cpp +++ b/src/storm/storage/bisimulation/Partition.cpp @@ -40,6 +40,7 @@ Partition::Partition(std::size_t numberOfStates, storm::storage::BitVe ++position; } firstBlock->data().setAbsorbing(true); + firstBlock->data().setProb0(true); } if (!prob1States.empty()) { @@ -53,6 +54,7 @@ Partition::Partition(std::size_t numberOfStates, storm::storage::BitVe ++position; } secondBlock->data().setAbsorbing(true); + secondBlock->data().setProb1(true); secondBlock->data().setRepresentativeState(representativeProb1State.value()); } diff --git a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp index eaaa2e0365..dc1674c464 100644 --- a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -3,11 +3,52 @@ #include "storm-parsers/parser/FormulaParser.h" #include "storm-parsers/parser/PrismParser.h" +#include "storm/api/storm.h" #include "storm/builder/ExplicitModelBuilder.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" +namespace { + +// Model checks propertyString on both the original model and its bisimulation quotient; returns (ground truth, +// quotient value) for the initial state. +std::pair computeGroundTruthAndBisimulationResult(std::string const& modelFile, std::string const& propertyString) { + storm::prism::Program program = storm::parser::PrismParser::parse(modelFile); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString(propertyString); + std::vector> formulas = {formula}; + + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas); + std::shared_ptr> mdp = model->as>(); + + double groundTruth = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)) + ->template asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + + typename storm::storage::NondeterministicModelBisimulationDecomposition>::Options options(*mdp, *formula); + storm::storage::NondeterministicModelBisimulationDecomposition> bisim(*mdp, options); + bisim.computeBisimulationDecomposition(); + std::shared_ptr> quotient = bisim.getQuotient(); + + double quotientValue = storm::api::verifyWithSparseEngine(quotient, storm::api::createTask(formula, true)) + ->template asExplicitQuantitativeCheckResult()[*quotient->getInitialStates().begin()]; + + return {groundTruth, quotientValue}; +} + +// EXPECT_NEAR fails on infinities (inf - inf = NaN). Mirrors expectVectorNear in storm-dft/bdd/TestBdd.cpp. +void expectRewardNear(double expected, double actual, double precision = 1e-6) { + if (std::isinf(expected)) { + EXPECT_EQ(expected, actual); + } else { + EXPECT_NEAR(expected, actual, precision); + } +} + +} // namespace + TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; @@ -58,3 +99,84 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { EXPECT_EQ(26ul, result->getNumberOfTransitions()); EXPECT_EQ(14ul, result->as>()->getNumberOfChoices()); } + +// Regression test: measure-driven partition used to merge all probability-1 states into one block regardless of +// their (differing, finite) expected reward, turning a finite Rmin into "infinity" in the quotient. +TEST(NondeterministicModelBisimulationDecomposition, MeasureDrivenRewardUnsound) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards2.nm"); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"goal\"]"); + std::vector> formulas = {formula}; + + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas); + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + std::shared_ptr> mdp = model->as>(); + size_t initialState = *model->getInitialStates().begin(); + + // Ground truth: model check the original, unreduced model. + std::unique_ptr groundTruthCheckResult = + storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); + double groundTruthValue = groundTruthCheckResult->asExplicitQuantitativeCheckResult()[initialState]; + // Sanity check: the correct result is finite (a scheduler exists that reaches "goal" almost surely). + ASSERT_LT(groundTruthValue, storm::utility::infinity()); + + typename storm::storage::NondeterministicModelBisimulationDecomposition>::Options options(*mdp, *formula); + storm::storage::NondeterministicModelBisimulationDecomposition> bisim(*mdp, options); + ASSERT_NO_THROW(bisim.computeBisimulationDecomposition()); + std::shared_ptr> quotient; + ASSERT_NO_THROW(quotient = bisim.getQuotient()); + size_t quotientInitialState = *quotient->getInitialStates().begin(); + + std::unique_ptr quotientCheckResult = + storm::api::verifyWithSparseEngine(quotient, storm::api::createTask(formula, true)); + double quotientValue = quotientCheckResult->asExplicitQuantitativeCheckResult()[quotientInitialState]; + + // The quotient must preserve the value of the formula it was built for. + EXPECT_NEAR(groundTruthValue, quotientValue, 1e-6); +} + +// Model from https://github.com/moves-rwth/storm/issues/683: action a3 (at s=2) loops back towards "goal" (finite +// Rmin), while a4 self-loops at s=2 forever (infinite Rmax). Exercises the Prob1E/Prob1A asymmetry. +TEST(NondeterministicModelBisimulationDecomposition, TinyRewards3Issue683) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + auto [groundTruthMin, quotientMin] = computeGroundTruthAndBisimulationResult(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards3.nm", "Rmin=? [F \"goal\"]"); + ASSERT_LT(groundTruthMin, storm::utility::infinity()); + expectRewardNear(groundTruthMin, quotientMin); + + auto [groundTruthMax, quotientMax] = computeGroundTruthAndBisimulationResult(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards3.nm", "Rmax=? [F \"goal\"]"); + ASSERT_TRUE(std::isinf(groundTruthMax)); + expectRewardNear(groundTruthMax, quotientMax); +} + +// s=0 can self-loop forever ("s=0 -> true"), avoiding "target" without incurring reward. Rmax is still infinite +// by convention, even though the self-loop's own reward is 0. +TEST(NondeterministicModelBisimulationDecomposition, TinyRewardsInfinity) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + auto [groundTruthMin, quotientMin] = computeGroundTruthAndBisimulationResult(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", "Rmin=? [F \"target\"]"); + ASSERT_LT(groundTruthMin, storm::utility::infinity()); + expectRewardNear(groundTruthMin, quotientMin); + + auto [groundTruthMax, quotientMax] = computeGroundTruthAndBisimulationResult(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", "Rmax=? [F \"target\"]"); + ASSERT_TRUE(std::isinf(groundTruthMax)); + expectRewardNear(groundTruthMax, quotientMax); +} + +// Coverage on a larger, non-artificial model: "coinflips" reward on two_dice.nm (Rmin == Rmax, no nondeterminism). +TEST(NondeterministicModelBisimulationDecomposition, TwoDiceExpectedCoinFlips) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + auto [groundTruthMin, quotientMin] = computeGroundTruthAndBisimulationResult(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", "Rmin=? [F \"done\"]"); + expectRewardNear(groundTruthMin, quotientMin); + + auto [groundTruthMax, quotientMax] = computeGroundTruthAndBisimulationResult(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", "Rmax=? [F \"done\"]"); + expectRewardNear(groundTruthMax, quotientMax); +} From 92a0385eab7de48c87d9cb1c2bccbf51dd6ac9c8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 11 Aug 2026 09:44:59 +0200 Subject: [PATCH 2/2] format --- .../NondeterministicModelBisimulationDecompositionTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp index 5f1376b2c0..50402a1a2f 100644 --- a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -29,7 +29,7 @@ std::pair computeGroundTruthAndBisimulationResult(std::string co ->template asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; typename storm::storage::NondeterministicModelBisimulationDecomposition>::Options options(*mdp, *formula, - DefaultTestTolerance); + DefaultTestTolerance); storm::storage::NondeterministicModelBisimulationDecomposition> bisim(*mdp, options); bisim.computeBisimulationDecomposition(); std::shared_ptr> quotient = bisim.getQuotient(); @@ -130,7 +130,7 @@ TEST(NondeterministicModelBisimulationDecomposition, MeasureDrivenRewardUnsound) ASSERT_LT(groundTruthValue, storm::utility::infinity()); typename storm::storage::NondeterministicModelBisimulationDecomposition>::Options options(*mdp, *formula, - DefaultTestTolerance); + DefaultTestTolerance); storm::storage::NondeterministicModelBisimulationDecomposition> bisim(*mdp, options); ASSERT_NO_THROW(bisim.computeBisimulationDecomposition()); std::shared_ptr> quotient;