From e54a774e800bc7e73ed8a66011f48befbbbfa20a Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 21 Oct 2014 22:26:34 +0200 Subject: [PATCH 01/11] Minor spellcheck. Former-commit-id: cc9ce2cfaea5dafb8eb6b91d59040e3787d9d608 --- src/properties/actions/BoundAction.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/properties/actions/BoundAction.h b/src/properties/actions/BoundAction.h index e911b9ca9..cddb36c0b 100644 --- a/src/properties/actions/BoundAction.h +++ b/src/properties/actions/BoundAction.h @@ -161,8 +161,7 @@ namespace storm { } } } else { - - //Fill the selction by comapring the values for all previously selected states with theegiven bound using the comparison operator. + // Fill the selection by comparing the values of all previously selected states with the given bound using the comparison operator. for(uint_fast64_t i = 0; i < result.stateMap.size(); i++) { if(result.selection[i]) { switch(comparisonOperator) { From eb9c1de59ba7699b2fc6a87c71990c9603b2e65b Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 22 Oct 2014 17:15:09 +0200 Subject: [PATCH 02/11] Added Boost DECLTYPE for MSVC. Former-commit-id: c70dfa5e6340d5dd626fffe002c99b9014a7f5b6 --- CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 2864e3882..91a8d7c7f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -118,6 +118,8 @@ elseif(MSVC) add_definitions(/D_VARIADIC_MAX=10) # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max add_definitions(/DNOMINMAX) + # Boost Defs + add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE) # since nobody cares at the moment add_definitions(/wd4250) From 1a4d4fd5a78becf88cd14d330c7dba042f0c42e1 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 22 Oct 2014 18:56:12 +0200 Subject: [PATCH 03/11] Added a test I used for finding the SCC Bug. Former-commit-id: 5936e79d04cb72fa389fd12d68030b850a514c45 --- ...glyConnectedComponentDecompositionTest.cpp | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp index a5872a921..48ece1776 100644 --- a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -1,9 +1,40 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/AutoParser.h" +#include "src/storage/SparseMatrix.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/MarkovAutomaton.h" + +TEST(StronglyConnectedComponentDecomposition, SmallSystemFromMatrix) { + storm::storage::SparseMatrixBuilder matrixBuilder(6, 6); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 0.3)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 5, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 2, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 1, 0.4)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, 0.3)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 3, 0.3)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 4, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 4, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(5, 1, 1.0)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + storm::storage::BitVector allBits(6, true); + + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, false, false)); + ASSERT_EQ(4, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, false)); + ASSERT_EQ(3, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(matrix, allBits, true, true)); + ASSERT_EQ(1, sccDecomposition.size()); +} + TEST(StronglyConnectedComponentDecomposition, FullSystem1) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); From 97158ee72e3e8d9299a175de01a7b4c573aa85a5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 22 Oct 2014 20:24:50 +0200 Subject: [PATCH 04/11] 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 - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) { + DeterministicModelStrongBisimulationDecomposition::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::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr); it->setIterator(it); @@ -263,7 +263,7 @@ namespace storm { } template - DeterministicModelStrongBisimulationDecomposition::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::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::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 blocks; @@ -355,6 +358,13 @@ namespace storm { // This vector keeps track of the position of each state in the state vector. std::vector 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 silentProbabilities; }; /*! From 56aec18a48ea3d584b01672fd11b16e401a18517 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Oct 2014 18:05:51 +0200 Subject: [PATCH 05/11] 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(new modules::CuddSettings(*this))); this->addModule(std::unique_ptr(new modules::GmmxxEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::NativeEquationSolverSettings(*this))); + this->addModule(std::unique_ptr(new modules::BisimulationSettings(*this))); this->addModule(std::unique_ptr(new modules::GlpkSettings(*this))); this->addModule(std::unique_ptr(new modules::GurobiSettings(*this))); } @@ -495,6 +496,10 @@ namespace storm { return dynamic_cast(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName)); } + storm::settings::modules::BisimulationSettings const& bisimulationSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::BisimulationSettings::moduleName)); + } + storm::settings::modules::GlpkSettings const& glpkSettings() { return dynamic_cast(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 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 +#include #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::const_iterator first1 = this->bucketVector.begin(); + std::vector::const_iterator last1 = this->bucketVector.end(); + std::vector::const_iterator first2 = other.bucketVector.begin(); + std::vector::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(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 bool DeterministicModelStrongBisimulationDecomposition::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(numberOfStates); + } } template @@ -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(numberOfStates); + } } template @@ -469,6 +473,46 @@ namespace storm { } } + template + bool DeterministicModelStrongBisimulationDecomposition::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator 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 + bool DeterministicModelStrongBisimulationDecomposition::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator 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 + ValueType const& DeterministicModelStrongBisimulationDecomposition::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 + void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbabilities(typename std::vector>::iterator first, typename std::vector>::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 + void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::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(); + } + } + + template + void DeterministicModelStrongBisimulationDecomposition::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 std::list::Block> const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() const { return this->blocks; @@ -530,17 +574,23 @@ namespace storm { } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool buildQuotient) { + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - Partition initialPartition = getLabelBasedInitialPartition(model); - 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 - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool buildQuotient) { + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - Partition initialPartition = getLabelBasedInitialPartition(model); - 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 @@ -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 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 @@ -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 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 @@ -648,7 +698,7 @@ namespace storm { template template - void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool buildQuotient) { + void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix 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(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>::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 + void DeterministicModelStrongBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { + std::vector 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 stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1)); + + std::vector 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 const& a, std::pair 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>::const_iterator begin = partition.getBegin(block); + typename std::vector>::const_iterator current = begin; + typename std::vector>::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 - void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue) { + std::vector DeterministicModelStrongBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition) { + std::vector 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& stateValuePair) { + ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first); + if (!comparator.isOne(silentProbability)) { + stateValuePair.second /= storm::utility::one() - silentProbability; + } + }); + + // Now sort the states based on their probabilities. + std::sort(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&partition] (std::pair const& a, std::pair 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>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin(); + typename std::vector>::const_iterator current = begin; + typename std::vector>::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 + void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue) { std::list 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 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 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 template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model) { - Partition partition(model.getNumberOfStates()); + typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::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 + template + void DeterministicModelStrongBisimulationDecomposition::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(); + + 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; } } \ 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 { 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 const& model, bool buildQuotient = false); + DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc 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 const& model, bool buildQuotient = false); + DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc 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>::iterator first, typename std::vector>::iterator end); + void updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::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 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 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>::iterator first, typename std::vector>::iterator last); + + // Sets the silent probabilities for all states in the range to zero. + void setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::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 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 - void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool buildQuotient); + void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix 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 const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue); + void refinePartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& 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& splitterQueue); + void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& backwardTransitions, std::deque& 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 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 - 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 + void initializeSilentProbabilities(ModelType const& model, Partition& partition); // If required, a quotient model is built and stored in this member. std::shared_ptr> 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> dtmc = result->template as>(); STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); - storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); + storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); result = bisimulationDecomposition.getQuotient(); From eeb859272f684ef9408c3babccdbc49d9c549e05 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 23 Oct 2014 18:58:51 +0200 Subject: [PATCH 06/11] 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 (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (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 Date: Thu, 23 Oct 2014 20:05:44 +0200 Subject: [PATCH 07/11] Further work on weak bisimulation. Former-commit-id: 3ad48ee0a353630c0d1cedf9c961cbda7e7e8e0a --- examples/dtmc/brp/brp.pm | 10 +++-- src/storage/BitVector.cpp | 4 ++ src/storage/BitVector.h | 9 +++++ ...icModelStrongBisimulationDecomposition.cpp | 39 ++++++++++++++----- 4 files changed, 48 insertions(+), 14 deletions(-) diff --git a/examples/dtmc/brp/brp.pm b/examples/dtmc/brp/brp.pm index f2eacc9ff..e09ed3e2c 100644 --- a/examples/dtmc/brp/brp.pm +++ b/examples/dtmc/brp/brp.pm @@ -127,8 +127,10 @@ module channelL // lost [TO_Ack] (l=2) -> (l'=0); -endmodule - -rewards - [aF] i=1 : 1; +endmodule + +rewards + [aF] i=1 : 1; endrewards + +label "target" = s=5; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index b1c5003ce..0fb08f028 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -144,6 +144,10 @@ namespace storm { return true; } + bool BitVector::operator!=(BitVector const& other) { + return !(*this == other); + } + void BitVector::set(uint_fast64_t index, bool value) { if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::set: written index " << index << " out of bounds."; uint_fast64_t bucket = index >> 6; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index f20c00005..806febcc9 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -135,9 +135,18 @@ namespace storm { * Compares the given bit vector with the current one. * * @param other The bitvector with which to compare the current one. + * @return True iff the other bit vector is semantically the same as the current one. */ bool operator==(BitVector const& other); + /*! + * Compares the given bit vector with the current one. + * + * @param other The bitvector with which to compare the current one. + * @return True iff the other bit vector is semantically not the same as the current one. + */ + bool operator!=(BitVector const& other); + /*! * Assigns the contents of the given bit vector to the current bit vector via a deep copy. * diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index 97f054f1b..fba714149 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -577,9 +577,6 @@ namespace storm { DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); Partition initialPartition = getLabelBasedInitialPartition(model, weak); - if (weak) { - this->initializeSilentProbabilities(model, initialPartition); - } partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient); } @@ -587,9 +584,6 @@ namespace storm { DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); Partition initialPartition = getLabelBasedInitialPartition(model, weak); - if (weak) { - this->initializeSilentProbabilities(model, initialPartition); - } partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient); } @@ -709,6 +703,8 @@ namespace storm { // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); + std::cout << "refining with splitter " << splitterQueue.front()->getId() << std::endl; + partition.print(); refinePartition(backwardTransitions, *splitterQueue.front(), partition, weak, splitterQueue); splitterQueue.pop_front(); } @@ -848,6 +844,15 @@ namespace storm { // labels and then scan for ranges that agree on the label. std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair const& a, std::pair const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; }); + for (auto const& label : stateLabels) { + std::cout << label << std::endl; + } + + std::cout << "sorted?" << std::endl; + for (auto it = partition.getBegin(block), ite = partition.getEnd(block); it != ite; ++it) { + std::cout << stateLabels[partition.getPosition(it->first) - block.getBegin()] << std::endl; + } + // Update the positions vector. storm::storage::sparse::state_type position = block.getBegin(); for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { @@ -862,16 +867,16 @@ namespace storm { // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. - bool blockSplit = !comparator.isEqual(begin->second, end->second); - while (!comparator.isEqual(begin->second, end->second)) { + bool blockSplit = stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()]; + while (stateLabels[partition.getPosition(begin->first) - block.getBegin()] != stateLabels[partition.getPosition(end->first) - block.getBegin()]) { // Now we scan for the first state in the block that disagrees on the labeling value. // Note that we do not have to check currentIndex for staying within bounds, because we know the matching // state is within bounds. - ValueType const& currentValue = begin->second; + storm::storage::BitVector const& currentValue = stateLabels[partition.getPosition(begin->first) - block.getBegin()]; ++begin; ++currentIndex; - while (begin != end && comparator.isEqual(begin->second, currentValue)) { + while (begin != end && stateLabels[partition.getPosition(begin->first) - block.getBegin()] == currentValue) { ++begin; ++currentIndex; } @@ -879,6 +884,7 @@ namespace storm { // Now we split the block and mark it as a potential splitter. Block& newBlock = partition.splitBlock(block, currentIndex); if (!newBlock.isMarkedAsSplitter()) { + std::cout << "adding block " << newBlock.getId() << " as splitter" << std::endl; splitterQueue.push_back(&newBlock); newBlock.markAsSplitter(); } @@ -900,7 +906,9 @@ namespace storm { std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair& stateValuePair) { ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first); if (!comparator.isOne(silentProbability)) { + std::cout << "before: " << stateValuePair.second << std::endl; stateValuePair.second /= storm::utility::one() - silentProbability; + std::cout << "scaled: " << stateValuePair.second << std::endl; } }); @@ -1095,8 +1103,11 @@ namespace storm { // If the splitter is also the predecessor block, we must not refine it at this point. if (&block != &splitter) { + std::cout << "refining pred block " << block.getId() << std::endl; refineBlockWeak(block, partition, backwardTransitions, splitterQueue); } else { + Block& newBlock = partition.insertBlock(block); + // Restore the begin of the block. block.setBegin(block.getOriginalBegin()); } @@ -1125,6 +1136,14 @@ namespace storm { } partition.splitLabel(model.getLabeledStates(label)); } + + // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent + // states of each initial block and (b) initialize the vector of silent probabilities held by the partition. + if (weak) { + // FIXME: split off divergent states. + + this->initializeSilentProbabilities(model, partition); + } return partition; } From 391f3225e4e13ab19758ee6b05cecf0be3a5b4b2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 24 Oct 2014 16:21:39 +0200 Subject: [PATCH 08/11] 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 (s'=1); // do next nand if have not done N yet + [] s=0 & (c=N) & (u (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 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 (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 (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 void DeterministicModelStrongBisimulationDecomposition::Block::incrementBegin() { ++this->begin; - } - - template - void DeterministicModelStrongBisimulationDecomposition::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 @@ -149,6 +154,7 @@ namespace storm { template bool DeterministicModelStrongBisimulationDecomposition::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 DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - Partition initialPartition = getLabelBasedInitialPartition(model, weak); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); + partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient); } template DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - Partition initialPartition = getLabelBasedInitialPartition(model, weak); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak, buildQuotient); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak); + partitionRefinement(model, backwardTransitions, initialPartition, weak, buildQuotient); } template @@ -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 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 - void DeterministicModelStrongBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { + void DeterministicModelStrongBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { std::vector 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 const& a, std::pair 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>::const_iterator begin = partition.getBegin(block); typename std::vector>::const_iterator current = begin; typename std::vector>::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(); + 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(); + 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& 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() - 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>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin(); typename std::vector>::const_iterator current = begin; typename std::vector>::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 - void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue) { + void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue) { std::list 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 @@ -1128,7 +1212,7 @@ namespace storm { template template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, bool weak) { + typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix 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 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 const& a, std::pair 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 const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue); + void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& 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& splitterQueue); - void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue); + void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& 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 - Partition getLabelBasedInitialPartition(ModelType const& model, bool weak); + Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix 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 Date: Fri, 24 Oct 2014 18:50:44 +0200 Subject: [PATCH 09/11] 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 void DeterministicModelStrongBisimulationDecomposition::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 bool DeterministicModelStrongBisimulationDecomposition::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 template - void DeterministicModelStrongBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition) { + void DeterministicModelStrongBisimulationDecomposition::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 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() - 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 stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1)); std::vector 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 const& a, std::pair 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>::const_iterator begin = partition.getBegin(block); typename std::vector>::const_iterator current = begin; typename std::vector>::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(); 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(); 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& 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() - 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>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin(); typename std::vector>::const_iterator current = begin; typename std::vector>::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 - 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> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty()); generateCounterexample(model, filterFormula->getChild()); + } else if (settings.isPctlPropertySet()) { + std::shared_ptr> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty()); + + if (model->getType() == storm::models::DTMC) { + std::shared_ptr> dtmc = model->as>(); + modelchecker::prctl::SparseDtmcPrctlModelChecker modelchecker(*dtmc); + filterFormula->check(modelchecker); + } } - } - } } } From f90ac5c8c39fa26407cf432eba6369c18397a016 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 25 Oct 2014 17:03:37 +0200 Subject: [PATCH 10/11] 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 - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) { + DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc 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 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 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(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 Date: Sat, 25 Oct 2014 18:09:50 +0200 Subject: [PATCH 11/11] 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 #include @@ -13,10 +13,10 @@ namespace storm { namespace storage { template - std::size_t DeterministicModelStrongBisimulationDecomposition::Block::blockId = 0; + std::size_t DeterministicModelBisimulationDecomposition::Block::blockId = 0; template - DeterministicModelStrongBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) { + DeterministicModelBisimulationDecomposition::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr 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 - void DeterministicModelStrongBisimulationDecomposition::Block::print(Partition const& partition) const { + void DeterministicModelBisimulationDecomposition::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 - void DeterministicModelStrongBisimulationDecomposition::Block::setBegin(storm::storage::sparse::state_type begin) { + void DeterministicModelBisimulationDecomposition::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 - void DeterministicModelStrongBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { + void DeterministicModelBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { this->end = end; STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); } template - void DeterministicModelStrongBisimulationDecomposition::Block::incrementBegin() { + void DeterministicModelBisimulationDecomposition::Block::incrementBegin() { ++this->begin; STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size."); } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getBegin() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getBegin() const { return this->begin; } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getOriginalBegin() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getOriginalBegin() const { if (this->hasPreviousBlock()) { return this->getPreviousBlock().getEnd(); } else { @@ -85,72 +85,72 @@ namespace storm { } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getEnd() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getEnd() const { return this->end; } template - void DeterministicModelStrongBisimulationDecomposition::Block::setIterator(iterator it) { + void DeterministicModelBisimulationDecomposition::Block::setIterator(iterator it) { this->selfIt = it; } template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getIterator() const { return this->selfIt; } template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getNextIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getNextIterator() const { return this->getNextBlock().getIterator(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getPreviousIterator() const { + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getPreviousIterator() const { return this->getPreviousBlock().getIterator(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getNextBlock() { return *this->next; } template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getNextBlock() const { return *this->next; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasNextBlock() const { + bool DeterministicModelBisimulationDecomposition::Block::hasNextBlock() const { return this->next != nullptr; } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() { return *this->prev; } template - typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlockPointer() { + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { return this->prev; } template - typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getNextBlockPointer() { + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { return this->next; } template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { return *this->prev; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasPreviousBlock() const { + bool DeterministicModelBisimulationDecomposition::Block::hasPreviousBlock() const { return this->prev != nullptr; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::check() const { + bool DeterministicModelBisimulationDecomposition::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 - std::size_t DeterministicModelStrongBisimulationDecomposition::Block::getNumberOfStates() const { + std::size_t DeterministicModelBisimulationDecomposition::Block::getNumberOfStates() const { // We need to take the original begin here, because the begin is temporarily moved. return (this->end - this->getOriginalBegin()); } template - bool DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsSplitter() const { + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsSplitter() const { return this->markedAsSplitter; } template - void DeterministicModelStrongBisimulationDecomposition::Block::markAsSplitter() { + void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { this->markedAsSplitter = true; } template - void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsSplitter() { + void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { this->markedAsSplitter = false; } template - std::size_t DeterministicModelStrongBisimulationDecomposition::Block::getId() const { + std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { return this->id; } template - void DeterministicModelStrongBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { + void DeterministicModelBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { this->absorbing = absorbing; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::isAbsorbing() const { + bool DeterministicModelBisimulationDecomposition::Block::isAbsorbing() const { return this->absorbing; } template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getMarkedPosition() const { + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { return this->markedPosition; } template - void DeterministicModelStrongBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { + void DeterministicModelBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { this->markedPosition = position; } template - void DeterministicModelStrongBisimulationDecomposition::Block::resetMarkedPosition() { + void DeterministicModelBisimulationDecomposition::Block::resetMarkedPosition() { this->markedPosition = this->begin; } template - void DeterministicModelStrongBisimulationDecomposition::Block::incrementMarkedPosition() { + void DeterministicModelBisimulationDecomposition::Block::incrementMarkedPosition() { ++this->markedPosition; } template - void DeterministicModelStrongBisimulationDecomposition::Block::markAsPredecessorBlock() { + void DeterministicModelBisimulationDecomposition::Block::markAsPredecessorBlock() { this->markedAsPredecessorBlock = true; } template - void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { + void DeterministicModelBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { this->markedAsPredecessorBlock = false; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsPredecessor() const { + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsPredecessor() const { return markedAsPredecessorBlock; } template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasLabel() const { + bool DeterministicModelBisimulationDecomposition::Block::hasLabel() const { return this->label != nullptr; } template - std::string const& DeterministicModelStrongBisimulationDecomposition::Block::getLabel() const { + std::string const& DeterministicModelBisimulationDecomposition::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 - std::shared_ptr const& DeterministicModelStrongBisimulationDecomposition::Block::getLabelPtr() const { + std::shared_ptr const& DeterministicModelBisimulationDecomposition::Block::getLabelPtr() const { return this->label; } template - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { + DeterministicModelBisimulationDecomposition::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::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr); it->setIterator(it); @@ -264,7 +264,7 @@ namespace storm { } template - DeterministicModelStrongBisimulationDecomposition::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::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::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 - void DeterministicModelStrongBisimulationDecomposition::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + void DeterministicModelBisimulationDecomposition::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 - void DeterministicModelStrongBisimulationDecomposition::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { + void DeterministicModelBisimulationDecomposition::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 - storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::Partition::getPosition(storm::storage::sparse::state_type state) const { + storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getPosition(storm::storage::sparse::state_type state) const { return this->positions[state]; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { + void DeterministicModelBisimulationDecomposition::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { this->positions[state] = position; } template - storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { + storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { return this->statesAndValues[position].first; } template - ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { return this->statesAndValues[this->positions[state]].second; } template - ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { return this->statesAndValues[position].second; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { this->statesAndValues[this->positions[state]].second = value; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { + void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { this->statesAndValues[this->positions[state]].second += value; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last) { for (; first != last; ++first) { this->stateToBlockMapping[first->first] = █ } } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::getFirstBlock() { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getFirstBlock() { return *this->blocks.begin(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { return *this->stateToBlockMapping[state]; } template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { return *this->stateToBlockMapping[state]; } template - typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) { + typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) { return this->statesAndValues.begin() + block.getBegin(); } template - typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) { + typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) { return this->statesAndValues.begin() + block.getEnd(); } template - typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) const { + typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) const { return this->statesAndValues.begin() + block.getBegin(); } template - typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) const { + typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) const { return this->statesAndValues.begin() + block.getEnd(); } template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::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 DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::insertBlock(Block& block) { + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::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 - void DeterministicModelStrongBisimulationDecomposition::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) { + void DeterministicModelBisimulationDecomposition::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 - bool DeterministicModelStrongBisimulationDecomposition::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const { + bool DeterministicModelBisimulationDecomposition::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator 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 - bool DeterministicModelStrongBisimulationDecomposition::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator const& comparator) const { + bool DeterministicModelBisimulationDecomposition::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator 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 - ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getSilentProbability(storm::storage::sparse::state_type state) const { + ValueType const& DeterministicModelBisimulationDecomposition::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 - void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbabilities(typename std::vector>::iterator first, typename std::vector>::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::setSilentProbabilities(typename std::vector>::iterator first, typename std::vector>::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 - void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::iterator last) { + void DeterministicModelBisimulationDecomposition::Partition::setSilentProbabilitiesToZero(typename std::vector>::iterator first, typename std::vector>::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(); @@ -510,28 +510,28 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) { + void DeterministicModelBisimulationDecomposition::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 - std::list::Block> const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() const { + std::list::Block> const& DeterministicModelBisimulationDecomposition::Partition::getBlocks() const { return this->blocks; } template - std::vector>& DeterministicModelStrongBisimulationDecomposition::Partition::getStatesAndValues() { + std::vector>& DeterministicModelBisimulationDecomposition::Partition::getStatesAndValues() { return this->statesAndValues; } template - std::list::Block>& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() { + std::list::Block>& DeterministicModelBisimulationDecomposition::Partition::getBlocks() { return this->blocks; } template - bool DeterministicModelStrongBisimulationDecomposition::Partition::check() const { + bool DeterministicModelBisimulationDecomposition::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 - void DeterministicModelStrongBisimulationDecomposition::Partition::print() const { + void DeterministicModelBisimulationDecomposition::Partition::print() const { for (auto const& block : this->blocks) { block.print(*this); } @@ -571,51 +571,53 @@ namespace storm { } template - std::size_t DeterministicModelStrongBisimulationDecomposition::Partition::size() const { + std::size_t DeterministicModelBisimulationDecomposition::Partition::size() const { return this->blocks.size(); } template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool weak, bool buildQuotient) : comparator(0) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc 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 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 - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc const& model, bool weak, bool buildQuotient) { STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); storm::storage::SparseMatrix 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 - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Dtmc 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 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 - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(storm::models::Ctmc 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 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 - std::shared_ptr> DeterministicModelStrongBisimulationDecomposition::getQuotient() const { + std::shared_ptr> DeterministicModelBisimulationDecomposition::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 template - void DeterministicModelStrongBisimulationDecomposition::buildQuotient(ModelType const& model, Partition const& partition, bool weak) { + void DeterministicModelBisimulationDecomposition::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() - partition.getSilentProbability(representativeState))); } else { builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); @@ -725,7 +727,7 @@ namespace storm { template template - void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient) { + void DeterministicModelBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix 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 - void DeterministicModelStrongBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { // Sort the states in the block based on their probabilities. std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); @@ -831,7 +833,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& splitterQueue) { std::vector splitPoints = getSplitPointsWeak(block, partition); // Restore the original begin of the block. @@ -952,7 +954,7 @@ namespace storm { } template - std::vector DeterministicModelStrongBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition) { + std::vector DeterministicModelBisimulationDecomposition::getSplitPointsWeak(Block& block, Partition& partition) { std::vector 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& stateValuePair) { @@ -1003,7 +1005,7 @@ namespace storm { } template - void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue) { std::list 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 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 template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded) { + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded) { std::pair 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 template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix 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 stateStack; - stateStack.reserve(model.getNumberOfStates()); - storm::storage::BitVector nondivergentStates(model.getNumberOfStates()); - for (auto& block : partition.getBlocks()) { - nondivergentStates.clear(); + void DeterministicModelBisimulationDecomposition::splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition) { + std::vector 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 const& a, std::pair 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 const& a, std::pair 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 + template + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix 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 template - void DeterministicModelStrongBisimulationDecomposition::initializeSilentProbabilities(ModelType const& model, Partition& partition) { + void DeterministicModelBisimulationDecomposition::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(); @@ -1276,6 +1297,6 @@ namespace storm { } } - template class DeterministicModelStrongBisimulationDecomposition; + template class DeterministicModelBisimulationDecomposition; } } \ 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 #include @@ -19,23 +19,25 @@ namespace storm { * This class represents the decomposition model into its (strong) bisimulation quotient. */ template - class DeterministicModelStrongBisimulationDecomposition : public Decomposition { + class DeterministicModelBisimulationDecomposition : public Decomposition { 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 const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc 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 const& model, bool weak = false, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc 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 const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Dtmc 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 const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false); + DeterministicModelBisimulationDecomposition(storm::models::Ctmc 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> 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 - void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool weak, bool buildQuotient); + void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix 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 const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, bool weak, std::deque& splitterQueue); + void refinePartition(storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque& 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& splitterQueue); + void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque& splitterQueue); void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix const& forwardTransitions, storm::storage::SparseMatrix const& backwardTransitions, std::deque& 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 - 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 - Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded = false); + Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix 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 Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix 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 + void splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix 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> dtmc = result->template as>(); STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl); - storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); result = bisimulationDecomposition.getQuotient();