Fix for measure-driven bisim partitions

src/storm-cli-utilities/model-handling.h

@@ -702,7 +702,8 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> preprocessSparseModelBi
     std::optional<double> tolerance = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision();
 
     STORM_LOG_INFO("Performing bisimulation minimization...");
-    return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType, graphPreserving, tolerance);
+    return storm::api::performBisimulationMinimization<ValueType>(model, createFormulasToRespect(input.properties), bisimType, graphPreserving, tolerance,
+                                                                  !bisimulationSettings.isMeasureDrivenPartitionDisabled());
 }
 
 template<typename ValueType>

src/storm/api/bisimulation.h

@@ -24,7 +24,8 @@ template<typename ModelType>
 std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
                                                                               std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
                                                                               storm::storage::BisimulationType type, bool graphPreserving = true,
-                                                                              std::optional<double> const& tolerance = std::nullopt) {
+                                                                              std::optional<double> const& tolerance = std::nullopt,
+                                                                              bool allowMeasureDrivenInitialPartition = true) {
     using OptionsType = typename storm::storage::DeterministicModelBisimulationDecomposition<ModelType>::Options;
     // Falls back to the general precision setting when the caller does not deliberately choose a tolerance;
     // may be reworked to require an explicit choice throughout the API in the future.
@@ -42,6 +43,7 @@ std::shared_ptr<ModelType> performDeterministicSparseBisimulationMinimization(st
         options.setKeepRewards(true);
     }
     options.setType(type);
+    options.setAllowMeasureDrivenInitialPartition(allowMeasureDrivenInitialPartition);
 
     storm::storage::DeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
     bisimulationDecomposition.computeBisimulationDecomposition();
@@ -52,7 +54,8 @@ template<typename ModelType>
 std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization(std::shared_ptr<ModelType> model,
                                                                                  std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
                                                                                  storm::storage::BisimulationType type, bool graphPreserving = true,
-                                                                                 std::optional<double> const& tolerance = std::nullopt) {
+                                                                                 std::optional<double> const& tolerance = std::nullopt,
+                                                                                 bool allowMeasureDrivenInitialPartition = true) {
     using OptionsType = typename storm::storage::NondeterministicModelBisimulationDecomposition<ModelType>::Options;
     // Falls back to the general precision setting when the caller does not deliberately choose a tolerance;
     // may be reworked to require an explicit choice throughout the API in the future.
@@ -70,6 +73,7 @@ std::shared_ptr<ModelType> performNondeterministicSparseBisimulationMinimization
         options.setKeepRewards(true);
     }
     options.setType(type);
+    options.setAllowMeasureDrivenInitialPartition(allowMeasureDrivenInitialPartition);
 
     storm::storage::NondeterministicModelBisimulationDecomposition<ModelType> bisimulationDecomposition(*model, options);
     bisimulationDecomposition.computeBisimulationDecomposition();
@@ -80,7 +84,7 @@ template<typename ValueType>
 std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMinimization(
     std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
     storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong, bool graphPreserving = true,
-    std::optional<double> const& tolerance = std::nullopt) {
+    std::optional<double> const& tolerance = std::nullopt, 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.");
@@ -90,13 +94,13 @@ std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulationMini
 
     if (model->isOfType(storm::models::ModelType::Dtmc)) {
         return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Dtmc<ValueType>>(
-            model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type, graphPreserving, tolerance);
+            model->template as<storm::models::sparse::Dtmc<ValueType>>(), formulas, type, graphPreserving, tolerance, allowMeasureDrivenInitialPartition);
     } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
         return performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(
-            model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type, graphPreserving, tolerance);
+            model->template as<storm::models::sparse::Ctmc<ValueType>>(), formulas, type, graphPreserving, tolerance, allowMeasureDrivenInitialPartition);
     } else {
         return performNondeterministicSparseBisimulationMinimization<storm::models::sparse::Mdp<ValueType>>(
-            model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type, graphPreserving, tolerance);
+            model->template as<storm::models::sparse::Mdp<ValueType>>(), formulas, type, graphPreserving, tolerance, allowMeasureDrivenInitialPartition);
     }
 }
 

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<std::string> 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<std::string> signatureModes = {"eager", "lazy"};
     this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.")
@@ -173,6 +178,10 @@ storm::dd::bisimulation::RefinementMode BisimulationSettings::getRefinementMode(
     return storm::dd::bisimulation::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<storm::settings::modules::GeneralSettings>().isBisimulationSet() || !optionsSet,

src/storm/settings/modules/BisimulationSettings.h

@@ -92,6 +92,12 @@ class BisimulationSettings : public ModuleSettings {
      */
     storm::dd::bisimulation::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.
@@ -109,6 +115,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

src/storm/storage/bisimulation/BisimulationDecomposition.cpp

@@ -128,21 +128,31 @@ void BisimulationDecomposition<ModelType, BlockDataType>::Options::checkAndSetMe
                 optimalityType = OptimizationDirection::Minimize;
             }
         }
+        formulaIsRewardObjective = true;
         newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer();
     }
 
     std::shared_ptr<storm::logic::Formula const> leftSubformula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
     std::shared_ptr<storm::logic::Formula const> 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;
         }
     }
 
@@ -354,17 +364,33 @@ void BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPa
 }
 
 template<typename ModelType, typename BlockDataType>
-void BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition() {
-    std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
+storm::storage::BitVector BisimulationDecomposition<ModelType, BlockDataType>::getStatesWithInfiniteReward() {
+    return this->getStatesWithProbability01().first;
+}
+
+template<typename ModelType, typename BlockDataType>
+storm::storage::BitVector BisimulationDecomposition<ModelType, BlockDataType>::getStatesWithRewardZero() {
+    return options.psiStates.value();
+}
 
+template<typename ModelType, typename BlockDataType>
+void BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition() {
     std::optional<storm::storage::sparse::state_type> representativePsiState;
     if (!options.psiStates.value().empty()) {
         representativePsiState = *options.psiStates.value().begin();
     }
 
-    partition = storm::storage::bisimulation::Partition<BlockDataType>(
-        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<BlockDataType>(model.getNumberOfStates(), infinityStates, rewardZeroStates, representativePsiState);
+    } else {
+        std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
+        partition = storm::storage::bisimulation::Partition<BlockDataType>(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.

src/storm/storage/bisimulation/BisimulationDecomposition.h

@@ -98,6 +98,15 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
             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<bool>(optimalityType);
         }
@@ -122,6 +131,10 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
         std::optional<storm::storage::BitVector> phiStates;
         std::optional<storm::storage::BitVector> 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<std::set<std::string>> respectedAtomicPropositions;
@@ -143,6 +156,9 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
         /// when computing strong bisimulation equivalence.
         bool bounded = false;
 
+        /// 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 = false;
@@ -262,6 +278,21 @@ class BisimulationDecomposition : public Decomposition<StateBlock> {
      */
     virtual std::pair<storm::storage::BitVector, storm::storage::BitVector> 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.
      */

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);
 }

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