diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 1134d8904..6c8641211 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -194,6 +194,22 @@ namespace storm { return this->absorbing; } + template + void DeterministicModelBisimulationDecomposition::Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) { + this->representativeState = representativeState; + } + + template + bool DeterministicModelBisimulationDecomposition::Block::hasRepresentativeState() const { + return static_cast(representativeState); + } + + template + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getRepresentativeState() const { + STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block."); + return representativeState.get(); + } + template storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { return this->markedPosition; @@ -249,7 +265,7 @@ namespace storm { } template - DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { + DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { storm::storage::sparse::state_type position = 0; Block* firstBlock = nullptr; Block* secondBlock = nullptr; @@ -280,6 +296,7 @@ namespace storm { ++position; } secondBlock->setAbsorbing(true); + secondBlock->setRepresentativeState(representativeProb1State.get()); } storm::storage::BitVector otherStates = ~(prob0States | prob1States); @@ -577,7 +594,7 @@ namespace storm { } template - DeterministicModelBisimulationDecomposition::Options::Options(storm::logic::Formula const& formula) : Options() { + DeterministicModelBisimulationDecomposition::Options::Options(storm::models::AbstractModel const& model, storm::logic::Formula const& formula) : Options() { if (!formula.containsRewardOperator()) { this->keepRewards = false; } @@ -632,13 +649,16 @@ namespace storm { } if (measureDrivenInitialPartition) { - phiStateFormula = leftSubformula; - psiStateFormula = rightSubformula; + storm::modelchecker::SparsePropositionalModelChecker checker(model); + std::unique_ptr phiStatesCheckResult = checker.check(*leftSubformula); + std::unique_ptr psiStatesCheckResult = checker.check(*rightSubformula); + phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); } } template - DeterministicModelBisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStateFormula(), psiStateFormula(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) { + DeterministicModelBisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) { // Intentionally left empty. } @@ -658,9 +678,9 @@ namespace storm { Partition initialPartition; if (options.measureDrivenInitialPartition) { - STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded); + STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); + STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); + initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded); } else { initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); } @@ -684,9 +704,9 @@ namespace storm { Partition initialPartition; if (options.measureDrivenInitialPartition) { - STORM_LOG_THROW(options.phiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - STORM_LOG_THROW(options.psiStateFormula, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); - initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStateFormula.get(), options.psiStateFormula.get(), bisimulationType, options.keepRewards, options.bounded); + STORM_LOG_THROW(options.phiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); + STORM_LOG_THROW(options.psiStates, storm::exceptions::InvalidOptionException, "Unable to compute measure-driven initial partition without phi and psi states."); + initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, options.phiStates.get(), options.psiStates.get(), bisimulationType, options.keepRewards, options.bounded); } else { initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); } @@ -751,8 +771,13 @@ namespace storm { if (oldBlock.isAbsorbing()) { builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne()); - // Otherwise add all atomic propositions to the equivalence class that the representative state - // satisfies. + // If the block has a special representative state, we retrieve it now. + if (oldBlock.hasRepresentativeState()) { + representativeState = oldBlock.getRepresentativeState(); + } + + // Add all of the selected atomic propositions that hold in the representative state to the state + // representing the block. for (auto const& ap : atomicPropositions) { if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { newLabeling.addAtomicPropositionToState(ap, blockIndex); @@ -1264,13 +1289,15 @@ namespace storm { template template - typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::shared_ptr const& phiStateFormula, std::shared_ptr const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards, bool bounded) { - storm::modelchecker::SparsePropositionalModelChecker checker(model); - std::unique_ptr phiStates = checker.check(*phiStateFormula); - std::unique_ptr psiStates = checker.check(*psiStateFormula); + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards, bool bounded) { + std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); + + boost::optional representativePsiState; + if (!psiStates.empty()) { + representativePsiState = *psiStates.begin(); + } - std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates->asExplicitQualitativeCheckResult().getTruthValuesVector(), psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector()); - Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates->asExplicitQualitativeCheckResult().getTruthValuesVector() : statesWithProbability01.second, bisimulationType == BisimulationType::WeakDtmc); + Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? psiStates : statesWithProbability01.second, representativePsiState, bisimulationType == BisimulationType::WeakDtmc); // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 03dc4f444..255e2c22a 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -31,16 +31,18 @@ namespace storm { * Creates an object representing the options necessary to obtain the smallest quotient while still * preserving the given formula. * + * @param The model for which the quotient model shall be computed. This needs to be given in order to + * derive a suitable initial partition. * @param formula The formula that is to be preserved. */ - Options(storm::logic::Formula const& formula); + Options(storm::models::AbstractModel const& model, storm::logic::Formula const& formula); // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the // measure driven initial partition wrt. to the states phi and psi is taken. bool measureDrivenInitialPartition; - boost::optional> phiStateFormula; - boost::optional> psiStateFormula; + boost::optional phiStates; + boost::optional psiStates; // 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. @@ -201,6 +203,15 @@ namespace storm { // Retrieves whether the block is to be interpreted as absorbing. bool isAbsorbing() const; + // Sets the representative state of this block + void setRepresentativeState(storm::storage::sparse::state_type representativeState); + + // Retrieves the representative state for this block. + bool hasRepresentativeState() const; + + // Retrieves the representative state for this block. + storm::storage::sparse::state_type getRepresentativeState() const; + private: // An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks // kept by the partition. @@ -228,6 +239,10 @@ namespace storm { // The ID of the block. This is only used for debugging purposes. std::size_t id; + + // An optional representative state for the block. If this is set, this state is used to derive the + // atomic propositions of the meta state in the quotient model. + boost::optional representativeState; }; class Partition { @@ -250,9 +265,12 @@ namespace storm { * @param numberOfStates The number of states the partition holds. * @param prob0States The states which have probability 0 of satisfying phi until psi. * @param prob1States The states which have probability 1 of satisfying phi until psi. + * @param representativeProb1State If the set of prob1States is non-empty, this needs to be a state + * that is representative for this block in the sense that the state representing this block in the quotient + * model will receive exactly the atomic propositions of the representative state. * @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked. */ - Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities = false); + Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State, bool keepSilentProbabilities = false); Partition() = default; Partition(Partition const& other) = default; @@ -464,15 +482,15 @@ namespace storm { * @param model The model whose state space is partitioned based on reachability of psi states from phi * states. * @param backwardTransitions The backward transitions of the model. - * @param phiStateFormula The formula that defines the phi states in the model. - * @param psiStateFormula The formula that defines the psi states in the model. + * @param phiStates The phi states in the model. + * @param psiStates The psi states in the model. * @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::shared_ptr const& phiStateFormula, std::shared_ptr const& psiStateFormula, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false); + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false); /*! * Creates the initial partition based on all the labels in the given model. diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp index 4a8f5f143..196cde5b8 100644 --- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -36,6 +36,16 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { EXPECT_EQ(storm::models::DTMC, result->getType()); EXPECT_EQ(5, result->getNumberOfStates()); EXPECT_EQ(8, result->getNumberOfTransitions()); + + auto labelFormula = std::make_shared("one"); + auto eventuallyFormula = std::make_shared(labelFormula); + + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); + storm::storage::DeterministicModelBisimulationDecomposition bisim4(*dtmc, options2); + ASSERT_NO_THROW(result = bisim4.getQuotient()); + EXPECT_EQ(storm::models::DTMC, result->getType()); + EXPECT_EQ(5, result->getNumberOfStates()); + EXPECT_EQ(8, result->getNumberOfTransitions()); } TEST(DeterministicModelBisimulationDecomposition, Crowds) { @@ -71,4 +81,35 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { EXPECT_EQ(storm::models::DTMC, result->getType()); EXPECT_EQ(43, result->getNumberOfStates()); EXPECT_EQ(83, result->getNumberOfTransitions()); + + auto labelFormula = std::make_shared("observe0Greater1"); + auto eventuallyFormula = std::make_shared(labelFormula); + + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options2(*dtmc, *eventuallyFormula); + storm::storage::DeterministicModelBisimulationDecomposition bisim4(*dtmc, options2); + ASSERT_NO_THROW(result = bisim4.getQuotient()); + + EXPECT_EQ(storm::models::DTMC, result->getType()); + EXPECT_EQ(64, result->getNumberOfStates()); + EXPECT_EQ(104, result->getNumberOfTransitions()); + + auto probabilityOperatorFormula = std::make_shared(eventuallyFormula); + + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options3(*dtmc, *probabilityOperatorFormula); + storm::storage::DeterministicModelBisimulationDecomposition bisim5(*dtmc, options3); + ASSERT_NO_THROW(result = bisim5.getQuotient()); + + EXPECT_EQ(storm::models::DTMC, result->getType()); + EXPECT_EQ(64, result->getNumberOfStates()); + EXPECT_EQ(104, result->getNumberOfTransitions()); + + auto boundedUntilFormula = std::make_shared(std::make_shared(true), labelFormula, 50); + + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options4(*dtmc, *boundedUntilFormula); + storm::storage::DeterministicModelBisimulationDecomposition bisim6(*dtmc, options4); + ASSERT_NO_THROW(result = bisim6.getQuotient()); + + EXPECT_EQ(storm::models::DTMC, result->getType()); + EXPECT_EQ(65, result->getNumberOfStates()); + EXPECT_EQ(105, result->getNumberOfTransitions()); }