From 495230609247fda9f9a9a8dc69c35fd034471337 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 30 Jan 2015 17:43:56 +0100 Subject: [PATCH 1/8] Worked on making bisimulation decomposition a bit easier to use. Former-commit-id: 0fe6b2af6a3ebc7611e54466ab1d5c24c29fb507 --- src/exceptions/InvalidOptionException.h | 15 ++ src/logic/BinaryPathFormula.cpp | 8 + src/logic/BinaryPathFormula.h | 2 + src/logic/BinaryStateFormula.cpp | 8 + src/logic/BinaryStateFormula.h | 2 + src/logic/BoundedUntilFormula.cpp | 4 + src/logic/BoundedUntilFormula.h | 2 + src/logic/Formula.cpp | 8 + src/logic/Formula.h | 2 + src/logic/NextFormula.cpp | 4 + src/logic/NextFormula.h | 2 + src/logic/UnaryPathFormula.cpp | 8 + src/logic/UnaryPathFormula.h | 2 + src/logic/UnaryStateFormula.cpp | 8 + src/logic/UnaryStateFormula.h | 2 + src/models/AbstractModel.h | 2 +- ...ministicModelBisimulationDecomposition.cpp | 245 +++++++++++------- ...erministicModelBisimulationDecomposition.h | 106 ++++---- src/utility/cli.h | 5 +- ...sticModelBisimulationDecompositionTest.cpp | 24 +- 20 files changed, 305 insertions(+), 154 deletions(-) create mode 100644 src/exceptions/InvalidOptionException.h diff --git a/src/exceptions/InvalidOptionException.h b/src/exceptions/InvalidOptionException.h new file mode 100644 index 000000000..ec94cf8a9 --- /dev/null +++ b/src/exceptions/InvalidOptionException.h @@ -0,0 +1,15 @@ +#ifndef STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_ +#define STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(InvalidOptionException) + + } // namespace exceptions +} // namespace storm + +#endif /* STORM_EXCEPTIONS_INVALIDOPTIONEXCEPTION_H_ */ diff --git a/src/logic/BinaryPathFormula.cpp b/src/logic/BinaryPathFormula.cpp index fb2e77687..a8e30ec4c 100644 --- a/src/logic/BinaryPathFormula.cpp +++ b/src/logic/BinaryPathFormula.cpp @@ -18,6 +18,14 @@ namespace storm { return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula(); } + bool BinaryPathFormula::containsBoundedUntilFormula() const { + return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula(); + } + + bool BinaryPathFormula::containsNextFormula() const { + return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula(); + } + bool BinaryPathFormula::containsProbabilityOperator() const { return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator(); } diff --git a/src/logic/BinaryPathFormula.h b/src/logic/BinaryPathFormula.h index 8ce897168..3d9ce2a00 100644 --- a/src/logic/BinaryPathFormula.h +++ b/src/logic/BinaryPathFormula.h @@ -19,6 +19,8 @@ namespace storm { virtual bool isPctlPathFormula() const override; virtual bool isLtlFormula() const override; + virtual bool containsBoundedUntilFormula() const override; + virtual bool containsNextFormula() const override; virtual bool containsProbabilityOperator() const override; virtual bool containsNestedProbabilityOperators() const override; virtual bool containsRewardOperator() const override; diff --git a/src/logic/BinaryStateFormula.cpp b/src/logic/BinaryStateFormula.cpp index fb9a7560e..bf11df80b 100644 --- a/src/logic/BinaryStateFormula.cpp +++ b/src/logic/BinaryStateFormula.cpp @@ -18,6 +18,14 @@ namespace storm { return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula(); } + bool BinaryStateFormula::containsBoundedUntilFormula() const { + return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula(); + } + + bool BinaryStateFormula::containsNextFormula() const { + return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula(); + } + bool BinaryStateFormula::containsProbabilityOperator() const { return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator(); } diff --git a/src/logic/BinaryStateFormula.h b/src/logic/BinaryStateFormula.h index 409c5b969..075ae236a 100644 --- a/src/logic/BinaryStateFormula.h +++ b/src/logic/BinaryStateFormula.h @@ -17,6 +17,8 @@ namespace storm { virtual bool isPctlStateFormula() const override; virtual bool isLtlFormula() const override; + virtual bool containsBoundedUntilFormula() const override; + virtual bool containsNextFormula() const override; virtual bool containsProbabilityOperator() const override; virtual bool containsNestedProbabilityOperators() const override; virtual bool containsRewardOperator() const override; diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp index 3efb6af82..5c148bc1f 100644 --- a/src/logic/BoundedUntilFormula.cpp +++ b/src/logic/BoundedUntilFormula.cpp @@ -18,6 +18,10 @@ namespace storm { return true; } + bool BoundedUntilFormula::containsBoundedUntilFormula() const { + return true; + } + bool BoundedUntilFormula::isIntervalBounded() const { return bounds.which() == 1; } diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h index e79451f0f..0ed97524a 100644 --- a/src/logic/BoundedUntilFormula.h +++ b/src/logic/BoundedUntilFormula.h @@ -14,6 +14,8 @@ namespace storm { virtual bool isBoundedUntilFormula() const override; + virtual bool containsBoundedUntilFormula() const override; + bool isIntervalBounded() const; bool isIntegerUpperBounded() const; diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index 715c3f502..6cf27dfdd 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -138,6 +138,14 @@ namespace storm { return false; } + bool Formula::containsBoundedUntilFormula() const { + return false; + } + + bool Formula::containsNextFormula() const { + return false; + } + bool Formula::containsProbabilityOperator() const { return false; } diff --git a/src/logic/Formula.h b/src/logic/Formula.h index ba6dedd67..bb2e74a7c 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -83,6 +83,8 @@ namespace storm { virtual bool isPltlFormula() const; virtual bool isLtlFormula() const; virtual bool isPropositionalFormula() const; + virtual bool containsBoundedUntilFormula() const; + virtual bool containsNextFormula() const; virtual bool containsProbabilityOperator() const; virtual bool containsNestedProbabilityOperators() const; virtual bool containsRewardOperator() const; diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp index 37f4c4b3f..4bdf98d1f 100644 --- a/src/logic/NextFormula.cpp +++ b/src/logic/NextFormula.cpp @@ -10,6 +10,10 @@ namespace storm { return true; } + bool NextFormula::containsNextFormula() const { + return true; + } + std::ostream& NextFormula::writeToStream(std::ostream& out) const { out << "X "; this->getSubformula().writeToStream(out); diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h index 186f81e51..179185f48 100644 --- a/src/logic/NextFormula.h +++ b/src/logic/NextFormula.h @@ -15,6 +15,8 @@ namespace storm { virtual bool isNextFormula() const override; + virtual bool containsNextFormula() const override; + virtual std::ostream& writeToStream(std::ostream& out) const override; }; } diff --git a/src/logic/UnaryPathFormula.cpp b/src/logic/UnaryPathFormula.cpp index a30979311..d6d6dd01d 100644 --- a/src/logic/UnaryPathFormula.cpp +++ b/src/logic/UnaryPathFormula.cpp @@ -18,6 +18,14 @@ namespace storm { return this->getSubformula().isLtlFormula(); } + bool UnaryPathFormula::containsBoundedUntilFormula() const { + return this->getSubformula().containsBoundedUntilFormula(); + } + + bool UnaryPathFormula::containsNextFormula() const { + return this->getSubformula().containsNextFormula(); + } + bool UnaryPathFormula::containsProbabilityOperator() const { return this->getSubformula().containsProbabilityOperator(); } diff --git a/src/logic/UnaryPathFormula.h b/src/logic/UnaryPathFormula.h index faabd4a25..f02c7a830 100644 --- a/src/logic/UnaryPathFormula.h +++ b/src/logic/UnaryPathFormula.h @@ -19,6 +19,8 @@ namespace storm { virtual bool isPctlPathFormula() const override; virtual bool isLtlFormula() const override; + virtual bool containsBoundedUntilFormula() const override; + virtual bool containsNextFormula() const override; virtual bool containsProbabilityOperator() const override; virtual bool containsNestedProbabilityOperators() const override; virtual bool containsRewardOperator() const override; diff --git a/src/logic/UnaryStateFormula.cpp b/src/logic/UnaryStateFormula.cpp index 9dfd1286d..ab2718d69 100644 --- a/src/logic/UnaryStateFormula.cpp +++ b/src/logic/UnaryStateFormula.cpp @@ -22,6 +22,14 @@ namespace storm { return this->getSubformula().isLtlFormula(); } + bool UnaryStateFormula::containsBoundedUntilFormula() const { + return this->getSubformula().containsBoundedUntilFormula(); + } + + bool UnaryStateFormula::containsNextFormula() const { + return this->getSubformula().containsNextFormula(); + } + bool UnaryStateFormula::containsProbabilityOperator() const { return getSubformula().containsProbabilityOperator(); } diff --git a/src/logic/UnaryStateFormula.h b/src/logic/UnaryStateFormula.h index cac202275..f604262e8 100644 --- a/src/logic/UnaryStateFormula.h +++ b/src/logic/UnaryStateFormula.h @@ -18,6 +18,8 @@ namespace storm { virtual bool isPropositionalFormula() const override; virtual bool isPctlStateFormula() const override; virtual bool isLtlFormula() const override; + virtual bool containsBoundedUntilFormula() const override; + virtual bool containsNextFormula() const override; virtual bool containsProbabilityOperator() const override; virtual bool containsNestedProbabilityOperators() const override; virtual bool containsRewardOperator() const override; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 958f248aa..c6c2e7e3d 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -340,7 +340,7 @@ class AbstractModel: public std::enable_shared_from_this> { } else { this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get()); } - this->transitionRewardMatrix.reset(); + this->transitionRewardMatrix = boost::optional>(); } /*! diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 8455825f2..1134d8904 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -6,14 +6,18 @@ #include #include +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" + #include "src/utility/graph.h" #include "src/exceptions/IllegalFunctionCallException.h" +#include "src/exceptions/InvalidOptionException.h" namespace storm { namespace storage { template - DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id), label(label) { + DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id) { if (next != nullptr) { next->prev = this; } @@ -130,12 +134,12 @@ namespace storm { typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { return this->prev; } - + template typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { return this->next; } - + template typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { return *this->prev; @@ -169,12 +173,12 @@ namespace storm { void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { this->markedAsSplitter = true; } - + template void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { this->markedAsSplitter = false; } - + template std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { return this->id; @@ -225,22 +229,6 @@ namespace storm { return markedAsPredecessorBlock; } - template - bool DeterministicModelBisimulationDecomposition::Block::hasLabel() const { - return this->label != nullptr; - } - - template - std::string const& DeterministicModelBisimulationDecomposition::Block::getLabel() const { - STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none."); - return *this->label; - } - - template - std::shared_ptr const& DeterministicModelBisimulationDecomposition::Block::getLabelPtr() const { - return this->label; - } - template DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { // Create the block and give it an iterator to itself. @@ -261,7 +249,7 @@ namespace storm { } template - DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, 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, 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; @@ -270,7 +258,7 @@ namespace storm { typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++); firstBlock = &(*firstIt); firstBlock->setIterator(firstIt); - + for (auto state : prob0States) { statesAndValues[position] = std::make_pair(state, storm::utility::zero()); positions[state] = position; @@ -279,9 +267,9 @@ namespace storm { } firstBlock->setAbsorbing(true); } - + if (!prob1States.empty()) { - typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++, std::shared_ptr(new std::string(prob1Label))); + typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++); secondBlock = &(*secondIt); secondBlock->setIterator(secondIt); @@ -296,7 +284,7 @@ namespace storm { storm::storage::BitVector otherStates = ~(prob0States | prob1States); if (!otherStates.empty()) { - typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); + typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++); thirdBlock = &(*thirdIt); thirdBlock->setIterator(thirdIt); @@ -319,7 +307,7 @@ namespace storm { std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]); std::swap(this->positions[state1], this->positions[state2]); } - + template void DeterministicModelBisimulationDecomposition::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first; @@ -365,7 +353,7 @@ namespace storm { void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { this->statesAndValues[this->positions[state]].second += value; } - + template void DeterministicModelBisimulationDecomposition::Partition::updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last) { for (; first != last; ++first) { @@ -382,12 +370,12 @@ namespace storm { typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { return *this->stateToBlockMapping[state]; } - + template typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { return *this->stateToBlockMapping[state]; } - + template typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) { return this->statesAndValues.begin() + block.getBegin(); @@ -397,7 +385,7 @@ namespace storm { typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) { return this->statesAndValues.begin() + block.getEnd(); } - + template typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) const { return this->statesAndValues.begin() + block.getBegin(); @@ -417,7 +405,7 @@ namespace storm { } // Actually create the new block and insert it at the correct position. - typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, numberOfBlocks++, block.getLabelPtr()); + typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, numberOfBlocks++); selfIt->setIterator(selfIt); Block& newBlock = *selfIt; @@ -589,41 +577,121 @@ namespace storm { } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) : comparator() { - STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards); - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards, buildQuotient); + DeterministicModelBisimulationDecomposition::Options::Options(storm::logic::Formula const& formula) : Options() { + if (!formula.containsRewardOperator()) { + this->keepRewards = false; + } + + // As a tradeoff, we compute a strong bisimulation, because that is typically much faster. If the number of + // states is to be minimized, this should be set to weak by the calling site. + weak = false; + + // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula. + bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula(); + + std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); + std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); + + std::set labelsToRespect; + for (auto const& labelFormula : atomicLabelFormulas) { + labelsToRespect.insert(labelFormula->getLabel()); + } + for (auto const& expressionFormula : atomicExpressionFormulas) { + std::stringstream stream; + stream << expressionFormula; + labelsToRespect.insert(stream.str()); + } + respectedAtomicPropositions = labelsToRespect; + + std::shared_ptr newFormula = formula.asSharedPointer(); + + if (formula.isProbabilityOperatorFormula()) { + newFormula = formula.asProbabilityOperatorFormula().getSubformula().asSharedPointer(); + } else if (formula.isRewardOperatorFormula()) { + 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->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) { + measureDrivenInitialPartition = true; + } + } else if (newFormula->isEventuallyFormula()) { + rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); + if (rightSubformula->isPropositionalFormula()) { + measureDrivenInitialPartition = true; + } + } else if (newFormula->isReachabilityRewardFormula()) { + rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); + if (rightSubformula->isPropositionalFormula()) { + measureDrivenInitialPartition = true; + } + } + + if (measureDrivenInitialPartition) { + phiStateFormula = leftSubformula; + psiStateFormula = rightSubformula; + } } - + template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions, bool keepRewards, bool weak, bool buildQuotient) { - STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; - Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, keepRewards); - partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, keepRewards,buildQuotient); + DeterministicModelBisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStateFormula(), psiStateFormula(), respectedAtomicPropositions(), keepRewards(true), weak(false), bounded(true), buildQuotient(true) { + // Intentionally left empty. } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) { - STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); - STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, Options const& options) { + STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded); - partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient); + BisimulationType bisimulationType = options.weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; + + std::set atomicPropositions; + if (options.respectedAtomicPropositions) { + atomicPropositions = options.respectedAtomicPropositions.get(); + } else { + atomicPropositions = model.getStateLabeling().getAtomicPropositions(); + } + + 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); + } else { + initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); + } + + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient); } template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient) { - STORM_LOG_THROW(!keepRewards || !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards."); - STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties."); + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, Options const& options) { + STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without transition rewards. Consider converting the transition rewards to state rewards (via suitable function calls)."); + STORM_LOG_THROW(!options.weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, keepRewards, bounded); - partitionRefinement(model, std::set({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, keepRewards, buildQuotient); + BisimulationType bisimulationType = options.weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; + + std::set atomicPropositions; + if (options.respectedAtomicPropositions) { + atomicPropositions = options.respectedAtomicPropositions.get(); + } else { + atomicPropositions = model.getStateLabeling().getAtomicPropositions(); + } + + 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); + } else { + initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions, options.keepRewards); + } + + partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, options.keepRewards, options.buildQuotient); } template @@ -683,15 +751,11 @@ namespace storm { if (oldBlock.isAbsorbing()) { builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne()); - if (oldBlock.hasLabel()) { - newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex); - } else { - // Otherwise add all atomic propositions to the equivalence class that the representative state - // satisfies. - for (auto const& ap : atomicPropositions) { - if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { - newLabeling.addAtomicPropositionToState(ap, blockIndex); - } + // Otherwise add all atomic propositions to the equivalence class that the representative state + // satisfies. + for (auto const& ap : atomicPropositions) { + if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { + newLabeling.addAtomicPropositionToState(ap, blockIndex); } } } else { @@ -722,16 +786,11 @@ namespace storm { } } - // If the block has a special label, we only add that to the block. - if (oldBlock.hasLabel()) { - newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex); - } else { - // Otherwise add all atomic propositions to the equivalence class that the representative state - // satisfies. - for (auto const& ap : atomicPropositions) { - if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { - newLabeling.addAtomicPropositionToState(ap, blockIndex); - } + // Otherwise add all atomic propositions to the equivalence class that the representative state + // satisfies. + for (auto const& ap : atomicPropositions) { + if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { + newLabeling.addAtomicPropositionToState(ap, blockIndex); } } } @@ -757,17 +816,17 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); - + // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now(); std::deque splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); }); - + // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters). std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - + // Get and prepare the next splitter. Block* splitter = splitterQueue.front(); splitterQueue.pop_front(); @@ -777,7 +836,7 @@ namespace storm { refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue); } std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; - + // Now move the states from the internal partition into their final place in the decomposition. We do so in // a way that maintains the block IDs as indices. std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now(); @@ -790,12 +849,12 @@ namespace storm { std::function const&)> projection = [](std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), projection), boost::make_transform_iterator(partition.getEnd(block), projection), true); } - + // If we are required to build the quotient model, do so now. if (buildQuotient) { this->buildQuotient(model, atomicPropositions, partition, bisimulationType, keepRewards); } - + std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; @@ -1007,7 +1066,7 @@ namespace storm { typename std::vector>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1; storm::storage::sparse::state_type currentIndex = block.getOriginalBegin(); result.push_back(currentIndex); - + // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. while (!comparator.isEqual(begin->second, end->second)) { @@ -1022,7 +1081,7 @@ namespace storm { ++begin; ++currentIndex; } - + // Remember the index at which the probabilities were different. result.push_back(currentIndex); } @@ -1115,7 +1174,7 @@ namespace storm { storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); Block& predecessorBlock = partition.getBlock(predecessor); storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); - + if (predecessorPosition >= predecessorBlock.getBegin()) { partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); predecessorBlock.incrementBegin(); @@ -1130,7 +1189,7 @@ namespace storm { } } } - + if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) { std::list blocksToSplit; @@ -1181,7 +1240,7 @@ namespace storm { partition.setSilentProbabilities(partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), partition.getStatesAndValues().begin() + splitter.getBegin()); partition.setSilentProbabilitiesToZero(partition.getStatesAndValues().begin() + splitter.getBegin(), partition.getStatesAndValues().begin() + splitter.getEnd()); } - + // Now refine all predecessor blocks in a weak manner. That is, we split according to the criterion of // weak bisimulation. for (auto blockPtr : predecessorBlocks) { @@ -1194,7 +1253,7 @@ namespace storm { // Restore the begin of the block. block.setBegin(block.getOriginalBegin()); } - + block.unmarkAsPredecessorBlock(); block.resetMarkedPosition(); } @@ -1205,9 +1264,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, BisimulationType bisimulationType, bool keepRewards, 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 || keepRewards ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc); + 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); + + 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); // 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 3fb4331fd..03dc4f444 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -6,6 +6,7 @@ #include "src/storage/sparse/StateType.h" #include "src/storage/Decomposition.h" +#include "src/logic/Formulas.h" #include "src/models/Dtmc.h" #include "src/models/Ctmc.h" #include "src/storage/Distribution.h" @@ -21,53 +22,62 @@ namespace storm { template class DeterministicModelBisimulationDecomposition : public Decomposition { public: - /*! - * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. - * - * @param model The model to decompose. - * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the - * model will be respected. If built, the quotient model will only contain the respected atomic propositions. - * @param weak A flag indication whether a weak bisimulation is to be computed. - * @param buildQuotient Sets whether or not the quotient model is to be built. - */ - DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false); + // A class that offers the possibility to customize the bisimulation. + struct Options { + // Creates an object representing the default values for all options. + Options(); - /*! - * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation. - * - * @param model The model to decompose. - * @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the - * model will be respected. If built, the quotient model will only contain the respected atomic propositions. - * @param weak A flag indication whether a weak bisimulation is to be computed. - * @param buildQuotient Sets whether or not the quotient model is to be built. - */ - DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, boost::optional> const& atomicPropositions = boost::optional>(), bool keepRewards = true, bool weak = false, bool buildQuotient = false); + /*! + * Creates an object representing the options necessary to obtain the smallest quotient while still + * preserving the given formula. + * + * @param formula The formula that is to be preserved. + */ + Options(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; + + // 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. + boost::optional> respectedAtomicPropositions; + + // A flag that indicates whether or not the state-rewards of the model are to be respected (and should + // be kept in the quotient model, if one is built). + bool keepRewards; + + // A flag that indicates whether a strong or a weak bisimulation is to be computed. + bool weak; + + // A flag that indicates whether step-bounded properties are to be preserved. This may only be set to tru + // when computing strong bisimulation equivalence. + bool bounded; + + // A flag that governs whether the quotient model is actually built or only the decomposition is computed. + bool buildQuotient; + }; /*! - * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely - * preserves formulas of the form phi until psi. + * Decomposes the given DTMC into equivalance classes of a bisimulation. Which kind of bisimulation is + * computed, is customizable via the given options. * * @param model The model to decompose. - * @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 indication whether a weak bisimulation is to be computed. - * @param bounded If set to true, also bounded until formulas are preserved. - * @param buildQuotient Sets whether or not the quotient model is to be built. + * @param options The options that customize the computed bisimulation. */ - DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc const& model, Options const& options = Options()); /*! - * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely - * preserves formulas of the form phi until psi. + * Decomposes the given CTMC into equivalance classes of a bisimulation. Which kind of bisimulation is + * computed, is customizable via the given options. * * @param model The model to decompose. - * @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 indication whether a weak bisimulation is to be computed. - * @param bounded If set to true, also bounded until formulas are preserved. - * @param buildQuotient Sets whether or not the quotient model is to be built. + * @param options The options that customize the computed bisimulation. */ - DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool keepRewards, bool weak, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, Options const& options = Options()); /*! * Retrieves the quotient of the model under the previously computed bisimulation. @@ -87,7 +97,7 @@ namespace storm { typedef typename std::list::const_iterator const_iterator; // Creates a new block with the given begin and end. - Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr const& label = nullptr); + Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id); // Prints the block. void print(Partition const& partition) const; @@ -191,15 +201,6 @@ namespace storm { // Retrieves whether the block is to be interpreted as absorbing. bool isAbsorbing() const; - // Retrieves whether the block has a special label. - bool hasLabel() const; - - // Retrieves the special label of the block if it has one. - std::string const& getLabel() const; - - // Retrieves a pointer to the label of the block (which is the nullptr if there is none). - std::shared_ptr const& getLabelPtr() const; - private: // An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks // kept by the partition. @@ -227,9 +228,6 @@ namespace storm { // The ID of the block. This is only used for debugging purposes. std::size_t id; - - // The label of the block or nullptr if it has none. - std::shared_ptr label; }; class Partition { @@ -252,11 +250,9 @@ 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 otherLabel The label that is to be attached to all other states. - * @param prob1Label The label that is to be attached to all states with probability 1. * @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, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities = false); + Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, bool keepSilentProbabilities = false); Partition() = default; Partition(Partition const& other) = default; @@ -468,15 +464,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 phiLabel The label that all phi states carry in the model. - * @param psiLabel The label that all psi states carry in 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 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, BisimulationType bisimulationType, bool keepRewards = true, bool bounded = false); + 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); /*! * Creates the initial partition based on all the labels in the given model. diff --git a/src/utility/cli.h b/src/utility/cli.h index 07fb2fbd5..195a4c0be 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -293,7 +293,10 @@ namespace storm { } std::cout << "Performing bisimulation minimization... "; - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, boost::optional>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); + + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); model = bisimulationDecomposition.getQuotient(); std::cout << "done." << std::endl << std::endl; } diff --git a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp index ffe337d31..4a8f5f143 100644 --- a/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -9,7 +9,7 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); std::shared_ptr> dtmc = abstractModel->as>(); - storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), true, false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc); std::shared_ptr> result; ASSERT_NO_THROW(result = bisim.getQuotient()); @@ -17,14 +17,20 @@ TEST(DeterministicModelBisimulationDecomposition, Die) { EXPECT_EQ(13, result->getNumberOfStates()); EXPECT_EQ(20, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, std::set({"one"}), true, false, true); + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + options.respectedAtomicPropositions = std::set({"one"}); + + storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, options); ASSERT_NO_THROW(result = bisim2.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); EXPECT_EQ(5, result->getNumberOfStates()); EXPECT_EQ(8, result->getNumberOfTransitions()); + + options.bounded = false; + options.weak = true; - storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, std::set({"one"}), true, true, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, options); ASSERT_NO_THROW(result = bisim3.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); @@ -38,7 +44,7 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); std::shared_ptr> dtmc = abstractModel->as>(); - storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc, boost::optional>(), true, false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisim(*dtmc); std::shared_ptr> result; ASSERT_NO_THROW(result = bisim.getQuotient()); @@ -46,14 +52,20 @@ TEST(DeterministicModelBisimulationDecomposition, Crowds) { EXPECT_EQ(334, result->getNumberOfStates()); EXPECT_EQ(546, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, std::set({"observe0Greater1"}), true, false, true); + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + options.respectedAtomicPropositions = std::set({"observe0Greater1"}); + + storm::storage::DeterministicModelBisimulationDecomposition bisim2(*dtmc, options); ASSERT_NO_THROW(result = bisim2.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); EXPECT_EQ(65, result->getNumberOfStates()); EXPECT_EQ(105, result->getNumberOfTransitions()); - storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, std::set({"observe0Greater1"}), true, true, true); + options.bounded = false; + options.weak = true; + + storm::storage::DeterministicModelBisimulationDecomposition bisim3(*dtmc, options); ASSERT_NO_THROW(result = bisim3.getQuotient()); EXPECT_EQ(storm::models::DTMC, result->getType()); From ed4f1bb7cfc185da79c361e2f8eee4075fbd04a3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 30 Jan 2015 22:59:26 +0100 Subject: [PATCH 2/8] Added the possibility to build the bisimulation options from a formula in the sense that it automatically picks suitable settings for the formula. Former-commit-id: 932c7d899a2a70a5a631b63fe7122a599adc67c3 --- ...ministicModelBisimulationDecomposition.cpp | 65 +++++++++++++------ ...erministicModelBisimulationDecomposition.h | 32 +++++++-- ...sticModelBisimulationDecompositionTest.cpp | 41 ++++++++++++ 3 files changed, 112 insertions(+), 26 deletions(-) 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()); } From 2dae5862c882a39e7c49730c9b09edc47c5b57cc Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 30 Jan 2015 23:26:29 +0100 Subject: [PATCH 3/8] Small fix to bisimulation options. Former-commit-id: 555c5ef697fb7ae638d472a4787175cbbe17d756 --- .../DeterministicModelBisimulationDecomposition.cpp | 8 ++++---- .../DeterministicModelBisimulationDecomposition.h | 12 +++++------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 6c8641211..08c11a2f2 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -615,7 +615,7 @@ namespace storm { } for (auto const& expressionFormula : atomicExpressionFormulas) { std::stringstream stream; - stream << expressionFormula; + stream << *expressionFormula; labelsToRespect.insert(stream.str()); } respectedAtomicPropositions = labelsToRespect; @@ -722,7 +722,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) { + void DeterministicModelBisimulationDecomposition::buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards) { // In order to create the quotient model, we need to construct // (a) the new transition matrix, // (b) the new labeling, @@ -733,7 +733,7 @@ namespace storm { // Prepare the new state labeling for (b). storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); - std::set atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions(); + std::set atomicPropositionsSet = selectedAtomicPropositions; atomicPropositionsSet.insert("init"); std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); for (auto const& ap : atomicPropositions) { @@ -839,7 +839,7 @@ namespace storm { template template - void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 255e2c22a..eae63f442 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -413,8 +413,7 @@ namespace storm { * getQuotient(). * * @param model The model on whose state space to compute the coarses strong bisimulation relation. - * @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given, - * all atomic propositions are considered. + * @param atomicPropositions The set of atomic propositions that the bisimulation considers. * @param backwardTransitions The backward transitions of the model. * @param The initial partition. * @param bisimulationType The kind of bisimulation that is to be computed. @@ -422,7 +421,7 @@ namespace storm { * method. */ template - void partitionRefinement(ModelType const& model, boost::optional> const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient); + void partitionRefinement(ModelType const& model, std::set const& atomicPropositions, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool keepRewards, bool buildQuotient); /*! * Refines the partition based on the provided splitter. After calling this method all blocks are stable @@ -466,15 +465,14 @@ namespace storm { * * @param model The model whose state space was used for computing the equivalence classes. This is used for * determining the transitions of each equivalence class. - * @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The - * quotient will only have these atomic propositions. If not given, all atomic propositions will be - * considered. + * @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. + * The quotient will only have these atomic propositions. * @param partition The previously computed partition. This is used for quickly retrieving the block of a * state. * @param bisimulationType The kind of bisimulation that is to be computed. */ template - void buildQuotient(ModelType const& model, boost::optional> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards); + void buildQuotient(ModelType const& model, std::set const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType, bool keepRewards); /*! * Creates the measure-driven initial partition for reaching psi states from phi states. From f49d89144e96cbdb0161f42d35e8df84fe592e61 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 31 Jan 2015 14:24:55 +0100 Subject: [PATCH 4/8] Fixed issue that could cause wrong models to be generated. Former-commit-id: 8f1f9b46128e67b62182b3e73662b4e090432e3f --- src/builder/ExplicitPrismModelBuilder.cpp | 7 ++++--- src/storage/BitVector.cpp | 2 +- src/storage/prism/BooleanVariable.cpp | 2 +- src/utility/cli.h | 12 +++++++++--- test/functional/storage/BitVectorTest.cpp | 9 +++++++++ 5 files changed, 24 insertions(+), 8 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 6b13b1193..01d06cd11 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -13,7 +13,7 @@ namespace storm { namespace builder { template - ExplicitPrismModelBuilder::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 1000000), bitsPerState(bitsPerState), reachableStates() { + ExplicitPrismModelBuilder::StateInformation::StateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() { // Intentionally left empty. } @@ -97,7 +97,7 @@ namespace storm { // Start by defining the undefined constants in the model. storm::prism::Program preparedProgram; if (options.constantDefinitions) { - preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get()); + preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get()); } else { preparedProgram = program; } @@ -220,6 +220,7 @@ namespace storm { int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); + STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) == assignedValue, "Writing to the bit vector bucket failed."); } // Check that we processed all assignments. @@ -328,7 +329,7 @@ namespace storm { choice.addProbability(stateIndex, probability); probabilitySum += probability; } - + // Check that the resulting distribution is in fact a distribution. STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); } diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 0cafd4c0c..d919f56ea 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -459,7 +459,7 @@ namespace storm { bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value << (64 - (bitIndexInBucket + numberOfBits))); } else if (bitIndexInBucket + numberOfBits > 64) { // Write the part of the value that falls into the first bucket. - bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (64 - bitIndexInBucket)); + bucketVector[bucket] = (bucketVector[bucket] & ~mask) | (value >> (numberOfBits + (bitIndexInBucket - 64))); ++bucket; // Compute the remaining number of bits. diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index 7f32fd7ea..35df52356 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -11,7 +11,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { - stream << variable.getName() << ": bool " << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": bool init" << variable.getInitialValueExpression() << ";"; return stream; } diff --git a/src/utility/cli.h b/src/utility/cli.h index 195a4c0be..fc8abc3e2 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -294,7 +294,13 @@ namespace storm { std::cout << "Performing bisimulation minimization... "; typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; - options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); + if (formula) { + options = storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, *formula.get()); + } + if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) { + options.weak = true; + options.bounded = false; + } storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); model = bisimulationDecomposition.getQuotient(); @@ -373,8 +379,8 @@ namespace storm { std::unique_ptr result; if (model->getType() == storm::models::DTMC) { std::shared_ptr> dtmc = model->as>(); -// storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); - storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); + storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); +// storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); result = modelchecker.check(*formula.get()); } else if (model->getType() == storm::models::MDP) { std::shared_ptr> mdp = model->as>(); diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index 0854f364e..ff06e1815 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -98,6 +98,7 @@ TEST(BitVectorTest, SetFromInt) { EXPECT_FALSE(vector.get(62)); EXPECT_TRUE(vector.get(63)); + vector = storm::storage::BitVector(77); vector.setFromInt(62, 4, 15); EXPECT_TRUE(vector.get(62)); @@ -108,6 +109,14 @@ TEST(BitVectorTest, SetFromInt) { vector.setFromInt(62, 5, 17); } +TEST(BitVectorTest, GetSetInt) { + storm::storage::BitVector vector(77); + + vector.setFromInt(63, 3, 2); + EXPECT_EQ(2, vector.getAsInt(63, 3)); +} + + TEST(BitVectorDeathTest, GetSetAssertion) { storm::storage::BitVector vector(32); From adc1aa1442bc07349a9cf742367a3e01e2d633e6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 1 Feb 2015 23:39:11 +0100 Subject: [PATCH 5/8] Corrected an assertion. Former-commit-id: 54804b1599b603f01bd09bdda59f86ce21aff125 --- src/builder/ExplicitPrismModelBuilder.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 7df300c73..7079b69b9 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -220,7 +220,7 @@ namespace storm { int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); - STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) == assignedValue, "Writing to the bit vector bucket failed."); + STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } // Check that we processed all assignments. From 5e3eab8058825a72948c024ff5844a7fdb1f2a2a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 1 Feb 2015 23:43:59 +0100 Subject: [PATCH 6/8] Fixed another bug Former-commit-id: 27c666dcb6a8d45ecefb52ffad9bd8075a422ce9 --- src/storage/DeterministicModelBisimulationDecomposition.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 6cf4f00ca..33d2589da 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -643,7 +643,7 @@ namespace storm { measureDrivenInitialPartition = true; } } else if (newFormula->isReachabilityRewardFormula()) { - rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); + rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer(); if (rightSubformula->isPropositionalFormula()) { measureDrivenInitialPartition = true; } From f5a9ebe2f7da3677fd5c99a15c3c03d3a58b2357 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 1 Feb 2015 23:52:40 +0100 Subject: [PATCH 7/8] And another minor bug. Former-commit-id: af2e9d05ee3731dbf23b3c52b22d2ba92094dd8a --- src/stormParametric.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 049f638f1..137a2b285 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -154,6 +154,11 @@ void check() { std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + // Convert the transition rewards to state rewards if necessary. + if (model->hasTransitionRewards()) { + model->convertTransitionRewardsToStateRewards(); + } + model->printModelInformationToStream(std::cout); // Program Translation Time Measurement, End From a371d0eb04e730943c4ce3ac72fd7ad180ecb492 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 Feb 2015 09:28:16 +0100 Subject: [PATCH 8/8] Fixed assertion. Former-commit-id: 7125d92b071370c1d1d1665969ee0502289ff7c3 --- .../reachability/SparseDtmcEliminationModelChecker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 950e0d834..e7ac8c425 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -203,7 +203,7 @@ namespace storm { storm::storage::BitVector trueStates(model.getNumberOfStates(), true); // Do some sanity checks to establish some required properties. - STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() != storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities."); + STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities."); STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state."); storm::storage::sparse::state_type initialState = *model.getInitialStates().begin();