You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
663 lines
42 KiB
663 lines
42 KiB
#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
|
|
|
|
#include <algorithm>
|
|
#include <unordered_map>
|
|
#include <chrono>
|
|
#include <iomanip>
|
|
#include <boost/iterator/zip_iterator.hpp>
|
|
|
|
#include "src/adapters/CarlAdapter.h"
|
|
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
|
|
|
#include "src/models/sparse/Dtmc.h"
|
|
#include "src/models/sparse/Ctmc.h"
|
|
#include "src/models/sparse/StandardRewardModel.h"
|
|
|
|
#include "src/utility/graph.h"
|
|
#include "src/utility/constants.h"
|
|
#include "src/utility/ConstantsComparator.h"
|
|
#include "src/exceptions/IllegalFunctionCallException.h"
|
|
#include "src/exceptions/InvalidArgumentException.h"
|
|
|
|
#include "src/settings/SettingsManager.h"
|
|
#include "src/settings/modules/GeneralSettings.h"
|
|
|
|
namespace storm {
|
|
namespace storage {
|
|
|
|
using namespace bisimulation;
|
|
|
|
template<typename ModelType>
|
|
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>()) {
|
|
// Intentionally left empty.
|
|
}
|
|
|
|
template<typename ModelType>
|
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> DeterministicModelBisimulationDecomposition<ModelType>::getStatesWithProbability01() {
|
|
return storm::utility::graph::performProb01(this->backwardTransitions, this->options.phiStates.get(), this->options.psiStates.get());
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::splitOffDivergentStates() {
|
|
std::vector<storm::storage::sparse::state_type> stateStack;
|
|
stateStack.reserve(this->model.getNumberOfStates());
|
|
storm::storage::BitVector nondivergentStates(this->model.getNumberOfStates());
|
|
|
|
uint_fast64_t currentSize = this->partition.size();
|
|
for (uint_fast64_t blockIndex = 0; blockIndex < currentSize; ++blockIndex) {
|
|
auto& block = *this->partition.getBlocks()[blockIndex];
|
|
nondivergentStates.clear();
|
|
|
|
for (auto stateIt = this->partition.begin(block), stateIte = this->partition.end(block); stateIt != stateIte; ++stateIt) {
|
|
if (nondivergentStates.get(*stateIt)) {
|
|
continue;
|
|
}
|
|
|
|
// Now traverse the forward transitions of the current state and check whether there is a
|
|
// transition to some other block.
|
|
bool isDirectlyNonDivergent = false;
|
|
for (auto const& successor : this->model.getRows(*stateIt)) {
|
|
// If there is such a transition, then we can mark all states in the current block that can
|
|
// reach the state as non-divergent.
|
|
if (this->partition.getBlock(successor.getColumn()) != block) {
|
|
isDirectlyNonDivergent = true;
|
|
break;
|
|
}
|
|
}
|
|
|
|
if (isDirectlyNonDivergent) {
|
|
stateStack.push_back(*stateIt);
|
|
|
|
while (!stateStack.empty()) {
|
|
storm::storage::sparse::state_type currentState = stateStack.back();
|
|
stateStack.pop_back();
|
|
nondivergentStates.set(currentState);
|
|
|
|
for (auto const& predecessor : this->backwardTransitions.getRow(currentState)) {
|
|
if (this->partition.getBlock(predecessor.getColumn()) == block && !nondivergentStates.get(predecessor.getColumn())) {
|
|
stateStack.push_back(predecessor.getColumn());
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
if (!nondivergentStates.empty() && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) {
|
|
// After performing the split, the current block will contain the divergent states only.
|
|
this->partition.splitStates(block, nondivergentStates);
|
|
|
|
// Since the remaining states in the block are divergent, we can mark the block as absorbing.
|
|
// This also guarantees that the self-loop will be added to the state of the quotient
|
|
// representing this block of states.
|
|
block.data().setAbsorbing(true);
|
|
} else if (nondivergentStates.empty()) {
|
|
// If there are only diverging states in the block, we need to make it absorbing.
|
|
block.data().setAbsorbing(true);
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
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<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();
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::initializeWeakDtmcBisimulation() {
|
|
// If we are creating the initial partition for weak bisimulation on DTMCs, we need to (a) split off all
|
|
// divergent states of each initial block and (b) initialize the vector of silent probabilities.
|
|
this->splitOffDivergentStates();
|
|
this->initializeSilentProbabilities();
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::initializeMeasureDrivenPartition() {
|
|
BisimulationDecomposition<ModelType, BlockDataType>::initializeMeasureDrivenPartition();
|
|
|
|
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
|
|
this->initializeWeakDtmcBisimulation();
|
|
}
|
|
}
|
|
|
|
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();
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
typename DeterministicModelBisimulationDecomposition<ModelType>::ValueType const& DeterministicModelBisimulationDecomposition<ModelType>::getProbabilityToSplitter(storm::storage::sparse::state_type const& state) const {
|
|
return probabilitiesToCurrentSplitter[state];
|
|
}
|
|
|
|
template<typename ModelType>
|
|
bool DeterministicModelBisimulationDecomposition<ModelType>::isSilent(storm::storage::sparse::state_type const& state) const {
|
|
return this->comparator.isOne(silentProbabilities[state]);
|
|
}
|
|
|
|
template<typename ModelType>
|
|
bool DeterministicModelBisimulationDecomposition<ModelType>::hasNonZeroSilentProbability(storm::storage::sparse::state_type const& state) const {
|
|
return !this->comparator.isZero(silentProbabilities[state]);
|
|
}
|
|
|
|
template<typename ModelType>
|
|
typename DeterministicModelBisimulationDecomposition<ModelType>::ValueType DeterministicModelBisimulationDecomposition<ModelType>::getSilentProbability(storm::storage::sparse::state_type const& state) const {
|
|
return silentProbabilities[state];
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::deque<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 queue if it is not already
|
|
// marked as a splitter.
|
|
if (split && !blockToRefineProbabilistically->data().splitter()) {
|
|
splitterQueue.emplace_back(blockToRefineProbabilistically);
|
|
blockToRefineProbabilistically->data().setSplitter();
|
|
}
|
|
|
|
// If the block was *not* split, we need to reset the markers by notifying the data.
|
|
block->resetMarkers();
|
|
|
|
// Remember that we have refined the block.
|
|
block->data().setNeedsRefinement(false);
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
bool DeterministicModelBisimulationDecomposition<ModelType>::possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& predecessorBlock) const {
|
|
return predecessorBlock.getNumberOfStates() > 1 && !predecessorBlock.data().absorbing();
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType> const& predecessorBlock, ValueType const& value) {
|
|
STORM_LOG_TRACE("Increasing probability of " << predecessor << " to splitter by " << value << ".");
|
|
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
|
|
|
|
// If the position of the state is to the right of marker1, we have not seen it before.
|
|
if (predecessorPosition >= predecessorBlock.data().marker1()) {
|
|
// 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>::moveStateToMarker1(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock) {
|
|
this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().marker1()));
|
|
predecessorBlock.data().incrementMarker1();
|
|
}
|
|
|
|
template <typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::moveStateToMarker2(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock) {
|
|
this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().marker2()));
|
|
predecessorBlock.data().incrementMarker2();
|
|
}
|
|
|
|
template <typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block<BlockDataType>& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter, uint_fast64_t& elementsToSkip) {
|
|
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
|
|
|
|
// If the predecessors of the given predecessor were already explored, we can move it easily.
|
|
if (predecessorPosition <= currentPositionInSplitter + elementsToSkip) {
|
|
this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().marker1()));
|
|
predecessorBlock.data().incrementMarker1();
|
|
} else {
|
|
// Otherwise, we need to move the predecessor, but we need to make sure that we explore its
|
|
// predecessors later. We do this by moving it to a range at the beginning of the block that will hold
|
|
// all predecessors in the splitter whose predecessors have yet to be explored.
|
|
if (predecessorBlock.data().marker2() == predecessorBlock.data().marker1()) {
|
|
this->partition.swapStatesAtPositions(predecessorBlock.data().marker2(), predecessorPosition);
|
|
this->partition.swapStatesAtPositions(predecessorPosition, currentPositionInSplitter + elementsToSkip + 1);
|
|
} else {
|
|
this->partition.swapStatesAtPositions(predecessorBlock.data().marker2(), predecessorPosition);
|
|
this->partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.data().marker1());
|
|
this->partition.swapStatesAtPositions(predecessorPosition, currentPositionInSplitter + elementsToSkip + 1);
|
|
}
|
|
|
|
// Since we had to move an already explored state to the right of the current position,
|
|
++elementsToSkip;
|
|
predecessorBlock.data().incrementMarker1();
|
|
predecessorBlock.data().incrementMarker2();
|
|
}
|
|
}
|
|
|
|
template <typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::exploreRemainingStatesOfSplitter(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*>& predecessorBlocks) {
|
|
for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.begin(splitter) + (splitter.data().marker2() - splitter.getBeginIndex()); splitterIt != splitterIte; ++splitterIt) {
|
|
storm::storage::sparse::state_type currentState = *splitterIt;
|
|
|
|
for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) {
|
|
storm::storage::sparse::state_type 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;
|
|
}
|
|
|
|
// If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
|
|
// need to ignore it and proceed to the next predecessor.
|
|
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
|
|
continue;
|
|
}
|
|
|
|
// We keep track of the probability of the predecessor moving to the splitter.
|
|
increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
|
|
|
|
// Only move the state if it has not been seen as a predecessor before.
|
|
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
|
|
if (predecessorPosition >= predecessorBlock.data().marker1()) {
|
|
moveStateToMarker1(predecessor, predecessorBlock);
|
|
}
|
|
|
|
// We must not insert the the splitter itself if we are not computing a weak bisimulation on CTMCs.
|
|
if (this->options.getType() != BisimulationType::Weak || this->model.getType() != storm::models::ModelType::Ctmc || predecessorBlock != splitter) {
|
|
insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
|
|
}
|
|
}
|
|
}
|
|
|
|
// Finally, we can reset the second marker.
|
|
splitter.data().setMarker2(splitter.getBeginIndex());
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(bisimulation::Block<BlockDataType>& block) {
|
|
// For all predecessors, we can set the probability to the current probability of moving to the splitter.
|
|
for (auto stateIt = this->partition.begin(block), stateIte = this->partition.begin() + block.data().marker1(); stateIt != stateIte; ++stateIt) {
|
|
silentProbabilities[*stateIt] = probabilitiesToCurrentSplitter[*stateIt];
|
|
}
|
|
// All non-predecessors have a silent probability of zero.
|
|
for (auto stateIt = this->partition.begin() + block.data().marker1(), stateIte = this->partition.end(block); stateIt != stateIte; ++stateIt) {
|
|
silentProbabilities[*stateIt] = storm::utility::zero<ValueType>();
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block) {
|
|
for (auto stateIt = this->partition.begin(block), stateIte = this->partition.end(block); stateIt != stateIte; ++stateIt) {
|
|
if (hasNonZeroSilentProbability(*stateIt)) {
|
|
ValueType newSilentProbability = storm::utility::zero<ValueType>();
|
|
for (auto const& successorEntry : this->model.getTransitionMatrix().getRow(*stateIt)) {
|
|
if (this->partition.getBlock(successorEntry.getColumn()) == block) {
|
|
newSilentProbability += successorEntry.getValue();
|
|
}
|
|
}
|
|
silentProbabilities[*stateIt] = newSilentProbability;
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::computeConditionalProbabilitiesForNonSilentStates(bisimulation::Block<BlockDataType>& block) {
|
|
for (auto stateIt = this->partition.begin() + block.getBeginIndex(), stateIte = this->partition.begin() + block.data().marker1(); stateIt != stateIte; ++stateIt) {
|
|
if (!this->comparator.isOne(getSilentProbability(*stateIt))) {
|
|
probabilitiesToCurrentSplitter[*stateIt] /= storm::utility::one<ValueType>() - getSilentProbability(*stateIt);
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
std::vector<uint_fast64_t> DeterministicModelBisimulationDecomposition<ModelType>::computeNonSilentBlocks(bisimulation::Block<BlockDataType>& block) {
|
|
auto less = [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return probabilitiesToCurrentSplitter[state1] < probabilitiesToCurrentSplitter[state2]; };
|
|
this->partition.sortRange(block.getBeginIndex(), block.data().marker1(), less);
|
|
return this->partition.computeRangesOfEqualValue(block.getBeginIndex(), block.data().marker1(), less);
|
|
}
|
|
|
|
template<typename ModelType>
|
|
std::vector<storm::storage::BitVector> DeterministicModelBisimulationDecomposition<ModelType>::computeWeakStateLabelingBasedOnNonSilentBlocks(bisimulation::Block<BlockDataType> const& block, std::vector<uint_fast64_t> const& nonSilentBlockIndices) {
|
|
// Now that we have the split points of the non-silent states, we perform a backward search from
|
|
// each non-silent state and label the predecessors with the class of the non-silent state.
|
|
std::vector<storm::storage::BitVector> stateLabels(block.getNumberOfStates(), storm::storage::BitVector(nonSilentBlockIndices.size() - 1));
|
|
|
|
std::vector<storm::storage::sparse::state_type> stateStack;
|
|
stateStack.reserve(block.getNumberOfStates());
|
|
for (uint_fast64_t stateClassIndex = 0; stateClassIndex < nonSilentBlockIndices.size() - 1; ++stateClassIndex) {
|
|
for (auto stateIt = this->partition.begin() + nonSilentBlockIndices[stateClassIndex], stateIte = this->partition.begin() + nonSilentBlockIndices[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) {
|
|
|
|
stateStack.push_back(*stateIt);
|
|
stateLabels[this->partition.getPosition(*stateIt) - block.getBeginIndex()].set(stateClassIndex);
|
|
while (!stateStack.empty()) {
|
|
storm::storage::sparse::state_type currentState = stateStack.back();
|
|
stateStack.pop_back();
|
|
|
|
for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) {
|
|
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
|
|
|
|
if (this->comparator.isZero(predecessorEntry.getValue())) {
|
|
continue;
|
|
}
|
|
|
|
// Only if the state is in the same block, is a silent state and it has not yet been
|
|
// labeled with the current label.
|
|
if (this->partition.getBlock(predecessor) == block && isSilent(predecessor) && !stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].get(stateClassIndex)) {
|
|
stateStack.push_back(predecessor);
|
|
stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].set(stateClassIndex);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
return stateLabels;
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
|
|
// First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities
|
|
// for all non-silent states.
|
|
computeConditionalProbabilitiesForNonSilentStates(block);
|
|
|
|
// Then, we need to compute a labeling of the states that expresses which of the non-silent blocks they can reach.
|
|
std::vector<uint_fast64_t> nonSilentBlockIndices = computeNonSilentBlocks(block);
|
|
std::vector<storm::storage::BitVector> weakStateLabels = computeWeakStateLabelingBasedOnNonSilentBlocks(block, nonSilentBlockIndices);
|
|
|
|
// Then split the block according to this labeling.
|
|
// CAUTION: that this assumes that the positions of the states in the partition are not update until after
|
|
// the sorting is over. Otherwise, this interferes with the data used in the sorting process.
|
|
storm::storage::sparse::state_type originalBlockIndex = block.getBeginIndex();
|
|
auto split = this->partition.splitBlock(block,
|
|
[&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);
|
|
|
|
// Insert the new block as a splitter.
|
|
block.data().setSplitter();
|
|
splitterQueue.emplace_back(&block);
|
|
});
|
|
|
|
// If the block was split, we also update the silent probabilities.
|
|
if (split) {
|
|
updateSilentProbabilitiesBasedOnTransitions(block);
|
|
|
|
if (!block.data().splitter()) {
|
|
// Insert the new block as a splitter.
|
|
block.data().setSplitter();
|
|
splitterQueue.emplace_back(&block);
|
|
}
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
|
|
for (auto block : predecessorBlocks) {
|
|
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();
|
|
block->data().setNeedsRefinement(false);
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::insertIntoPredecessorList(bisimulation::Block<BlockDataType>& predecessorBlock, std::list<bisimulation::Block<BlockDataType>*>& predecessorBlocks) {
|
|
// Insert the block into the list of blocks to refine (if that has not already happened).
|
|
if (!predecessorBlock.data().needsRefinement()) {
|
|
predecessorBlocks.emplace_back(&predecessorBlock);
|
|
predecessorBlock.data().setNeedsRefinement();
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) {
|
|
STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId());
|
|
|
|
// The outline of the refinement is as follows.
|
|
//
|
|
// We iterate over all states of the splitter and determine for each predecessor the state the probability
|
|
// entering the splitter. These probabilities are written to a member vector so that after the iteration
|
|
// process we have the probabilities of all predecessors of the splitter of entering the splitter in one
|
|
// step. To directly separate the states having a transition into the splitter from the ones who do not,
|
|
// we move the states to certain locations. That is, on encountering a predecessor of the splitter, it is
|
|
// moved to the beginning of its block. If the predecessor is in the splitter itself, we have to be a bit
|
|
// careful about where to move states.
|
|
//
|
|
// After this iteration, there may be states of the splitter whose predecessors have not yet been explored,
|
|
// so this needs to be done now.
|
|
//
|
|
// Finally, we use the information obtained in the first part for the actual splitting process in which all
|
|
// predecessor blocks of the splitter are split based on the probabilities computed earlier.
|
|
std::list<Block<BlockDataType>*> predecessorBlocks;
|
|
storm::storage::sparse::state_type currentPosition = splitter.getBeginIndex();
|
|
bool splitterIsPredecessorBlock = false;
|
|
for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt, ++currentPosition) {
|
|
storm::storage::sparse::state_type currentState = *splitterIt;
|
|
|
|
uint_fast64_t elementsToSkip = 0;
|
|
for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) {
|
|
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
|
|
storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor);
|
|
Block<BlockDataType>& predecessorBlock = this->partition.getBlock(predecessor);
|
|
|
|
// If the block does not need to be refined, we skip it.
|
|
if (!possiblyNeedsRefinement(predecessorBlock)) {
|
|
continue;
|
|
}
|
|
|
|
// If we are computing a weak bisimulation on CTMCs and the predecessor block is the splitter, we
|
|
// need to ignore it and proceed to the next predecessor.
|
|
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Ctmc && predecessorBlock == splitter) {
|
|
continue;
|
|
}
|
|
|
|
// We keep track of the probability of the predecessor moving to the splitter.
|
|
increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue());
|
|
|
|
// We only need to move the predecessor if its not already known as a predecessor already.
|
|
if (predecessorPosition >= predecessorBlock.data().marker1()) {
|
|
// If the predecessor block is not the splitter, we can move the state easily.
|
|
if (predecessorBlock != splitter) {
|
|
moveStateToMarker1(predecessor, predecessorBlock);
|
|
} else {
|
|
// If the predecessor is in the splitter, we need to be a bit more careful.
|
|
splitterIsPredecessorBlock = true;
|
|
moveStateInSplitter(predecessor, predecessorBlock, currentPosition, elementsToSkip);
|
|
}
|
|
|
|
insertIntoPredecessorList(predecessorBlock, predecessorBlocks);
|
|
}
|
|
}
|
|
|
|
// If, as a consequence of shifting states, we need to skip some elements, do so now.
|
|
splitterIt += elementsToSkip;
|
|
currentPosition += elementsToSkip;
|
|
}
|
|
|
|
// If the splitter was a predecessor block of itself, we potentially need to explore some states that have
|
|
// not been explored yet.
|
|
if (splitterIsPredecessorBlock) {
|
|
exploreRemainingStatesOfSplitter(splitter, predecessorBlocks);
|
|
}
|
|
|
|
// Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type.
|
|
if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) {
|
|
// In the case of CTMCs and weak bisimulation, we still call the "splitStrong" method, but we already have
|
|
// taken care of not adding the splitter to the predecessor blocks, so this is safe.
|
|
refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue);
|
|
} else {
|
|
// If the splitter is a predecessor of we can use the computed probabilities to update the silent
|
|
// probabilities.
|
|
if (splitterIsPredecessorBlock) {
|
|
updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(splitter);
|
|
}
|
|
|
|
refinePredecessorBlocksOfSplitterWeak(splitter, predecessorBlocks, splitterQueue);
|
|
}
|
|
}
|
|
|
|
template<typename ModelType>
|
|
void DeterministicModelBisimulationDecomposition<ModelType>::buildQuotient() {
|
|
// In order to create the quotient model, we need to construct
|
|
// (a) the new transition matrix,
|
|
// (b) the new labeling,
|
|
// (c) the new reward structures.
|
|
|
|
// Prepare a matrix builder for (a).
|
|
storm::storage::SparseMatrixBuilder<ValueType> builder(this->size(), this->size());
|
|
|
|
// Prepare the new state labeling for (b).
|
|
storm::models::sparse::StateLabeling newLabeling(this->size());
|
|
std::set<std::string> atomicPropositionsSet = this->options.respectedAtomicPropositions.get();
|
|
atomicPropositionsSet.insert("init");
|
|
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
|
|
for (auto const& ap : atomicPropositions) {
|
|
newLabeling.addLabel(ap);
|
|
}
|
|
|
|
// If the model had state rewards, we need to build the state rewards for the quotient as well.
|
|
boost::optional<std::vector<ValueType>> stateRewards;
|
|
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
|
|
stateRewards = std::vector<ValueType>(this->blocks.size());
|
|
}
|
|
|
|
// Now build (a) and (b) by traversing all blocks.
|
|
for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) {
|
|
auto const& block = this->blocks[blockIndex];
|
|
|
|
// Pick one representative state. For strong bisimulation it doesn't matter which state it is, because
|
|
// they all behave equally.
|
|
storm::storage::sparse::state_type representativeState = *block.begin();
|
|
|
|
// However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if
|
|
// there is any such state).
|
|
if (this->options.getType() == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) {
|
|
for (auto const& state : block) {
|
|
if (!isSilent(state)) {
|
|
representativeState = state;
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
|
|
Block<BlockDataType> const& oldBlock = this->partition.getBlock(representativeState);
|
|
|
|
// If the block is absorbing, we simply add a self-loop.
|
|
if (oldBlock.data().absorbing()) {
|
|
builder.addNextValue(blockIndex, blockIndex, storm::utility::one<ValueType>());
|
|
|
|
// If the block has a special representative state, we retrieve it now.
|
|
if (oldBlock.data().hasRepresentativeState()) {
|
|
representativeState = oldBlock.data().representativeState();
|
|
}
|
|
|
|
// 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 (this->model.getStateLabeling().getStateHasLabel(ap, representativeState)) {
|
|
newLabeling.addLabelToState(ap, blockIndex);
|
|
}
|
|
}
|
|
} else {
|
|
// Compute the outgoing transitions of the block.
|
|
std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
|
|
for (auto const& entry : this->model.getTransitionMatrix().getRow(representativeState)) {
|
|
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) {
|
|
continue;
|
|
}
|
|
|
|
auto probIterator = blockProbability.find(targetBlock);
|
|
if (probIterator != blockProbability.end()) {
|
|
probIterator->second += entry.getValue();
|
|
} else {
|
|
blockProbability[targetBlock] = entry.getValue();
|
|
}
|
|
}
|
|
|
|
// 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) {
|
|
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - getSilentProbability(representativeState)));
|
|
} else {
|
|
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
|
|
}
|
|
}
|
|
|
|
// Otherwise add all atomic propositions to the equivalence class that the representative state
|
|
// satisfies.
|
|
for (auto const& ap : atomicPropositions) {
|
|
if (this->model.getStateLabeling().getStateHasLabel(ap, representativeState)) {
|
|
newLabeling.addLabelToState(ap, blockIndex);
|
|
}
|
|
}
|
|
}
|
|
|
|
// If the model has state rewards, we simply copy the state reward of the representative state, because
|
|
// all states in a block are guaranteed to have the same state reward.
|
|
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
|
|
typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
|
|
stateRewards.get()[blockIndex] = nameRewardModelPair->second.getStateRewardVector()[representativeState];
|
|
}
|
|
}
|
|
|
|
// Now check which of the blocks of the partition contain at least one initial state.
|
|
for (auto initialState : this->model.getInitialStates()) {
|
|
Block<BlockDataType> const& initialBlock = this->partition.getBlock(initialState);
|
|
newLabeling.addLabelToState("init", initialBlock.getId());
|
|
}
|
|
|
|
// Construct the reward model mapping.
|
|
std::unordered_map<std::string, typename ModelType::RewardModelType> rewardModels;
|
|
if (this->options.getKeepRewards() && this->model.hasRewardModel()) {
|
|
typename std::unordered_map<std::string, typename ModelType::RewardModelType>::const_iterator nameRewardModelPair = this->model.getUniqueRewardModel();
|
|
rewardModels.insert(std::make_pair(nameRewardModelPair->first, typename ModelType::RewardModelType(stateRewards)));
|
|
}
|
|
|
|
// Finally construct the quotient model.
|
|
this->quotient = std::shared_ptr<ModelType>(new ModelType(builder.build(), std::move(newLabeling), std::move(rewardModels)));
|
|
}
|
|
|
|
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
|
|
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
|
|
|
|
#ifdef STORM_HAVE_CARL
|
|
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>>;
|
|
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>>;
|
|
|
|
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
|
|
template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
|
|
#endif
|
|
}
|
|
}
|