diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h
index 229ccfe9e..b3c1f1ef1 100644
--- a/src/models/Ctmc.h
+++ b/src/models/Ctmc.h
@@ -36,8 +36,9 @@ public:
* propositions to each state.
*/
Ctmc(storm::storage::SparseMatrix<T> const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling,
- boost::optional<std::vector<T>> const& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix,
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+ boost::optional<std::vector<T>> const& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+ boost::optional<storm::storage::SparseMatrix<T>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
// Intentionally left empty.
}
@@ -51,8 +52,9 @@ public:
* propositions to each state.
*/
Ctmc(storm::storage::SparseMatrix<T>&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling,
- boost::optional<std::vector<T>>&& optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix,
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+ boost::optional<std::vector<T>>&& optionalStateRewardVector = boost::optional<std::vector<T>>(),
+ boost::optional<storm::storage::SparseMatrix<T>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<T>>(),
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>())
// The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class
: AbstractDeterministicModel<T>(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
std::move(optionalChoiceLabeling)) {
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
similarity index 57%
rename from src/storage/DeterministicModelBisimulationDecomposition.cpp
rename to src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index d9023d153..93433d19f 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -1,19 +1,21 @@
-#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
#include <algorithm>
#include <unordered_map>
#include <chrono>
#include <iomanip>
+#include "src/utility/graph.h"
#include "src/exceptions/IllegalFunctionCallException.h"
namespace storm {
namespace storage {
- static std::size_t globalId = 0;
+ template<typename ValueType>
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::blockId = 0;
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), id(globalId++) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) {
if (next != nullptr) {
next->prev = this;
}
@@ -23,7 +25,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl;
std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
std::cout << "states:" << std::endl;
@@ -42,33 +44,33 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
this->begin = begin;
this->markedPosition = begin;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
this->end = end;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementBegin() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementBegin() {
++this->begin;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::decrementEnd() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::decrementEnd() {
++this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getBegin() const {
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getBegin() const {
return this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
if (this->hasPreviousBlock()) {
return this->getPreviousBlock().getEnd();
} else {
@@ -77,72 +79,72 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getEnd() const {
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getEnd() const {
return this->end;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setIterator(const_iterator it) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setIterator(const_iterator it) {
this->selfIt = it;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getIterator() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getIterator() const {
return this->selfIt;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
return this->getNextBlock().getIterator();
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
return this->getPreviousBlock().getIterator();
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() {
return *this->next;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
return *this->next;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
return this->next != nullptr;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
return *this->prev;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
return this->prev;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
return this->next;
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
return *this->prev;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
return this->prev != nullptr;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::check() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
if (this->begin >= this->end) {
assert(false);
}
@@ -156,68 +158,94 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
// We need to take the original begin here, because the begin is temporarily moved.
return (this->end - this->getOriginalBegin());
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
return this->markedAsSplitter;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
this->markedAsSplitter = true;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
this->markedAsSplitter = false;
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getId() const {
return this->id;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setAbsorbing(bool absorbing) {
+ this->absorbing = absorbing;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isAbsorbing() const {
+ return this->absorbing;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
return this->markedPosition;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
this->markedPosition = position;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
this->markedPosition = this->begin;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
++this->markedPosition;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
this->markedAsPredecessorBlock = true;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
this->markedAsPredecessorBlock = false;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
return markedAsPredecessorBlock;
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasLabel() const {
+ return this->label != nullptr;
+ }
+
+ template<typename ValueType>
+ std::string const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabel() const {
+ STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none.");
+ return *this->label;
+ }
+
+ template<typename ValueType>
+ std::shared_ptr<std::string> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
+ return this->label;
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
// Create the block and give it an iterator to itself.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
it->setIterator(it);
@@ -231,14 +259,54 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) {
+ typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
+ Block& firstBlock = *firstIt;
+ firstBlock.setIterator(firstIt);
+
+ storm::storage::sparse::state_type position = 0;
+ for (auto state : prob0States) {
+ states[position] = state;
+ positions[state] = position;
+ stateToBlockMapping[state] = &firstBlock;
+ ++position;
+ }
+ firstBlock.setAbsorbing(true);
+
+ typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr<std::string>(new std::string(prob1Label)));
+ Block& secondBlock = *secondIt;
+ secondBlock.setIterator(secondIt);
+
+ for (auto state : prob1States) {
+ states[position] = state;
+ positions[state] = position;
+ stateToBlockMapping[state] = &secondBlock;
+ ++position;
+ }
+ secondBlock.setAbsorbing(true);
+
+ typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
+ Block& thirdBlock = *thirdIt;
+ thirdBlock.setIterator(thirdIt);
+
+ storm::storage::BitVector otherStates = ~(prob0States | prob1States);
+ for (auto state : otherStates) {
+ states[position] = state;
+ positions[state] = position;
+ stateToBlockMapping[state] = &thirdBlock;
+ ++position;
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::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->values[this->positions[state1]], this->values[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::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];
@@ -250,94 +318,99 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
+ storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
return this->positions[state];
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
this->positions[state] = position;
}
template<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
+ storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
return this->states[position];
}
template<typename ValueType>
- ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
+ ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
return this->values[this->positions[state]];
}
template<typename ValueType>
- ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
+ ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
return this->values[position];
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] = value;
}
template<typename ValueType>
- std::vector<ValueType>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValues() {
+ std::vector<ValueType>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValues() {
return this->values;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
this->values[this->positions[state]] += value;
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator last) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& 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] = █
}
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getFirstBlock() {
+ return *this->blocks.begin();
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
+ std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) {
+ std::vector<storm::storage::sparse::state_type>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) {
return this->states.begin() + block.getEnd();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) const {
+ std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfStates(Block const& block) const {
return this->states.begin() + block.getBegin();
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) const {
+ std::vector<storm::storage::sparse::state_type>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfStates(Block const& block) const {
return this->states.begin() + block.getEnd();
}
template<typename ValueType>
- typename std::vector<ValueType>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBeginOfValues(Block const& block) {
+ typename std::vector<ValueType>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBeginOfValues(Block const& block) {
return this->values.begin() + block.getBegin();
}
template<typename ValueType>
- typename std::vector<ValueType>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEndOfValues(Block const& block) {
+ typename std::vector<ValueType>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEndOfValues(Block const& block) {
return this->values.begin() + block.getEnd();
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
// FIXME: this could be improved by splitting off the smaller of the two resulting blocks.
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
@@ -347,7 +420,7 @@ namespace storm {
}
// Actually create the new block and insert it at the correct position.
- typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block);
+ typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
selfIt->setIterator(selfIt);
Block& newBlock = *selfIt;
@@ -363,7 +436,7 @@ namespace storm {
}
template<typename ValueType>
- typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
// Find the beginning of the new block.
storm::storage::sparse::state_type begin;
if (block.hasPreviousBlock()) {
@@ -386,7 +459,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
Block& block = *blockIterator;
@@ -414,22 +487,22 @@ namespace storm {
}
template<typename ValueType>
- std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block> const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
+ std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
return this->blocks;
}
template<typename ValueType>
- std::vector<storm::storage::sparse::state_type>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getStates() {
+ std::vector<storm::storage::sparse::state_type>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getStates() {
return this->states;
}
template<typename ValueType>
- std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() {
+ std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() {
return this->blocks;
}
template<typename ValueType>
- bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::check() const {
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::check() const {
for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
if (this->states[this->positions[state]] != state) {
assert(false);
@@ -447,7 +520,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::Partition::print() const {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::print() const {
for (auto const& block : this->blocks) {
block.print(*this);
}
@@ -469,24 +542,49 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Partition::size() const {
+ std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::size() const {
return this->blocks.size();
}
template<typename ValueType>
- DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& dtmc, bool weak, bool buildQuotient) {
- STORM_LOG_THROW(!dtmc.hasStateRewards() && !dtmc.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- computeBisimulationEquivalenceClasses(dtmc, weak, buildQuotient);
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, 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);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, 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);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
}
template<typename ValueType>
- std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelBisimulationDecomposition<ValueType>::getQuotient() const {
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelStrongBisimulationDecomposition<ValueType>::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 ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(storm::models::Dtmc<ValueType> const& dtmc, Partition const& partition) {
+ template<typename ModelType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
@@ -496,8 +594,8 @@ namespace storm {
storm::storage::SparseMatrixBuilder<ValueType> builder(this->size(), this->size());
// Prepare the new state labeling for (b).
- storm::models::AtomicPropositionsLabeling newLabeling(this->size(), dtmc.getStateLabeling().getNumberOfAtomicPropositions());
- std::set<std::string> atomicPropositionsSet = dtmc.getStateLabeling().getAtomicPropositions();
+ storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
+ std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) {
newLabeling.addAtomicProposition(ap);
@@ -510,33 +608,50 @@ namespace storm {
// Pick one representative state. It doesn't matter which state it is, because they all behave equally.
storm::storage::sparse::state_type representativeState = *block.begin();
- // Compute the outgoing transitions of the block.
- std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
- for (auto const& entry : dtmc.getTransitionMatrix().getRow(representativeState)) {
- storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId();
- 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) {
- builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
- }
+ Block const& oldBlock = partition.getBlock(representativeState);
- // Add all atomic propositions to the equivalence class that the representative state satisfies.
- for (auto const& ap : atomicPropositions) {
- if (dtmc.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
- newLabeling.addAtomicPropositionToState(ap, blockIndex);
+ // If the block is absorbing, we simply add a self-loop.
+ if (oldBlock.isAbsorbing()) {
+ builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne<ValueType>());
+
+ if (oldBlock.hasLabel()) {
+ newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
+ }
+ } else {
+ // Compute the outgoing transitions of the block.
+ std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
+ for (auto const& entry : model.getTransitionMatrix().getRow(representativeState)) {
+ storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId();
+ 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) {
+ builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
+ }
+
+ // If the block has a special label, we only add that to the block.
+ if (oldBlock.hasLabel()) {
+ newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
+ } else {
+ // Otherwise add all atomic propositions to the equivalence class that the representative state
+ // satisfies.
+ for (auto const& ap : atomicPropositions) {
+ if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ newLabeling.addAtomicPropositionToState(ap, blockIndex);
+ }
+ }
}
}
}
// Now check which of the blocks of the partition contain at least one initial state.
- for (auto initialState : dtmc.getInitialStates()) {
+ for (auto initialState : model.getInitialStates()) {
Block const& initialBlock = partition.getBlock(initialState);
newLabeling.addAtomicPropositionToState("init", initialBlock.getId());
}
@@ -545,33 +660,21 @@ namespace storm {
// If reward structures are allowed, the quotient structures need to be built here.
// Finally construct the quotient model.
- this->quotient = std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>>(new storm::models::Dtmc<ValueType>(builder.build(), std::move(newLabeling)));
+ this->quotient = std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>>(new ModelType(builder.build(), std::move(newLabeling)));
}
template<typename ValueType>
- void DeterministicModelBisimulationDecomposition<ValueType>::computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& dtmc, bool weak, bool buildQuotient) {
+ template<typename ModelType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
- // We start by computing the initial partition.
- Partition partition(dtmc.getNumberOfStates());
- for (auto const& label : dtmc.getStateLabeling().getAtomicPropositions()) {
- if (label == "init") {
- continue;
- }
- partition.splitLabel(dtmc.getLabeledStates(label));
- }
-
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
- // FIXME: if weak is set, we want to eliminate the self-loops before doing bisimulation.
-
- storm::storage::SparseMatrix<ValueType> backwardTransitions = dtmc.getBackwardTransitions();
-
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
- splitPartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
+ refinePartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
splitterQueue.pop_front();
}
@@ -579,12 +682,14 @@ namespace storm {
// a way that maintains the block IDs as indices.
this->blocks.resize(partition.size());
for (auto const& block : partition.getBlocks()) {
+ // We need to sort the states to allow for rapid construction of the blocks.
+ std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block));
this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block), true);
}
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
- this->buildQuotient(dtmc, partition);
+ this->buildQuotient(model, partition);
}
std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart;
@@ -595,7 +700,7 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
// Sort the states in the block based on their probabilities.
std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } );
@@ -615,8 +720,7 @@ 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.
- std::size_t createdBlocks = 0;
- while (std::abs(partition.getValueAtPosition(beginIndex) - partition.getValueAtPosition(endIndex - 1)) >= 1e-6) {
+ while (!comparator.isEqual(partition.getValueAtPosition(beginIndex), partition.getValueAtPosition(endIndex - 1))) {
// Now we scan for the first state in the block that disagrees on the probability value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
@@ -624,13 +728,12 @@ namespace storm {
typename std::vector<ValueType>::const_iterator valueIterator = partition.getValues().begin() + beginIndex + 1;
++currentIndex;
- while (currentIndex < endIndex && std::abs(*valueIterator - currentValue) <= 1e-6) {
+ while (currentIndex < endIndex && comparator.isEqual(*valueIterator, currentValue)) {
++valueIterator;
++currentIndex;
}
// Now we split the block and mark it as a potential splitter.
- ++createdBlocks;
Block& newBlock = partition.splitBlock(block, currentIndex);
if (!newBlock.isMarkedAsSplitter()) {
splitterQueue.push_back(&newBlock);
@@ -638,12 +741,10 @@ namespace storm {
}
beginIndex = currentIndex;
}
-
- return createdBlocks;
}
template<typename ValueType>
- std::size_t DeterministicModelBisimulationDecomposition<ValueType>::splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
@@ -658,7 +759,7 @@ namespace storm {
Block& predecessorBlock = partition.getBlock(predecessor);
// If the predecessor block has just one state, there is no point in splitting it.
- if (predecessorBlock.getNumberOfStates() <= 1) {
+ if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) {
continue;
}
@@ -773,12 +874,31 @@ namespace storm {
continue;
}
- splitBlockProbabilities(*blockPtr, partition, splitterQueue);
+ refineBlockProbabilities(*blockPtr, partition, splitterQueue);
}
-
- return 0;
}
- template class DeterministicModelBisimulationDecomposition<double>;
+ template<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel));
+ Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel);
+ return partition;
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model) {
+ Partition partition(model.getNumberOfStates());
+ for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(model.getLabeledStates(label));
+ }
+ return partition;
+ }
+
+ template class DeterministicModelStrongBisimulationDecomposition<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
similarity index 56%
rename from src/storage/DeterministicModelBisimulationDecomposition.h
rename to src/storage/DeterministicModelStrongBisimulationDecomposition.h
index c1ca37c18..e5ac547db 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_
+#ifndef STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_
+#define STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_
#include <queue>
#include <deque>
@@ -7,21 +7,59 @@
#include "src/storage/sparse/StateType.h"
#include "src/storage/Decomposition.h"
#include "src/models/Dtmc.h"
+#include "src/models/Ctmc.h"
#include "src/storage/Distribution.h"
+#include "src/utility/ConstantsComparator.h"
+#include "src/utility/OsDetection.h"
namespace storm {
namespace storage {
/*!
- * This class represents the decomposition model into its bisimulation quotient.
+ * This class represents the decomposition model into its (strong) bisimulation quotient.
*/
template <typename ValueType>
- class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
+ class DeterministicModelStrongBisimulationDecomposition : public Decomposition<StateBlock> {
public:
/*!
- * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
+ * Decomposes the given DTMC into equivalence classes under strong bisimulation.
+ *
+ * @param model The model to decompose.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
+ */
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool buildQuotient = false);
+
+ /*!
+ * Decomposes the given CTMC into equivalence classes under strong bisimulation.
+ *
+ * @param model The model to decompose.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
+ */
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool buildQuotient = false);
+
+ /*!
+ * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
+ * preserves formulas of the form phi until psi.
+ *
+ * @param model The model to decompose.
+ * @param phiLabel The label that all phi states carry in the model.
+ * @param psiLabel The label that all psi states carry in the model.
+ * @param bounded If set to true, also bounded until formulas are preserved.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
*/
- DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
+
+ /*!
+ * Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely
+ * preserves formulas of the form phi until psi.
+ *
+ * @param model The model to decompose.
+ * @param phiLabel The label that all phi states carry in the model.
+ * @param psiLabel The label that all psi states carry in the model.
+ * @param bounded If set to true, also bounded until formulas are preserved.
+ * @param buildQuotient Sets whether or not the quotient model is to be built.
+ */
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
/*!
* Retrieves the quotient of the model under the previously computed bisimulation.
@@ -37,7 +75,7 @@ namespace storm {
public:
typedef typename std::list<Block>::const_iterator const_iterator;
- Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next);
+ Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label = nullptr);
// Prints the block.
void print(Partition const& partition) const;
@@ -138,6 +176,21 @@ namespace storm {
// Removes the marking.
void unmarkAsPredecessorBlock();
+ // Sets whether or not the block is to be interpreted as absorbing.
+ void setAbsorbing(bool absorbing);
+
+ // Retrieves whether the block is to be interpreted as absorbing.
+ bool isAbsorbing() const;
+
+ // Retrieves whether the block has a special label.
+ bool hasLabel() const;
+
+ // Retrieves the special label of the block if it has one.
+ std::string const& getLabel() const;
+
+ // Retrieves a pointer to the label of the block (which is the nullptr if there is none).
+ std::shared_ptr<std::string> const& getLabelPtr() const;
+
private:
// An iterator to itself. This is needed to conveniently insert elements in the overall list of blocks
// kept by the partition.
@@ -160,8 +213,17 @@ namespace storm {
// A position that can be used to store a certain position within the block.
storm::storage::sparse::state_type markedPosition;
+ // A flag indicating whether the block is to be interpreted as absorbing or not.
+ bool absorbing;
+
// The ID of the block. This is only used for debugging purposes.
std::size_t id;
+
+ // The label of the block or nullptr if it has none.
+ std::shared_ptr<std::string> label;
+
+ // A counter for the IDs of the blocks.
+ static std::size_t blockId;
};
class Partition {
@@ -170,8 +232,31 @@ namespace storm {
/*!
* Creates a partition with one block consisting of all the states.
+ *
+ * @param numberOfStates The number of states the partition holds.
*/
Partition(std::size_t numberOfStates);
+
+ /*!
+ * Creates a partition with three blocks: one with all phi states, one with all psi states and one with
+ * all other states. The former two blocks are marked as being absorbing, because their outgoing
+ * transitions shall not be taken into account for future refinement.
+ *
+ * @param numberOfStates The number of states the partition holds.
+ * @param prob0States The states which have probability 0 of satisfying phi until psi.
+ * @param prob1States The states which have probability 1 of satisfying phi until psi.
+ * @param otherLabel The label that is to be attached to all other states.
+ * @param prob1Label The label that is to be attached to all states with probability 1.
+ */
+ Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label);
+
+ Partition() = default;
+ Partition(Partition const& other) = default;
+ Partition& operator=(Partition const& other) = default;
+#ifndef WINDOWS
+ Partition(Partition&& other) = default;
+ Partition& operator=(Partition&& other) = default;
+#endif
/*!
* Splits all blocks of the partition such that afterwards all blocks contain only states with the label
@@ -262,6 +347,8 @@ namespace storm {
// Updates the block mapping for the given range of states to the specified block.
void updateBlockMapping(Block& block, std::vector<storm::storage::sparse::state_type>::iterator first, std::vector<storm::storage::sparse::state_type>::iterator end);
+ // Retrieves the first block of the partition.
+ Block& getFirstBlock();
private:
// The list of blocks in the partition.
std::list<Block> blocks;
@@ -280,18 +367,86 @@ namespace storm {
std::vector<ValueType> values;
};
- void computeBisimulationEquivalenceClasses(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient);
+ /*!
+ * Performs the partition refinement on the model and thereby computes the equivalence classes under strong
+ * bisimulation equivalence. If required, the quotient model is built and may be retrieved using
+ * getQuotient().
+ *
+ * @param model The model on whose state space to compute the coarses strong bisimulation relation.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param The initial partition.
+ * @param buildQuotient If set, the quotient model is built and may be retrieved using the getQuotient()
+ * method.
+ */
+ template<typename ModelType>
+ void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient);
- std::size_t splitPartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
+ /*!
+ * Refines the partition based on the provided splitter. After calling this method all blocks are stable
+ * with respect to the splitter.
+ *
+ * @param backwardTransitions A matrix that can be used to retrieve the predecessors (and their
+ * probabilities).
+ * @param splitter The splitter to use.
+ * @param partition The partition to split.
+ * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated
+ * as splitters in the future.
+ */
+ void refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
- std::size_t splitBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
+ /*!
+ * Refines the block based on their probability values (leading into the splitter).
+ *
+ * @param block The block to refine.
+ * @param partition The partition that contains the block.
+ * @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated
+ * as splitters in the future.
+ */
+ void refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
- void buildQuotient(storm::models::Dtmc<ValueType> const& dtmc, Partition const& partition);
+ /*!
+ * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
+ * of the decomposition.
+ *
+ * @param model The model whose state space was used for computing the equivalence classes. This is used for
+ * determining the transitions of each equivalence class.
+ * @param partition The previously computed partition. This is used for quickly retrieving the block of a
+ * state.
+ */
+ template<typename ModelType>
+ void buildQuotient(ModelType const& model, Partition const& partition);
+ /*!
+ * Creates the measure-driven initial partition for reaching psi states from phi states.
+ *
+ * @param model The model whose state space is partitioned based on reachability of psi states from phi
+ * states.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param phiLabel The label that all phi states carry in the model.
+ * @param psiLabel The label that all psi states carry in the model.
+ * @param bounded If set to true, the initial partition will be chosen in such a way that preserves bounded
+ * reachability queries.
+ * @return The resulting partition.
+ */
+ template<typename ModelType>
+ Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded = false);
+
+ /*!
+ * Creates the initial partition based on all the labels in the given model.
+ *
+ * @param model The model whose state space is partitioned based on its labels.
+ * @return The resulting partition.
+ */
+ template<typename ModelType>
+ Partition getLabelBasedInitialPartition(ModelType const& model);
+
// If required, a quotient model is built and stored in this member.
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> quotient;
+
+ // A comparator that is used for determining whether two probabilities are considered to be equal.
+ storm::utility::ConstantsComparator<ValueType> comparator;
};
}
}
-#endif /* STORM_STORAGE_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h
new file mode 100644
index 000000000..fc46b251f
--- /dev/null
+++ b/src/utility/ConstantsComparator.h
@@ -0,0 +1,84 @@
+#ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_
+#define STORM_UTILITY_CONSTANTSCOMPARATOR_H_
+
+#ifdef max
+# undef max
+#endif
+
+#ifdef min
+# undef min
+#endif
+
+#include <limits>
+#include <cstdint>
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+ namespace utility {
+
+ template<typename ValueType>
+ ValueType one() {
+ return ValueType(1);
+ }
+
+ template<typename ValueType>
+ ValueType zero() {
+ return ValueType(0);
+ }
+
+ template<typename ValueType>
+ ValueType infinity() {
+ return std::numeric_limits<ValueType>::infinity();
+ }
+
+ // A class that can be used for comparing constants.
+ template<typename ValueType>
+ class ConstantsComparator {
+ public:
+ bool isOne(ValueType const& value) {
+ return value == one<ValueType>();
+ }
+
+ bool isZero(ValueType const& value) {
+ return value == zero<ValueType>();
+ }
+
+ bool isEqual(ValueType const& value1, ValueType const& value2) {
+ return value1 == value2;
+ }
+ };
+
+ // For doubles we specialize this class and consider the comparison modulo some predefined precision.
+ template<>
+ class ConstantsComparator<double> {
+ public:
+ ConstantsComparator() : precision(storm::settings::generalSettings().getPrecision()) {
+ // Intentionally left empty.
+ }
+
+ ConstantsComparator(double precision) : precision(precision) {
+ // Intentionally left empty.
+ }
+
+ bool isOne(double const& value) {
+ return std::abs(value - one<double>()) <= precision;
+ }
+
+ bool isZero(double const& value) {
+ return std::abs(value) <= precision;
+ }
+
+ bool isEqual(double const& value1, double const& value2) {
+ return std::abs(value1 - value2) <= precision;
+ }
+
+ private:
+ // The precision used for comparisons.
+ double precision;
+ };
+
+ }
+}
+
+#endif /* STORM_UTILITY_CONSTANTSCOMPARATOR_H_ */
\ No newline at end of file
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 813a6fa74..908d7dc52 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -47,7 +47,7 @@ log4cplus::Logger logger;
// Headers for model processing.
#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
-#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
@@ -267,7 +267,7 @@ namespace storm {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, false, true);
+ storm::storage::DeterministicModelStrongBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, true);
result = bisimulationDecomposition.getQuotient();
@@ -285,7 +285,7 @@ namespace storm {
std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
- // FIXME: re-parse the program.
+ // FIXME: do not re-parse the program.
std::string const programFile = storm::settings::generalSettings().getSymbolicModelFilename();
std::string const constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
diff --git a/src/utility/graph.h b/src/utility/graph.h
index 21972adbc..3af235fe3 100644
--- a/src/utility/graph.h
+++ b/src/utility/graph.h
@@ -204,6 +204,25 @@ namespace storm {
return result;
}
+ /*!
+ * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
+ * deterministic model.
+ *
+ * @param backwardTransitions The backward transitions of the model whose graph structure to search.
+ * @param phiStates The set of all states satisfying phi.
+ * @param psiStates The set of all states satisfying psi.
+ * @return A pair of bit vectors such that the first bit vector stores the indices of all states
+ * with probability 0 and the second stores all indices of states with probability 1.
+ */
+ template <typename T>
+ static std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<T> backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> result;
+ result.first = performProbGreater0(backwardTransitions, phiStates, psiStates);
+ result.second = performProb1(backwardTransitions, phiStates, psiStates, result.first);
+ result.first.complement();
+ return result;
+ }
+
/*!
* Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least
* one possible resolution of non-determinism in a non-deterministic model. Stated differently,