From 97158ee72e3e8d9299a175de01a7b4c573aa85a5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 22 Oct 2014 20:24:50 +0200
Subject: [PATCH 1/8] Started on weak bisimulation.
Former-commit-id: 595caab54e045c513e24e7f06f3115ea01ce251d
---
...inisticModelStrongBisimulationDecomposition.cpp | 4 ++--
...rministicModelStrongBisimulationDecomposition.h | 14 ++++++++++++--
2 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index 1c11a8107..6c1e0e4a8 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -249,7 +249,7 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) {
+ DeterministicModelStrongBisimulationDecomposition<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.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
it->setIterator(it);
@@ -263,7 +263,7 @@ namespace storm {
}
template<typename ValueType>
- 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), statesAndValues(numberOfStates), positions(numberOfStates) {
+ 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, 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);
Block& firstBlock = *firstIt;
firstBlock.setIterator(firstIt);
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
index c2fdec62e..a29d2e82e 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
@@ -236,8 +236,9 @@ namespace storm {
* Creates a partition with one block consisting of all the states.
*
* @param numberOfStates The number of states the partition holds.
+ * @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked.
*/
- Partition(std::size_t numberOfStates);
+ Partition(std::size_t numberOfStates, bool keepSilentProbabilities = false);
/*!
* Creates a partition with three blocks: one with all phi states, one with all psi states and one with
@@ -249,8 +250,9 @@ namespace storm {
* @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.
+ * @param keepSilentProbabilities A flag indicating whether or not silent probabilities are to be tracked.
*/
- Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label);
+ 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 = false);
Partition() = default;
Partition(Partition const& other) = default;
@@ -342,6 +344,7 @@ namespace storm {
// Retrieves the first block of the partition.
Block& getFirstBlock();
+
private:
// The list of blocks in the partition.
std::list<Block> blocks;
@@ -355,6 +358,13 @@ namespace storm {
// This vector keeps track of the position of each state in the state vector.
std::vector<storm::storage::sparse::state_type> positions;
+
+ // A flag that indicates whether or not the vector with silent probabilities exists.
+ bool keepSilentProbabilities;
+
+ // This vector keeps track of the silent probabilities (i.e. the probabilities going into the very own
+ // equivalence class) of each state. This means that a state is silent iff its entry is non-zero.
+ std::vector<ValueType> silentProbabilities;
};
/*!
From 56aec18a48ea3d584b01672fd11b16e401a18517 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 23 Oct 2014 18:05:51 +0200
Subject: [PATCH 2/8] Added bisimulation settings. Further work on weak
bisimulation.
Former-commit-id: c04759575a5cb5a52dc49323debc893b4a1e552f
---
src/settings/SettingsManager.cpp | 5 +
src/settings/SettingsManager.h | 8 +
src/settings/modules/BisimulationSettings.cpp | 33 ++
src/settings/modules/BisimulationSettings.h | 50 +++
src/storage/BitVector.cpp | 25 +-
src/storage/BitVector.h | 10 +-
...icModelStrongBisimulationDecomposition.cpp | 364 +++++++++++++++---
...sticModelStrongBisimulationDecomposition.h | 57 ++-
src/utility/cli.h | 2 +-
9 files changed, 487 insertions(+), 67 deletions(-)
create mode 100644 src/settings/modules/BisimulationSettings.cpp
create mode 100644 src/settings/modules/BisimulationSettings.h
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 5c311c602..4c841acaa 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -24,6 +24,7 @@ namespace storm {
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::CuddSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GmmxxEquationSolverSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::NativeEquationSolverSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::BisimulationSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GlpkSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
}
@@ -495,6 +496,10 @@ namespace storm {
return dynamic_cast<storm::settings::modules::NativeEquationSolverSettings const&>(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName));
}
+ storm::settings::modules::BisimulationSettings const& bisimulationSettings() {
+ return dynamic_cast<storm::settings::modules::BisimulationSettings const&>(manager().getModule(storm::settings::modules::BisimulationSettings::moduleName));
+ }
+
storm::settings::modules::GlpkSettings const& glpkSettings() {
return dynamic_cast<storm::settings::modules::GlpkSettings const&>(manager().getModule(storm::settings::modules::GlpkSettings::moduleName));
}
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 3daa43beb..9d597ca2e 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -25,6 +25,7 @@
#include "src/settings/modules/CuddSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
+#include "src/settings/modules/BisimulationSettings.h"
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
@@ -286,6 +287,13 @@ namespace storm {
* @return An object that allows accessing the settings of the native equation solver.
*/
storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings();
+
+ /*!
+ * Retrieves the settings of the native equation solver.
+ *
+ * @return An object that allows accessing the settings of the native equation solver.
+ */
+ storm::settings::modules::BisimulationSettings const& bisimulationSettings();
/*!
* Retrieves the settings of glpk.
diff --git a/src/settings/modules/BisimulationSettings.cpp b/src/settings/modules/BisimulationSettings.cpp
new file mode 100644
index 000000000..d68337368
--- /dev/null
+++ b/src/settings/modules/BisimulationSettings.cpp
@@ -0,0 +1,33 @@
+#include "src/settings/modules/BisimulationSettings.h"
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string BisimulationSettings::moduleName = "bisimulation";
+ const std::string BisimulationSettings::typeOptionName = "type";
+
+ BisimulationSettings::BisimulationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+ std::vector<std::string> types = { "strong", "weak" };
+ this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used. Available are: { strong, weak }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("strong").build()).build());
+ }
+
+ bool BisimulationSettings::isStrongBisimulationSet() const {
+ if (this->getOption(typeOptionName).getArgumentByName("name").getValueAsString() == "strong") {
+ return true;
+ }
+ return false;
+ }
+
+ bool BisimulationSettings::isWeakBisimulationSet() const {
+ if (this->getOption(typeOptionName).getArgumentByName("name").getValueAsString() == "weak") {
+ return true;
+ }
+ return false;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/BisimulationSettings.h b/src/settings/modules/BisimulationSettings.h
new file mode 100644
index 000000000..2ff715122
--- /dev/null
+++ b/src/settings/modules/BisimulationSettings.h
@@ -0,0 +1,50 @@
+#ifndef STORM_SETTINGS_MODULES_BISIMULATIONSETTINGS_H_
+#define STORM_SETTINGS_MODULES_BISIMULATIONSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ /*!
+ * This class represents the bisimulation settings.
+ */
+ class BisimulationSettings : public ModuleSettings {
+ public:
+ // An enumeration of all available bisimulation types.
+ enum class BisimulationType { Strong, Weak };
+
+ /*!
+ * Creates a new set of bisimulation settings that is managed by the given manager.
+ *
+ * @param settingsManager The responsible manager.
+ */
+ BisimulationSettings(storm::settings::SettingsManager& settingsManager);
+
+ /*!
+ * Retrieves whether strong bisimulation is to be used.
+ *
+ * @return True iff strong bisimulation is to be used.
+ */
+ bool isStrongBisimulationSet() const;
+
+ /*!
+ * Retrieves whether weak bisimulation is to be used.
+ *
+ * @return True iff weak bisimulation is to be used.
+ */
+ bool isWeakBisimulationSet() const;
+
+ // The name of the module.
+ static const std::string moduleName;
+
+ private:
+ // Define the string names of the options as constants.
+ static const std::string typeOptionName;
+ };
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_BISIMULATIONSETTINGS_H_ */
diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp
index 6907c45be..b1c5003ce 100644
--- a/src/storage/BitVector.cpp
+++ b/src/storage/BitVector.cpp
@@ -1,4 +1,5 @@
#include <boost/container/flat_set.hpp>
+#include <iostream>
#include "src/storage/BitVector.h"
#include "src/exceptions/InvalidArgumentException.h"
@@ -96,6 +97,28 @@ namespace storm {
return *this;
}
+ bool BitVector::operator<(BitVector const& other) const {
+ if (this->size() < other.size()) {
+ return true;
+ } else if (this->size() > other.size()) {
+ return false;
+ }
+
+ std::vector<uint64_t>::const_iterator first1 = this->bucketVector.begin();
+ std::vector<uint64_t>::const_iterator last1 = this->bucketVector.end();
+ std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
+ std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
+
+ for (; first1 != last1; ++first1, ++first2) {
+ if (*first1 < *first2) {
+ return true;
+ } else if (*first1 > *first2) {
+ return false;
+ }
+ }
+ return false;
+ }
+
BitVector& BitVector::operator=(BitVector&& other) {
// Only perform the assignment if the source and target are not identical.
if (this != &other) {
@@ -122,8 +145,8 @@ namespace storm {
}
void BitVector::set(uint_fast64_t index, bool value) {
- uint_fast64_t bucket = index >> 6;
if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::set: written index " << index << " out of bounds.";
+ uint_fast64_t bucket = index >> 6;
uint_fast64_t mask = static_cast<uint_fast64_t>(1) << (index & mod64mask);
if (value) {
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index de73dc07c..f20c00005 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -155,7 +155,15 @@ namespace storm {
* into it.
*/
BitVector& operator=(BitVector&& other);
-
+
+ /*!
+ * Retrieves whether the current bit vector is (in some order) smaller than the given one.
+ *
+ * @param other The other bit vector.
+ * @return True iff the current bit vector is smaller than the given one.
+ */
+ bool operator<(BitVector const& other) const;
+
/*!
* Sets the given truth value at the given index.
*
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index 6c1e0e4a8..97f054f1b 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -149,15 +149,9 @@ namespace storm {
template<typename ValueType>
bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
- if (this->begin >= this->end) {
- assert(false);
- }
- if (this->prev != nullptr) {
- assert (this->prev->next == this);
- }
- if (this->next != nullptr) {
- assert (this->next->prev == this);
- }
+ assert(this->begin < this->end);
+ assert(this->prev == nullptr || this->prev->next == this);
+ assert(this->next == nullptr || this->next->prev == this);
return true;
}
@@ -260,6 +254,11 @@ namespace storm {
positions[state] = state;
stateToBlockMapping[state] = &blocks.back();
}
+
+ // If we are requested to store silent probabilities, we need to prepare the vector.
+ if (this->keepSilentProbabilities) {
+ silentProbabilities = std::vector<ValueType>(numberOfStates);
+ }
}
template<typename ValueType>
@@ -300,6 +299,11 @@ namespace storm {
stateToBlockMapping[state] = &thirdBlock;
++position;
}
+
+ // If we are requested to store silent probabilities, we need to prepare the vector.
+ if (this->keepSilentProbabilities) {
+ silentProbabilities = std::vector<ValueType>(numberOfStates);
+ }
}
template<typename ValueType>
@@ -469,6 +473,46 @@ namespace storm {
}
}
+ template<typename ValueType>
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked.");
+ return comparator.isOne(this->silentProbabilities[state]);
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked.");
+ return !comparator.isZero(this->silentProbabilities[state]);
+ }
+
+ template<typename ValueType>
+ ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getSilentProbability(storm::storage::sparse::state_type state) const {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silent probability of state, because silent probabilities are not tracked.");
+ return this->silentProbabilities[state];
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setSilentProbabilities(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
+ for (; first != last; ++first) {
+ this->silentProbabilities[first->first] = first->second;
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setSilentProbabilitiesToZero(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
+ for (; first != last; ++first) {
+ this->silentProbabilities[first->first] = storm::utility::zero<ValueType>();
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
+ this->silentProbabilities[state] = value;
+ }
+
template<typename ValueType>
std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
return this->blocks;
@@ -530,17 +574,23 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool buildQuotient) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- Partition initialPartition = getLabelBasedInitialPartition(model);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ Partition initialPartition = getLabelBasedInitialPartition(model, weak);
+ if (weak) {
+ this->initializeSilentProbabilities(model, initialPartition);
+ }
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient);
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool buildQuotient) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- Partition initialPartition = getLabelBasedInitialPartition(model);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
+ Partition initialPartition = getLabelBasedInitialPartition(model, weak);
+ if (weak) {
+ this->initializeSilentProbabilities(model, initialPartition);
+ }
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient);
}
template<typename ValueType>
@@ -548,7 +598,7 @@ namespace storm {
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);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, false, buildQuotient);
}
template<typename ValueType>
@@ -556,7 +606,7 @@ namespace storm {
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);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, false, buildQuotient);
}
template<typename ValueType>
@@ -648,7 +698,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient) {
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.
@@ -659,7 +709,7 @@ namespace storm {
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
- refinePartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue);
+ refinePartition(backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue);
splitterQueue.pop_front();
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
@@ -679,6 +729,7 @@ namespace storm {
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
+ // FIXME: this needs to do a bit more work for weak bisimulation.
this->buildQuotient(model, partition);
}
@@ -693,6 +744,7 @@ namespace storm {
std::cout << "------------------------------------------" << std::endl;
std::cout << " * total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms" << std::endl;
std::cout << std::endl;
+ std::cout << "Number of equivalence classes: " << this->size() << std::endl;
}
}
@@ -713,9 +765,9 @@ namespace storm {
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
storm::storage::sparse::state_type currentIndex = block.getBegin();
-
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
+ bool blockSplit = !comparator.isEqual(begin->second, end->second);
while (!comparator.isEqual(begin->second, end->second)) {
// 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
@@ -736,13 +788,168 @@ namespace storm {
newBlock.markAsSplitter();
}
}
+
+ // If the block was split, we also need to insert itself into the splitter queue.
+ if (blockSplit) {
+ if (!block.isMarkedAsSplitter()) {
+ splitterQueue.push_back(&block);
+ block.markAsSplitter();
+ }
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue) {
+ std::vector<uint_fast64_t> splitPoints = getSplitPointsWeak(block, partition);
+
+ // Restore the original begin of the block.
+ block.setBegin(block.getOriginalBegin());
+
+ // Now that we have the split points of the non-silent states, we perform a backward search from
+ // each non-silent state and label the predecessors with the class of the non-silent state.
+ std::cout << "creating labels " << block.getEnd() << " // " << block.getBegin() << std::endl;
+ std::cout << "split points: " << std::endl;
+ for (auto const& point : splitPoints) {
+ std::cout << point << std::endl;
+ }
+ block.print(partition);
+ std::vector<storm::storage::BitVector> stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1));
+
+ std::vector<storm::storage::sparse::state_type> stateStack;
+ stateStack.reserve(block.getEnd() - block.getBegin());
+ for (uint_fast64_t stateClassIndex = 0; stateClassIndex < splitPoints.size() - 1; ++stateClassIndex) {
+ for (auto stateIt = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex], stateIte = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) {
+
+ stateStack.push_back(stateIt->first);
+ stateLabels[partition.getPosition(stateIt->first) - block.getBegin()].set(stateClassIndex);
+ while (!stateStack.empty()) {
+ storm::storage::sparse::state_type currentState = stateStack.back();
+ stateStack.pop_back();
+
+ for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
+ if (comparator.isZero(predecessorEntry.getValue())) {
+ continue;
+ }
+
+ storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+
+ // Only if the state is in the same block, is a silent state and it has not yet been
+ // labeled with the current label.
+ if (&partition.getBlock(predecessor) == &block && partition.isSilent(predecessor, comparator) && !stateLabels[partition.getPosition(predecessor) - block.getBegin()].get(stateClassIndex)) {
+ stateStack.push_back(predecessor);
+ stateLabels[partition.getPosition(predecessor) - block.getBegin()].set(stateClassIndex);
+ }
+ }
+ }
+ }
+ }
+
+ // Now that all silent states were appropriately labeled, we can sort the states according to their
+ // labels and then scan for ranges that agree on the label.
+ std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; });
+
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.getBegin();
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(stateIt->first, position);
+ }
+
+ // Now we have everything in place to actually split the block by just scanning for ranges of equal label.
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
+ storm::storage::sparse::state_type currentIndex = block.getBegin();
+
+ // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
+ // first and the last state are different.
+ bool blockSplit = !comparator.isEqual(begin->second, end->second);
+ while (!comparator.isEqual(begin->second, end->second)) {
+ // Now we scan for the first state in the block that disagrees on the labeling value.
+ // Note that we do not have to check currentIndex for staying within bounds, because we know the matching
+ // state is within bounds.
+ ValueType const& currentValue = begin->second;
+
+ ++begin;
+ ++currentIndex;
+ while (begin != end && comparator.isEqual(begin->second, currentValue)) {
+ ++begin;
+ ++currentIndex;
+ }
+
+ // Now we split the block and mark it as a potential splitter.
+ Block& newBlock = partition.splitBlock(block, currentIndex);
+ if (!newBlock.isMarkedAsSplitter()) {
+ splitterQueue.push_back(&newBlock);
+ newBlock.markAsSplitter();
+ }
+ }
+
+ // If the block was split, we also need to insert itself into the splitter queue.
+ if (blockSplit) {
+ if (!block.isMarkedAsSplitter()) {
+ splitterQueue.push_back(&block);
+ block.markAsSplitter();
+ }
+ }
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
+ std::vector<uint_fast64_t> DeterministicModelStrongBisimulationDecomposition<ValueType>::getSplitPointsWeak(Block& block, Partition& partition) {
+ std::vector<uint_fast64_t> result;
+ // We first scale all probabilities with (1-p[s]) where p[s] is the silent probability of state s.
+ std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair<storm::storage::sparse::state_type, ValueType>& stateValuePair) {
+ ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first);
+ if (!comparator.isOne(silentProbability)) {
+ stateValuePair.second /= storm::utility::one<ValueType>() - silentProbability;
+ }
+ });
+
+ // Now sort the states based on their probabilities.
+ std::sort(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&partition] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.second < b.second; } );
+
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.getOriginalBegin();
+ for (auto stateIt = partition.getStatesAndValues().begin() + block.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + block.getBegin(); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(stateIt->first, position);
+ }
+
+ // Then, we scan for the ranges of states that agree on the probability.
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin();
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
+ storm::storage::sparse::state_type currentIndex = block.getOriginalBegin();
+ result.push_back(currentIndex);
+
+ // 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.
+ while (!comparator.isEqual(begin->second, end->second)) {
+ // 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.
+ ValueType const& currentValue = begin->second;
+
+ ++begin;
+ ++currentIndex;
+ while (begin != end && comparator.isEqual(begin->second, currentValue)) {
+ ++begin;
+ ++currentIndex;
+ }
+
+ // Remember the index at which the probabilities were different.
+ result.push_back(currentIndex);
+ }
+
+ // Push a sentinel element and return result.
+ result.push_back(block.getEnd());
+ return result;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue) {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
+ bool splitterIsPredecessor = false;
storm::storage::sparse::state_type currentPosition = splitter.getBegin();
for (auto stateIterator = partition.getBegin(splitter), stateIte = partition.getEnd(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) {
storm::storage::sparse::state_type currentState = stateIterator->first;
@@ -751,7 +958,11 @@ namespace storm {
for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+ // Get predecessor block and remember if the splitter was a predecessor of itself.
Block& predecessorBlock = partition.getBlock(predecessor);
+ if (&predecessorBlock == &splitter) {
+ splitterIsPredecessor = true;
+ }
// If the predecessor block has just one state, there is no point in splitting it.
if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) {
@@ -831,45 +1042,68 @@ namespace storm {
}
}
}
-
- // Reset the marked position of the splitter to the begin.
- splitter.setMarkedPosition(splitter.getBegin());
-
- std::list<Block*> blocksToSplit;
-
- // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
- // predecessors of the splitter.
- for (auto blockPtr : predecessorBlocks) {
- Block& block = *blockPtr;
+
+ if (!weak) {
+ std::list<Block*> blocksToSplit;
- block.unmarkAsPredecessorBlock();
- block.resetMarkedPosition();
+ // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
+ // predecessors of the splitter.
+ for (auto blockPtr : predecessorBlocks) {
+ Block& block = *blockPtr;
+
+ block.unmarkAsPredecessorBlock();
+ block.resetMarkedPosition();
+
+ // If we have moved the begin of the block to somewhere in the middle of the block, we need to split it.
+ if (block.getBegin() != block.getEnd()) {
+ Block& newBlock = partition.insertBlock(block);
+ if (!newBlock.isMarkedAsSplitter()) {
+ splitterQueue.push_back(&newBlock);
+ newBlock.markAsSplitter();
+ }
+
+ // Schedule the block of predecessors for refinement based on probabilities.
+ blocksToSplit.emplace_back(&newBlock);
+ } else {
+ // In this case, we can keep the block by setting its begin to the old value.
+ block.setBegin(block.getOriginalBegin());
+ blocksToSplit.emplace_back(&block);
+ }
+ }
- // If we have moved the begin of the block to somewhere in the middle of the block, we need to split it.
- if (block.getBegin() != block.getEnd()) {
- Block& newBlock = partition.insertBlock(block);
- if (!newBlock.isMarkedAsSplitter()) {
- splitterQueue.push_back(&newBlock);
- newBlock.markAsSplitter();
+ // Finally, we walk through the blocks that have a transition to the splitter and split them using
+ // probabilistic information.
+ for (auto blockPtr : blocksToSplit) {
+ if (blockPtr->getNumberOfStates() <= 1) {
+ continue;
}
- // Schedule the block of predecessors for refinement based on probabilities.
- blocksToSplit.emplace_back(&newBlock);
- } else {
- // In this case, we can keep the block by setting its begin to the old value.
- block.setBegin(block.getOriginalBegin());
- blocksToSplit.emplace_back(&block);
+ refineBlockProbabilities(*blockPtr, partition, splitterQueue);
}
- }
-
- // Finally, we walk through the blocks that have a transition to the splitter and split them using
- // probabilistic information.
- for (auto blockPtr : blocksToSplit) {
- if (blockPtr->getNumberOfStates() <= 1) {
- continue;
+ } else {
+ // If the splitter was a predecessor of itself and we are computing a weak bisimulation, we need to update
+ // the silent probabilities.
+ if (splitterIsPredecessor) {
+ partition.setSilentProbabilities(partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), partition.getStatesAndValues().begin() + splitter.getBegin());
+ partition.setSilentProbabilitiesToZero(partition.getStatesAndValues().begin() + splitter.getBegin(), partition.getStatesAndValues().begin() + splitter.getEnd());
+ }
+
+ // Now refine all predecessor blocks in a weak manner. That is, we split according to the criterion of
+ // weak bisimulation.
+ for (auto blockPtr : predecessorBlocks) {
+ Block& block = *blockPtr;
+
+ // If the splitter is also the predecessor block, we must not refine it at this point.
+ if (&block != &splitter) {
+ refineBlockWeak(block, partition, backwardTransitions, splitterQueue);
+ } else {
+ // Restore the begin of the block.
+ block.setBegin(block.getOriginalBegin());
+ }
+
+ block.unmarkAsPredecessorBlock();
+ block.resetMarkedPosition();
}
-
- refineBlockProbabilities(*blockPtr, partition, splitterQueue);
}
}
@@ -883,8 +1117,8 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model) {
- Partition partition(model.getNumberOfStates());
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, bool weak) {
+ Partition partition(model.getNumberOfStates(), weak);
for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
if (label == "init") {
continue;
@@ -894,6 +1128,24 @@ namespace storm {
return partition;
}
+ template<typename ValueType>
+ template<typename ModelType>
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::initializeSilentProbabilities(ModelType const& model, Partition& partition) {
+ for (auto const& block : partition.getBlocks()) {
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
+ ValueType silentProbability = storm::utility::zero<ValueType>();
+
+ for (auto const& successorEntry : model.getRows(stateIt->first)) {
+ if (&partition.getBlock(successorEntry.getColumn()) == &block) {
+ silentProbability += successorEntry.getValue();
+ }
+ }
+
+ partition.setSilentProbability(stateIt->first, silentProbability);
+ }
+ }
+ }
+
template class DeterministicModelStrongBisimulationDecomposition<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
index a29d2e82e..4c0024f90 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
@@ -22,20 +22,20 @@ namespace storm {
class DeterministicModelStrongBisimulationDecomposition : public Decomposition<StateBlock> {
public:
/*!
- * Decomposes the given DTMC into equivalence classes under strong bisimulation.
+ * Decomposes the given DTMC into equivalence classes under weak or 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);
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
- * Decomposes the given CTMC into equivalence classes under strong bisimulation.
+ * Decomposes the given CTMC into equivalence classes under weak or 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);
+ DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
* Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -340,11 +340,29 @@ namespace storm {
void increaseValue(storm::storage::sparse::state_type state, ValueType value);
// Updates the block mapping for the given range of states to the specified block.
- void updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator end);
+ void updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last);
// Retrieves the first block of the partition.
Block& getFirstBlock();
+ // Retrieves whether the given state is fully silent (only in case the silent probabilities are tracked).
+ bool isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+
+ // Retrieves whether the given state has a non-zero silent probability.
+ bool hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+
+ // Retrieves the silent probability (i.e. the probability to stay within the own equivalence class).
+ ValueType const& getSilentProbability(storm::storage::sparse::state_type state) const;
+
+ // Sets the silent probabilities for all the states in the range to their values in the range.
+ void setSilentProbabilities(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last);
+
+ // Sets the silent probabilities for all states in the range to zero.
+ void setSilentProbabilitiesToZero(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last);
+
+ // Sets the silent probability for the given state to the given value.
+ void setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value);
+
private:
// The list of blocks in the partition.
std::list<Block> blocks;
@@ -375,11 +393,12 @@ namespace storm {
* @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 weak A flag indicating whether a weak or a strong bisimulation is to be computed.
* @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);
+ void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient);
/*!
* Refines the partition based on the provided splitter. After calling this method all blocks are stable
@@ -389,10 +408,11 @@ namespace storm {
* probabilities).
* @param splitter The splitter to use.
* @param partition The partition to split.
+ * @param weak A flag indicating whether a weak or a strong bisimulation is to be computed.
* @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);
+ void refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue);
/*!
* Refines the block based on their probability values (leading into the splitter).
@@ -404,6 +424,16 @@ namespace storm {
*/
void refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
+ void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue);
+
+ /*!
+ * Determines the split offsets in the given block.
+ *
+ * @param block The block that is to be analyzed for splits.
+ * @param partition The partition that contains the block.
+ */
+ std::vector<uint_fast64_t> getSplitPointsWeak(Block& block, Partition& partition);
+
/*!
* Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
* of the decomposition.
@@ -435,10 +465,21 @@ namespace storm {
* 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.
+ * @param weak A flag indicating whether a weak bisimulation is to be computed.
* @return The resulting partition.
*/
template<typename ModelType>
- Partition getLabelBasedInitialPartition(ModelType const& model);
+ Partition getLabelBasedInitialPartition(ModelType const& model, bool weak);
+
+ /*!
+ * Initializes the silent probabilities by traversing all blocks and adding the probability of going to
+ * the very own equivalence class for each state.
+ *
+ * @param model The model from which to look-up the probabilities.
+ * @param partition The partition that holds the silent probabilities.
+ */
+ template<typename ModelType>
+ void initializeSilentProbabilities(ModelType const& model, Partition& partition);
// If required, a quotient model is built and stored in this member.
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> quotient;
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 908d7dc52..0d9098579 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.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::DeterministicModelStrongBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, true);
+ storm::storage::DeterministicModelStrongBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
result = bisimulationDecomposition.getQuotient();
From eeb859272f684ef9408c3babccdbc49d9c549e05 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 23 Oct 2014 18:58:51 +0200
Subject: [PATCH 3/8] Added (non-parametric) brp case study.
Former-commit-id: 30950730be09fd9faa6ecab482c36c29985b8150
---
examples/dtmc/brp/brp.pm | 134 +++++++++++++++++++++++++++++++++++++++
1 file changed, 134 insertions(+)
create mode 100644 examples/dtmc/brp/brp.pm
diff --git a/examples/dtmc/brp/brp.pm b/examples/dtmc/brp/brp.pm
new file mode 100644
index 000000000..f2eacc9ff
--- /dev/null
+++ b/examples/dtmc/brp/brp.pm
@@ -0,0 +1,134 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+dtmc
+
+// number of chunks
+const int N;
+// maximum number of retransmissions
+const int MAX;
+
+module sender
+
+ s : [0..6];
+ // 0 idle
+ // 1 next_frame
+ // 2 wait_ack
+ // 3 retransmit
+ // 4 success
+ // 5 error
+ // 6 wait sync
+ srep : [0..3];
+ // 0 bottom
+ // 1 not ok (nok)
+ // 2 do not know (dk)
+ // 3 ok (ok)
+ nrtr : [0..MAX];
+ i : [0..N];
+ bs : bool;
+ s_ab : bool;
+ fs : bool;
+ ls : bool;
+
+ // idle
+ [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+ // next_frame
+ [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+ // wait_ack
+ [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+ [TO_Msg] (s=2) -> (s'=3);
+ [TO_Ack] (s=2) -> (s'=3);
+ // retransmit
+ [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+ [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+ [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+ // success
+ [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+ [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+ // error
+ [SyncWait] (s=5) -> (s'=6);
+ // wait sync
+ [SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+ r : [0..5];
+ // 0 new_file
+ // 1 fst_safe
+ // 2 frame_received
+ // 3 frame_reported
+ // 4 idle
+ // 5 resync
+ rrep : [0..4];
+ // 0 bottom
+ // 1 fst
+ // 2 inc
+ // 3 ok
+ // 4 nok
+ fr : bool;
+ lr : bool;
+ br : bool;
+ r_ab : bool;
+ recv : bool;
+
+
+ // new_file
+ [SyncWait] (r=0) -> (r'=0);
+ [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ // fst_safe_frame
+ [] (r=1) -> (r'=2) & (r_ab'=br);
+ // frame_received
+ [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
+ [aA] (r=2) & !(r_ab=br) -> (r'=4);
+ // frame_reported
+ [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+ // idle
+ [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ [SyncWait] (r=4) & (ls=true) -> (r'=5);
+ [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+ // resync
+ [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+module checker // prevents more than one frame being set
+
+ T : bool;
+
+ [NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+module channelK
+
+ k : [0..2];
+
+ // idle
+ [aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2);
+ // sending
+ [aG] (k=1) -> (k'=0);
+ // lost
+ [TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+ l : [0..2];
+
+ // idle
+ [aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2);
+ // sending
+ [aB] (l=1) -> (l'=0);
+ // lost
+ [TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+rewards
+ [aF] i=1 : 1;
+endrewards
From 5bc593174ed5d0fba93fe9742df69b6472dd298c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 23 Oct 2014 20:05:44 +0200
Subject: [PATCH 4/8] Further work on weak bisimulation.
Former-commit-id: 3ad48ee0a353630c0d1cedf9c961cbda7e7e8e0a
---
examples/dtmc/brp/brp.pm | 10 +++--
src/storage/BitVector.cpp | 4 ++
src/storage/BitVector.h | 9 +++++
...icModelStrongBisimulationDecomposition.cpp | 39 ++++++++++++++-----
4 files changed, 48 insertions(+), 14 deletions(-)
diff --git a/examples/dtmc/brp/brp.pm b/examples/dtmc/brp/brp.pm
index f2eacc9ff..e09ed3e2c 100644
--- a/examples/dtmc/brp/brp.pm
+++ b/examples/dtmc/brp/brp.pm
@@ -127,8 +127,10 @@ module channelL
// lost
[TO_Ack] (l=2) -> (l'=0);
-endmodule
-
-rewards
- [aF] i=1 : 1;
+endmodule
+
+rewards
+ [aF] i=1 : 1;
endrewards
+
+label "target" = s=5;
diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp
index b1c5003ce..0fb08f028 100644
--- a/src/storage/BitVector.cpp
+++ b/src/storage/BitVector.cpp
@@ -144,6 +144,10 @@ namespace storm {
return true;
}
+ bool BitVector::operator!=(BitVector const& other) {
+ return !(*this == other);
+ }
+
void BitVector::set(uint_fast64_t index, bool value) {
if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::set: written index " << index << " out of bounds.";
uint_fast64_t bucket = index >> 6;
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index f20c00005..806febcc9 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -135,9 +135,18 @@ namespace storm {
* Compares the given bit vector with the current one.
*
* @param other The bitvector with which to compare the current one.
+ * @return True iff the other bit vector is semantically the same as the current one.
*/
bool operator==(BitVector const& other);
+ /*!
+ * Compares the given bit vector with the current one.
+ *
+ * @param other The bitvector with which to compare the current one.
+ * @return True iff the other bit vector is semantically not the same as the current one.
+ */
+ bool operator!=(BitVector const& other);
+
/*!
* Assigns the contents of the given bit vector to the current bit vector via a deep copy.
*
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index 97f054f1b..fba714149 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -577,9 +577,6 @@ namespace storm {
DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
Partition initialPartition = getLabelBasedInitialPartition(model, weak);
- if (weak) {
- this->initializeSilentProbabilities(model, initialPartition);
- }
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient);
}
@@ -587,9 +584,6 @@ namespace storm {
DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
Partition initialPartition = getLabelBasedInitialPartition(model, weak);
- if (weak) {
- this->initializeSilentProbabilities(model, initialPartition);
- }
partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient);
}
@@ -709,6 +703,8 @@ namespace storm {
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
+ std::cout << "refining with splitter " << splitterQueue.front()->getId() << std::endl;
+ partition.print();
refinePartition(backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue);
splitterQueue.pop_front();
}
@@ -848,6 +844,15 @@ namespace storm {
// labels and then scan for ranges that agree on the label.
std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; });
+ for (auto const& label : stateLabels) {
+ std::cout << label << std::endl;
+ }
+
+ std::cout << "sorted?" << std::endl;
+ for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) {
+ std::cout << stateLabels[partition.getPosition(it->first) - block.getBegin()] << std::endl;
+ }
+
// Update the positions vector.
storm::storage::sparse::state_type position = block.getBegin();
for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
@@ -862,16 +867,16 @@ namespace storm {
// Now we can check whether the block needs to be split, which is the case iff the probabilities for the
// first and the last state are different.
- bool blockSplit = !comparator.isEqual(begin->second, end->second);
- while (!comparator.isEqual(begin->second, end->second)) {
+ bool blockSplit = stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()];
+ while (stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()]) {
// Now we scan for the first state in the block that disagrees on the labeling value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
- ValueType const& currentValue = begin->second;
+ storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - block.getBegin()];
++begin;
++currentIndex;
- while (begin != end && comparator.isEqual(begin->second, currentValue)) {
+ while (begin != end && stateLabels[partition.getPosition(begin->first) - block.getBegin()] == currentValue) {
++begin;
++currentIndex;
}
@@ -879,6 +884,7 @@ namespace storm {
// Now we split the block and mark it as a potential splitter.
Block& newBlock = partition.splitBlock(block, currentIndex);
if (!newBlock.isMarkedAsSplitter()) {
+ std::cout << "adding block " << newBlock.getId() << " as splitter" << std::endl;
splitterQueue.push_back(&newBlock);
newBlock.markAsSplitter();
}
@@ -900,7 +906,9 @@ namespace storm {
std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair<storm::storage::sparse::state_type, ValueType>& stateValuePair) {
ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first);
if (!comparator.isOne(silentProbability)) {
+ std::cout << "before: " << stateValuePair.second << std::endl;
stateValuePair.second /= storm::utility::one<ValueType>() - silentProbability;
+ std::cout << "scaled: " << stateValuePair.second << std::endl;
}
});
@@ -1095,8 +1103,11 @@ namespace storm {
// If the splitter is also the predecessor block, we must not refine it at this point.
if (&block != &splitter) {
+ std::cout << "refining pred block " << block.getId() << std::endl;
refineBlockWeak(block, partition, backwardTransitions, splitterQueue);
} else {
+ Block& newBlock = partition.insertBlock(block);
+
// Restore the begin of the block.
block.setBegin(block.getOriginalBegin());
}
@@ -1125,6 +1136,14 @@ namespace storm {
}
partition.splitLabel(model.getLabeledStates(label));
}
+
+ // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
+ // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
+ if (weak) {
+ // FIXME: split off divergent states.
+
+ this->initializeSilentProbabilities(model, partition);
+ }
return partition;
}
From 391f3225e4e13ab19758ee6b05cecf0be3a5b4b2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 24 Oct 2014 16:21:39 +0200
Subject: [PATCH 5/8] Added unparameterized NAND example. Further work on weak
bisimulation.
Former-commit-id: 0936743f1e3b2d617c00f7b0388975e675201651
---
examples/dtmc/nand/nand.pm | 74 ++++++
src/settings/modules/BisimulationSettings.cpp | 7 +
src/settings/modules/BisimulationSettings.h | 2 +
...icModelStrongBisimulationDecomposition.cpp | 211 ++++++++++++++----
...sticModelStrongBisimulationDecomposition.h | 11 +-
5 files changed, 259 insertions(+), 46 deletions(-)
create mode 100644 examples/dtmc/nand/nand.pm
diff --git a/examples/dtmc/nand/nand.pm b/examples/dtmc/nand/nand.pm
new file mode 100644
index 000000000..3ae3cc754
--- /dev/null
+++ b/examples/dtmc/nand/nand.pm
@@ -0,0 +1,74 @@
+// nand multiplex system
+// gxn/dxp 20/03/03
+
+// U (correctly) performs a random permutation of the outputs of the previous stage
+
+dtmc
+
+const int N; // number of inputs in each bundle
+const int K; // number of restorative stages
+
+const int M = 2*K+1; // total number of multiplexing units
+
+// parameters taken from the following paper
+// A system architecture solution for unreliable nanoelectric devices
+// J. Han & P. Jonker
+// IEEEE trans. on nanotechnology vol 1(4) 2002
+
+const double perr = 0.02; // probability nand works correctly
+const double prob1 = 0.9; // probability initial inputs are stimulated
+
+// model whole system as a single module by resuing variables
+// to decrease the state space
+module multiplex
+
+ u : [1..M]; // number of stages
+ c : [0..N]; // counter (number of copies of the nand done)
+
+ s : [0..4]; // local state
+ // 0 - initial state
+ // 1 - set x inputs
+ // 2 - set y inputs
+ // 3 - set outputs
+ // 4 - done
+
+ z : [0..N]; // number of new outputs equal to 1
+ zx : [0..N]; // number of old outputs equal to 1
+ zy : [0..N]; // need second copy for y
+ // initially 9 since initially probability of stimulated state is 0.9
+
+ x : [0..1]; // value of first input
+ y : [0..1]; // value of second input
+
+ [] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
+ [] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+ [] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+ // choose x permute selection (have zx stimulated inputs)
+ // note only need y to be random
+ [] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+ [] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+ [] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+ // choose x randomly from selection (have zy stimulated inputs)
+ [] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+ [] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+ [] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+ [] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+ // use nand gate
+ [] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
+ // [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ // + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
+
+ [] s=4 -> (s'=s);
+
+endmodule
+
+// rewards: final value of gate
+rewards
+ [] s=0 & (c=N) & (u=M) : z/N;
+endrewards
+
+label "target" = s=4 & z/N<0.1;
diff --git a/src/settings/modules/BisimulationSettings.cpp b/src/settings/modules/BisimulationSettings.cpp
index d68337368..2d0f79e79 100644
--- a/src/settings/modules/BisimulationSettings.cpp
+++ b/src/settings/modules/BisimulationSettings.cpp
@@ -28,6 +28,13 @@ namespace storm {
return false;
}
+ bool BisimulationSettings::check() const {
+ bool optionsSet = isStrongBisimulationSet() || isWeakBisimulationSet();
+
+ STORM_LOG_WARN_COND(!storm::settings::generalSettings().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for gmm++ has no effect.");
+
+ return true;
+ }
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/BisimulationSettings.h b/src/settings/modules/BisimulationSettings.h
index 2ff715122..3e2d1efe7 100644
--- a/src/settings/modules/BisimulationSettings.h
+++ b/src/settings/modules/BisimulationSettings.h
@@ -36,6 +36,8 @@ namespace storm {
*/
bool isWeakBisimulationSet() const;
+ virtual bool check() const override;
+
// The name of the module.
static const std::string moduleName;
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index fba714149..f413a12e7 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -42,6 +42,12 @@ namespace storm {
for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
std::cout << std::setprecision(3) << partition.statesAndValues[index].second << " ";
}
+ if (partition.keepSilentProbabilities) {
+ std::cout << std::endl << "silent:" << std::endl;
+ for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) {
+ std::cout << std::setprecision(3) << partition.silentProbabilities[partition.statesAndValues[index].first] << " ";
+ }
+ }
std::cout << std::endl;
}
@@ -61,11 +67,10 @@ namespace storm {
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementBegin() {
++this->begin;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::decrementEnd() {
- ++this->begin;
+ if (begin == end) {
+ std::cout << "moved begin to end!" << std::endl;
+ }
+ STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size.");
}
template<typename ValueType>
@@ -149,6 +154,7 @@ namespace storm {
template<typename ValueType>
bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
+ std::cout << "checking block " << this->getId() << std::endl;
assert(this->begin < this->end);
assert(this->prev == nullptr || this->prev->next == this);
assert(this->next == nullptr || this->next->prev == this);
@@ -576,15 +582,17 @@ namespace storm {
template<typename ValueType>
DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- Partition initialPartition = getLabelBasedInitialPartition(model, weak);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient);
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
+ partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient);
}
template<typename ValueType>
DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- Partition initialPartition = getLabelBasedInitialPartition(model, weak);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient);
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
+ partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient);
}
template<typename ValueType>
@@ -698,18 +706,25 @@ namespace storm {
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
std::deque<Block*> splitterQueue;
- std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
-
+ std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); });
+
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
std::cout << "refining with splitter " << splitterQueue.front()->getId() << std::endl;
+ for (auto const& entry : splitterQueue) {
+ std::cout << entry->getId();
+ }
+ std::cout << std::endl;
partition.print();
- refinePartition(backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue);
+ refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue);
splitterQueue.pop_front();
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
+ std::cout << "final partition: " << std::endl;
+ partition.print();
+
// Now move the states from the internal partition into their final place in the decomposition. We do so in
// a way that maintains the block IDs as indices.
std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
@@ -795,7 +810,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue) {
std::vector<uint_fast64_t> splitPoints = getSplitPointsWeak(block, partition);
// Restore the original begin of the block.
@@ -840,62 +855,123 @@ namespace storm {
}
}
- // Now that all silent states were appropriately labeled, we can sort the states according to their
- // labels and then scan for ranges that agree on the label.
+ // Now that all states were appropriately labeled, we can sort the states according to their labels and then
+ // scan for ranges that agree on the label.
std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; });
+ std::cout << "sorted states:" << std::endl;
+ for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) {
+ std::cout << it->first << " ";
+ }
+ std::cout << std::endl;
+
for (auto const& label : stateLabels) {
std::cout << label << std::endl;
}
+ // Note that we do not yet repair the positions vector, but for the sake of efficiency temporariliy keep the
+ // data structure in an inconsistent state.
+
std::cout << "sorted?" << std::endl;
for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) {
- std::cout << stateLabels[partition.getPosition(it->first) - block.getBegin()] << std::endl;
- }
-
- // Update the positions vector.
- storm::storage::sparse::state_type position = block.getBegin();
- for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
- partition.setPosition(stateIt->first, position);
+ std::cout << "state " << it->first << " and label " << stateLabels[partition.getPosition(it->first) - block.getBegin()] << std::endl;
}
// Now we have everything in place to actually split the block by just scanning for ranges of equal label.
+ std::cout << "scanning range " << block.getBegin() << " to " << block.getEnd() << " for equal labelings" << std::endl;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
storm::storage::sparse::state_type currentIndex = block.getBegin();
- // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
- // first and the last state are different.
- bool blockSplit = stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()];
- while (stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()]) {
+ // Now we can check whether the block needs to be split, which is the case iff the labels for the first and
+ // the last state are different. Store the offset of the block seperately, because it will potentially
+ // modified by splits.
+ storm::storage::sparse::state_type blockOffset = block.getBegin();
+ bool blockSplit = stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset];
+ while (stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset]) {
+ std::cout << "still scanning range " << currentIndex << " to " << block.getEnd() << " for equal labelings" << std::endl;
+ std::cout << "found different labels " << stateLabels[partition.getPosition(begin->first) - blockOffset] << " and " << stateLabels[partition.getPosition(end->first) - blockOffset] << std::endl;
// Now we scan for the first state in the block that disagrees on the labeling value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
- storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - block.getBegin()];
+ storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - blockOffset];
++begin;
++currentIndex;
- while (begin != end && stateLabels[partition.getPosition(begin->first) - block.getBegin()] == currentValue) {
+ while (begin != end && stateLabels[partition.getPosition(begin->first) - blockOffset] == currentValue) {
++begin;
++currentIndex;
}
// Now we split the block and mark it as a potential splitter.
Block& newBlock = partition.splitBlock(block, currentIndex);
+ std::cout << "splitting block created new block " << std::endl;
+ newBlock.print(partition);
+ std::cout << "old block remained: " << std::endl;
+ block.print(partition);
+
+ // Update the silent probabilities for all the states in the new block.
+ for (auto stateIt = partition.getBegin(newBlock), stateIte = partition.getEnd(newBlock); stateIt != stateIte; ++stateIt) {
+ if (partition.hasSilentProbability(stateIt->first, comparator)) {
+ ValueType newSilentProbability = storm::utility::zero<ValueType>();
+ for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) {
+ if (&partition.getBlock(successorEntry.getColumn()) == &newBlock) {
+ std::cout << successorEntry.getColumn() << " is in block " << newBlock.getId() << std::endl;
+ newSilentProbability += successorEntry.getValue();
+ } else {
+ std::cout << successorEntry.getColumn() << " is not in block " << newBlock.getId() << std::endl;
+ }
+ }
+ partition.setSilentProbability(stateIt->first, newSilentProbability);
+ }
+ }
+
+ std::cout << "after updating silent probs:" << std::endl;
+ newBlock.print(partition);
+
if (!newBlock.isMarkedAsSplitter()) {
- std::cout << "adding block " << newBlock.getId() << " as splitter" << std::endl;
+ std::cout << "adding " << newBlock.getId() << " to the queue." << std::endl;
splitterQueue.push_back(&newBlock);
newBlock.markAsSplitter();
}
+ std::cout << "end of loop; currentIndex = " << currentIndex << std::endl;
}
// If the block was split, we also need to insert itself into the splitter queue.
if (blockSplit) {
if (!block.isMarkedAsSplitter()) {
+ std::cout << "adding " << block.getId() << " to the queue." << std::endl;
splitterQueue.push_back(&block);
block.markAsSplitter();
}
+
+ // Update the silent probabilities for all the states in the old block.
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
+ std::cout << "computing silent prob of " << stateIt->first << std::endl;
+ if (partition.hasSilentProbability(stateIt->first, comparator)) {
+ ValueType newSilentProbability = storm::utility::zero<ValueType>();
+ for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) {
+ if (&partition.getBlock(successorEntry.getColumn()) == &block) {
+ std::cout << successorEntry.getColumn() << " is in block " << block.getId() << std::endl;
+ newSilentProbability += successorEntry.getValue();
+ } else {
+ std::cout << successorEntry.getColumn() << " is not in block " << block.getId() << std::endl;
+ }
+ }
+ partition.setSilentProbability(stateIt->first, newSilentProbability);
+ }
+ }
+
+ std::cout << "after updating silent probs for block itself:" << std::endl;
+ block.print(partition);
+ }
+
+ // Finally update the positions vector.
+ storm::storage::sparse::state_type position = blockOffset;
+ for (auto stateIt = partition.getStatesAndValues().begin() + blockOffset, stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
+ std::cout << "setting position of state " << stateIt->first << " to " << position << std::endl;
+ partition.setPosition(stateIt->first, position);
}
}
@@ -905,10 +981,12 @@ namespace storm {
// We first scale all probabilities with (1-p[s]) where p[s] is the silent probability of state s.
std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair<storm::storage::sparse::state_type, ValueType>& stateValuePair) {
ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first);
- if (!comparator.isOne(silentProbability)) {
- std::cout << "before: " << stateValuePair.second << std::endl;
+ if (!comparator.isOne(silentProbability) && !comparator.isZero(silentProbability)) {
+ std::cout << "prob for state " << stateValuePair.first << " before: " << stateValuePair.second << std::endl;
stateValuePair.second /= storm::utility::one<ValueType>() - silentProbability;
- std::cout << "scaled: " << stateValuePair.second << std::endl;
+ std::cout << "and scaled: " << stateValuePair.second << std::endl;
+ } else {
+ std::cout << "not scaling prob for state " << stateValuePair.first << " because silent prob is " << silentProbability << " and prob is " << stateValuePair.second << std::endl;
}
});
@@ -922,6 +1000,7 @@ namespace storm {
}
// Then, we scan for the ranges of states that agree on the probability.
+ std::cout << "range to scan for split points: " << block.getOriginalBegin() << " to " << (block.getBegin() - 1) << std::endl;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
@@ -948,12 +1027,12 @@ namespace storm {
}
// Push a sentinel element and return result.
- result.push_back(block.getEnd());
+ result.push_back(block.getBegin());
return result;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue) {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
@@ -972,6 +1051,8 @@ namespace storm {
splitterIsPredecessor = true;
}
+ std::cout << " got predecessor " << predecessor << " of state " << currentState << " in block " << predecessorBlock.getId() << " with prob " << predecessorEntry.getValue() << std::endl;
+
// If the predecessor block has just one state, there is no point in splitting it.
if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) {
continue;
@@ -1035,6 +1116,8 @@ namespace storm {
storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
Block& predecessorBlock = partition.getBlock(predecessor);
storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor);
+
+ std::cout << " got predecessor(2) " << predecessor << " of state " << stateIterator->first << " in block " << predecessorBlock.getId() << " with prob " << predecessorEntry.getValue() << std::endl;
if (predecessorPosition >= predecessorBlock.getBegin()) {
partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin());
@@ -1103,12 +1186,11 @@ namespace storm {
// If the splitter is also the predecessor block, we must not refine it at this point.
if (&block != &splitter) {
- std::cout << "refining pred block " << block.getId() << std::endl;
- refineBlockWeak(block, partition, backwardTransitions, splitterQueue);
+ std::cout << "refining predecessor block " << block.getId() << std::endl;
+ refineBlockWeak(block, partition, forwardTransitions, backwardTransitions, splitterQueue);
} else {
- Block& newBlock = partition.insertBlock(block);
-
// Restore the begin of the block.
+ std::cout << "not splitting because predecessor block is the splitter" << std::endl;
block.setBegin(block.getOriginalBegin());
}
@@ -1116,6 +1198,8 @@ namespace storm {
block.resetMarkedPosition();
}
}
+
+ STORM_LOG_ASSERT(partition.check(), "Partition became inconsistent.");
}
template<typename ValueType>
@@ -1128,7 +1212,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, bool weak) {
+ typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak) {
Partition partition(model.getNumberOfStates(), weak);
for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
if (label == "init") {
@@ -1140,7 +1224,54 @@ namespace storm {
// If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
// states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
if (weak) {
- // FIXME: split off divergent states.
+ std::vector<storm::storage::sparse::state_type> stateStack;
+ stateStack.reserve(model.getNumberOfStates());
+ storm::storage::BitVector nondivergentStates(model.getNumberOfStates());
+ for (auto& block : partition.getBlocks()) {
+ nondivergentStates.clear();
+
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
+ if (nondivergentStates.get(stateIt->first)) {
+ continue;
+ }
+
+ // Now traverse the forward transitions of the current state and check whether there is a
+ // transition to some other block.
+ for (auto const& successor : model.getRows(stateIt->first)) {
+ // If there is such a transition, then we can mark all states in the current block that can
+ // reach the state as non-divergent.
+ if (&partition.getBlock(successor.getColumn()) != &block) {
+ stateStack.push_back(stateIt->first);
+
+ while (!stateStack.empty()) {
+ storm::storage::sparse::state_type currentState = stateStack.back();
+ stateStack.pop_back();
+ nondivergentStates.set(currentState);
+
+ for (auto const& predecessor : backwardTransitions.getRow(stateIt->first)) {
+ if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) {
+ stateStack.push_back(predecessor.getColumn());
+ }
+ }
+ }
+ }
+ }
+ }
+
+ if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) {
+ // Now that we have determined all (non)divergent states in the current block, we need to split them
+ // off.
+ std::sort(partition.getBegin(block), partition.getEnd(block), [&nondivergentStates] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return nondivergentStates.get(a.first) && !nondivergentStates.get(b.first); } );
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.getBegin();
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(stateIt->first, position);
+ }
+
+ // Finally, split the block.
+ partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits());
+ }
+ }
this->initializeSilentProbabilities(model, partition);
}
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
index 4c0024f90..5c34c02e9 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
@@ -91,9 +91,6 @@ namespace storm {
// Sets the end index of the block.
void setEnd(storm::storage::sparse::state_type end);
- // Moves the end index of the block one step to the front.
- void decrementEnd();
-
// Returns the beginning index of the block.
storm::storage::sparse::state_type getBegin() const;
@@ -404,6 +401,7 @@ namespace storm {
* Refines the partition based on the provided splitter. After calling this method all blocks are stable
* with respect to the splitter.
*
+ * @param forwardTransitions The forward transitions of the model.
* @param backwardTransitions A matrix that can be used to retrieve the predecessors (and their
* probabilities).
* @param splitter The splitter to use.
@@ -412,7 +410,7 @@ namespace storm {
* @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, bool weak, std::deque<Block*>& splitterQueue);
+ void refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue);
/*!
* Refines the block based on their probability values (leading into the splitter).
@@ -424,7 +422,7 @@ namespace storm {
*/
void refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
- void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue);
+ void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue);
/*!
* Determines the split offsets in the given block.
@@ -465,11 +463,12 @@ namespace storm {
* 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.
+ * @param backwardTransitions The backward transitions of the model.
* @param weak A flag indicating whether a weak bisimulation is to be computed.
* @return The resulting partition.
*/
template<typename ModelType>
- Partition getLabelBasedInitialPartition(ModelType const& model, bool weak);
+ Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak);
/*!
* Initializes the silent probabilities by traversing all blocks and adding the probability of going to
From 7257bb23c3219e800bdc415f2e186e09e827b417 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 24 Oct 2014 18:50:44 +0200
Subject: [PATCH 6/8] Further work on weak bisimulation. Model checking can now
be done from tne command line again.
Former-commit-id: 5f338260e6ee5db17fa9ac789f21d794b23df418
---
src/settings/modules/BisimulationSettings.cpp | 2 +-
...icModelStrongBisimulationDecomposition.cpp | 148 ++++++++----------
...sticModelStrongBisimulationDecomposition.h | 3 +-
src/utility/cli.h | 14 +-
4 files changed, 76 insertions(+), 91 deletions(-)
diff --git a/src/settings/modules/BisimulationSettings.cpp b/src/settings/modules/BisimulationSettings.cpp
index 2d0f79e79..4e2f3975e 100644
--- a/src/settings/modules/BisimulationSettings.cpp
+++ b/src/settings/modules/BisimulationSettings.cpp
@@ -31,7 +31,7 @@ namespace storm {
bool BisimulationSettings::check() const {
bool optionsSet = isStrongBisimulationSet() || isWeakBisimulationSet();
- STORM_LOG_WARN_COND(!storm::settings::generalSettings().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for gmm++ has no effect.");
+ STORM_LOG_WARN_COND(storm::settings::generalSettings().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");
return true;
}
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index f413a12e7..f057b4406 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -67,9 +67,6 @@ namespace storm {
template<typename ValueType>
void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementBegin() {
++this->begin;
- if (begin == end) {
- std::cout << "moved begin to end!" << std::endl;
- }
STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size.");
}
@@ -154,7 +151,6 @@ namespace storm {
template<typename ValueType>
bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
- std::cout << "checking block " << this->getId() << std::endl;
assert(this->begin < this->end);
assert(this->prev == nullptr || this->prev->next == this);
assert(this->next == nullptr || this->next->prev == this);
@@ -619,7 +615,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition) {
+ void DeterministicModelStrongBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, bool weak) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
@@ -640,9 +636,20 @@ namespace storm {
for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) {
auto const& block = this->blocks[blockIndex];
- // Pick one representative state. It doesn't matter which state it is, because they all behave equally.
+ // Pick one representative state. For strong bisimulation it doesn't matter which state it is, because
+ // they all behave equally.
storm::storage::sparse::state_type representativeState = *block.begin();
+ // However, for weak bisimulation, we need to make sure the representative state is a non-silent one.
+ if (weak) {
+ for (auto const& state : block) {
+ if (!partition.isSilent(state, comparator)) {
+ representativeState = state;
+ break;
+ }
+ }
+ }
+
Block const& oldBlock = partition.getBlock(representativeState);
// If the block is absorbing, we simply add a self-loop.
@@ -651,12 +658,26 @@ namespace storm {
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);
+ }
+ }
}
} 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();
+
+ // If we are computing a weak bisimulation quotient, there is no need to add self-loops.
+ if (weak && targetBlock == blockIndex) {
+ continue;
+ }
+
auto probIterator = blockProbability.find(targetBlock);
if (probIterator != blockProbability.end()) {
probIterator->second += entry.getValue();
@@ -667,7 +688,11 @@ namespace storm {
// Now add them to the actual matrix.
for (auto const& probabilityEntry : blockProbability) {
- builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
+ if (weak) {
+ builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - partition.getSilentProbability(representativeState)));
+ } else {
+ builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
+ }
}
// If the block has a special label, we only add that to the block.
@@ -711,20 +736,11 @@ namespace storm {
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
- std::cout << "refining with splitter " << splitterQueue.front()->getId() << std::endl;
- for (auto const& entry : splitterQueue) {
- std::cout << entry->getId();
- }
- std::cout << std::endl;
- partition.print();
refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue);
splitterQueue.pop_front();
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
- std::cout << "final partition: " << std::endl;
- partition.print();
-
// Now move the states from the internal partition into their final place in the decomposition. We do so in
// a way that maintains the block IDs as indices.
std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now();
@@ -740,8 +756,7 @@ namespace storm {
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
- // FIXME: this needs to do a bit more work for weak bisimulation.
- this->buildQuotient(model, partition);
+ this->buildQuotient(model, partition, weak);
}
std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
@@ -818,12 +833,6 @@ namespace storm {
// Now that we have the split points of the non-silent states, we perform a backward search from
// each non-silent state and label the predecessors with the class of the non-silent state.
- std::cout << "creating labels " << block.getEnd() << " // " << block.getBegin() << std::endl;
- std::cout << "split points: " << std::endl;
- for (auto const& point : splitPoints) {
- std::cout << point << std::endl;
- }
- block.print(partition);
std::vector<storm::storage::BitVector> stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1));
std::vector<storm::storage::sparse::state_type> stateStack;
@@ -859,26 +868,10 @@ namespace storm {
// scan for ranges that agree on the label.
std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; });
- std::cout << "sorted states:" << std::endl;
- for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) {
- std::cout << it->first << " ";
- }
- std::cout << std::endl;
-
- for (auto const& label : stateLabels) {
- std::cout << label << std::endl;
- }
-
// Note that we do not yet repair the positions vector, but for the sake of efficiency temporariliy keep the
// data structure in an inconsistent state.
- std::cout << "sorted?" << std::endl;
- for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) {
- std::cout << "state " << it->first << " and label " << stateLabels[partition.getPosition(it->first) - block.getBegin()] << std::endl;
- }
-
// Now we have everything in place to actually split the block by just scanning for ranges of equal label.
- std::cout << "scanning range " << block.getBegin() << " to " << block.getEnd() << " for equal labelings" << std::endl;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
@@ -890,8 +883,6 @@ namespace storm {
storm::storage::sparse::state_type blockOffset = block.getBegin();
bool blockSplit = stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset];
while (stateLabels[partition.getPosition(begin->first) - blockOffset] != stateLabels[partition.getPosition(end->first) - blockOffset]) {
- std::cout << "still scanning range " << currentIndex << " to " << block.getEnd() << " for equal labelings" << std::endl;
- std::cout << "found different labels " << stateLabels[partition.getPosition(begin->first) - blockOffset] << " and " << stateLabels[partition.getPosition(end->first) - blockOffset] << std::endl;
// Now we scan for the first state in the block that disagrees on the labeling value.
// Note that we do not have to check currentIndex for staying within bounds, because we know the matching
// state is within bounds.
@@ -906,10 +897,6 @@ namespace storm {
// Now we split the block and mark it as a potential splitter.
Block& newBlock = partition.splitBlock(block, currentIndex);
- std::cout << "splitting block created new block " << std::endl;
- newBlock.print(partition);
- std::cout << "old block remained: " << std::endl;
- block.print(partition);
// Update the silent probabilities for all the states in the new block.
for (auto stateIt = partition.getBegin(newBlock), stateIte = partition.getEnd(newBlock); stateIt != stateIte; ++stateIt) {
@@ -917,60 +904,43 @@ namespace storm {
ValueType newSilentProbability = storm::utility::zero<ValueType>();
for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) {
if (&partition.getBlock(successorEntry.getColumn()) == &newBlock) {
- std::cout << successorEntry.getColumn() << " is in block " << newBlock.getId() << std::endl;
newSilentProbability += successorEntry.getValue();
- } else {
- std::cout << successorEntry.getColumn() << " is not in block " << newBlock.getId() << std::endl;
}
}
partition.setSilentProbability(stateIt->first, newSilentProbability);
}
}
- std::cout << "after updating silent probs:" << std::endl;
- newBlock.print(partition);
-
if (!newBlock.isMarkedAsSplitter()) {
- std::cout << "adding " << newBlock.getId() << " to the queue." << std::endl;
splitterQueue.push_back(&newBlock);
newBlock.markAsSplitter();
}
- std::cout << "end of loop; currentIndex = " << currentIndex << std::endl;
}
// If the block was split, we also need to insert itself into the splitter queue.
if (blockSplit) {
if (!block.isMarkedAsSplitter()) {
- std::cout << "adding " << block.getId() << " to the queue." << std::endl;
splitterQueue.push_back(&block);
block.markAsSplitter();
}
// Update the silent probabilities for all the states in the old block.
for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
- std::cout << "computing silent prob of " << stateIt->first << std::endl;
if (partition.hasSilentProbability(stateIt->first, comparator)) {
ValueType newSilentProbability = storm::utility::zero<ValueType>();
for (auto const& successorEntry : forwardTransitions.getRow(stateIt->first)) {
if (&partition.getBlock(successorEntry.getColumn()) == &block) {
- std::cout << successorEntry.getColumn() << " is in block " << block.getId() << std::endl;
newSilentProbability += successorEntry.getValue();
- } else {
- std::cout << successorEntry.getColumn() << " is not in block " << block.getId() << std::endl;
}
- }
+ }
partition.setSilentProbability(stateIt->first, newSilentProbability);
}
}
-
- std::cout << "after updating silent probs for block itself:" << std::endl;
- block.print(partition);
}
// Finally update the positions vector.
storm::storage::sparse::state_type position = blockOffset;
for (auto stateIt = partition.getStatesAndValues().begin() + blockOffset, stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
- std::cout << "setting position of state " << stateIt->first << " to " << position << std::endl;
partition.setPosition(stateIt->first, position);
}
}
@@ -982,11 +952,7 @@ namespace storm {
std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair<storm::storage::sparse::state_type, ValueType>& stateValuePair) {
ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first);
if (!comparator.isOne(silentProbability) && !comparator.isZero(silentProbability)) {
- std::cout << "prob for state " << stateValuePair.first << " before: " << stateValuePair.second << std::endl;
stateValuePair.second /= storm::utility::one<ValueType>() - silentProbability;
- std::cout << "and scaled: " << stateValuePair.second << std::endl;
- } else {
- std::cout << "not scaling prob for state " << stateValuePair.first << " because silent prob is " << silentProbability << " and prob is " << stateValuePair.second << std::endl;
}
});
@@ -1000,7 +966,6 @@ namespace storm {
}
// Then, we scan for the ranges of states that agree on the probability.
- std::cout << "range to scan for split points: " << block.getOriginalBegin() << " to " << (block.getBegin() - 1) << std::endl;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin();
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
@@ -1051,9 +1016,7 @@ namespace storm {
splitterIsPredecessor = true;
}
- std::cout << " got predecessor " << predecessor << " of state " << currentState << " in block " << predecessorBlock.getId() << " with prob " << predecessorEntry.getValue() << std::endl;
-
- // If the predecessor block has just one state, there is no point in splitting it.
+ // If the predecessor block has just one state or is marked as being absorbing, we must not split it.
if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) {
continue;
}
@@ -1117,8 +1080,6 @@ namespace storm {
Block& predecessorBlock = partition.getBlock(predecessor);
storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor);
- std::cout << " got predecessor(2) " << predecessor << " of state " << stateIterator->first << " in block " << predecessorBlock.getId() << " with prob " << predecessorEntry.getValue() << std::endl;
-
if (predecessorPosition >= predecessorBlock.getBegin()) {
partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin());
predecessorBlock.incrementBegin();
@@ -1186,11 +1147,9 @@ namespace storm {
// If the splitter is also the predecessor block, we must not refine it at this point.
if (&block != &splitter) {
- std::cout << "refining predecessor block " << block.getId() << std::endl;
refineBlockWeak(block, partition, forwardTransitions, backwardTransitions, splitterQueue);
} else {
// Restore the begin of the block.
- std::cout << "not splitting because predecessor block is the splitter" << std::endl;
block.setBegin(block.getOriginalBegin());
}
@@ -1237,27 +1196,34 @@ namespace storm {
// Now traverse the forward transitions of the current state and check whether there is a
// transition to some other block.
+ bool isDirectlyNonDivergent = false;
for (auto const& successor : model.getRows(stateIt->first)) {
// If there is such a transition, then we can mark all states in the current block that can
// reach the state as non-divergent.
if (&partition.getBlock(successor.getColumn()) != &block) {
- stateStack.push_back(stateIt->first);
+ isDirectlyNonDivergent = true;
+ break;
+ }
+ }
+
+ if (isDirectlyNonDivergent) {
+ stateStack.push_back(stateIt->first);
+
+ while (!stateStack.empty()) {
+ storm::storage::sparse::state_type currentState = stateStack.back();
+ stateStack.pop_back();
+ nondivergentStates.set(currentState);
- while (!stateStack.empty()) {
- storm::storage::sparse::state_type currentState = stateStack.back();
- stateStack.pop_back();
- nondivergentStates.set(currentState);
-
- for (auto const& predecessor : backwardTransitions.getRow(stateIt->first)) {
- if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) {
- stateStack.push_back(predecessor.getColumn());
- }
+ for (auto const& predecessor : backwardTransitions.getRow(currentState)) {
+ if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) {
+ stateStack.push_back(predecessor.getColumn());
}
}
}
}
}
+
if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) {
// Now that we have determined all (non)divergent states in the current block, we need to split them
// off.
@@ -1269,7 +1235,15 @@ namespace storm {
}
// Finally, split the block.
- partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits());
+ Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits());
+
+ // Since the remaining states in the block are divergent, we can mark the block as absorbing.
+ // This also guarantees that the self-loop will be added to the state of the quotient
+ // representing this block of states.
+ block.setAbsorbing(true);
+ } else if (nondivergentStates.getNumberOfSetBits() == 0) {
+ // If there are only diverging states in the block, we need to make it absorbing.
+ block.setAbsorbing(true);
}
}
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
index 5c34c02e9..9719569d3 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h
@@ -440,9 +440,10 @@ namespace storm {
* determining the transitions of each equivalence class.
* @param partition The previously computed partition. This is used for quickly retrieving the block of a
* state.
+ * @param weak A flag indicating whether the quotient is built for weak bisimulation.
*/
template<typename ModelType>
- void buildQuotient(ModelType const& model, Partition const& partition);
+ void buildQuotient(ModelType const& model, Partition const& partition, bool weak);
/*!
* Creates the measure-driven initial partition for reaching psi states from phi states.
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 0d9098579..925f085d1 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -49,6 +49,10 @@ log4cplus::Logger logger;
#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
+// Headers for model checking.
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
@@ -315,10 +319,16 @@ namespace storm {
STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty());
generateCounterexample(model, filterFormula->getChild());
+ } else if (settings.isPctlPropertySet()) {
+ std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty());
+
+ if (model->getType() == storm::models::DTMC) {
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
+ modelchecker::prctl::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
+ filterFormula->check(modelchecker);
+ }
}
-
}
-
}
}
}
From f90ac5c8c39fa26407cf432eba6369c18397a016 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 25 Oct 2014 17:03:37 +0200
Subject: [PATCH 7/8] First working version of weak bisimulation for DTMCs.
Former-commit-id: 8a7d76de4fc182b487c40199c78a338aede88bd9
---
...inisticModelStrongBisimulationDecomposition.cpp | 14 ++++++++++----
1 file changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index f057b4406..4cc536c1b 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -576,7 +576,7 @@ namespace storm {
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) {
+ DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator(0) {
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 = getLabelBasedInitialPartition(model, backwardTransitions, weak);
@@ -732,12 +732,19 @@ namespace storm {
std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
std::deque<Block*> splitterQueue;
std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); });
-
+
// Then perform the actual splitting until there are no more splitters.
while (!splitterQueue.empty()) {
+ // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters).
std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
- refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue);
+
+ // Get and prepare the next splitter.
+ Block* splitter = splitterQueue.front();
splitterQueue.pop_front();
+ splitter->unmarkAsSplitter();
+
+ // Now refine the partition using the current splitter.
+ refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, weak, splitterQueue);
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
@@ -770,7 +777,6 @@ namespace storm {
std::cout << "------------------------------------------" << std::endl;
std::cout << " * total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms" << std::endl;
std::cout << std::endl;
- std::cout << "Number of equivalence classes: " << this->size() << std::endl;
}
}
From e6904dcb213daa04ed839d5b59ebb213f990186c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 25 Oct 2014 18:09:50 +0200
Subject: [PATCH 8/8] Renamed bisimulation decomposition class to reflect that
now also weak bisimulations can be computed.
Former-commit-id: 1a654b7110d16c670900ee1f4abaedd6979ac55b
---
...inisticModelBisimulationDecomposition.cpp} | 355 ++++++++++--------
...rministicModelBisimulationDecomposition.h} | 51 ++-
src/utility/cli.h | 4 +-
3 files changed, 225 insertions(+), 185 deletions(-)
rename src/storage/{DeterministicModelStrongBisimulationDecomposition.cpp => DeterministicModelBisimulationDecomposition.cpp} (74%)
rename src/storage/{DeterministicModelStrongBisimulationDecomposition.h => DeterministicModelBisimulationDecomposition.h} (89%)
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
similarity index 74%
rename from src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
rename to src/storage/DeterministicModelBisimulationDecomposition.cpp
index 4cc536c1b..2f46baa55 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -1,4 +1,4 @@
-#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
#include <algorithm>
#include <unordered_map>
@@ -13,10 +13,10 @@ namespace storm {
namespace storage {
template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::blockId = 0;
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::blockId = 0;
template<typename ValueType>
- 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) {
+ 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) {
if (next != nullptr) {
next->prev = this;
}
@@ -27,7 +27,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
+ void DeterministicModelBisimulationDecomposition<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;
@@ -52,31 +52,31 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
this->begin = begin;
this->markedPosition = begin;
STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
this->end = end;
STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementBegin() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementBegin() {
++this->begin;
STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size.");
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getBegin() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getBegin() const {
return this->begin;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
if (this->hasPreviousBlock()) {
return this->getPreviousBlock().getEnd();
} else {
@@ -85,72 +85,72 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getEnd() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getEnd() const {
return this->end;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setIterator(iterator it) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setIterator(iterator it) {
this->selfIt = it;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getIterator() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getIterator() const {
return this->selfIt;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
return this->getNextBlock().getIterator();
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
return this->getPreviousBlock().getIterator();
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() {
return *this->next;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
return *this->next;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
return this->next != nullptr;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
return *this->prev;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
return this->prev;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
return this->next;
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
return *this->prev;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
return this->prev != nullptr;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::check() const {
assert(this->begin < this->end);
assert(this->prev == nullptr || this->prev->next == this);
assert(this->next == nullptr || this->next->prev == this);
@@ -158,94 +158,94 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
+ std::size_t DeterministicModelBisimulationDecomposition<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 DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
return this->markedAsSplitter;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
this->markedAsSplitter = true;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
this->markedAsSplitter = false;
}
template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getId() const {
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
return this->id;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setAbsorbing(bool absorbing) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setAbsorbing(bool absorbing) {
this->absorbing = absorbing;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isAbsorbing() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isAbsorbing() const {
return this->absorbing;
}
template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
return this->markedPosition;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
this->markedPosition = position;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
this->markedPosition = this->begin;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
++this->markedPosition;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
this->markedAsPredecessorBlock = true;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
this->markedAsPredecessorBlock = false;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
return markedAsPredecessorBlock;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasLabel() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasLabel() const {
return this->label != nullptr;
}
template<typename ValueType>
- std::string const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabel() const {
+ std::string const& DeterministicModelBisimulationDecomposition<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 {
+ std::shared_ptr<std::string> const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
return this->label;
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<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.
typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
it->setIterator(it);
@@ -264,7 +264,7 @@ namespace storm {
}
template<typename ValueType>
- 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, 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);
Block& firstBlock = *firstIt;
firstBlock.setIterator(firstIt);
@@ -309,13 +309,13 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]);
std::swap(this->positions[state1], this->positions[state2]);
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first;
storm::storage::sparse::state_type state2 = this->statesAndValues[position2].first;
@@ -326,84 +326,84 @@ namespace storm {
}
template<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
+ storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
return this->positions[state];
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
+ void DeterministicModelBisimulationDecomposition<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& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
+ storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
return this->statesAndValues[position].first;
}
template<typename ValueType>
- ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
return this->statesAndValues[this->positions[state]].second;
}
template<typename ValueType>
- ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
return this->statesAndValues[position].second;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
this->statesAndValues[this->positions[state]].second = value;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
this->statesAndValues[this->positions[state]].second += value;
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
for (; first != last; ++first) {
this->stateToBlockMapping[first->first] = █
}
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getFirstBlock() {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getFirstBlock() {
return *this->blocks.begin();
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
return *this->stateToBlockMapping[state];
}
template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
return this->statesAndValues.begin() + block.getBegin();
}
template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
return this->statesAndValues.begin() + block.getEnd();
}
template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
return this->statesAndValues.begin() + block.getBegin();
}
template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) const {
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) const {
return this->statesAndValues.begin() + block.getEnd();
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
// In case one of the resulting blocks would be empty, we simply return the current block and do not create
// a new one.
if (position == block.getBegin() || position == block.getEnd()) {
@@ -425,7 +425,7 @@ namespace storm {
}
template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
// Find the beginning of the new block.
storm::storage::sparse::state_type begin;
if (block.hasPreviousBlock()) {
@@ -448,7 +448,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
+ void DeterministicModelBisimulationDecomposition<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;
@@ -476,25 +476,25 @@ namespace storm {
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked.");
return comparator.isOne(this->silentProbabilities[state]);
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked.");
return !comparator.isZero(this->silentProbabilities[state]);
}
template<typename ValueType>
- ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getSilentProbability(storm::storage::sparse::state_type state) const {
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getSilentProbability(storm::storage::sparse::state_type state) const {
STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silent probability of state, because silent probabilities are not tracked.");
return this->silentProbabilities[state];
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setSilentProbabilities(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setSilentProbabilities(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
for (; first != last; ++first) {
this->silentProbabilities[first->first] = first->second;
@@ -502,7 +502,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setSilentProbabilitiesToZero(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setSilentProbabilitiesToZero(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
for (; first != last; ++first) {
this->silentProbabilities[first->first] = storm::utility::zero<ValueType>();
@@ -510,28 +510,28 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) {
STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
this->silentProbabilities[state] = value;
}
template<typename ValueType>
- std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
+ std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block> const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
return this->blocks;
}
template<typename ValueType>
- std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getStatesAndValues() {
+ std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getStatesAndValues() {
return this->statesAndValues;
}
template<typename ValueType>
- std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() {
+ std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() {
return this->blocks;
}
template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::check() const {
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::check() const {
for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
if (this->statesAndValues[this->positions[state]].first != state) {
assert(false);
@@ -549,7 +549,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::print() const {
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::print() const {
for (auto const& block : this->blocks) {
block.print(*this);
}
@@ -571,51 +571,53 @@ namespace storm {
}
template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::size() const {
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Partition::size() const {
return this->blocks.size();
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator(0) {
+ 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.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
- partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient);
+ partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient);
}
template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
- partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient);
+ partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, 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) {
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, 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_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, false, buildQuotient);
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, 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) {
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, 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_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, false, buildQuotient);
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient);
}
template<typename ValueType>
- std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelStrongBisimulationDecomposition<ValueType>::getQuotient() const {
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelBisimulationDecomposition<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>
template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, bool weak) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) {
// In order to create the quotient model, we need to construct
// (a) the new transition matrix,
// (b) the new labeling,
@@ -641,7 +643,7 @@ namespace storm {
storm::storage::sparse::state_type representativeState = *block.begin();
// However, for weak bisimulation, we need to make sure the representative state is a non-silent one.
- if (weak) {
+ if (bisimulationType == BisimulationType::WeakDtmc) {
for (auto const& state : block) {
if (!partition.isSilent(state, comparator)) {
representativeState = state;
@@ -674,7 +676,7 @@ namespace storm {
storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId();
// If we are computing a weak bisimulation quotient, there is no need to add self-loops.
- if (weak && targetBlock == blockIndex) {
+ if ((bisimulationType == BisimulationType::WeakDtmc || bisimulationType == BisimulationType::WeakCtmc) && targetBlock == blockIndex) {
continue;
}
@@ -688,7 +690,7 @@ namespace storm {
// Now add them to the actual matrix.
for (auto const& probabilityEntry : blockProbability) {
- if (weak) {
+ if (bisimulationType == BisimulationType::WeakDtmc) {
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second / (storm::utility::one<ValueType>() - partition.getSilentProbability(representativeState)));
} else {
builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
@@ -725,7 +727,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, 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();
// Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
@@ -744,7 +746,7 @@ namespace storm {
splitter->unmarkAsSplitter();
// Now refine the partition using the current splitter.
- refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, weak, splitterQueue);
+ refinePartition(model.getTransitionMatrix(), backwardTransitions, *splitter, partition, bisimulationType, splitterQueue);
}
std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart;
@@ -763,7 +765,7 @@ namespace storm {
// If we are required to build the quotient model, do so now.
if (buildQuotient) {
- this->buildQuotient(model, partition, weak);
+ this->buildQuotient(model, partition, bisimulationType);
}
std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart;
@@ -781,7 +783,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue) {
// Sort the states in the block based on their probabilities.
std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.second < b.second; } );
@@ -831,7 +833,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue) {
std::vector<uint_fast64_t> splitPoints = getSplitPointsWeak(block, partition);
// Restore the original begin of the block.
@@ -952,7 +954,7 @@ namespace storm {
}
template<typename ValueType>
- std::vector<uint_fast64_t> DeterministicModelStrongBisimulationDecomposition<ValueType>::getSplitPointsWeak(Block& block, Partition& partition) {
+ std::vector<uint_fast64_t> DeterministicModelBisimulationDecomposition<ValueType>::getSplitPointsWeak(Block& block, Partition& partition) {
std::vector<uint_fast64_t> result;
// We first scale all probabilities with (1-p[s]) where p[s] is the silent probability of state s.
std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair<storm::storage::sparse::state_type, ValueType>& stateValuePair) {
@@ -1003,7 +1005,7 @@ namespace storm {
}
template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue) {
std::list<Block*> predecessorBlocks;
// Iterate over all states of the splitter and check its predecessors.
@@ -1101,7 +1103,7 @@ namespace storm {
}
}
- if (!weak) {
+ if (bisimulationType == BisimulationType::Strong || bisimulationType == BisimulationType::WeakCtmc) {
std::list<Block*> blocksToSplit;
// Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
@@ -1136,9 +1138,15 @@ namespace storm {
continue;
}
- refineBlockProbabilities(*blockPtr, partition, splitterQueue);
+ // In the case of weak bisimulation for CTMCs, we don't need to make sure the rate of staying inside
+ // the own block is the same.
+ if (bisimulationType == BisimulationType::WeakCtmc && blockPtr == &splitter) {
+ continue;
+ }
+
+ refineBlockProbabilities(*blockPtr, partition, bisimulationType, splitterQueue);
}
- } else {
+ } else { // In this case, we are computing a weak bisimulation on a DTMC.
// If the splitter was a predecessor of itself and we are computing a weak bisimulation, we need to update
// the silent probabilities.
if (splitterIsPredecessor) {
@@ -1169,90 +1177,103 @@ namespace storm {
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) {
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, 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);
+
+ // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
+ // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
+ if (weak) {
+ this->splitOffDivergentStates(model, backwardTransitions, partition);
+ this->initializeSilentProbabilities(model, partition);
+ }
+
return partition;
}
template<typename ValueType>
template<typename ModelType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak) {
- Partition partition(model.getNumberOfStates(), weak);
- for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
- if (label == "init") {
- continue;
- }
- partition.splitLabel(model.getLabeledStates(label));
- }
-
- // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
- // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
- if (weak) {
- std::vector<storm::storage::sparse::state_type> stateStack;
- stateStack.reserve(model.getNumberOfStates());
- storm::storage::BitVector nondivergentStates(model.getNumberOfStates());
- for (auto& block : partition.getBlocks()) {
- nondivergentStates.clear();
+ void DeterministicModelBisimulationDecomposition<ValueType>::splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition) {
+ std::vector<storm::storage::sparse::state_type> stateStack;
+ stateStack.reserve(model.getNumberOfStates());
+ storm::storage::BitVector nondivergentStates(model.getNumberOfStates());
+ for (auto& block : partition.getBlocks()) {
+ nondivergentStates.clear();
+
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
+ if (nondivergentStates.get(stateIt->first)) {
+ continue;
+ }
- for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
- if (nondivergentStates.get(stateIt->first)) {
- continue;
- }
-
- // Now traverse the forward transitions of the current state and check whether there is a
- // transition to some other block.
- bool isDirectlyNonDivergent = false;
- for (auto const& successor : model.getRows(stateIt->first)) {
- // If there is such a transition, then we can mark all states in the current block that can
- // reach the state as non-divergent.
- if (&partition.getBlock(successor.getColumn()) != &block) {
- isDirectlyNonDivergent = true;
- break;
- }
+ // Now traverse the forward transitions of the current state and check whether there is a
+ // transition to some other block.
+ bool isDirectlyNonDivergent = false;
+ for (auto const& successor : model.getRows(stateIt->first)) {
+ // If there is such a transition, then we can mark all states in the current block that can
+ // reach the state as non-divergent.
+ if (&partition.getBlock(successor.getColumn()) != &block) {
+ isDirectlyNonDivergent = true;
+ break;
}
+ }
+
+ if (isDirectlyNonDivergent) {
+ stateStack.push_back(stateIt->first);
- if (isDirectlyNonDivergent) {
- stateStack.push_back(stateIt->first);
+ while (!stateStack.empty()) {
+ storm::storage::sparse::state_type currentState = stateStack.back();
+ stateStack.pop_back();
+ nondivergentStates.set(currentState);
- while (!stateStack.empty()) {
- storm::storage::sparse::state_type currentState = stateStack.back();
- stateStack.pop_back();
- nondivergentStates.set(currentState);
-
- for (auto const& predecessor : backwardTransitions.getRow(currentState)) {
- if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) {
- stateStack.push_back(predecessor.getColumn());
- }
+ for (auto const& predecessor : backwardTransitions.getRow(currentState)) {
+ if (&partition.getBlock(predecessor.getColumn()) == &block && !nondivergentStates.get(predecessor.getColumn())) {
+ stateStack.push_back(predecessor.getColumn());
}
}
}
}
+ }
+
+
+ if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) {
+ // Now that we have determined all (non)divergent states in the current block, we need to split them
+ // off.
+ std::sort(partition.getBegin(block), partition.getEnd(block), [&nondivergentStates] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return nondivergentStates.get(a.first) && !nondivergentStates.get(b.first); } );
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.getBegin();
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(stateIt->first, position);
+ }
+ // Finally, split the block.
+ Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits());
- if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) {
- // Now that we have determined all (non)divergent states in the current block, we need to split them
- // off.
- std::sort(partition.getBegin(block), partition.getEnd(block), [&nondivergentStates] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return nondivergentStates.get(a.first) && !nondivergentStates.get(b.first); } );
- // Update the positions vector.
- storm::storage::sparse::state_type position = block.getBegin();
- for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
- partition.setPosition(stateIt->first, position);
- }
-
- // Finally, split the block.
- Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits());
-
- // Since the remaining states in the block are divergent, we can mark the block as absorbing.
- // This also guarantees that the self-loop will be added to the state of the quotient
- // representing this block of states.
- block.setAbsorbing(true);
- } else if (nondivergentStates.getNumberOfSetBits() == 0) {
- // If there are only diverging states in the block, we need to make it absorbing.
- block.setAbsorbing(true);
- }
+ // Since the remaining states in the block are divergent, we can mark the block as absorbing.
+ // This also guarantees that the self-loop will be added to the state of the quotient
+ // representing this block of states.
+ block.setAbsorbing(true);
+ } else if (nondivergentStates.getNumberOfSetBits() == 0) {
+ // If there are only diverging states in the block, we need to make it absorbing.
+ block.setAbsorbing(true);
}
-
+ }
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak) {
+ Partition partition(model.getNumberOfStates(), weak);
+ for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(model.getLabeledStates(label));
+ }
+
+ // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
+ // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
+ if (weak) {
+ this->splitOffDivergentStates(model, backwardTransitions, partition);
this->initializeSilentProbabilities(model, partition);
}
return partition;
@@ -1260,7 +1281,7 @@ namespace storm {
template<typename ValueType>
template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::initializeSilentProbabilities(ModelType const& model, Partition& partition) {
+ void DeterministicModelBisimulationDecomposition<ValueType>::initializeSilentProbabilities(ModelType const& model, Partition& partition) {
for (auto const& block : partition.getBlocks()) {
for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
ValueType silentProbability = storm::utility::zero<ValueType>();
@@ -1276,6 +1297,6 @@ namespace storm {
}
}
- template class DeterministicModelStrongBisimulationDecomposition<double>;
+ template class DeterministicModelBisimulationDecomposition<double>;
}
}
\ No newline at end of file
diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h
similarity index 89%
rename from src/storage/DeterministicModelStrongBisimulationDecomposition.h
rename to src/storage/DeterministicModelBisimulationDecomposition.h
index 9719569d3..a14d5af1b 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h
+++ b/src/storage/DeterministicModelBisimulationDecomposition.h
@@ -1,5 +1,5 @@
-#ifndef STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_
-#define STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_
+#ifndef STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_
+#define STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_
#include <queue>
#include <deque>
@@ -19,23 +19,25 @@ namespace storm {
* This class represents the decomposition model into its (strong) bisimulation quotient.
*/
template <typename ValueType>
- class DeterministicModelStrongBisimulationDecomposition : public Decomposition<StateBlock> {
+ class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
public:
/*!
* Decomposes the given DTMC into equivalence classes under weak or strong bisimulation.
*
* @param model The model to decompose.
+ * @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.
*/
- DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
* Decomposes the given CTMC into equivalence classes under weak or strong bisimulation.
*
* @param model The model to decompose.
+ * @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.
*/
- DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
* Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -44,10 +46,11 @@ namespace storm {
* @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 weak A flag indication whether a weak bisimulation is to be computed.
* @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::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false);
/*!
* Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -56,10 +59,11 @@ namespace storm {
* @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 weak A flag indication whether a weak bisimulation is to be computed.
* @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);
+ DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false);
/*!
* Retrieves the quotient of the model under the previously computed bisimulation.
@@ -69,6 +73,8 @@ namespace storm {
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> getQuotient() const;
private:
+ enum class BisimulationType { Strong, WeakDtmc, WeakCtmc };
+
class Partition;
class Block {
@@ -390,12 +396,12 @@ namespace storm {
* @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 weak A flag indicating whether a weak or a strong bisimulation is to be computed.
+ * @param bisimulationType The kind of bisimulation that is to be computed.
* @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 weak, bool buildQuotient);
+ void partitionRefinement(ModelType const& model, 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
@@ -406,21 +412,22 @@ namespace storm {
* probabilities).
* @param splitter The splitter to use.
* @param partition The partition to split.
- * @param weak A flag indicating whether a weak or a strong bisimulation is to be computed.
+ * @param bisimulationType The kind of bisimulation that is to be computed.
* @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& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque<Block*>& splitterQueue);
+ void refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, 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 bisimulationType The kind of bisimulation that is to be computed.
* @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 refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue);
void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue);
@@ -440,10 +447,10 @@ namespace storm {
* determining the transitions of each equivalence class.
* @param partition The previously computed partition. This is used for quickly retrieving the block of a
* state.
- * @param weak A flag indicating whether the quotient is built for weak bisimulation.
+ * @param bisimulationType The kind of bisimulation that is to be computed.
*/
template<typename ModelType>
- void buildQuotient(ModelType const& model, Partition const& partition, bool weak);
+ void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType);
/*!
* Creates the measure-driven initial partition for reaching psi states from phi states.
@@ -453,12 +460,13 @@ namespace storm {
* @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 weak A flag indicating whether a weak bisimulation is to be computed.
* @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);
+ Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded = false);
/*!
* Creates the initial partition based on all the labels in the given model.
@@ -471,6 +479,17 @@ namespace storm {
template<typename ModelType>
Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak);
+ /*!
+ * Splits all blocks of the given partition into a block that contains all divergent states and another block
+ * containing the non-divergent states.
+ *
+ * @param model The model from which to look-up the probabilities.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param partition The partition that holds the silent probabilities.
+ */
+ template<typename ModelType>
+ void splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition);
+
/*!
* Initializes the silent probabilities by traversing all blocks and adding the probability of going to
* the very own equivalence class for each state.
@@ -490,4 +509,4 @@ namespace storm {
}
}
-#endif /* STORM_STORAGE_DETERMINISTICMODELSTRONGBISIMULATIONDECOMPOSITION_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_DeterministicModelBisimulationDecomposition_H_ */
\ No newline at end of file
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 925f085d1..df8aa248a 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -47,7 +47,7 @@ log4cplus::Logger logger;
// Headers for model processing.
#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
-#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
// Headers for model checking.
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@@ -271,7 +271,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::DeterministicModelStrongBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
result = bisimulationDecomposition.getQuotient();