diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 2f46baa55..7ad0bd8ec 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -579,16 +579,18 @@ namespace storm { DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) : comparator() { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); - partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient); + BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType); + partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient); } template DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); - partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient); + BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType); + partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient); } template @@ -596,8 +598,9 @@ namespace storm { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient); + BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); } template @@ -605,8 +608,9 @@ namespace storm { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient); + BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; + Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient); } template @@ -1177,13 +1181,13 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool bounded) { std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel)); - Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel); + Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc); // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. - if (weak) { + if (bisimulationType == BisimulationType::WeakDtmc) { this->splitOffDivergentStates(model, backwardTransitions, partition); this->initializeSilentProbabilities(model, partition); } @@ -1261,8 +1265,8 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, bool weak) { - Partition partition(model.getNumberOfStates(), weak); + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType) { + Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc); for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { if (label == "init") { continue; @@ -1272,7 +1276,7 @@ namespace storm { // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. - if (weak) { + if (bisimulationType == BisimulationType::WeakDtmc) { this->splitOffDivergentStates(model, backwardTransitions, partition); this->initializeSilentProbabilities(model, partition); } diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index a14d5af1b..47d605b99 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -460,24 +460,24 @@ namespace storm { * @param backwardTransitions The backward transitions of the model. * @param phiLabel The label that all phi states carry in the model. * @param psiLabel The label that all psi states carry in the model. - * @param weak A flag indicating whether a weak bisimulation is to be computed. + * @param bisimulationType The kind of bisimulation that is to be computed. * @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded * reachability queries. * @return The resulting partition. */ template - Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded = false); + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool bounded = false); /*! * Creates the initial partition based on all the labels in the given model. * * @param model The model whose state space is partitioned based on its labels. * @param backwardTransitions The backward transitions of the model. - * @param weak A flag indicating whether a weak bisimulation is to be computed. + * @param bisimulationType The kind of bisimulation that is to be computed. * @return The resulting partition. */ template - Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, bool weak); + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, BisimulationType bisimulationType); /*! * Splits all blocks of the given partition into a block that contains all divergent states and another block