sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

work on making bisimulation fast again :( 

Former-commit-id: bb89091b2d
tempestpy_adaptions
dehnert 9 years ago
parent
2484a515a0
commit
1f5110b90c
10 changed files with 529 additions and 180 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 85
      src/storage/bisimulation/BisimulationDecomposition.cpp
  2. 6
      src/storage/bisimulation/BisimulationDecomposition.h
  3. 105
      src/storage/bisimulation/Block.cpp
  4. 15
      src/storage/bisimulation/Block.h
  5. 44
      src/storage/bisimulation/DeterministicBlockData.cpp
  6. 64
      src/storage/bisimulation/DeterministicBlockData.h
  7. 164
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  8. 33
      src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
  9. 137
      src/storage/bisimulation/Partition.cpp
  10. 56
      src/storage/bisimulation/Partition.h

85
src/storage/bisimulation/BisimulationDecomposition.cpp
View File

@ -6,6 +6,8 @@
#include "src/models/sparse/Ctmc.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/storage/bisimulation/DeterministicBlockData.h"
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
@ -21,13 +23,13 @@ namespace storm {
using namespace bisimulation;
template<typename ModelType>
BisimulationDecomposition<ModelType>::Options::Options(ModelType const& model, storm::logic::Formula const& formula) : Options() {
template<typename ModelType, typename BlockDataType>
BisimulationDecomposition<ModelType, BlockDataType>::Options::Options(ModelType const& model, storm::logic::Formula const& formula) : Options() {
this->preserveSingleFormula(model, formula);
}
template<typename ModelType>
BisimulationDecomposition<ModelType>::Options::Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
template<typename ModelType, typename BlockDataType>
BisimulationDecomposition<ModelType, BlockDataType>::Options::Options(ModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : Options() {
if (formulas.empty()) {
this->respectedAtomicPropositions = model.getStateLabeling().getLabels();
this->keepRewards = true;
@ -40,13 +42,13 @@ namespace storm {
}
}
template<typename ModelType>
BisimulationDecomposition<ModelType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) {
template<typename ModelType, typename BlockDataType>
BisimulationDecomposition<ModelType, BlockDataType>::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) {
// Intentionally left empty.
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::Options::preserveFormula(ModelType const& model, storm::logic::Formula const& formula) {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::Options::preserveFormula(ModelType const& model, storm::logic::Formula const& formula) {
// Disable the measure driven initial partition.
measureDrivenInitialPartition = false;
phiStates = boost::none;
@ -62,8 +64,8 @@ namespace storm {
this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) {
keepRewards = formula.containsRewardOperator();
// We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
@ -76,8 +78,8 @@ namespace storm {
this->checkAndSetMeasureDrivenInitialPartition(model, formula);
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::Options::checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula) {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::Options::checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula) {
std::shared_ptr<storm::logic::Formula const> newFormula = formula.asSharedPointer();
if (formula.isProbabilityOperatorFormula()) {
@ -115,8 +117,8 @@ namespace storm {
}
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::Options::addToRespectedAtomicPropositions(std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> const& expressions, std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> const& labels) {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::Options::addToRespectedAtomicPropositions(std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> const& expressions, std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> const& labels) {
std::set<std::string> labelsToRespect;
for (auto const& labelFormula : labels) {
labelsToRespect.insert(labelFormula->getLabel());
@ -131,16 +133,16 @@ namespace storm {
}
}
template<typename ModelType>
BisimulationDecomposition<ModelType>::BisimulationDecomposition(ModelType const& model, Options const& options) : model(model), backwardTransitions(model.getBackwardTransitions()), options(options), partition(), comparator(), quotient(nullptr) {
template<typename ModelType, typename BlockDataType>
BisimulationDecomposition<ModelType, BlockDataType>::BisimulationDecomposition(ModelType const& model, Options const& options) : model(model), backwardTransitions(model.getBackwardTransitions()), options(options), partition(), comparator(), quotient(nullptr) {
// Fix the respected atomic propositions if they were not explicitly given.
if (!this->options.respectedAtomicPropositions) {
this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels();
}
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::computeBisimulationDecomposition() {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::computeBisimulationDecomposition() {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point initialPartitionStart = std::chrono::high_resolution_clock::now();
@ -188,19 +190,21 @@ namespace storm {
}
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::performPartitionRefinement() {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::performPartitionRefinement() {
// Insert all blocks into the splitter queue that are initially marked as being a (potential) splitter.
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block> const& block) { if (block->isMarkedAsSplitter()) { splitterQueue.push_back(block.get()); } } );
std::deque<Block<BlockDataType>*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block<BlockDataType>> const& block) { if (block->isMarkedAsSplitter()) { splitterQueue.push_back(block.get()); } } );
// Then perform the actual splitting until there are no more splitters.
uint_fast64_t iterations = 0;
while (!splitterQueue.empty()) {
++iterations;
// 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(); } );
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
// Get and prepare the next splitter.
Block* splitter = splitterQueue.front();
Block<BlockDataType>* splitter = splitterQueue.front();
splitterQueue.pop_front();
splitter->unmarkAsSplitter();
@ -208,23 +212,24 @@ namespace storm {
// std::cout << "refining based on splitter " << splitter->getId() << std::endl;
refinePartitionBasedOnSplitter(*splitter, splitterQueue);
}
std::cout << "done within " << iterations << " iterations." << std::endl;
}
template<typename ModelType>
std::shared_ptr<ModelType> BisimulationDecomposition<ModelType>::getQuotient() const {
template<typename ModelType, typename BlockDataType>
std::shared_ptr<ModelType> BisimulationDecomposition<ModelType, BlockDataType>::getQuotient() const {
STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
return this->quotient;
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::splitInitialPartitionBasedOnStateRewards() {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::splitInitialPartitionBasedOnStateRewards() {
std::vector<ValueType> const& stateRewardVector = model.getUniqueRewardModel()->second.getStateRewardVector();
partition.split([&stateRewardVector] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return stateRewardVector[a] < stateRewardVector[b]; });
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::initializeLabelBasedPartition() {
partition = storm::storage::bisimulation::Partition(model.getNumberOfStates());
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition() {
partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates());
for (auto const& label : options.respectedAtomicPropositions.get()) {
if (label == "init") {
@ -243,8 +248,8 @@ namespace storm {
// partition.print();
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition() {
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = this->getStatesWithProbability01();
boost::optional<storm::storage::sparse::state_type> representativePsiState;
@ -252,7 +257,7 @@ namespace storm {
representativePsiState = *options.psiStates.get().begin();
}
partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
partition = storm::storage::bisimulation::Partition<BlockDataType>(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState);
// If the model has state rewards, we need to consider them, because otherwise reward properties are not
// preserved.
@ -264,8 +269,8 @@ namespace storm {
// partition.print();
}
template<typename ModelType>
void BisimulationDecomposition<ModelType>::extractDecompositionBlocks() {
template<typename ModelType, typename BlockDataType>
void BisimulationDecomposition<ModelType, BlockDataType>::extractDecompositionBlocks() {
// 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.
this->blocks.resize(partition.size());
@ -278,12 +283,12 @@ namespace storm {
}
}
template class BisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
template class BisimulationDecomposition<storm::models::sparse::Dtmc<double>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>, bisimulation::DeterministicBlockData>;
#ifdef STORM_HAVE_CARL
template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
#endif
}
}

6
src/storage/bisimulation/BisimulationDecomposition.h
View File

@ -29,7 +29,7 @@ namespace storm {
/*!
* This class is the superclass of all decompositions of a sparse model into its bisimulation quotient.
*/
template <typename ModelType>
template <typename ModelType, typename BlockDataType>
class BisimulationDecomposition : public Decomposition<StateBlock> {
public:
typedef typename ModelType::ValueType ValueType;
@ -158,7 +158,7 @@ namespace storm {
* @param splitter The splitter to use.
* @param splitterQueue The queue into which to insert the newly discovered potential splitters.
*/
virtual void refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque<bisimulation::Block*>& splitterQueue) = 0;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0;
/*!
* Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
@ -204,7 +204,7 @@ namespace storm {
Options options;
// The current partition (used by partition refinement).
storm::storage::bisimulation::Partition partition;
storm::storage::bisimulation::Partition<BlockDataType> partition;
// A comparator used for comparing the distances of constants.
storm::utility::ConstantsComparator<ValueType> comparator;

105
src/storage/bisimulation/Block.cpp
View File

@ -4,6 +4,7 @@
#include <iomanip>
#include "src/storage/bisimulation/Partition.h"
#include "src/storage/bisimulation/DeterministicBlockData.h"
#include "src/exceptions/InvalidOperationException.h"
#include "src/utility/macros.h"
@ -12,136 +13,180 @@ namespace storm {
namespace storage {
namespace bisimulation {
Block::Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previousBlock, Block* nextBlock, std::size_t id) : nextBlock(nextBlock), previousBlock(previousBlock), beginIndex(beginIndex), endIndex(endIndex), markedAsSplitter(false), needsRefinementFlag(false), absorbing(false), id(id) {
template<typename DataType>
Block<DataType>::Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previousBlock, Block* nextBlock, std::size_t id) : nextBlock(nextBlock), previousBlock(previousBlock), beginIndex(beginIndex), endIndex(endIndex), markedAsSplitter(false), needsRefinementFlag(false), absorbing(false), id(id), mData() {
if (nextBlock != nullptr) {
nextBlock->previousBlock = this;
}
if (previousBlock != nullptr) {
previousBlock->nextBlock = this;
}
data().notify(*this);
STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Unable to create block of illegal size.");
}
bool Block::operator==(Block const& other) const {
template<typename DataType>
bool Block<DataType>::operator==(Block const& other) const {
return this == &other;
}
bool Block::operator!=(Block const& other) const {
template<typename DataType>
bool Block<DataType>::operator!=(Block const& other) const {
return this != &other;
}
void Block::print(Partition const& partition) const {
template<typename DataType>
void Block<DataType>::print(Partition<DataType> const& partition) const {
std::cout << "block [" << this << "] " << this->id << " from " << this->beginIndex << " to " << this->endIndex << std::endl;
}
void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) {
// std::cout << "setting beg index to " << beginIndex << " [" << this << "]" << std::endl;
template<typename DataType>
void Block<DataType>::setBeginIndex(storm::storage::sparse::state_type beginIndex) {
this->beginIndex = beginIndex;
data().notify(*this);
STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size.");
}
void Block::setEndIndex(storm::storage::sparse::state_type endIndex) {
template<typename DataType>
void Block<DataType>::setEndIndex(storm::storage::sparse::state_type endIndex) {
this->endIndex = endIndex;
data().notify(*this);
STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size.");
}
storm::storage::sparse::state_type Block::getBeginIndex() const {
template<typename DataType>
storm::storage::sparse::state_type Block<DataType>::getBeginIndex() const {
return this->beginIndex;
}
storm::storage::sparse::state_type Block::getEndIndex() const {
template<typename DataType>
storm::storage::sparse::state_type Block<DataType>::getEndIndex() const {
return this->endIndex;
}
Block const& Block::getNextBlock() const {
template<typename DataType>
Block<DataType> const& Block<DataType>::getNextBlock() const {
return *this->nextBlock;
}
bool Block::hasNextBlock() const {
template<typename DataType>
bool Block<DataType>::hasNextBlock() const {
return this->nextBlock != nullptr;
}
Block* Block::getNextBlockPointer() {
template<typename DataType>
Block<DataType>* Block<DataType>::getNextBlockPointer() {
return this->nextBlock;
}
Block const* Block::getNextBlockPointer() const {
template<typename DataType>
Block<DataType> const* Block<DataType>::getNextBlockPointer() const {
return this->nextBlock;
}
Block const& Block::getPreviousBlock() const {
template<typename DataType>
Block<DataType> const& Block<DataType>::getPreviousBlock() const {
return *this->previousBlock;
}
Block* Block::getPreviousBlockPointer() {
template<typename DataType>
Block<DataType>* Block<DataType>::getPreviousBlockPointer() {
return this->previousBlock;
}
Block const* Block::getPreviousBlockPointer() const {
template<typename DataType>
Block<DataType> const* Block<DataType>::getPreviousBlockPointer() const {
return this->previousBlock;
}
bool Block::hasPreviousBlock() const {
template<typename DataType>
bool Block<DataType>::hasPreviousBlock() const {
return this->previousBlock != nullptr;
}
bool Block::check() const {
template<typename DataType>
bool Block<DataType>::check() const {
STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Block has negative size.");
STORM_LOG_ASSERT(!this->hasPreviousBlock() || this->getPreviousBlock().getNextBlockPointer() == this, "Illegal previous block.");
STORM_LOG_ASSERT(!this->hasNextBlock() || this->getNextBlock().getPreviousBlockPointer() == this, "Illegal next block.");
return true;
}
std::size_t Block::getNumberOfStates() const {
template<typename DataType>
std::size_t Block<DataType>::getNumberOfStates() const {
return (this->endIndex - this->beginIndex);
}
bool Block::isMarkedAsSplitter() const {
template<typename DataType>
bool Block<DataType>::isMarkedAsSplitter() const {
return this->markedAsSplitter;
}
void Block::markAsSplitter() {
template<typename DataType>
void Block<DataType>::markAsSplitter() {
this->markedAsSplitter = true;
}
void Block::unmarkAsSplitter() {
template<typename DataType>
void Block<DataType>::unmarkAsSplitter() {
this->markedAsSplitter = false;
}
std::size_t Block::getId() const {
template<typename DataType>
std::size_t Block<DataType>::getId() const {
return this->id;
}
void Block::setAbsorbing(bool absorbing) {
template<typename DataType>
void Block<DataType>::setAbsorbing(bool absorbing) {
this->absorbing = absorbing;
}
bool Block::isAbsorbing() const {
template<typename DataType>
bool Block<DataType>::isAbsorbing() const {
return this->absorbing;
}
void Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
template<typename DataType>
void Block<DataType>::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
this->representativeState = representativeState;
}
bool Block::hasRepresentativeState() const {
template<typename DataType>
bool Block<DataType>::hasRepresentativeState() const {
return static_cast<bool>(representativeState);
}
storm::storage::sparse::state_type Block::getRepresentativeState() const {
template<typename DataType>
storm::storage::sparse::state_type Block<DataType>::getRepresentativeState() const {
STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block.");
return representativeState.get();
}
// Retrieves whether the block is marked as a predecessor.
bool Block::needsRefinement() const {
template<typename DataType>
bool Block<DataType>::needsRefinement() const {
return needsRefinementFlag;
}
// Marks the block as needing refinement (or not).
void Block::setNeedsRefinement(bool value) {
template<typename DataType>
void Block<DataType>::setNeedsRefinement(bool value) {
needsRefinementFlag = value;
}
template<typename DataType>
DataType& Block<DataType>::data() {
return mData;
}
template<typename DataType>
DataType const& Block<DataType>::data() const {
return mData;
}
template class Block<DeterministicBlockData>;
}
}
}

15
src/storage/bisimulation/Block.h
View File

@ -10,11 +10,13 @@ namespace storm {
namespace storage {
namespace bisimulation {
// Forward-declare partition class.
template<typename DataType>
class Partition;
template<typename DataType>
class Block {
public:
friend class Partition;
friend class Partition<DataType>;
// Creates a new block with the given begin and end.
Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previous, Block* next, std::size_t id);
@ -29,7 +31,7 @@ namespace storm {
bool operator!=(Block const& other) const;
// Prints the block to the standard output.
void print(Partition const& partition) const;
void print(Partition<DataType> const& partition) const;
// Returns the beginning index of the block.
storm::storage::sparse::state_type getBeginIndex() const;
@ -100,6 +102,12 @@ namespace storm {
// Retrieves the representative state for this block.
storm::storage::sparse::state_type getRepresentativeState() const;
// Retrieves the additional data associated with this block.
DataType& data();
// Retrieves the additional data associated with this block.
DataType const& data() const;
private:
// Sets the beginning index of the block.
void setBeginIndex(storm::storage::sparse::state_type beginIndex);
@ -130,6 +138,9 @@ namespace storm {
// 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<storm::storage::sparse::state_type> representativeState;
// A member that stores additional data that depends on the kind of bisimulation.
DataType mData;
};
}
}

44
src/storage/bisimulation/DeterministicBlockData.cpp
View File

@ -0,0 +1,44 @@
#include "src/storage/bisimulation/DeterministicBlockData.h"
namespace storm {
namespace storage {
namespace bisimulation {
DeterministicBlockData::DeterministicBlockData() : newBeginIndex(0), newEndIndex(0) {
// Intentionally left empty.
}
DeterministicBlockData::DeterministicBlockData(uint_fast64_t newBeginIndex, uint_fast64_t newEndIndex) : newBeginIndex(newBeginIndex), newEndIndex(newEndIndex) {
// Intentionally left empty.
}
uint_fast64_t DeterministicBlockData::getNewBeginIndex() const {
return newBeginIndex;
}
void DeterministicBlockData::increaseNewBeginIndex() {
++newBeginIndex;
}
uint_fast64_t DeterministicBlockData::getNewEndIndex() const {
return newEndIndex;
}
void DeterministicBlockData::decreaseNewEndIndex() {
--newEndIndex;
}
void DeterministicBlockData::increaseNewEndIndex() {
++newEndIndex;
}
bool DeterministicBlockData::notify(Block<DeterministicBlockData> const& block) {
bool result = block.getBeginIndex() != this->newBeginIndex || block.getEndIndex() != this->newEndIndex;
this->newBeginIndex = block.getBeginIndex();
this->newEndIndex = block.getEndIndex();
return result;
}
}
}
}

64
src/storage/bisimulation/DeterministicBlockData.h
View File

@ -0,0 +1,64 @@
#ifndef STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_
#define STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_
#include <cstdint>
#include "src/storage/bisimulation/Block.h"
namespace storm {
namespace storage {
namespace bisimulation {
class DeterministicBlockData {
public:
DeterministicBlockData();
DeterministicBlockData(uint_fast64_t newBeginIndex, uint_fast64_t newEndIndex);
/*!
* Retrieves the new begin index.
*
* @return The new begin index.
*/
uint_fast64_t getNewBeginIndex() const;
/*!
* Increases the new begin index by one.
*/
void increaseNewBeginIndex();
/*!
* Retrieves the new end index.
*
* @return The new end index.
*/
uint_fast64_t getNewEndIndex() const;
/*!
* Decreases the new end index.
*/
void decreaseNewEndIndex();
/*!
* Increases the new end index.
*/
void increaseNewEndIndex();
/*!
* This method needs to be called whenever the block was modified to notify the data of the change.
*
* @param block The block that this data belongs to.
* @return True iff the data changed as a consequence of notifying it.
*/
bool notify(Block<DeterministicBlockData> const& block);
public:
// A marker that can be used to mark a the new beginning of the block.
uint_fast64_t newBeginIndex;
// A marker that can be used to mark a the new end of the block.
uint_fast64_t newEndIndex;
};
}
}
}
#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_ */

164
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
View File

@ -28,7 +28,7 @@ namespace storm {
using namespace bisimulation;
template<typename ModelType>
DeterministicModelBisimulationDecomposition<ModelType>::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType>::Options const& options) : BisimulationDecomposition<ModelType>(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero<ValueType>()), predecessorsOfCurrentSplitter(model.getNumberOfStates()) {
DeterministicModelBisimulationDecomposition<ModelType>::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType, DeterministicModelBisimulationDecomposition::BlockDataType>::Options const& options) : BisimulationDecomposition<ModelType, DeterministicModelBisimulationDecomposition::BlockDataType>(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero<ValueType>()) {
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.");
@ -102,7 +102,7 @@ namespace storm {
void DeterministicModelBisimulationDecomposition<ModelType>::initializeSilentProbabilities() {
silentProbabilities.resize(this->model.getNumberOfStates(), storm::utility::zero<ValueType>());
for (storm::storage::sparse::state_type state = 0; state < this->model.getNumberOfStates(); ++state) {
Block const* currentBlockPtr = &this->partition.getBlock(state);
Block<BlockDataType> const* currentBlockPtr = &this->partition.getBlock(state);
for (auto const& successorEntry : this->model.getRows(state)) {
if (&this->partition.getBlock(successorEntry.getColumn()) == currentBlockPtr) {
silentProbabilities[state] += successorEntry.getValue();
@ -121,7 +121,7 @@ namespace storm {
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
BisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition();
BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
this->initializeWeakDtmcBisimulation();
@ -130,7 +130,7 @@ namespace storm {
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::initializeLabelBasedPartition() {
BisimulationDecomposition<ModelType>::initializeLabelBasedPartition();
BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition();
if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
this->initializeWeakDtmcBisimulation();
@ -153,29 +153,20 @@ namespace storm {
}
template<typename ModelType>
bool DeterministicModelBisimulationDecomposition<ModelType>::isPredecessorOfCurrentSplitter(storm::storage::sparse::state_type const& state) const {
return this->predecessorsOfCurrentSplitter.get(state);
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitter(std::list<Block*>& predecessorBlocks, std::deque<bisimulation::Block*>& splitterQueue) {
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitter(std::list<Block<BlockDataType>*>& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
for (auto block : predecessorBlocks) {
// std::cout << "splitting predecessor block " << block->getId() << " of splitter" << std::endl;
this->partition.splitBlock(*block, [this] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) {
bool firstIsPredecessor = isPredecessorOfCurrentSplitter(state1);
bool secondIsPredecessor = isPredecessorOfCurrentSplitter(state2);
if (firstIsPredecessor && !secondIsPredecessor) {
return true;
} else if (firstIsPredecessor && secondIsPredecessor) {
return getProbabilityToSplitter(state1) < getProbabilityToSplitter(state2);
} else {
return false;
// Depending on the actions we need to take, the block to refine changes, so we need to keep track of it.
Block<BlockDataType>* blockToRefineProbabilistically = block;
if (block->data().getNewBeginIndex() != block->getBeginIndex()) {
// If the new begin index has shifted to a non-trivial position, we need to split the block.
if (block->data().getNewBeginIndex() != block->getEndIndex()) {
auto result = this->partition.splitBlock(*block, block->data().getNewBeginIndex());
if (result.second) {
blockToRefineProbabilistically = block->getPreviousBlockPointer();
}
}
}, [&splitterQueue] (Block& block) {
splitterQueue.emplace_back(&block);
});
// this->partition.print();
// std::cout << "size: " << this->partition.size() << std::endl;
}
// Remember that we have refined the block.
block->setNeedsRefinement(false);
@ -184,7 +175,91 @@ namespace storm {
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque<bisimulation::Block*>& splitterQueue) {
bool DeterministicModelBisimulationDecomposition<ModelType>::possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& predecessorBlock) const {
return predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing();
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType> const& predecessorBlock, ValueType const& value) {
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
// If the position of the state is between the new begin and end index, we have not yet seen this predecessor.
if (predecessorPosition >= predecessorBlock.data().getNewBeginIndex() && predecessorPosition < predecessorBlock.data().getNewEndIndex()) {
// Then, we just set the value.
probabilitiesToCurrentSplitter[predecessor] = value;
} else {
// If the state was seen as a predecessor before, we add the value to the existing value.
probabilitiesToCurrentSplitter[predecessor] += value;
}
}
template <typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::moveStateToNewBeginningOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock) {
this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().getNewBeginIndex()));
predecessorBlock.data().increaseNewBeginIndex();
}
template <typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::moveStateToNewEndOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock) {
this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().getNewEndIndex() - 1));
predecessorBlock.data().decreaseNewEndIndex();
}
template <typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter) {
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
// If the predecessor is one of the states for which we have already explored its predecessors, we can move
// it to the new beginning of the block like for any other block.
if (predecessorPosition <= currentPositionInSplitter) {
moveStateToNewBeginningOfBlock(predecessor, predecessorBlock);
} else {
// Otherwise, we move it to the new end of the block in which we assemble all states that are predecessors
// of the splitter, but for which the predecessors still need to be explored.
moveStateToNewEndOfBlock(predecessor, predecessorBlock);
}
}
template <typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::explorePredecessorsOfNewEndOfSplitter(bisimulation::Block<BlockDataType>& splitter) {
for (auto splitterIt = this->partition.begin() + splitter.data().getNewEndIndex(), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt) {
storm::storage::sparse::state_type currentState = *splitterIt;
for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
Block<BlockDataType>& 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, predecessorBlock, predecessorEntry.getValue());
if (predecessorBlock != splitter) {
moveStateToNewBeginningOfBlock(predecessor, predecessorBlock);
} else {
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
// In this case, we must only move the predecessor its predecessors were already explored.
// If we have not yet explored its predecessors, it has to be to the right of the currently
// considered state and will be transferred to the beginning of the block anyway.
if (predecessorPosition < splitter.data().getNewEndIndex()) {
moveStateToNewBeginningOfBlock(predecessor, predecessorBlock);
}
}
}
// Now that we have explored its predecessors and know that the current state is itself a predecessor of
// the splitter, we can safely move it to the beginning of the block.
moveStateToNewBeginningOfBlock(currentState, splitter);
splitter.data().increaseNewEndIndex();
}
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
// The outline of the refinement is as follows.
//
// (0) we prepare the environment for the splitting process.
@ -194,32 +269,34 @@ namespace storm {
// all predecessors of the splitter in a member bit vector.
// (0)
predecessorsOfCurrentSplitter.clear();
std::list<Block*> predecessorBlocks;
std::list<Block<BlockDataType>*> predecessorBlocks;
// (1)
for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt) {
storm::storage::sparse::state_type currentPosition = splitter.getBeginIndex();
bool splitterIsItsOwnPredecessor = false;
for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte && currentPosition < splitter.data().getNewEndIndex(); ++splitterIt, ++currentPosition) {
storm::storage::sparse::state_type currentState = *splitterIt;
for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
Block& predecessorBlock = this->partition.getBlock(predecessor);
Block<BlockDataType>& predecessorBlock = this->partition.getBlock(predecessor);
// If the predecessor block has just one state or is marked as being absorbing, we must not split it.
if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) {
// 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, predecessorBlock, predecessorEntry.getValue());
// If we have not seen this predecessor before, we reset its value and mark it as a predecessor of
// the splitter.
if (!predecessorsOfCurrentSplitter.get(predecessor)) {
predecessorsOfCurrentSplitter.set(predecessor);
probabilitiesToCurrentSplitter[predecessor] = predecessorEntry.getValue();
if (predecessorBlock != splitter) {
moveStateToNewBeginningOfBlock(predecessor, predecessorBlock);
} else {
// Otherwise, we increase the probability by the current transition.
probabilitiesToCurrentSplitter[predecessor] += predecessorEntry.getValue();
splitterIsItsOwnPredecessor = true;
moveStateInSplitter(predecessor, predecessorBlock, currentPosition);
}
// Insert the block into the list of blocks to refine (if that has not already happened).
if (!predecessorBlock.needsRefinement()) {
predecessorBlocks.emplace_back(&predecessorBlock);
predecessorBlock.setNeedsRefinement();
@ -227,6 +304,11 @@ namespace storm {
}
}
// If the splitter is its own predecessor block, we need to treat the states at the end of the block.
if (splitterIsItsOwnPredecessor) {
explorePredecessorsOfNewEndOfSplitter(splitter);
}
// std::cout << "probs of splitter predecessors: " << std::endl;
// for (auto state : predecessorsOfCurrentSplitter) {
// std::cout << state << " [" << this->partition.getBlock(state).getId() << "]" << " -> " << probabilitiesToCurrentSplitter[state] << std::endl;
@ -283,7 +365,7 @@ namespace storm {
}
}
Block const& oldBlock = this->partition.getBlock(representativeState);
Block<BlockDataType> const& oldBlock = this->partition.getBlock(representativeState);
// If the block is absorbing, we simply add a self-loop.
if (oldBlock.isAbsorbing()) {
@ -348,7 +430,7 @@ namespace storm {
// Now check which of the blocks of the partition contain at least one initial state.
for (auto initialState : this->model.getInitialStates()) {
Block const& initialBlock = this->partition.getBlock(initialState);
Block<BlockDataType> const& initialBlock = this->partition.getBlock(initialState);
newLabeling.addLabelToState("init", initialBlock.getId());
}

33
src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
View File

@ -2,6 +2,7 @@
#define STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
#include "src/storage/bisimulation/BisimulationDecomposition.h"
#include "src/storage/bisimulation/DeterministicBlockData.h"
namespace storm {
namespace utility {
@ -14,8 +15,9 @@ namespace storm {
* This class represents the decomposition of a deterministic model into its bisimulation quotient.
*/
template<typename ModelType>
class DeterministicModelBisimulationDecomposition : public BisimulationDecomposition<ModelType> {
class DeterministicModelBisimulationDecomposition : public BisimulationDecomposition<ModelType, bisimulation::DeterministicBlockData> {
public:
typedef bisimulation::DeterministicBlockData BlockDataType;
typedef typename ModelType::ValueType ValueType;
typedef typename ModelType::RewardModelType RewardModelType;
@ -26,7 +28,7 @@ namespace storm {
* @param model The model to decompose.
* @param options The options that customize the computed bisimulation.
*/
DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType>::Options const& options = typename BisimulationDecomposition<ModelType>::Options());
DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition<ModelType, BlockDataType>::Options const& options = typename BisimulationDecomposition<ModelType, BlockDataType>::Options());
protected:
virtual std::pair<storm::storage::BitVector, storm::storage::BitVector> getStatesWithProbability01() override;
@ -37,10 +39,10 @@ namespace storm {
virtual void buildQuotient() override;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque<bisimulation::Block*>& splitterQueue) override;
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override;
private:
virtual void refinePredecessorBlocksOfSplitter(std::list<bisimulation::Block*>& predecessorBlocks, std::deque<bisimulation::Block*>& splitterQueue);
virtual void refinePredecessorBlocksOfSplitter(std::list<bisimulation::Block<BlockDataType>*>& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue);
/*!
* Performs the necessary steps to compute a weak bisimulation on a DTMC.
@ -67,16 +69,29 @@ namespace storm {
// Retrieves whether the given state is silent.
bool isSilent(storm::storage::sparse::state_type const& state) const;
// Retrieves whether the given state is a predecessor of the current splitter.
bool isPredecessorOfCurrentSplitter(storm::storage::sparse::state_type const& state) const;
// Retrieves whether the given predecessor of the splitters possibly needs refinement.
bool possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& predecessorBlock) const;
// Moves the given state to the new begin index of the given block and increases the new begin.
void moveStateToNewBeginningOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock);
// Moves the given state to the new end index of the given block and decreases the new end.
void moveStateToNewEndOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock);
// Moves the given state to the new begin or new end of the block, depending on where the predecessor is located.
void moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter);
// Increases the probability of moving to the current splitter for the given state.
void increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType> const& predecessorBlock, ValueType const& value);
// Explores the predecessors of the states that were identified as predecessors themselves that have not yet
// been explored.
void explorePredecessorsOfNewEndOfSplitter(bisimulation::Block<BlockDataType>& splitter);
// A vector that holds the probabilities of states going into the splitter. This is used by the method that
// refines a block based on probabilities.
std::vector<ValueType> probabilitiesToCurrentSplitter;
// A bit vector storing the predecessors of the current splitter.
storm::storage::BitVector predecessorsOfCurrentSplitter;
// A vector mapping each state to its silent probability.
std::vector<ValueType> silentProbabilities;
};

137
src/storage/bisimulation/Partition.cpp
View File

@ -2,14 +2,17 @@
#include <iostream>
#include "src/storage/bisimulation/DeterministicBlockData.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
namespace storage {
namespace bisimulation {
Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) {
blocks.emplace_back(new Block(0, numberOfStates, nullptr, nullptr, blocks.size()));
template<typename DataType>
Partition<DataType>::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) {
blocks.emplace_back(new Block<DataType>(0, numberOfStates, nullptr, nullptr, blocks.size()));
// Set up the different parts of the internal structure.
for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) {
@ -19,13 +22,14 @@ namespace storm {
}
}
Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional<storm::storage::sparse::state_type> representativeProb1State) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) {
template<typename DataType>
Partition<DataType>::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional<storm::storage::sparse::state_type> representativeProb1State) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) {
storm::storage::sparse::state_type position = 0;
Block* firstBlock = nullptr;
Block* secondBlock = nullptr;
Block* thirdBlock = nullptr;
Block<DataType>* firstBlock = nullptr;
Block<DataType>* secondBlock = nullptr;
Block<DataType>* thirdBlock = nullptr;
if (!prob0States.empty()) {
blocks.emplace_back(new Block(0, prob0States.getNumberOfSetBits(), nullptr, nullptr, blocks.size()));
blocks.emplace_back(new Block<DataType>(0, prob0States.getNumberOfSetBits(), nullptr, nullptr, blocks.size()));
firstBlock = blocks.front().get();
for (auto state : prob0States) {
@ -39,7 +43,7 @@ namespace storm {
}
if (!prob1States.empty()) {
blocks.emplace_back(new Block(position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, blocks.size()));
blocks.emplace_back(new Block<DataType>(position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, blocks.size()));
secondBlock = blocks[1].get();
for (auto state : prob1States) {
@ -55,7 +59,7 @@ namespace storm {
storm::storage::BitVector otherStates = ~(prob0States | prob1States);
if (!otherStates.empty()) {
blocks.emplace_back(new Block(position, numberOfStates, secondBlock, nullptr, blocks.size()));
blocks.emplace_back(new Block<DataType>(position, numberOfStates, secondBlock, nullptr, blocks.size()));
thirdBlock = blocks[2].get();
for (auto state : otherStates) {
@ -68,12 +72,14 @@ namespace storm {
}
}
void Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
template<typename DataType>
void Partition<DataType>::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
void Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
template<typename DataType>
void Partition<DataType>::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
storm::storage::sparse::state_type state1 = this->states[position1];
storm::storage::sparse::state_type state2 = this->states[position2];
@ -82,64 +88,96 @@ namespace storm {
this->positions[state2] = position1;
}
storm::storage::sparse::state_type const& Partition::getPosition(storm::storage::sparse::state_type state) const {
template<typename DataType>
storm::storage::sparse::state_type const& Partition<DataType>::getPosition(storm::storage::sparse::state_type state) const {
return this->positions[state];
}
void Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
template<typename DataType>
void Partition<DataType>::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
this->positions[state] = position;
}
storm::storage::sparse::state_type const& Partition::getState(storm::storage::sparse::state_type position) const {
template<typename DataType>
storm::storage::sparse::state_type const& Partition<DataType>::getState(storm::storage::sparse::state_type position) const {
return this->states[position];
}
void Partition::mapStatesToBlock(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
template<typename DataType>
void Partition<DataType>::mapStatesToBlock(Block<DataType>& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
for (; first != last; ++first) {
this->stateToBlockMapping[*first] = &block;
}
}
void Partition::mapStatesToPositions(Block const& block) {
template<typename DataType>
void Partition<DataType>::mapStatesToPositions(Block<DataType> const& block) {
storm::storage::sparse::state_type position = block.getBeginIndex();
for (auto stateIt = this->begin(block), stateIte = this->end(block); stateIt != stateIte; ++stateIt, ++position) {
this->positions[*stateIt] = position;
}
}
Block& Partition::getBlock(storm::storage::sparse::state_type state) {
template<typename DataType>
Block<DataType>& Partition<DataType>::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
Block const& Partition::getBlock(storm::storage::sparse::state_type state) const {
template<typename DataType>
Block<DataType> const& Partition<DataType>::getBlock(storm::storage::sparse::state_type state) const {
return *this->stateToBlockMapping[state];
}
std::vector<storm::storage::sparse::state_type>::iterator Partition::begin(Block const& block) {
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::iterator Partition<DataType>::begin(Block<DataType> const& block) {
auto it = this->states.begin();
std::advance(it, block.getBeginIndex());
return it;
}
std::vector<storm::storage::sparse::state_type>::const_iterator Partition::begin(Block const& block) const {
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::const_iterator Partition<DataType>::begin(Block<DataType> const& block) const {
auto it = this->states.begin();
std::advance(it, block.getBeginIndex());
return it;
}
std::vector<storm::storage::sparse::state_type>::iterator Partition::end(Block const& block) {
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::iterator Partition<DataType>::end(Block<DataType> const& block) {
auto it = this->states.begin();
std::advance(it, block.getEndIndex());
return it;
}
std::vector<storm::storage::sparse::state_type>::const_iterator Partition::end(Block const& block) const {
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::const_iterator Partition<DataType>::end(Block<DataType> const& block) const {
auto it = this->states.begin();
std::advance(it, block.getEndIndex());
return it;
}
std::pair<std::vector<std::unique_ptr<Block>>::iterator, bool> Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::iterator Partition<DataType>::begin() {
return this->states.begin();
}
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::const_iterator Partition<DataType>::begin() const {
return this->states.begin();
}
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::iterator Partition<DataType>::end() {
return this->states.end();
}
template<typename DataType>
std::vector<storm::storage::sparse::state_type>::const_iterator Partition<DataType>::end() const {
return this->states.end();
}
template<typename DataType>
std::pair<typename std::vector<std::unique_ptr<Block<DataType>>>::iterator, bool> Partition<DataType>::splitBlock(Block<DataType>& block, storm::storage::sparse::state_type position) {
STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position.");
// std::cout << "splitting " << block.getId() << " at pos " << position << " (was " << block.getBeginIndex() << " to " << block.getEndIndex() << ")" << std::endl;
@ -153,7 +191,7 @@ namespace storm {
}
// Actually create the new block.
blocks.emplace_back(new Block(block.getBeginIndex(), position, block.getPreviousBlockPointer(), &block, blocks.size()));
blocks.emplace_back(new Block<DataType>(block.getBeginIndex(), position, block.getPreviousBlockPointer(), &block, blocks.size()));
auto newBlockIt = std::prev(blocks.end());
// Resize the current block appropriately.
@ -170,7 +208,8 @@ namespace storm {
return std::make_pair(newBlockIt, true);
}
bool Partition::splitBlock(Block& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block&)> const& newBlockCallback) {
template<typename DataType>
bool Partition<DataType>::splitBlock(Block<DataType>& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block<DataType>&)> const& newBlockCallback) {
// std::cout << "sorting the block [" << block.getId() << "]" << std::endl;
// Sort the range of the block such that all states that have the label are moved to the front.
std::sort(this->begin(block), this->end(block), less);
@ -213,7 +252,15 @@ namespace storm {
return wasSplit;
}
bool Partition::split(std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block&)> const& newBlockCallback) {
// Splits the block by sorting the states according to the given function and then identifying the split
// points.
template<typename DataType>
bool Partition<DataType>::splitBlock(Block<DataType>& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less) {
return this->splitBlock(block, less, [] (Block<DataType>& block) {});
}
template<typename DataType>
bool Partition<DataType>::split(std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block<DataType>&)> const& newBlockCallback) {
bool result = false;
// Since the underlying storage of the blocks may change during iteration, we remember the current size
// and iterate over indices. This assumes that new blocks will be added at the end of the blocks vector.
@ -224,26 +271,35 @@ namespace storm {
return result;
}
void Partition::splitStates(Block& block, storm::storage::BitVector const& states) {
template<typename DataType>
bool Partition<DataType>::split(std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less) {
return this->split(less, [] (Block<DataType>& block) {});
}
template<typename DataType>
void Partition<DataType>::splitStates(Block<DataType>& block, storm::storage::BitVector const& states) {
this->splitBlock(block, [&states] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return states.get(a) && !states.get(b); });
}
void Partition::splitStates(storm::storage::BitVector const& states) {
template<typename DataType>
void Partition<DataType>::splitStates(storm::storage::BitVector const& states) {
this->split([&states] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return states.get(a) && !states.get(b); });
}
void Partition::sortBlock(Block const& block) {
template<typename DataType>
void Partition<DataType>::sortBlock(Block<DataType> const& block) {
std::sort(this->begin(block), this->end(block), [] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return a < b; });
mapStatesToPositions(block);
}
Block& Partition::insertBlock(Block& block) {
template<typename DataType>
Block<DataType>& Partition<DataType>::insertBlock(Block<DataType>& block) {
// Find the beginning of the new block.
storm::storage::sparse::state_type begin = block.hasPreviousBlock() ? block.getPreviousBlock().getEndIndex() : 0;
// Actually insert the new block.
blocks.emplace_back(new Block(begin, block.getBeginIndex(), block.getPreviousBlockPointer(), &block, blocks.size()));
Block& newBlock = *blocks.back();
blocks.emplace_back(new Block<DataType>(begin, block.getBeginIndex(), block.getPreviousBlockPointer(), &block, blocks.size()));
Block<DataType>& newBlock = *blocks.back();
// Update the mapping of the states in the newly created block.
for (auto it = this->begin(newBlock), ite = this->end(newBlock); it != ite; ++it) {
@ -253,15 +309,18 @@ namespace storm {
return newBlock;
}
std::vector<std::unique_ptr<Block>> const& Partition::getBlocks() const {
template<typename DataType>
std::vector<std::unique_ptr<Block<DataType>>> const& Partition<DataType>::getBlocks() const {
return this->blocks;
}
std::vector<std::unique_ptr<Block>>& Partition::getBlocks() {
template<typename DataType>
std::vector<std::unique_ptr<Block<DataType>>>& Partition<DataType>::getBlocks() {
return this->blocks;
}
bool Partition::check() const {
template<typename DataType>
bool Partition<DataType>::check() const {
for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
STORM_LOG_ASSERT(this->states[this->positions[state]] == state, "Position mapping corrupted.");
}
@ -274,7 +333,8 @@ namespace storm {
return true;
}
void Partition::print() const {
template<typename DataType>
void Partition<DataType>::print() const {
for (auto const& block : this->blocks) {
block->print(*this);
}
@ -295,10 +355,13 @@ namespace storm {
STORM_LOG_ASSERT(this->check(), "Partition corrupted.");
}
std::size_t Partition::size() const {
template<typename DataType>
std::size_t Partition<DataType>::size() const {
return blocks.size();
}
template class Partition<DeterministicBlockData>;
}
}
}

56
src/storage/bisimulation/Partition.h
View File

@ -12,6 +12,7 @@ namespace storm {
namespace storage {
namespace bisimulation {
template<typename DataType>
class Partition {
public:
/*!
@ -49,20 +50,27 @@ namespace storm {
// Splits the block at the given position and inserts a new block after the current one holding the rest
// of the states.
std::pair<std::vector<std::unique_ptr<Block>>::iterator, bool> splitBlock(Block& block, storm::storage::sparse::state_type position);
std::pair<typename std::vector<std::unique_ptr<Block<DataType>>>::iterator, bool> splitBlock(Block<DataType>& block, storm::storage::sparse::state_type position);
// Splits the block by sorting the states according to the given function and then identifying the split
// points. The callback function is called for every newly created block.
bool splitBlock(Block& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block&)> const& newBlockCallback = [] (Block&) {});
bool splitBlock(Block<DataType>& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block<DataType>&)> const& newBlockCallback);
// Splits the block by sorting the states according to the given function and then identifying the split
// points.
bool splitBlock(Block<DataType>& block, std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less);
// Splits all blocks by using the sorting-based splitting. The callback is called for all newly created
// blocks.
bool split(std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block&)> const& newBlockCallback = [] (Block&) {});
bool split(std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less, std::function<void (Block<DataType>&)> const& newBlockCallback);
// Splits all blocks by using the sorting-based splitting.
bool split(std::function<bool (storm::storage::sparse::state_type, storm::storage::sparse::state_type)> const& less);
// Splits the block such that the resulting blocks contain only states in the given set or none at all.
// If the block is split, the given block will contain the states *not* in the given set and the newly
// created block will contain the states *in* the given set.
void splitStates(Block& block, storm::storage::BitVector const& states);
void splitStates(Block<DataType>& block, storm::storage::BitVector const& states);
/*!
* Splits all blocks of the partition such that afterwards all blocks contain only states within the given
@ -71,37 +79,49 @@ namespace storm {
void splitStates(storm::storage::BitVector const& states);
// Sorts the block based on the state indices.
void sortBlock(Block const& block);
void sortBlock(Block<DataType> const& block);
// Retrieves the blocks of the partition.
std::vector<std::unique_ptr<Block>> const& getBlocks() const;
std::vector<std::unique_ptr<Block<DataType>>> const& getBlocks() const;
// Retrieves the blocks of the partition.
std::vector<std::unique_ptr<Block>>& getBlocks();
std::vector<std::unique_ptr<Block<DataType>>>& getBlocks();
// Checks the partition for internal consistency.
bool check() const;
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::iterator begin(Block const& block);
std::vector<storm::storage::sparse::state_type>::iterator begin(Block<DataType> const& block);
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::const_iterator begin(Block const& block) const;
std::vector<storm::storage::sparse::state_type>::const_iterator begin(Block<DataType> const& block) const;
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::iterator end(Block const& block);
std::vector<storm::storage::sparse::state_type>::iterator end(Block<DataType> const& block);
// Returns an iterator to the beginning of the states of the given block.
std::vector<storm::storage::sparse::state_type>::const_iterator end(Block const& block) const;
std::vector<storm::storage::sparse::state_type>::const_iterator end(Block<DataType> const& block) const;
// Returns an iterator to the beginning of the states in the partition.
std::vector<storm::storage::sparse::state_type>::iterator begin();
// Returns an iterator to the beginning of the states in the partition.
std::vector<storm::storage::sparse::state_type>::const_iterator begin() const;
// Returns an iterator to the end of the states in the partition.
std::vector<storm::storage::sparse::state_type>::iterator end();
// Returns an iterator to the end of the states in the partition.
std::vector<storm::storage::sparse::state_type>::const_iterator end() const;
// Swaps the positions of the two given states.
void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2);
// Retrieves the block of the given state.
Block& getBlock(storm::storage::sparse::state_type state);
Block<DataType>& getBlock(storm::storage::sparse::state_type state);
// Retrieves the block of the given state.
Block const& getBlock(storm::storage::sparse::state_type state) const;
Block<DataType> const& getBlock(storm::storage::sparse::state_type state) const;
// Retrieves the position of the given state.
storm::storage::sparse::state_type const& getPosition(storm::storage::sparse::state_type state) const;
@ -110,10 +130,10 @@ namespace storm {
storm::storage::sparse::state_type const& getState(storm::storage::sparse::state_type position) const;
// Updates the block mapping for the given range of states to the specified block.
void mapStatesToBlock(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last);
void mapStatesToBlock(Block<DataType>& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last);
// Update the state to position for the states in the given block.
void mapStatesToPositions(Block const& block);
void mapStatesToPositions(Block<DataType> const& block);
private:
// FIXME: necessary?
@ -123,17 +143,17 @@ namespace storm {
// FIXME: necessary?
// Inserts a block before the given block. The new block will cover all states between the beginning
// of the given block and the end of the previous block.
Block& insertBlock(Block& block);
Block<DataType>& insertBlock(Block<DataType>& block);
// FIXME: necessary?
// Sets the position of the given state.
void setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position);
// The of blocks in the partition.
std::vector<std::unique_ptr<Block>> blocks;
std::vector<std::unique_ptr<Block<DataType>>> blocks;
// A mapping of states to their blocks.
std::vector<Block*> stateToBlockMapping;
std::vector<Block<DataType>*> stateToBlockMapping;
// A vector containing all the states. It is ordered in a way such that the blocks only need to define
// their start/end indices.

Write Preview
Loading…
Cancel
Save