From c2a0bd5ab0338ca0eb79b5c15e2dbfd829f78885 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 5 Nov 2015 17:22:41 +0100 Subject: [PATCH] initial outline of strong MDP bisimulation Former-commit-id: 06452543eab8d40c509e84eddc6dc90ce6356167 --- .../BisimulationDecomposition.cpp | 15 +- .../bisimulation/BisimulationDecomposition.h | 13 +- ...ministicModelBisimulationDecomposition.cpp | 4 +- ...erministicModelBisimulationDecomposition.h | 5 +- ...ministicModelBisimulationDecomposition.cpp | 230 ++++++++++++++++++ ...erministicModelBisimulationDecomposition.h | 82 +++++++ 6 files changed, 341 insertions(+), 8 deletions(-) create mode 100644 src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp create mode 100644 src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 178b5a965..86ac56378 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -83,8 +83,10 @@ namespace storm { std::shared_ptr newFormula = formula.asSharedPointer(); if (formula.isProbabilityOperatorFormula()) { + optimalityType = formula.asProbabilityOperatorFormula().getOptimalityType(); newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer(); } else if (formula.isRewardOperatorFormula()) { + optimalityType = formula.asRewardOperatorFormula().getOptimalityType(); newFormula = formula.asRewardOperatorFormula().getSubformula().asSharedPointer(); } @@ -114,6 +116,8 @@ namespace storm { std::unique_ptr psiStatesCheckResult = checker.check(*rightSubformula); phiStates = phiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); psiStates = psiStatesCheckResult->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } else { + optimalityType = boost::none; } } @@ -134,7 +138,16 @@ namespace storm { } template - BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, Options const& options) : model(model), backwardTransitions(model.getBackwardTransitions()), options(options), partition(), comparator(), quotient(nullptr) { + BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, Options const& options) : BisimulationDecomposition(model, model.getBackwardTransitions(), options) { + // Intentionally left empty. + } + + template + BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Options const& options) : model(model), backwardTransitions(backwardTransitions), options(options), partition(), comparator(), quotient(nullptr) { + STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); + STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); + // Fix the respected atomic propositions if they were not explicitly given. if (!this->options.respectedAtomicPropositions) { this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels(); diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 816dc7436..280737797 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -74,6 +74,7 @@ namespace storm { bool measureDrivenInitialPartition; boost::optional phiStates; boost::optional psiStates; + boost::optional optimalityType; // 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. @@ -125,8 +126,7 @@ namespace storm { * Decomposes the given model into equivalance classes of a bisimulation. * * @param model The model to decompose. - * @param type The type of the bisimulation to compute. - * @param buildQuotient A flag specifying whether the quotient is to be build. + * @param options The options to use during for the decomposition. */ BisimulationDecomposition(ModelType const& model, Options const& options); @@ -144,6 +144,15 @@ namespace storm { void computeBisimulationDecomposition(); protected: + /*! + * Decomposes the given model into equivalance classes of a bisimulation. + * + * @param model The model to decompose. + * @param backwardTransition The backward transitions of the model. + * @param options The options to use during for the decomposition. + */ + BisimulationDecomposition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Options const& options); + /*! * Performs the partition refinement on the model and thereby computes the equivalence classes under strong * bisimulation equivalence. If required, the quotient model is built and may be retrieved using diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 5805fe15d..e3867f2de 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -29,9 +29,7 @@ namespace storm { template DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options) : BisimulationDecomposition(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero()) { - STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); - STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); - STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); + // Intentionally left empty. } template diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index b49390659..b9f2a2a5a 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -42,7 +42,8 @@ namespace storm { virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; private: - virtual void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + // Refines the predecessor blocks wrt. strong bisimulation. + void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -87,7 +88,7 @@ namespace storm { // Increases the probability of moving to the current splitter for the given state. void increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block const& predecessorBlock, ValueType const& value); - // Explores the remaining predecessors of the splitter. + // Explores the remaining states of the splitter. void exploreRemainingStatesOfSplitter(bisimulation::Block& splitter, std::list*>& predecessorBlocks); // Updates the silent probabilities of the states in the block based on the probabilities of going to the splitter. diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp new file mode 100644 index 000000000..e519e1b2f --- /dev/null +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -0,0 +1,230 @@ +#include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" + +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/utility/graph.h" + +#include "src/exceptions/IllegalFunctionCallException.h" + +namespace storm { + namespace storage { + + using namespace bisimulation; + + template + NondeterministicModelBisimulationDecomposition::NondeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options) : BisimulationDecomposition(model, model.getTransitionMatrix().transpose(false), options), choiceToStateMapping(model.getNumberOfChoices()), probabilitiesToCurrentSplitter(model.getNumberOfChoices(), storm::utility::zero()) { + STORM_LOG_THROW(options.type == BisimulationType::Strong, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation is currently not supported for nondeterministic models."); + this->createChoiceToStateMapping(); + } + + template + std::pair NondeterministicModelBisimulationDecomposition::getStatesWithProbability01() { + STORM_LOG_THROW(static_cast(this->options.optimalityType), storm::exceptions::IllegalFunctionCallException, "Can only compute states with probability 0/1 with an optimization direction (min/max)."); + if (this->options.optimalityType.get() == OptimizationDirection::Minimize) { + return storm::utility::graph::performProb01Min(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get()); + } else { + return storm::utility::graph::performProb01Max(this->model.getTransitionMatrix(), this->model.getTransitionMatrix().getRowGroupIndices(), this->model.getBackwardTransitions(), this->options.phiStates.get(), this->options.psiStates.get()); + } + } + + template + void NondeterministicModelBisimulationDecomposition::createChoiceToStateMapping() { + std::vector nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); + for (storm::storage::sparse::state_type state = 0; state < this->model.getNumberOfStates(); ++state) { + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + choiceToStateMapping[choice] = state; + } + } + } + + template + void NondeterministicModelBisimulationDecomposition::buildQuotient() { + STORM_LOG_ASSERT(false, "Not yet implemented"); + } + + template + bool NondeterministicModelBisimulationDecomposition::possiblyNeedsRefinement(bisimulation::Block const& predecessorBlock) const { + return predecessorBlock.getNumberOfStates() > 1 && !predecessorBlock.data().absorbing(); + } + + template + void NondeterministicModelBisimulationDecomposition::clearProbabilitiesToSplitter(storm::storage::sparse::state_type state) { + std::vector nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); + for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { + probabilitiesToCurrentSplitter[choice] = storm::utility::zero(); + } + } + + template + void NondeterministicModelBisimulationDecomposition::increaseProbabilityToSplitter(storm::storage::sparse::state_type state, uint_fast64_t choice, bisimulation::Block const& predecessorBlock, ValueType const& value) { + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(state); + + // If the position of the state is to the right of marker1, we have not seen it before. That means we need to + // clear the probability associated with all choices of the given state. + if (predecessorPosition >= predecessorBlock.data().marker1()) { + clearProbabilitiesToSplitter(state); + } + + // Now increase the probability of the given choice of the given state. + probabilitiesToCurrentSplitter[choice] += value; + } + + template + void NondeterministicModelBisimulationDecomposition::moveStateToMarker1(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock) { + this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().marker1())); + predecessorBlock.data().incrementMarker1(); + } + + template + void NondeterministicModelBisimulationDecomposition::moveStateToMarker2(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock) { + this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().marker2())); + predecessorBlock.data().incrementMarker2(); + } + + template + void NondeterministicModelBisimulationDecomposition::moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter, uint_fast64_t& elementsToSkip) { + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); + + // If the predecessors of the given predecessor were already explored, we can move it easily. + if (predecessorPosition <= currentPositionInSplitter + elementsToSkip) { + this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().marker1())); + predecessorBlock.data().incrementMarker1(); + } else { + // Otherwise, we need to move the predecessor, but we need to make sure that we explore its + // predecessors later. We do this by moving it to a range at the beginning of the block that will hold + // all predecessors in the splitter whose predecessors have yet to be explored. + if (predecessorBlock.data().marker2() == predecessorBlock.data().marker1()) { + this->partition.swapStatesAtPositions(predecessorBlock.data().marker2(), predecessorPosition); + this->partition.swapStatesAtPositions(predecessorPosition, currentPositionInSplitter + elementsToSkip + 1); + } else { + this->partition.swapStatesAtPositions(predecessorBlock.data().marker2(), predecessorPosition); + this->partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.data().marker1()); + this->partition.swapStatesAtPositions(predecessorPosition, currentPositionInSplitter + elementsToSkip + 1); + } + + // Since we had to move an already explored state to the right of the current position, + ++elementsToSkip; + predecessorBlock.data().incrementMarker1(); + predecessorBlock.data().incrementMarker2(); + } + } + + template + void NondeterministicModelBisimulationDecomposition::insertIntoPredecessorList(bisimulation::Block& predecessorBlock, std::list*>& predecessorBlocks) { + // Insert the block into the list of blocks to refine (if that has not already happened). + if (!predecessorBlock.data().needsRefinement()) { + predecessorBlocks.emplace_back(&predecessorBlock); + predecessorBlock.data().setNeedsRefinement(); + } + } + + template + void NondeterministicModelBisimulationDecomposition::exploreRemainingStatesOfSplitter(bisimulation::Block& splitter, std::list*>& predecessorBlocks) { + for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.begin(splitter) + (splitter.data().marker2() - splitter.getBeginIndex()); splitterIt != splitterIte; ++splitterIt) { + storm::storage::sparse::state_type currentState = *splitterIt; + + for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type choice = predecessorEntry.getColumn(); + storm::storage::sparse::state_type predecessor = choiceToStateMapping[choice]; + Block& predecessorBlock = this->partition.getBlock(predecessor); + + // If the block does not need to be refined, we skip it. + if (!possiblyNeedsRefinement(predecessorBlock)) { + continue; + } + + // We keep track of the probability of the predecessor moving to the splitter. + increaseProbabilityToSplitter(predecessor, choice, predecessorBlock, predecessorEntry.getValue()); + + // Only move the state if it has not been seen as a predecessor before. + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); + if (predecessorPosition >= predecessorBlock.data().marker1()) { + moveStateToMarker1(predecessor, predecessorBlock); + } + + insertIntoPredecessorList(predecessorBlock, predecessorBlocks); + } + } + + // Finally, we can reset the second marker. + splitter.data().setMarker2(splitter.getBeginIndex()); + } + + template + void NondeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitter(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + // TODO + } + + template + void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + // The outline of the refinement is as follows. + // + // We iterate over all states of the splitter and determine for each predecessor the state the probability + // entering the splitter. These probabilities are written to a member vector so that after the iteration + // process we have the probabilities of all predecessors of the splitter of entering the splitter in one + // step. To directly separate the states having a transition into the splitter from the ones who do not, + // we move the states to certain locations. That is, on encountering a predecessor of the splitter, it is + // moved to the beginning of its block. If the predecessor is in the splitter itself, we have to be a bit + // careful about where to move states. + // + // After this iteration, there may be states of the splitter whose predecessors have not yet been explored, + // so this needs to be done now. + // + // Finally, we use the information obtained in the first part for the actual splitting process in which all + // predecessor blocks of the splitter are split based on the probabilities computed earlier. + std::list*> predecessorBlocks; + storm::storage::sparse::state_type currentPosition = splitter.getBeginIndex(); + bool splitterIsPredecessorBlock = false; + for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt, ++currentPosition) { + storm::storage::sparse::state_type currentState = *splitterIt; + + uint_fast64_t elementsToSkip = 0; + for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type choice = predecessorEntry.getColumn(); + storm::storage::sparse::state_type predecessor = choiceToStateMapping[choice]; + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); + Block& predecessorBlock = this->partition.getBlock(predecessor); + + // If the block does not need to be refined, we skip it. + if (!possiblyNeedsRefinement(predecessorBlock)) { + continue; + } + + // We keep track of the probability of the predecessor moving to the splitter. + increaseProbabilityToSplitter(predecessor, choice, predecessorBlock, predecessorEntry.getValue()); + + // We only need to move the predecessor if its not already known as a predecessor already. + if (predecessorPosition >= predecessorBlock.data().marker1()) { + // If the predecessor block is not the splitter, we can move the state easily. + if (predecessorBlock != splitter) { + moveStateToMarker1(predecessor, predecessorBlock); + } else { + // If the predecessor is in the splitter, we need to be a bit more careful. + splitterIsPredecessorBlock = true; + moveStateInSplitter(predecessor, predecessorBlock, currentPosition, elementsToSkip); + } + + insertIntoPredecessorList(predecessorBlock, predecessorBlocks); + } + } + + // If, as a consequence of shifting states, we need to skip some elements, do so now. + splitterIt += elementsToSkip; + currentPosition += elementsToSkip; + } + + // If the splitter was a predecessor block of itself, we potentially need to explore some states that have + // not been explored yet. + if (splitterIsPredecessorBlock) { + exploreRemainingStatesOfSplitter(splitter, predecessorBlocks); + } + + // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type. + refinePredecessorBlocksOfSplitter(predecessorBlocks, splitterQueue); + } + + template class NondeterministicModelBisimulationDecomposition>; + + } +} diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h new file mode 100644 index 000000000..eb315dce6 --- /dev/null +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -0,0 +1,82 @@ +#ifndef STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ + +#include "src/storage/bisimulation/BisimulationDecomposition.h" +#include "src/storage/bisimulation/DeterministicBlockData.h" + +namespace storm { + namespace utility { + template class ConstantsComparator; + } + + namespace storage { + + /*! + * This class represents the decomposition of a nondeterministic model into its bisimulation quotient. + */ + template + class NondeterministicModelBisimulationDecomposition : public BisimulationDecomposition { + public: + typedef bisimulation::DeterministicBlockData BlockDataType; + typedef typename ModelType::ValueType ValueType; + typedef typename ModelType::RewardModelType RewardModelType; + + /*! + * Computes the bisimulation relation for the given model. Which kind of bisimulation is computed, is + * customizable via the given options. + * + * @param model The model to decompose. + * @param options The options that customize the computed bisimulation. + */ + NondeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options = typename BisimulationDecomposition::Options()); + + protected: + virtual std::pair getStatesWithProbability01() override; + + virtual void buildQuotient() override; + + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + + private: + // Creates the mapping from the choice indices to the states. + void createChoiceToStateMapping(); + + // Retrieves whether the given predecessor of the splitters possibly needs refinement. + bool possiblyNeedsRefinement(bisimulation::Block const& predecessorBlock) const; + + // Increases the probability of moving to the current splitter for the given choice of the given state. + void increaseProbabilityToSplitter(storm::storage::sparse::state_type state, uint_fast64_t choice, bisimulation::Block const& predecessorBlock, ValueType const& value); + + // Clears the probabilities of all choices of the given state. + void clearProbabilitiesToSplitter(storm::storage::sparse::state_type state); + + // Moves the given state to the position marked by marker1 moves the marker one step further. + void moveStateToMarker1(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock); + + // Moves the given state to the position marked by marker2 the marker one step further. + void moveStateToMarker2(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock); + + // Moves the given state to a proper place in the splitter, depending on where the predecessor is located. + void moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter, uint_fast64_t& elementsToSkip); + + // Inserts the block into the list of predecessors if it is not already contained. + void insertIntoPredecessorList(bisimulation::Block& predecessorBlock, std::list*>& predecessorBlocks); + + // Explores the remaining states of the splitter. + void exploreRemainingStatesOfSplitter(bisimulation::Block& splitter, std::list*>& predecessorBlocks); + + // Refines the predecessor blocks wrt. strong bisimulation. + void refinePredecessorBlocksOfSplitter(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + + // A mapping from choice indices to the state state that has this choice. + std::vector choiceToStateMapping; + + // A vector that holds the probabilities for all nondeterministic choices of all states of going into the + // splitter. This is used by the method that refines a block based on probabilities. + std::vector probabilitiesToCurrentSplitter; + + }; + } +} + +#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file