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

As pointed out by Joachim Klein, weak bisimulation does not preserve reward properties. Therefore, weak bisimulation now refines blocks with non-zero reward wrt. strong bisimulation.

tempestpy_adaptions
dehnert 8 years ago
parent
c5d0b281ce
commit
a067527aa0
6 changed files with 132 additions and 95 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. 36
      src/storm/storage/bisimulation/DeterministicBlockData.cpp
  2. 24
      src/storm/storage/bisimulation/DeterministicBlockData.h
  3. 122
      src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
  4. 12
      src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
  5. 24
      src/storm/storage/bisimulation/Partition.cpp
  6. 9
      src/storm/storage/bisimulation/Partition.h

36
src/storm/storage/bisimulation/DeterministicBlockData.cpp
View File

@ -13,7 +13,7 @@ namespace storm {
// Intentionally left empty.
}
DeterministicBlockData::DeterministicBlockData(uint_fast64_t marker1, uint_fast64_t marker2) : valMarker1(marker1), valMarker2(marker2), splitterFlag(false), needsRefinementFlag(false), absorbingFlag(false), valRepresentativeState() {
DeterministicBlockData::DeterministicBlockData(uint_fast64_t marker1, uint_fast64_t marker2) : valMarker1(marker1), valMarker2(marker2), flags(0), valRepresentativeState() {
// Intentionally left empty.
}
@ -56,19 +56,27 @@ namespace storm {
}
bool DeterministicBlockData::splitter() const {
return this->splitterFlag;
return getFlag(SPLITTER_FLAG);
}
void DeterministicBlockData::setSplitter(bool value) {
this->splitterFlag = value;
setFlag(SPLITTER_FLAG, value);
}
void DeterministicBlockData::setAbsorbing(bool absorbing) {
this->absorbingFlag = absorbing;
setFlag(ABSORBING_FLAG, absorbing);
}
bool DeterministicBlockData::absorbing() const {
return this->absorbingFlag;
return getFlag(ABSORBING_FLAG);
}
void DeterministicBlockData::setHasRewards(bool value) {
setFlag(REWARD_FLAG, value);
}
bool DeterministicBlockData::hasRewards() const {
return getFlag(REWARD_FLAG);
}
void DeterministicBlockData::setRepresentativeState(storm::storage::sparse::state_type representativeState) {
@ -85,15 +93,27 @@ namespace storm {
}
bool DeterministicBlockData::needsRefinement() const {
return needsRefinementFlag;
return getFlag(REFINEMENT_FLAG);
}
void DeterministicBlockData::setNeedsRefinement(bool value) {
needsRefinementFlag = value;
setFlag(REFINEMENT_FLAG, value);
}
bool DeterministicBlockData::getFlag(uint64_t flag) const {
return (this->flags & flag) != 0ull;
}
void DeterministicBlockData::setFlag(uint64_t flag, bool value) {
if (value) {
this->flags |= flag;
} else {
this->flags &= ~flag;
}
}
std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data) {
out << "m1: " << data.marker1() << ", m2: " << data.marker2();
out << "m1: " << data.marker1() << ", m2: " << data.marker2() << ", r: " << data.hasRewards();
return out;
}
}

24
src/storm/storage/bisimulation/DeterministicBlockData.h
View File

@ -49,6 +49,12 @@ namespace storm {
// Retrieves whether the block is to be interpreted as absorbing.
bool absorbing() const;
// Sets whether the states in the block have rewards.
void setHasRewards(bool value = true);
// Retrieves whether the states in the block have rewards.
bool hasRewards() const;
// Sets the representative state of this block
void setRepresentativeState(storm::storage::sparse::state_type representativeState);
@ -61,19 +67,21 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& out, DeterministicBlockData const& data);
public:
// Helpers to set/retrieve flags.
bool getFlag(uint64_t flag) const;
void setFlag(uint64_t flag, bool value);
// Two markers that can be used for various purposes. Whenever the block is split, both the markers are
// set to the beginning index of the block.
uint_fast64_t valMarker1;
uint_fast64_t valMarker2;
// A flag that can be used for marking the block as being a splitter.
bool splitterFlag;
// A flag that can be used for marking the block as needing refinement.
bool needsRefinementFlag;
// A flag indicating whether the block is to be interpreted as absorbing or not.
bool absorbingFlag;
// Some bits to store flags: splitter flag, refinement flag, absorbing flag.
static const uint64_t SPLITTER_FLAG = 1ull;
static const uint64_t REFINEMENT_FLAG = 1ull << 1;
static const uint64_t ABSORBING_FLAG = 1ull << 2;
static const uint64_t REWARD_FLAG = 1ull << 3;
uint8_t flags;
// 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.

122
src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
View File

@ -118,22 +118,37 @@ namespace storm {
this->initializeSilentProbabilities();
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
void DeterministicModelBisimulationDecomposition<ModelType>::postProcessInitialPartition() {
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
this->initializeWeakDtmcBisimulation();
}
if (this->options.getKeepRewards() && this->model.hasRewardModel() && this->options.getType() == BisimulationType::Weak) {
// For a weak bisimulation that is to preserve reward properties, we have to flag all blocks of states
// with non-zero reward as reward blocks to they can be refined wrt. strong bisimulation.
// Here, we assume that the initial partition already respects state rewards. Therefore, it suffices to
// check the first state of each block for a non-zero reward.
std::vector<ValueType> const& stateRewardVector = this->model.getUniqueRewardModel().getStateRewardVector();
for (auto& block : this->partition.getBlocks()) {
auto state = *this->partition.begin(*block);
block->data().setHasRewards(!storm::utility::isZero(stateRewardVector[state]));
}
}
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
postProcessInitialPartition();
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::initializeLabelBasedPartition() {
BisimulationDecomposition<ModelType, BlockDataType>::initializeLabelBasedPartition();
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
this->initializeWeakDtmcBisimulation();
}
postProcessInitialPartition();
}
template<typename ModelType>
@ -156,37 +171,49 @@ namespace storm {
return silentProbabilities[state];
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterStrong(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
STORM_LOG_TRACE("Refining predecessor " << block.getId() << " of splitter");
// 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;
bool split = false;
// If the new begin index has shifted to a non-trivial position, we need to split the block.
if (block.getBeginIndex() != block.data().marker1() && block.getEndIndex() != block.data().marker1()) {
split = true;
this->partition.splitBlock(block, block.data().marker1());
blockToRefineProbabilistically = block.getPreviousBlockPointer();
// Keep track of whether this is a block with reward states.
blockToRefineProbabilistically->data().setHasRewards(block.data().hasRewards());
}
split |= this->partition.splitBlock(*blockToRefineProbabilistically,
[this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2));
},
[&splitterQueue,&block] (Block<BlockDataType>& newBlock) {
splitterQueue.emplace_back(&newBlock);
newBlock.data().setSplitter();
// Keep track of whether this is a block with reward states.
newBlock.data().setHasRewards(block.data().hasRewards());
});
// If the predecessor block was split, we need to insert it into the splitter vector if it is not already
// marked as a splitter.
if (split && !blockToRefineProbabilistically->data().splitter()) {
splitterQueue.emplace_back(blockToRefineProbabilistically);
blockToRefineProbabilistically->data().setSplitter();
}
}
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
for (auto block : predecessorBlocks) {
STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter");
// 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;
bool split = false;
// If the new begin index has shifted to a non-trivial position, we need to split the block.
if (block->getBeginIndex() != block->data().marker1() && block->getEndIndex() != block->data().marker1()) {
split = true;
this->partition.splitBlock(*block, block->data().marker1());
blockToRefineProbabilistically = block->getPreviousBlockPointer();
}
split |= this->partition.splitBlock(*blockToRefineProbabilistically,
[this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2));
},
[&splitterQueue] (Block<BlockDataType>& block) {
splitterQueue.emplace_back(&block); block.data().setSplitter();
});
// If the predecessor block was split, we need to insert it into the splitter vector if it is not already
// marked as a splitter.
if (split && !blockToRefineProbabilistically->data().splitter()) {
splitterQueue.emplace_back(blockToRefineProbabilistically);
blockToRefineProbabilistically->data().setSplitter();
}
refinePredecessorBlockOfSplitterStrong(*block, splitterQueue);
// If the block was *not* split, we need to reset the markers by notifying the data.
block->resetMarkers();
@ -395,12 +422,15 @@ namespace storm {
[&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex];
},
[this, &splitterQueue] (bisimulation::Block<BlockDataType>& block) {
updateSilentProbabilitiesBasedOnTransitions(block);
[this, &splitterQueue, &block] (bisimulation::Block<BlockDataType>& newBlock) {
updateSilentProbabilitiesBasedOnTransitions(newBlock);
// Insert the new block as a splitter.
block.data().setSplitter();
splitterQueue.emplace_back(&block);
newBlock.data().setSplitter();
splitterQueue.emplace_back(&newBlock);
// Keep track of whether this is a block with reward states.
newBlock.data().setHasRewards(block.data().hasRewards());
});
// If the block was split, we also update the silent probabilities.
@ -418,10 +448,14 @@ namespace storm {
template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) {
for (auto block : predecessorBlocks) {
if (*block != splitter) {
refinePredecessorBlockOfSplitterWeak(*block, splitterQueue);
if (block->data().hasRewards()) {
refinePredecessorBlockOfSplitterStrong(*block, splitterQueue);
} else {
// If the block to split is the splitter itself, we must not do any splitting here.
if (*block != splitter) {
refinePredecessorBlockOfSplitterWeak(*block, splitterQueue);
} else {
// If the block to split is the splitter itself, we must not do any splitting here.
}
}
block->resetMarkers();
@ -594,7 +628,7 @@ namespace storm {
storm::storage::sparse::state_type targetBlock = this->partition.getBlock(entry.getColumn()).getId();
// If we are computing a weak bisimulation quotient, there is no need to add self-loops.
if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex) {
if ((this->options.getType() == BisimulationType::Weak) && targetBlock == blockIndex && !oldBlock.data().hasRewards()) {
continue;
}
@ -608,7 +642,7 @@ namespace storm {
// Now add them to the actual matrix.
for (auto const& probabilityEntry : blockProbability) {
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc && !oldBlock.data().hasRewards()) {
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - getSilentProbability(representativeState)));
} else {
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);

12
src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h
View File

@ -42,6 +42,12 @@ namespace storm {
virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) override;
private:
// Post-processes the initial partition to properly initialize it.
void postProcessInitialPartition();
// Refines the given block wrt to strong bisimulation.
void refinePredecessorBlockOfSplitterStrong(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
// Refines the predecessor blocks wrt. strong bisimulation.
void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
@ -98,11 +104,11 @@ namespace storm {
// of the states.
void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block);
// Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs.
void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
// Refines the given block wrt to weak bisimulation in DTMCs.
void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
// Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs.
void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue);
// Converts the one-step probabilities of going into the splitter into the conditional probabilities needed
// for weak bisimulation (on DTMCs).

24
src/storm/storage/bisimulation/Partition.cpp
View File

@ -89,11 +89,6 @@ namespace storm {
return this->positions[state];
}
template<typename DataType>
void Partition<DataType>::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
this->positions[state] = position;
}
template<typename DataType>
storm::storage::sparse::state_type const& Partition<DataType>::getState(storm::storage::sparse::state_type position) const {
return this->states[position];
@ -214,7 +209,7 @@ namespace storm {
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.");
STORM_LOG_ASSERT(position >= block.getBeginIndex() && position <= block.getEndIndex(), "Cannot split block at illegal position.");
STORM_LOG_TRACE("Splitting " << block.getId() << " at position " << position << " (begin was " << block.getBeginIndex() << ").");
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
@ -308,23 +303,6 @@ namespace storm {
mapStatesToPositions(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<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) {
stateToBlockMapping[*it] = &newBlock;
}
return newBlock;
}
template<typename DataType>
std::vector<std::unique_ptr<Block<DataType>>> const& Partition<DataType>::getBlocks() const {
return this->blocks;

9
src/storm/storage/bisimulation/Partition.h
View File

@ -152,15 +152,6 @@ namespace storm {
void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2);
private:
// 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<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<DataType>>> blocks;

Write Preview
Loading…
Cancel
Save