From 5bc593174ed5d0fba93fe9742df69b6472dd298c Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Oct 2014 20:05:44 +0200 Subject: [PATCH] Further work on weak bisimulation. Former-commit-id: 3ad48ee0a353630c0d1cedf9c961cbda7e7e8e0a --- examples/dtmc/brp/brp.pm | 10 +++-- src/storage/BitVector.cpp | 4 ++ src/storage/BitVector.h | 9 +++++ ...icModelStrongBisimulationDecomposition.cpp | 39 ++++++++++++++----- 4 files changed, 48 insertions(+), 14 deletions(-) diff --git a/examples/dtmc/brp/brp.pm b/examples/dtmc/brp/brp.pm index f2eacc9ff..e09ed3e2c 100644 --- a/examples/dtmc/brp/brp.pm +++ b/examples/dtmc/brp/brp.pm @@ -127,8 +127,10 @@ module channelL // lost [TO_Ack] (l=2) -> (l'=0); -endmodule - -rewards - [aF] i=1 : 1; +endmodule + +rewards + [aF] i=1 : 1; endrewards + +label "target" = s=5; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index b1c5003ce..0fb08f028 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -144,6 +144,10 @@ namespace storm { return true; } + bool BitVector::operator!=(BitVector const& other) { + return !(*this == other); + } + void BitVector::set(uint_fast64_t index, bool value) { if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::set: written index " << index << " out of bounds."; uint_fast64_t bucket = index >> 6; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index f20c00005..806febcc9 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -135,9 +135,18 @@ namespace storm { * Compares the given bit vector with the current one. * * @param other The bitvector with which to compare the current one. + * @return True iff the other bit vector is semantically the same as the current one. */ bool operator==(BitVector const& other); + /*! + * Compares the given bit vector with the current one. + * + * @param other The bitvector with which to compare the current one. + * @return True iff the other bit vector is semantically not the same as the current one. + */ + bool operator!=(BitVector const& other); + /*! * Assigns the contents of the given bit vector to the current bit vector via a deep copy. * diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index 97f054f1b..fba714149 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -577,9 +577,6 @@ namespace storm { DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); Partition initialPartition = getLabelBasedInitialPartition(model, weak); - if (weak) { - this->initializeSilentProbabilities(model, initialPartition); - } partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient); } @@ -587,9 +584,6 @@ namespace storm { DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); Partition initialPartition = getLabelBasedInitialPartition(model, weak); - if (weak) { - this->initializeSilentProbabilities(model, initialPartition); - } partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient); } @@ -709,6 +703,8 @@ namespace storm { // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); + std::cout << "refining with splitter " << splitterQueue.front()->getId() << std::endl; + partition.print(); refinePartition(backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue); splitterQueue.pop_front(); } @@ -848,6 +844,15 @@ namespace storm { // labels and then scan for ranges that agree on the label. std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair const& a, std::pair const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; }); + for (auto const& label : stateLabels) { + std::cout << label << std::endl; + } + + std::cout << "sorted?" << std::endl; + for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) { + std::cout << stateLabels[partition.getPosition(it->first) - block.getBegin()] << std::endl; + } + // Update the positions vector. storm::storage::sparse::state_type position = block.getBegin(); for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { @@ -862,16 +867,16 @@ namespace storm { // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. - bool blockSplit = !comparator.isEqual(begin->second, end->second); - while (!comparator.isEqual(begin->second, end->second)) { + bool blockSplit = stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()]; + while (stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()]) { // Now we scan for the first state in the block that disagrees on the labeling value. // Note that we do not have to check currentIndex for staying within bounds, because we know the matching // state is within bounds. - ValueType const& currentValue = begin->second; + storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - block.getBegin()]; ++begin; ++currentIndex; - while (begin != end && comparator.isEqual(begin->second, currentValue)) { + while (begin != end && stateLabels[partition.getPosition(begin->first) - block.getBegin()] == currentValue) { ++begin; ++currentIndex; } @@ -879,6 +884,7 @@ namespace storm { // Now we split the block and mark it as a potential splitter. Block& newBlock = partition.splitBlock(block, currentIndex); if (!newBlock.isMarkedAsSplitter()) { + std::cout << "adding block " << newBlock.getId() << " as splitter" << std::endl; splitterQueue.push_back(&newBlock); newBlock.markAsSplitter(); } @@ -900,7 +906,9 @@ namespace storm { std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair& stateValuePair) { ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first); if (!comparator.isOne(silentProbability)) { + std::cout << "before: " << stateValuePair.second << std::endl; stateValuePair.second /= storm::utility::one() - silentProbability; + std::cout << "scaled: " << stateValuePair.second << std::endl; } }); @@ -1095,8 +1103,11 @@ namespace storm { // If the splitter is also the predecessor block, we must not refine it at this point. if (&block != &splitter) { + std::cout << "refining pred block " << block.getId() << std::endl; refineBlockWeak(block, partition, backwardTransitions, splitterQueue); } else { + Block& newBlock = partition.insertBlock(block); + // Restore the begin of the block. block.setBegin(block.getOriginalBegin()); } @@ -1125,6 +1136,14 @@ namespace storm { } partition.splitLabel(model.getLabeledStates(label)); } + + // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent + // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. + if (weak) { + // FIXME: split off divergent states. + + this->initializeSilentProbabilities(model, partition); + } return partition; }