diff --git a/CMakeLists.txt b/CMakeLists.txt index 4b74f4317..2d438e3a4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -123,8 +123,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) - # required for using boost's transform iterator - add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE) + # Boost Defs, required for using boost's transform iterator + add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE) # since nobody cares at the moment add_definitions(/wd4250) diff --git a/examples/dtmc/brp/brp.pm b/examples/dtmc/brp/brp.pm new file mode 100644 index 000000000..e09ed3e2c --- /dev/null +++ b/examples/dtmc/brp/brp.pm @@ -0,0 +1,136 @@ +// 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 + +label "target" = s=5; 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/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) { diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index c856517d8..739fa2f66 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))); this->addModule(std::unique_ptr(new modules::ParametricSettings(*this))); @@ -496,6 +497,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 632eb826a..53804a7c1 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" #include "src/settings/modules/ParametricSettings.h" @@ -287,6 +288,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..4e2f3975e --- /dev/null +++ b/src/settings/modules/BisimulationSettings.cpp @@ -0,0 +1,40 @@ +#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; + } + + 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 bisimulation 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 new file mode 100644 index 000000000..3e2d1efe7 --- /dev/null +++ b/src/settings/modules/BisimulationSettings.h @@ -0,0 +1,52 @@ +#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; + + virtual bool check() const override; + + // 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..0fb08f028 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) { @@ -121,9 +144,13 @@ namespace storm { return true; } + bool BitVector::operator!=(BitVector const& other) { + return !(*this == other); + } + 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..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. * @@ -155,7 +164,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/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp new file mode 100644 index 000000000..137525c05 --- /dev/null +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -0,0 +1,1306 @@ +#include "src/storage/DeterministicModelBisimulationDecomposition.h" + +#include +#include +#include +#include +#include + +#include "src/utility/graph.h" +#include "src/exceptions/IllegalFunctionCallException.h" + +namespace storm { + namespace storage { + + template + std::size_t DeterministicModelBisimulationDecomposition::Block::blockId = 0; + + template + 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; + } + if (prev != nullptr) { + prev->next = this; + } + STORM_LOG_ASSERT(begin < end, "Unable to create block of illegal size."); + } + + template + 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; + for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { + std::cout << partition.statesAndValues[index].first << " "; + } + std::cout << std::endl << "original: " << std::endl; + for (storm::storage::sparse::state_type index = this->getOriginalBegin(); index < this->end; ++index) { + std::cout << partition.statesAndValues[index].first << " "; + } + std::cout << std::endl << "values:" << std::endl; + 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; + } + + template + 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 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 DeterministicModelBisimulationDecomposition::Block::incrementBegin() { + ++this->begin; + STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size."); + } + + template + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getBegin() const { + return this->begin; + } + + template + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getOriginalBegin() const { + if (this->hasPreviousBlock()) { + return this->getPreviousBlock().getEnd(); + } else { + return 0; + } + } + + template + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getEnd() const { + return this->end; + } + + template + void DeterministicModelBisimulationDecomposition::Block::setIterator(iterator it) { + this->selfIt = it; + } + + template + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getIterator() const { + return this->selfIt; + } + + template + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getNextIterator() const { + return this->getNextBlock().getIterator(); + } + + template + typename DeterministicModelBisimulationDecomposition::Block::iterator DeterministicModelBisimulationDecomposition::Block::getPreviousIterator() const { + return this->getPreviousBlock().getIterator(); + } + + template + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getNextBlock() { + return *this->next; + } + + template + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getNextBlock() const { + return *this->next; + } + + template + bool DeterministicModelBisimulationDecomposition::Block::hasNextBlock() const { + return this->next != nullptr; + } + + template + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() { + return *this->prev; + } + + template + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getPreviousBlockPointer() { + return this->prev; + } + + template + typename DeterministicModelBisimulationDecomposition::Block* DeterministicModelBisimulationDecomposition::Block::getNextBlockPointer() { + return this->next; + } + + template + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Block::getPreviousBlock() const { + return *this->prev; + } + + template + bool DeterministicModelBisimulationDecomposition::Block::hasPreviousBlock() const { + return this->prev != nullptr; + } + + template + 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); + return true; + } + + template + 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 DeterministicModelBisimulationDecomposition::Block::isMarkedAsSplitter() const { + return this->markedAsSplitter; + } + + template + void DeterministicModelBisimulationDecomposition::Block::markAsSplitter() { + this->markedAsSplitter = true; + } + + template + void DeterministicModelBisimulationDecomposition::Block::unmarkAsSplitter() { + this->markedAsSplitter = false; + } + + template + std::size_t DeterministicModelBisimulationDecomposition::Block::getId() const { + return this->id; + } + + template + void DeterministicModelBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { + this->absorbing = absorbing; + } + + template + bool DeterministicModelBisimulationDecomposition::Block::isAbsorbing() const { + return this->absorbing; + } + + template + storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition::Block::getMarkedPosition() const { + return this->markedPosition; + } + + template + void DeterministicModelBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { + this->markedPosition = position; + } + + template + void DeterministicModelBisimulationDecomposition::Block::resetMarkedPosition() { + this->markedPosition = this->begin; + } + + template + void DeterministicModelBisimulationDecomposition::Block::incrementMarkedPosition() { + ++this->markedPosition; + } + + template + void DeterministicModelBisimulationDecomposition::Block::markAsPredecessorBlock() { + this->markedAsPredecessorBlock = true; + } + + template + void DeterministicModelBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { + this->markedAsPredecessorBlock = false; + } + + template + bool DeterministicModelBisimulationDecomposition::Block::isMarkedAsPredecessor() const { + return markedAsPredecessorBlock; + } + + template + bool DeterministicModelBisimulationDecomposition::Block::hasLabel() const { + return this->label != nullptr; + } + + template + 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& DeterministicModelBisimulationDecomposition::Block::getLabelPtr() const { + return this->label; + } + + template + 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); + + // Set up the different parts of the internal structure. + for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) { + statesAndValues[state] = std::make_pair(state, storm::utility::zero()); + 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 + 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); + + storm::storage::sparse::state_type position = 0; + for (auto state : prob0States) { + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); + positions[state] = position; + stateToBlockMapping[state] = &firstBlock; + ++position; + } + firstBlock.setAbsorbing(true); + + typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr(new std::string(prob1Label))); + Block& secondBlock = *secondIt; + secondBlock.setIterator(secondIt); + + for (auto state : prob1States) { + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); + positions[state] = position; + stateToBlockMapping[state] = &secondBlock; + ++position; + } + secondBlock.setAbsorbing(true); + + typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); + Block& thirdBlock = *thirdIt; + thirdBlock.setIterator(thirdIt); + + storm::storage::BitVector otherStates = ~(prob0States | prob1States); + for (auto state : otherStates) { + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); + positions[state] = position; + 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 + 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 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; + + std::swap(this->statesAndValues[position1], this->statesAndValues[position2]); + + this->positions[state1] = position2; + this->positions[state2] = position1; + } + + template + storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition::Partition::getPosition(storm::storage::sparse::state_type state) const { + return this->positions[state]; + } + + template + 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& DeterministicModelBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { + return this->statesAndValues[position].first; + } + + template + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { + return this->statesAndValues[this->positions[state]].second; + } + + template + ValueType const& DeterministicModelBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { + return this->statesAndValues[position].second; + } + + template + void DeterministicModelBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { + this->statesAndValues[this->positions[state]].second = value; + } + + template + void DeterministicModelBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { + this->statesAndValues[this->positions[state]].second += value; + } + + template + 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 DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getFirstBlock() { + return *this->blocks.begin(); + } + + template + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) { + return *this->stateToBlockMapping[state]; + } + + template + typename DeterministicModelBisimulationDecomposition::Block const& DeterministicModelBisimulationDecomposition::Partition::getBlock(storm::storage::sparse::state_type state) const { + return *this->stateToBlockMapping[state]; + } + + template + typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) { + return this->statesAndValues.begin() + block.getBegin(); + } + + template + typename std::vector>::iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) { + return this->statesAndValues.begin() + block.getEnd(); + } + + template + typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getBegin(Block const& block) const { + return this->statesAndValues.begin() + block.getBegin(); + } + + template + typename std::vector>::const_iterator DeterministicModelBisimulationDecomposition::Partition::getEnd(Block const& block) const { + return this->statesAndValues.begin() + block.getEnd(); + } + + template + 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()) { + return block; + } + + // Actually create the new block and insert it at the correct position. + typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); + selfIt->setIterator(selfIt); + Block& newBlock = *selfIt; + + // Resize the current block appropriately. + block.setBegin(position); + + // Update the mapping of the states in the newly created block. + this->updateBlockMapping(newBlock, this->getBegin(newBlock), this->getEnd(newBlock)); + + return newBlock; + } + + template + typename DeterministicModelBisimulationDecomposition::Block& DeterministicModelBisimulationDecomposition::Partition::insertBlock(Block& block) { + // Find the beginning of the new block. + storm::storage::sparse::state_type begin; + if (block.hasPreviousBlock()) { + begin = block.getPreviousBlock().getEnd(); + } else { + begin = 0; + } + + // Actually insert the new block. + typename std::list::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block); + Block& newBlock = *it; + newBlock.setIterator(it); + + // Update the mapping of the states in the newly created block. + for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) { + stateToBlockMapping[it->first] = &newBlock; + } + + return *it; + } + + template + 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; + + // Sort the range of the block such that all states that have the label are moved to the front. + std::sort(this->getBegin(block), this->getEnd(block), [&statesWithLabel] (std::pair const& a, std::pair const& b) { return statesWithLabel.get(a.first) && !statesWithLabel.get(b.first); } ); + + // Update the positions vector. + storm::storage::sparse::state_type position = block.getBegin(); + for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt, ++position) { + this->positions[stateIt->first] = position; + } + + // Now we can find the first position in the block that does not have the label and create new blocks. + typename std::vector>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair const& a) { return !statesWithLabel.get(a.first); }); + + // If not all the states agreed on the validity of the label, we need to split the block. + if (it != this->getBegin(block) && it != this->getEnd(block)) { + auto cutPoint = std::distance(this->statesAndValues.begin(), it); + this->splitBlock(block, cutPoint); + } else { + // Otherwise, we simply proceed to the next block. + ++blockIterator; + } + } + } + + template + 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 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& 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 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; + } + } + + template + 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(); + } + } + + template + 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& DeterministicModelBisimulationDecomposition::Partition::getBlocks() const { + return this->blocks; + } + + template + std::vector>& DeterministicModelBisimulationDecomposition::Partition::getStatesAndValues() { + return this->statesAndValues; + } + + template + std::list::Block>& DeterministicModelBisimulationDecomposition::Partition::getBlocks() { + return this->blocks; + } + + template + 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); + } + } + for (auto const& block : this->blocks) { + assert(block.check()); + for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt) { + if (this->stateToBlockMapping[stateIt->first] != &block) { + assert(false); + } + } + } + return true; + } + + template + void DeterministicModelBisimulationDecomposition::Partition::print() const { + for (auto const& block : this->blocks) { + block.print(*this); + } + std::cout << "states in partition" << std::endl; + for (auto const& stateValue : statesAndValues) { + std::cout << stateValue.first << " "; + } + std::cout << std::endl << "positions: " << std::endl; + for (auto const& index : positions) { + std::cout << index << " "; + } + std::cout << std::endl << "state to block mapping: " << std::endl; + for (auto const& block : stateToBlockMapping) { + std::cout << block << " "; + } + std::cout << std::endl; + std::cout << "size: " << this->blocks.size() << std::endl; + assert(this->check()); + } + + template + std::size_t DeterministicModelBisimulationDecomposition::Partition::size() const { + return this->blocks.size(); + } + + template + 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 ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient); + } + + template + 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 ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient); + } + + template + 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, weak, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient); + } + + template + 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, weak, bounded); + partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient); + } + + template + 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 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, + // (c) the new reward structures. + + // Prepare a matrix builder for (a). + storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); + + // Prepare the new state labeling for (b). + storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); + std::set atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions(); + std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); + for (auto const& ap : atomicPropositions) { + newLabeling.addAtomicProposition(ap); + } + + // Now build (a) and (b) by traversing all blocks. + for (uint_fast64_t blockIndex = 0; blockIndex < this->blocks.size(); ++blockIndex) { + auto const& block = this->blocks[blockIndex]; + + // 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 (bisimulationType == BisimulationType::WeakDtmc) { + 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. + if (oldBlock.isAbsorbing()) { + builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne()); + + 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 ((bisimulationType == BisimulationType::WeakDtmc || bisimulationType == BisimulationType::WeakCtmc) && targetBlock == blockIndex) { + continue; + } + + auto probIterator = blockProbability.find(targetBlock); + if (probIterator != blockProbability.end()) { + probIterator->second += entry.getValue(); + } else { + blockProbability[targetBlock] = entry.getValue(); + } + } + + // Now add them to the actual matrix. + for (auto const& probabilityEntry : blockProbability) { + 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); + } + } + + // If the block has a special label, we only add that to the block. + if (oldBlock.hasLabel()) { + newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex); + } else { + // Otherwise add all atomic propositions to the equivalence class that the representative state + // satisfies. + for (auto const& ap : atomicPropositions) { + if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { + newLabeling.addAtomicPropositionToState(ap, blockIndex); + } + } + } + } + } + + // Now check which of the blocks of the partition contain at least one initial state. + for (auto initialState : model.getInitialStates()) { + Block const& initialBlock = partition.getBlock(initialState); + newLabeling.addAtomicPropositionToState("init", initialBlock.getId()); + } + + // FIXME: + // If reward structures are allowed, the quotient structures need to be built here. + + // Finally construct the quotient model. + this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling))); + } + + template + template + 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. + 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(); } ); + + // 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, bisimulationType, splitterQueue); + } + std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; + + // 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(); + this->blocks.resize(partition.size()); + for (auto const& block : partition.getBlocks()) { + // We need to sort the states to allow for rapid construction of the blocks. + std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; }); + + // Convert the state-value-pairs to states only. + auto lambda = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; + this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), lambda), boost::make_transform_iterator(partition.getEnd(block), lambda), true); + } + + // If we are required to build the quotient model, do so now. + if (buildQuotient) { + this->buildQuotient(model, partition, bisimulationType); + } + + std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; + std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; + + if (storm::settings::generalSettings().isShowStatisticsSet()) { + std::cout << std::endl; + std::cout << "Time breakdown:" << std::endl; + std::cout << " * time for partitioning: " << std::chrono::duration_cast(refinementTime).count() << "ms" << std::endl; + std::cout << " * time for extraction: " << std::chrono::duration_cast(extractionTime).count() << "ms" << std::endl; + std::cout << "------------------------------------------" << std::endl; + std::cout << " * total time: " << std::chrono::duration_cast(totalTime).count() << "ms" << std::endl; + std::cout << std::endl; + } + } + + template + 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; } ); + + // 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, we need to scan the ranges of states that agree on the probability. + 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 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; + } + + // 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 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. + 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::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 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()]; }); + + // 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. + + // 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 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]) { + // 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) - blockOffset]; + + ++begin; + ++currentIndex; + 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); + + // 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) { + newSilentProbability += successorEntry.getValue(); + } + } + partition.setSilentProbability(stateIt->first, newSilentProbability); + } + } + + 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(); + } + + // 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) { + 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) { + newSilentProbability += successorEntry.getValue(); + } + } + partition.setSilentProbability(stateIt->first, newSilentProbability); + } + } + } + + // 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) { + partition.setPosition(stateIt->first, position); + } + } + + template + 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) { + ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first); + if (!comparator.isOne(silentProbability) && !comparator.isZero(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.getBegin()); + return result; + } + + template + 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. + 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; + + uint_fast64_t elementsToSkip = 0; + 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 or is marked as being absorbing, we must not split it. + if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) { + continue; + } + + storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); + + // If we have not seen this predecessor before, we move it to a part near the beginning of the block. + if (predecessorPosition >= predecessorBlock.getBegin()) { + if (&predecessorBlock == &splitter) { + // If the predecessor we just found was already processed (in terms of visiting its predecessors), + // we swap it with the state that is currently at the beginning of the block and move the start + // of the block one step further. + if (predecessorPosition <= currentPosition + elementsToSkip) { + partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); + predecessorBlock.incrementBegin(); + } else { + // Otherwise, we need to move the predecessor, but we need to make sure that we explore its + // predecessors later. + if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) { + partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); + partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); + } else { + partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); + partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); + partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); + } + + ++elementsToSkip; + predecessorBlock.incrementMarkedPosition(); + predecessorBlock.incrementBegin(); + } + } else { + partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); + predecessorBlock.incrementBegin(); + } + partition.setValue(predecessor, predecessorEntry.getValue()); + } else { + // Otherwise, we just need to update the probability for this predecessor. + partition.increaseValue(predecessor, predecessorEntry.getValue()); + } + + if (!predecessorBlock.isMarkedAsPredecessor()) { + predecessorBlocks.emplace_back(&predecessorBlock); + predecessorBlock.markAsPredecessorBlock(); + } + } + + // If we had to move some elements beyond the current element, we may have to skip them. + if (elementsToSkip > 0) { + stateIterator += elementsToSkip; + currentPosition += elementsToSkip; + } + } + + // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored. + for (auto stateIterator = partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { + storm::storage::sparse::state_type currentState = stateIterator->first; + + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); + Block& predecessorBlock = partition.getBlock(predecessor); + storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); + + if (predecessorPosition >= predecessorBlock.getBegin()) { + partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); + predecessorBlock.incrementBegin(); + partition.setValue(predecessor, predecessorEntry.getValue()); + } else { + partition.increaseValue(predecessor, predecessorEntry.getValue()); + } + + if (!predecessorBlock.isMarkedAsPredecessor()) { + predecessorBlocks.emplace_back(&predecessorBlock); + predecessorBlock.markAsPredecessorBlock(); + } + } + } + + 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 + // 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); + } + } + + // 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; + } + + // 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 { // 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) { + 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, forwardTransitions, backwardTransitions, splitterQueue); + } else { + // Restore the begin of the block. + block.setBegin(block.getOriginalBegin()); + } + + block.unmarkAsPredecessorBlock(); + block.resetMarkedPosition(); + } + } + + STORM_LOG_ASSERT(partition.check(), "Partition became inconsistent."); + } + + template + template + typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, 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, bisimulationType); + + // 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 + 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; + } + + // 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); + + 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()); + } + } + } + } + } + + + 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); + } + } + } + + 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; + } + + template + template + 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(); + + for (auto const& successorEntry : model.getRows(stateIt->first)) { + if (&partition.getBlock(successorEntry.getColumn()) == &block) { + silentProbability += successorEntry.getValue(); + } + } + + partition.setSilentProbability(stateIt->first, silentProbability); + } + } + } + + template class DeterministicModelBisimulationDecomposition; + +#ifdef PARAMETRIC_SYSTEMS + template class DeterministicModelBisimulationDecomposition; +#endif + } +} \ No newline at end of file diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h similarity index 74% rename from src/storage/DeterministicModelStrongBisimulationDecomposition.h rename to src/storage/DeterministicModelBisimulationDecomposition.h index c2fdec62e..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 strong bisimulation. + * 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 buildQuotient = false); + DeterministicModelBisimulationDecomposition(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 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 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 { @@ -91,9 +97,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; @@ -236,8 +239,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 +253,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; @@ -338,10 +343,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; @@ -355,6 +379,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; }; /*! @@ -365,34 +396,48 @@ 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 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 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 * 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. * @param partition The partition to split. + * @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& backwardTransitions, Block& splitter, Partition& partition, 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); + + /*! + * 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 @@ -402,9 +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 bisimulationType The kind of bisimulation that is to be computed. */ template - void buildQuotient(ModelType const& model, Partition const& partition); + void buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType); /*! * Creates the measure-driven initial partition for reaching psi states from phi states. @@ -414,21 +460,45 @@ 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. * * @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); + 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. + * + * @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; @@ -439,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/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp deleted file mode 100644 index 685f761d5..000000000 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ /dev/null @@ -1,955 +0,0 @@ -#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" - -#include -#include -#include -#include -#include - -#include "src/utility/graph.h" -#include "src/exceptions/IllegalFunctionCallException.h" - -namespace storm { - namespace storage { - - namespace { - static std::chrono::high_resolution_clock::duration probabilityRefineTime; - static std::chrono::high_resolution_clock::duration qualitativeRefineTime; - } - - template - std::size_t DeterministicModelStrongBisimulationDecomposition::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) { - if (next != nullptr) { - next->prev = this; - } - if (prev != nullptr) { - prev->next = this; - } - STORM_LOG_ASSERT(begin < end, "Unable to create block of illegal size."); - } - - template - void DeterministicModelStrongBisimulationDecomposition::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; - for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << partition.statesAndValues[index].first << " "; - } - std::cout << std::endl << "original: " << std::endl; - for (storm::storage::sparse::state_type index = this->getOriginalBegin(); index < this->end; ++index) { - std::cout << partition.statesAndValues[index].first << " "; - } - std::cout << std::endl << "values:" << std::endl; - for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << std::setprecision(3) << partition.statesAndValues[index].second << " "; - } - std::cout << std::endl; - } - - template - void DeterministicModelStrongBisimulationDecomposition::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) { - this->end = end; - STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::incrementBegin() { - ++this->begin; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::decrementEnd() { - ++this->begin; - } - - template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getBegin() const { - return this->begin; - } - - template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getOriginalBegin() const { - if (this->hasPreviousBlock()) { - return this->getPreviousBlock().getEnd(); - } else { - return 0; - } - } - - template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getEnd() const { - return this->end; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::setIterator(iterator it) { - this->selfIt = it; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getIterator() const { - return this->selfIt; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getNextIterator() const { - return this->getNextBlock().getIterator(); - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block::iterator DeterministicModelStrongBisimulationDecomposition::Block::getPreviousIterator() const { - return this->getPreviousBlock().getIterator(); - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() { - return *this->next; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getNextBlock() const { - return *this->next; - } - - template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasNextBlock() const { - return this->next != nullptr; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() { - return *this->prev; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlockPointer() { - return this->prev; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block* DeterministicModelStrongBisimulationDecomposition::Block::getNextBlockPointer() { - return this->next; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block const& DeterministicModelStrongBisimulationDecomposition::Block::getPreviousBlock() const { - return *this->prev; - } - - template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasPreviousBlock() const { - return this->prev != nullptr; - } - - 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); - } - return true; - } - - template - std::size_t DeterministicModelStrongBisimulationDecomposition::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 { - return this->markedAsSplitter; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::markAsSplitter() { - this->markedAsSplitter = true; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsSplitter() { - this->markedAsSplitter = false; - } - - template - std::size_t DeterministicModelStrongBisimulationDecomposition::Block::getId() const { - return this->id; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::setAbsorbing(bool absorbing) { - this->absorbing = absorbing; - } - - template - bool DeterministicModelStrongBisimulationDecomposition::Block::isAbsorbing() const { - return this->absorbing; - } - - template - storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition::Block::getMarkedPosition() const { - return this->markedPosition; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::setMarkedPosition(storm::storage::sparse::state_type position) { - this->markedPosition = position; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::resetMarkedPosition() { - this->markedPosition = this->begin; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::incrementMarkedPosition() { - ++this->markedPosition; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::markAsPredecessorBlock() { - this->markedAsPredecessorBlock = true; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Block::unmarkAsPredecessorBlock() { - this->markedAsPredecessorBlock = false; - } - - template - bool DeterministicModelStrongBisimulationDecomposition::Block::isMarkedAsPredecessor() const { - return markedAsPredecessorBlock; - } - - template - bool DeterministicModelStrongBisimulationDecomposition::Block::hasLabel() const { - return this->label != nullptr; - } - - template - std::string const& DeterministicModelStrongBisimulationDecomposition::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 { - return this->label; - } - - template - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) { - // 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); - - // Set up the different parts of the internal structure. - for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) { - statesAndValues[state] = std::make_pair(state, storm::utility::zero()); - positions[state] = state; - stateToBlockMapping[state] = &blocks.back(); - } - } - - 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) { - typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr); - Block& firstBlock = *firstIt; - firstBlock.setIterator(firstIt); - - storm::storage::sparse::state_type position = 0; - for (auto state : prob0States) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = &firstBlock; - ++position; - } - firstBlock.setAbsorbing(true); - - typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr(new std::string(prob1Label))); - Block& secondBlock = *secondIt; - secondBlock.setIterator(secondIt); - - for (auto state : prob1States) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = &secondBlock; - ++position; - } - secondBlock.setAbsorbing(true); - - typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); - Block& thirdBlock = *thirdIt; - thirdBlock.setIterator(thirdIt); - - storm::storage::BitVector otherStates = ~(prob0States | prob1States); - for (auto state : otherStates) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = &thirdBlock; - ++position; - } - } - - template - void DeterministicModelStrongBisimulationDecomposition::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) { - storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first; - storm::storage::sparse::state_type state2 = this->statesAndValues[position2].first; - - std::swap(this->statesAndValues[position1], this->statesAndValues[position2]); - - this->positions[state1] = position2; - this->positions[state2] = position1; - } - - template - storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::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) { - this->positions[state] = position; - } - - template - storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::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 { - return this->statesAndValues[this->positions[state]].second; - } - - template - ValueType const& DeterministicModelStrongBisimulationDecomposition::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) { - this->statesAndValues[this->positions[state]].second = value; - } - - template - void DeterministicModelStrongBisimulationDecomposition::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) { - for (; first != last; ++first) { - this->stateToBlockMapping[first->first] = █ - } - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::getFirstBlock() { - return *this->blocks.begin(); - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::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 { - return *this->stateToBlockMapping[state]; - } - - template - typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) { - return this->statesAndValues.begin() + block.getBegin(); - } - - template - typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) { - return this->statesAndValues.begin() + block.getEnd(); - } - - template - typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::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 { - return this->statesAndValues.begin() + block.getEnd(); - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::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()) { - return block; - } - - // Actually create the new block and insert it at the correct position. - typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); - selfIt->setIterator(selfIt); - Block& newBlock = *selfIt; - - // Resize the current block appropriately. - block.setBegin(position); - - // Update the mapping of the states in the newly created block. - this->updateBlockMapping(newBlock, this->getBegin(newBlock), this->getEnd(newBlock)); - - return newBlock; - } - - template - typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::insertBlock(Block& block) { - // Find the beginning of the new block. - storm::storage::sparse::state_type begin; - if (block.hasPreviousBlock()) { - begin = block.getPreviousBlock().getEnd(); - } else { - begin = 0; - } - - // Actually insert the new block. - typename std::list::iterator it = this->blocks.emplace(block.getIterator(), begin, block.getBegin(), block.getPreviousBlockPointer(), &block); - Block& newBlock = *it; - newBlock.setIterator(it); - - // Update the mapping of the states in the newly created block. - for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) { - stateToBlockMapping[it->first] = &newBlock; - } - - return *it; - } - - template - void DeterministicModelStrongBisimulationDecomposition::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; - - // Sort the range of the block such that all states that have the label are moved to the front. - std::sort(this->getBegin(block), this->getEnd(block), [&statesWithLabel] (std::pair const& a, std::pair const& b) { return statesWithLabel.get(a.first) && !statesWithLabel.get(b.first); } ); - - // Update the positions vector. - storm::storage::sparse::state_type position = block.getBegin(); - for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt, ++position) { - this->positions[stateIt->first] = position; - } - - // Now we can find the first position in the block that does not have the label and create new blocks. - typename std::vector>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair const& a) { return !statesWithLabel.get(a.first); }); - - // If not all the states agreed on the validity of the label, we need to split the block. - if (it != this->getBegin(block) && it != this->getEnd(block)) { - auto cutPoint = std::distance(this->statesAndValues.begin(), it); - this->splitBlock(block, cutPoint); - } else { - // Otherwise, we simply proceed to the next block. - ++blockIterator; - } - } - } - - template - std::list::Block> const& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() const { - return this->blocks; - } - - template - std::vector>& DeterministicModelStrongBisimulationDecomposition::Partition::getStatesAndValues() { - return this->statesAndValues; - } - - template - std::list::Block>& DeterministicModelStrongBisimulationDecomposition::Partition::getBlocks() { - return this->blocks; - } - - template - bool DeterministicModelStrongBisimulationDecomposition::Partition::check() const { - for (uint_fast64_t state = 0; state < this->positions.size(); ++state) { - if (this->statesAndValues[this->positions[state]].first != state) { - assert(false); - } - } - for (auto const& block : this->blocks) { - assert(block.check()); - for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt) { - if (this->stateToBlockMapping[stateIt->first] != &block) { - assert(false); - } - } - } - return true; - } - - template - void DeterministicModelStrongBisimulationDecomposition::Partition::print() const { - for (auto const& block : this->blocks) { - block.print(*this); - } - std::cout << "states in partition" << std::endl; - for (auto const& stateValue : statesAndValues) { - std::cout << stateValue.first << " "; - } - std::cout << std::endl << "positions: " << std::endl; - for (auto const& index : positions) { - std::cout << index << " "; - } - std::cout << std::endl << "state to block mapping: " << std::endl; - for (auto const& block : stateToBlockMapping) { - std::cout << block << " "; - } - std::cout << std::endl; - std::cout << "size: " << this->blocks.size() << std::endl; - assert(this->check()); - } - - template - std::size_t DeterministicModelStrongBisimulationDecomposition::Partition::size() const { - return this->blocks.size(); - } - - template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, bool buildQuotient) { - STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - Partition initialPartition = getLabelBasedInitialPartition(model); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); - } - - template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, bool buildQuotient) { - STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - Partition initialPartition = getLabelBasedInitialPartition(model); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); - } - - template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) { - STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); - } - - template - DeterministicModelStrongBisimulationDecomposition::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) { - STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures."); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded); - partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient); - } - - template - std::shared_ptr> DeterministicModelStrongBisimulationDecomposition::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) { - // In order to create the quotient model, we need to construct - // (a) the new transition matrix, - // (b) the new labeling, - // (c) the new reward structures. - - // Prepare a matrix builder for (a). - storm::storage::SparseMatrixBuilder builder(this->size(), this->size()); - - // Prepare the new state labeling for (b). - storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions()); - std::set atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions(); - std::vector atomicPropositions = std::vector(atomicPropositionsSet.begin(), atomicPropositionsSet.end()); - for (auto const& ap : atomicPropositions) { - newLabeling.addAtomicProposition(ap); - } - - // Now build (a) and (b) by traversing all blocks. - 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. - storm::storage::sparse::state_type representativeState = *block.begin(); - Block const& oldBlock = partition.getBlock(representativeState); - - // If the block is absorbing, we simply add a self-loop. - if (oldBlock.isAbsorbing()) { - builder.addNextValue(blockIndex, blockIndex, storm::utility::constantOne()); - - if (oldBlock.hasLabel()) { - newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), 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(); - auto probIterator = blockProbability.find(targetBlock); - if (probIterator != blockProbability.end()) { - probIterator->second += entry.getValue(); - } else { - blockProbability[targetBlock] = entry.getValue(); - } - } - -#ifdef DEBUG - // FIXME: take this out. - // As a debug check, we walk through all states and check if their behaviour is the same modulo the - // partition. - for (auto const& state : block) { - std::map stateProbability; - for (auto const& entry : model.getTransitionMatrix().getRow(state)) { - storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId(); - auto probIterator = stateProbability.find(targetBlock); - if (probIterator != stateProbability.end()) { - probIterator->second += entry.getValue(); - } else { - stateProbability[targetBlock] = entry.getValue(); - } - } - if (stateProbability != blockProbability) { - std::cout << "state: " << std::endl; - for (auto const& entry : stateProbability) { - std::cout << entry.first << " -> " << entry.second << std::endl; - } - std::cout << "block: " << std::endl; - for (auto const& entry : blockProbability) { - std::cout << entry.first << " -> " << entry.second << std::endl; - } - } - STORM_LOG_ASSERT(stateProbability == blockProbability, "Quotient distributions did not match."); - } -#endif - - // Now add them to the actual matrix. - for (auto const& probabilityEntry : blockProbability) { - builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second); - } - - // If the block has a special label, we only add that to the block. - if (oldBlock.hasLabel()) { - newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex); - } else { - // Otherwise add all atomic propositions to the equivalence class that the representative state - // satisfies. - for (auto const& ap : atomicPropositions) { - if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) { - newLabeling.addAtomicPropositionToState(ap, blockIndex); - } - } - } - } - } - - // Now check which of the blocks of the partition contain at least one initial state. - for (auto initialState : model.getInitialStates()) { - Block const& initialBlock = partition.getBlock(initialState); - newLabeling.addAtomicPropositionToState("init", initialBlock.getId()); - } - - // FIXME: - // If reward structures are allowed, the quotient structures need to be built here. - - // Finally construct the quotient model. - this->quotient = std::shared_ptr>(new ModelType(builder.build(), std::move(newLabeling))); - } - - template - template - void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, 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. - 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); }); - - // 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); - splitterQueue.pop_front(); - } - std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; - - // 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(); - this->blocks.resize(partition.size()); - for (auto const& block : partition.getBlocks()) { - // We need to sort the states to allow for rapid construction of the blocks. - std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; }); - - // Convert the state-value-pairs to states only. - auto lambda = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; - this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), lambda), boost::make_transform_iterator(partition.getEnd(block), lambda), true); - } - - // If we are required to build the quotient model, do so now. - if (buildQuotient) { - this->buildQuotient(model, partition); - } - - std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; - std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; - - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::cout << std::endl; - std::cout << "Time breakdown:" << std::endl; - std::cout << " * time for partitioning: " << std::chrono::duration_cast(refinementTime).count() << "ms" << std::endl; - std::cout << " * time for qualitative refinement: " << std::chrono::duration_cast(qualitativeRefineTime).count() << "ms" << std::endl; - std::cout << " * time for probability refinement: " << std::chrono::duration_cast(probabilityRefineTime).count() << "ms" << std::endl; - std::cout << " * time for extraction: " << std::chrono::duration_cast(extractionTime).count() << "ms" << std::endl; - std::cout << "------------------------------------------" << std::endl; - std::cout << " * total time: " << std::chrono::duration_cast(totalTime).count() << "ms" << std::endl; - std::cout << std::endl; - } - } - - template - void DeterministicModelStrongBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { - std::chrono::high_resolution_clock::time_point probabilityRefineStart = std::chrono::high_resolution_clock::now(); - - // First, we simplify all the values. For most types this does not change anything, but for rational - // functions, this achieves a canonicity that is used for sorting the rational functions later. - for (auto probabilityIt = partition.getBegin(block), probabilityIte = partition.getEnd(block); probabilityIt != probabilityIte; ++probabilityIt) { - storm::utility::simplify(probabilityIt->second); - } - - // Sort the states in the block based on their probabilities. - std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); - - // 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, we need to scan the ranges of states that agree on the probability. - 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(); - - // Perform a sanity check that the smallest probability is still not zero. - STORM_LOG_ASSERT(!comparator.isZero(begin->second), "Probability to go to splitter must not be zero."); - - // 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; - } - - // 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(); - } - - for (auto it = partition.getBegin(newBlock), ite = partition.getEnd(newBlock) - 1; it != ite; ++it) { - STORM_LOG_ASSERT(comparator.isEqual(partition.getValueAtPosition(it->first), partition.getValueAtPosition((it + 1)->first)), "Expected equal probabilities after sorting block, but got '" << partition.getValueAtPosition(it->first) << "' and '" << partition.getValueAtPosition((it + 1)->first) << "'."); - } - - } - - probabilityRefineTime += std::chrono::high_resolution_clock::now() - probabilityRefineStart; - } - - template - void DeterministicModelStrongBisimulationDecomposition::refinePartition(storm::storage::SparseMatrix const& backwardTransitions, Block& splitter, Partition& partition, std::deque& splitterQueue) { - std::list predecessorBlocks; - - // Iterate over all states of the splitter and check its predecessors. - std::chrono::high_resolution_clock::time_point qualitativeRefineStart = std::chrono::high_resolution_clock::now(); - 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; - - uint_fast64_t elementsToSkip = 0; - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - - Block& predecessorBlock = partition.getBlock(predecessor); - - // If the predecessor block has just one state, there is no point in splitting it. - if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) { - continue; - } - - storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); - - // If we have not seen this predecessor before, we move it to a part near the beginning of the block. - if (predecessorPosition >= predecessorBlock.getBegin()) { - if (&predecessorBlock == &splitter) { - // If the predecessor we just found was already processed (in terms of visiting its predecessors), - // we swap it with the state that is currently at the beginning of the block and move the start - // of the block one step further. - if (predecessorPosition <= currentPosition + elementsToSkip) { - partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); - predecessorBlock.incrementBegin(); - } else { - // Otherwise, we need to move the predecessor, but we need to make sure that we explore its - // predecessors later. - if (predecessorBlock.getMarkedPosition() == predecessorBlock.getBegin()) { - partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); - partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); - } else { - partition.swapStatesAtPositions(predecessorBlock.getMarkedPosition(), predecessorPosition); - partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); - partition.swapStatesAtPositions(predecessorPosition, currentPosition + elementsToSkip + 1); - } - - ++elementsToSkip; - predecessorBlock.incrementMarkedPosition(); - predecessorBlock.incrementBegin(); - } - } else { - partition.swapStates(predecessor, partition.getState(predecessorBlock.getBegin())); - predecessorBlock.incrementBegin(); - } - partition.setValue(predecessor, predecessorEntry.getValue()); - } else { - // Otherwise, we just need to update the probability for this predecessor. - partition.increaseValue(predecessor, predecessorEntry.getValue()); - } - - if (!predecessorBlock.isMarkedAsPredecessor()) { - predecessorBlocks.emplace_back(&predecessorBlock); - predecessorBlock.markAsPredecessorBlock(); - } - } - - // If we had to move some elements beyond the current element, we may have to skip them. - if (elementsToSkip > 0) { - stateIterator += elementsToSkip; - currentPosition += elementsToSkip; - } - } - - // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored. - for (auto stateIterator = partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { - storm::storage::sparse::state_type currentState = stateIterator->first; - - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - Block& predecessorBlock = partition.getBlock(predecessor); - storm::storage::sparse::state_type predecessorPosition = partition.getPosition(predecessor); - - if (predecessorPosition >= predecessorBlock.getBegin()) { - partition.swapStatesAtPositions(predecessorPosition, predecessorBlock.getBegin()); - predecessorBlock.incrementBegin(); - partition.setValue(predecessor, predecessorEntry.getValue()); - } else { - partition.increaseValue(predecessor, predecessorEntry.getValue()); - } - - if (!predecessorBlock.isMarkedAsPredecessor()) { - predecessorBlocks.emplace_back(&predecessorBlock); - predecessorBlock.markAsPredecessorBlock(); - } - } - } - - // 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; - - 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); - } - } - - qualitativeRefineTime += std::chrono::high_resolution_clock::now() - qualitativeRefineStart; - - // 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; - } - - refineBlockProbabilities(*blockPtr, partition, splitterQueue); - } - } - - 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) { - 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); - return partition; - } - - template - template - typename DeterministicModelStrongBisimulationDecomposition::Partition DeterministicModelStrongBisimulationDecomposition::getLabelBasedInitialPartition(ModelType const& model) { - Partition partition(model.getNumberOfStates()); - for (auto const& label : model.getStateLabeling().getAtomicPropositions()) { - if (label == "init") { - continue; - } - partition.splitLabel(model.getLabeledStates(label)); - } - return partition; - } - - template class DeterministicModelStrongBisimulationDecomposition; - template class DeterministicModelStrongBisimulationDecomposition; - } -} \ No newline at end of file diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 380a36e65..2907be328 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -11,7 +11,7 @@ #include "src/modelchecker/reachability/CollectConstraints.h" //#include "src/modelchecker/reachability/DirectEncoding.h" -#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" +#include "src/storage/DeterministicModelBisimulationDecomposition.h" #include "src/modelchecker/reachability/SparseSccModelChecker.h" #include "src/storage/parameters.h" #include "src/models/Dtmc.h" @@ -181,7 +181,7 @@ int main(const int argc, const char** argv) { STORM_LOG_THROW(phiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); STORM_LOG_THROW(psiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position."); - storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), false, true); + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, phiStateFormulaApFormula->getAp(), psiStateFormulaApFormula->getAp(), storm::settings::bisimulationSettings().isWeakBisimulationSet(), false, true); dtmc = bisimulationDecomposition.getQuotient()->as>(); dtmc->printModelInformationToStream(std::cout); diff --git a/src/utility/cli.h b/src/utility/cli.h index 227e09dfb..b3fa597c3 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -48,7 +48,11 @@ log4cplus::Logger printer; // 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" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" // Headers for counterexample generation. #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" @@ -271,7 +275,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::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true); result = bisimulationDecomposition.getQuotient(); @@ -323,10 +327,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); + } } - } - } } } 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", "", "");