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

Fixed some issues in bisimulation and added some tests. 

Former-commit-id: 98801de9db
main
dehnert 11 years ago
parent
f8a06b69f5
commit
370a0ae476
7 changed files with 134 additions and 43 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/exceptions/BaseException.cpp
  2. 2
      src/settings/OptionBuilder.h
  3. 76
      src/storage/DeterministicModelBisimulationDecomposition.cpp
  4. 26
      src/storage/DeterministicModelBisimulationDecomposition.h
  5. 2
      src/storage/StateBlock.h
  6. 2
      src/utility/cli.h
  7. 67
      test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp

2
src/exceptions/BaseException.cpp
View File

@ -18,7 +18,7 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
const char* BaseException::what() const {
const char* BaseException::what() const noexcept {
std::string errorString = this->stream.str(); std::string errorString = this->stream.str();
char* result = new char[errorString.size() + 1]; char* result = new char[errorString.size() + 1];
result[errorString.size()] = '\0'; result[errorString.size()] = '\0';

2
src/settings/OptionBuilder.h
View File

@ -68,7 +68,7 @@ namespace storm {
*/ */
OptionBuilder& addArgument(std::shared_ptr<ArgumentBase> argument) { OptionBuilder& addArgument(std::shared_ptr<ArgumentBase> argument) {
STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option."); STORM_LOG_THROW(!this->isBuild, storm::exceptions::IllegalFunctionCallException, "Cannot add an argument to an option builder that was already used to build the option.");
STORM_LOG_THROW(this->arguments.empty() || !argument->getIsOptional() || this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
STORM_LOG_THROW(this->arguments.empty() || argument->getIsOptional() || !this->arguments.back()->getIsOptional(), storm::exceptions::IllegalArgumentException, "Unable to add non-optional argument after an option that is optional.");
std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName()); std::string lowerArgumentName = boost::algorithm::to_lower_copy(argument->getName());
STORM_LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name."); STORM_LOG_THROW(argumentNameSet.find(lowerArgumentName) == argumentNameSet.end(), storm::exceptions::IllegalArgumentException, "Unable to add argument to option, because it already has an argument with the same name.");

76
src/storage/DeterministicModelBisimulationDecomposition.cpp
View File

@ -13,10 +13,7 @@ namespace storm {
namespace storage { namespace storage {
template<typename ValueType> template<typename ValueType>
std::size_t DeterministicModelBisimulationDecomposition<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, 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) {
DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(id), label(label) {
if (next != nullptr) { if (next != nullptr) {
next->prev = this; next->prev = this;
} }
@ -247,7 +244,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
// Create the block and give it an iterator to itself. // 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);
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr, this->blocks.size());
it->setIterator(it); it->setIterator(it);
// Set up the different parts of the internal structure. // Set up the different parts of the internal structure.
@ -265,7 +262,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
DeterministicModelBisimulationDecomposition<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, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { DeterministicModelBisimulationDecomposition<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, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, this->blocks.size());
Block& firstBlock = *firstIt; Block& firstBlock = *firstIt;
firstBlock.setIterator(firstIt); firstBlock.setIterator(firstIt);
@ -278,7 +275,7 @@ namespace storm {
} }
firstBlock.setAbsorbing(true); 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)));
typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, this->blocks.size(), std::shared_ptr<std::string>(new std::string(prob1Label)));
Block& secondBlock = *secondIt; Block& secondBlock = *secondIt;
secondBlock.setIterator(secondIt); secondBlock.setIterator(secondIt);
@ -290,7 +287,7 @@ namespace storm {
} }
secondBlock.setAbsorbing(true); 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)));
typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, this->blocks.size(), otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
Block& thirdBlock = *thirdIt; Block& thirdBlock = *thirdIt;
thirdBlock.setIterator(thirdIt); thirdBlock.setIterator(thirdIt);
@ -411,7 +408,7 @@ namespace storm {
} }
// Actually create the new block and insert it at the correct position. // 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, block.getLabelPtr());
typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, this->blocks.size(), block.getLabelPtr());
selfIt->setIterator(selfIt); selfIt->setIterator(selfIt);
Block& newBlock = *selfIt; Block& newBlock = *selfIt;
@ -435,7 +432,7 @@ namespace storm {
} }
// Actually insert the new block. // Actually insert the new block.
typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block);
typename std::list<Block>::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block, this->blocks.size());
Block& newBlock = *it; Block& newBlock = *it;
newBlock.setIterator(it); newBlock.setIterator(it);
@ -563,9 +560,16 @@ namespace storm {
} }
std::cout << std::endl << "state to block mapping: " << std::endl; std::cout << std::endl << "state to block mapping: " << std::endl;
for (auto const& block : stateToBlockMapping) { for (auto const& block : stateToBlockMapping) {
std::cout << block << " ";
std::cout << block << "[" << block->getId() <<"] ";
} }
std::cout << std::endl; std::cout << std::endl;
if (this->keepSilentProbabilities) {
std::cout << "silent probabilities" << std::endl;
for (auto const& prob : silentProbabilities) {
std::cout << prob << " ";
}
std::cout << std::endl;
}
std::cout << "size: " << this->blocks.size() << std::endl; std::cout << "size: " << this->blocks.size() << std::endl;
assert(this->check()); assert(this->check());
} }
@ -576,21 +580,21 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator() {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool weak, bool buildQuotient) : comparator() {
STORM_LOG_THROW(!model.hasStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions);
partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); 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(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType);
partitionRefinement(model, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, bisimulationType, atomicPropositions);
partitionRefinement(model, atomicPropositions, backwardTransitions, initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
@ -600,7 +604,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong; BisimulationType bisimulationType = weak ? BisimulationType::WeakDtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded); Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
@ -610,7 +614,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions(); storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong; BisimulationType bisimulationType = weak ? BisimulationType::WeakCtmc : BisimulationType::Strong;
Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded); Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bisimulationType, bounded);
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
partitionRefinement(model, std::set<std::string>({phiLabel, psiLabel}), model.getBackwardTransitions(), initialPartition, bisimulationType, buildQuotient);
} }
template<typename ValueType> template<typename ValueType>
@ -621,7 +625,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) {
void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType) {
// In order to create the quotient model, we need to construct // In order to create the quotient model, we need to construct
// (a) the new transition matrix, // (a) the new transition matrix,
// (b) the new labeling, // (b) the new labeling,
@ -632,7 +636,8 @@ namespace storm {
// Prepare the new state labeling for (b). // Prepare the new state labeling for (b).
storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
std::set<std::string> atomicPropositionsSet = selectedAtomicPropositions ? selectedAtomicPropositions.get() : model.getStateLabeling().getAtomicPropositions();
atomicPropositionsSet.insert("init");
std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
for (auto const& ap : atomicPropositions) { for (auto const& ap : atomicPropositions) {
newLabeling.addAtomicProposition(ap); newLabeling.addAtomicProposition(ap);
@ -646,7 +651,8 @@ namespace storm {
// they all behave equally. // they all behave equally.
storm::storage::sparse::state_type representativeState = *block.begin(); storm::storage::sparse::state_type representativeState = *block.begin();
// However, for weak bisimulation, we need to make sure the representative state is a non-silent one.
// However, for weak bisimulation, we need to make sure the representative state is a non-silent one (if
// there is any such state).
if (bisimulationType == BisimulationType::WeakDtmc) { if (bisimulationType == BisimulationType::WeakDtmc) {
for (auto const& state : block) { for (auto const& state : block) {
if (!partition.isSilent(state, comparator)) { if (!partition.isSilent(state, comparator)) {
@ -731,7 +737,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue. // Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
@ -769,7 +775,7 @@ namespace storm {
// If we are required to build the quotient model, do so now. // If we are required to build the quotient model, do so now.
if (buildQuotient) { if (buildQuotient) {
this->buildQuotient(model, partition, bisimulationType);
this->buildQuotient(model, atomicPropositions, partition, bisimulationType);
} }
std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
@ -1265,13 +1271,23 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
template<typename ModelType> template<typename ModelType>
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType) {
typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType, boost::optional<std::set<std::string>> const& atomicPropositions) {
Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc); Partition partition(model.getNumberOfStates(), bisimulationType == BisimulationType::WeakDtmc);
for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
if (label == "init") {
continue;
if (atomicPropositions) {
for (auto const& label : atomicPropositions.get()) {
if (label == "init") {
continue;
}
partition.splitLabel(model.getLabeledStates(label));
}
} else {
for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
if (label == "init") {
continue;
}
partition.splitLabel(model.getLabeledStates(label));
} }
partition.splitLabel(model.getLabeledStates(label));
} }
// If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent

26
src/storage/DeterministicModelBisimulationDecomposition.h
View File

@ -25,19 +25,23 @@ namespace storm {
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
* *
* @param model The model to decompose. * @param model The model to decompose.
* @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
* model will be respected. If built, the quotient model will only contain the respected atomic propositions.
* @param weak A flag indication whether a weak bisimulation is to be computed. * @param weak A flag indication whether a weak bisimulation is to be computed.
* @param buildQuotient Sets whether or not the quotient model is to be built. * @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);
DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool weak = false, bool buildQuotient = false);
/*! /*!
* Decomposes the given CTMC into equivalence classes under weak or strong bisimulation. * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation.
* *
* @param model The model to decompose. * @param model The model to decompose.
* @param A set of atomic propositions that is to be respected. If not given, all atomic propositions of the
* model will be respected. If built, the quotient model will only contain the respected atomic propositions.
* @param weak A flag indication whether a weak bisimulation is to be computed. * @param weak A flag indication whether a weak bisimulation is to be computed.
* @param buildQuotient Sets whether or not the quotient model is to be built. * @param buildQuotient Sets whether or not the quotient model is to be built.
*/ */
DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>(), bool weak = false, bool buildQuotient = false);
/*! /*!
* Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely * Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
@ -83,7 +87,7 @@ namespace storm {
typedef typename std::list<Block>::const_iterator const_iterator; typedef typename std::list<Block>::const_iterator const_iterator;
// Creates a new block with the given begin and end. // Creates a new block with the given begin and end.
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);
Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::size_t id, std::shared_ptr<std::string> const& label = nullptr);
// Prints the block. // Prints the block.
void print(Partition const& partition) const; void print(Partition const& partition) const;
@ -226,9 +230,6 @@ namespace storm {
// The label of the block or nullptr if it has none. // The label of the block or nullptr if it has none.
std::shared_ptr<std::string> label; std::shared_ptr<std::string> label;
// A counter for the IDs of the blocks.
static std::size_t blockId;
}; };
class Partition { class Partition {
@ -394,6 +395,8 @@ namespace storm {
* getQuotient(). * getQuotient().
* *
* @param model The model on whose state space to compute the coarses strong bisimulation relation. * @param model The model on whose state space to compute the coarses strong bisimulation relation.
* @param atomicPropositions The set of atomic propositions that the bisimulation considers. If not given,
* all atomic propositions are considered.
* @param backwardTransitions The backward transitions of the model. * @param backwardTransitions The backward transitions of the model.
* @param The initial partition. * @param The initial partition.
* @param bisimulationType The kind of bisimulation that is to be computed. * @param bisimulationType The kind of bisimulation that is to be computed.
@ -401,7 +404,7 @@ namespace storm {
* method. * method.
*/ */
template<typename ModelType> template<typename ModelType>
void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient);
void partitionRefinement(ModelType const& model, boost::optional<std::set<std::string>> const& atomicPropositions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient);
/*! /*!
* Refines the partition based on the provided splitter. After calling this method all blocks are stable * Refines the partition based on the provided splitter. After calling this method all blocks are stable
@ -445,12 +448,15 @@ namespace storm {
* *
* @param model The model whose state space was used for computing the equivalence classes. This is used for * @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. * determining the transitions of each equivalence class.
* @param selectedAtomicPropositions The set of atomic propositions that was considered by the bisimulation. The
* quotient will only have these atomic propositions. If not given, all atomic propositions will be
* considered.
* @param partition The previously computed partition. This is used for quickly retrieving the block of a * @param partition The previously computed partition. This is used for quickly retrieving the block of a
* state. * state.
* @param bisimulationType The kind of bisimulation that is to be computed. * @param bisimulationType The kind of bisimulation that is to be computed.
*/ */
template<typename ModelType> template<typename ModelType>
void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType);
void buildQuotient(ModelType const& model, boost::optional<std::set<std::string>> const& selectedAtomicPropositions, Partition const& partition, BisimulationType bisimulationType);
/*! /*!
* Creates the measure-driven initial partition for reaching psi states from phi states. * Creates the measure-driven initial partition for reaching psi states from phi states.
@ -474,10 +480,12 @@ namespace storm {
* @param model The model whose state space is partitioned based on its labels. * @param model The model whose state space is partitioned based on its labels.
* @param backwardTransitions The backward transitions of the model. * @param backwardTransitions The backward transitions of the model.
* @param bisimulationType The kind of bisimulation that is to be computed. * @param bisimulationType The kind of bisimulation that is to be computed.
* @param atomicPropositions The set of atomic propositions to respect. If not given, then all atomic
* propositions of the model are respected.
* @return The resulting partition. * @return The resulting partition.
*/ */
template<typename ModelType> template<typename ModelType>
Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType);
Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, BisimulationType bisimulationType, boost::optional<std::set<std::string>> const& atomicPropositions = boost::optional<std::set<std::string>>());
/*! /*!
* Splits all blocks of the given partition into a block that contains all divergent states and another block * Splits all blocks of the given partition into a block that contains all divergent states and another block

2
src/storage/StateBlock.h
View File

@ -10,7 +10,7 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
// Typedef the most common state container
// Typedef the most common state container.
typedef boost::container::flat_set<sparse::state_type> FlatSetStateContainer; typedef boost::container::flat_set<sparse::state_type> FlatSetStateContainer;
std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block); std::ostream& operator<<(std::ostream& out, FlatSetStateContainer const& block);

2
src/utility/cli.h
View File

@ -271,7 +271,7 @@ namespace storm {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>(); 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_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
result = bisimulationDecomposition.getQuotient(); result = bisimulationDecomposition.getQuotient();

67
test/functional/storage/DeterministicModelBisimulationDecompositionTest.cpp
View File

@ -0,0 +1,67 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "storage/DeterministicModelBisimulationDecomposition.h"
TEST(DeterministicModelBisimulationDecomposition, Die) {
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), false, true);
std::shared_ptr<storm::models::AbstractModel<double>> result;
ASSERT_NO_THROW(result = bisim.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(13, result->getNumberOfStates());
EXPECT_EQ(20, result->getNumberOfTransitions());
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"one"}), false, true);
ASSERT_NO_THROW(result = bisim2.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(5, result->getNumberOfStates());
EXPECT_EQ(8, result->getNumberOfTransitions());
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"one"}), true, true);
ASSERT_NO_THROW(result = bisim3.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(5, result->getNumberOfStates());
EXPECT_EQ(8, result->getNumberOfTransitions());
// std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
//
// ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
// std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
}
TEST(DeterministicModelBisimulationDecomposition, Crowds) {
std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim(*dtmc, boost::optional<std::set<std::string>>(), false, true);
std::shared_ptr<storm::models::AbstractModel<double>> result;
ASSERT_NO_THROW(result = bisim.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(334, result->getNumberOfStates());
EXPECT_EQ(546, result->getNumberOfTransitions());
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim2(*dtmc, std::set<std::string>({"observe0Greater1"}), false, true);
ASSERT_NO_THROW(result = bisim2.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(65, result->getNumberOfStates());
EXPECT_EQ(105, result->getNumberOfTransitions());
storm::storage::DeterministicModelBisimulationDecomposition<double> bisim3(*dtmc, std::set<std::string>({"observe0Greater1"}), true, true);
ASSERT_NO_THROW(result = bisim3.getQuotient());
EXPECT_EQ(storm::models::DTMC, result->getType());
EXPECT_EQ(43, result->getNumberOfStates());
EXPECT_EQ(83, result->getNumberOfTransitions());
}
Write Preview
Loading…
Cancel
Save