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

Renamed some classes to indicate that only strong bisimulation can be computed. Added option to start with an initial partition that preserves only certain formulas. Added ConstantsComparator concept that is to be used when constants have to be compared with other constants. 

Former-commit-id: feacadfa38
main
dehnert 11 years ago
parent
6fa974dcb9
commit
1c091d7640
6 changed files with 523 additions and 143 deletions
Split View
  1. 10
      src/models/Ctmc.h
  2. 368
      src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
  3. 179
      src/storage/DeterministicModelStrongBisimulationDecomposition.h
  4. 84
      src/utility/ConstantsComparator.h
  5. 6
      src/utility/cli.h
  6. 19
      src/utility/graph.h

10
src/models/Ctmc.h
View File

@ -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)) {

368
src/storage/DeterministicModelBisimulationDecomposition.cpp → src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
View File

@ -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] = &block;
}
}
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>;
}
}

179
src/storage/DeterministicModelBisimulationDecomposition.h → src/storage/DeterministicModelStrongBisimulationDecomposition.h
View File

@ -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_ */
#endif /* STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ */

84
src/utility/ConstantsComparator.h
View File

@ -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_ */

6
src/utility/cli.h
View File

@ -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);

19
src/utility/graph.h
View File

@ -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,

Write Preview
|||||||
100:0
Loading…
Cancel
Save