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<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+ [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+ [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+ // success
+ [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+ [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+ // error
+ [SyncWait] (s=5) -> (s'=6);
+ // wait sync
+ [SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+ r : [0..5];
+ // 0 new_file
+ // 1 fst_safe
+ // 2 frame_received
+ // 3 frame_reported
+ // 4 idle
+ // 5 resync
+ rrep : [0..4];
+ // 0 bottom
+ // 1 fst
+ // 2 inc
+ // 3 ok
+ // 4 nok
+ fr : bool;
+ lr : bool;
+ br : bool;
+ r_ab : bool;
+ recv : bool;
+
+
+ // new_file
+ [SyncWait] (r=0) -> (r'=0);
+ [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ // fst_safe_frame
+ [] (r=1) -> (r'=2) & (r_ab'=br);
+ // frame_received
+ [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
+ [aA] (r=2) & !(r_ab=br) -> (r'=4);
+ // frame_reported
+ [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+ // idle
+ [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ [SyncWait] (r=4) & (ls=true) -> (r'=5);
+ [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+ // resync
+ [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+module checker // prevents more than one frame being set
+
+ T : bool;
+
+ [NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+module channelK
+
+ k : [0..2];
+
+ // idle
+ [aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2);
+ // sending
+ [aG] (k=1) -> (k'=0);
+ // lost
+ [TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+ l : [0..2];
+
+ // idle
+ [aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2);
+ // sending
+ [aB] (l=1) -> (l'=0);
+ // lost
+ [TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+rewards
+ [aF] i=1 : 1;
+endrewards
+
+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<N) -> (s'=1); // do next nand if have not done N yet
+ [] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+ [] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+ // choose x permute selection (have zx stimulated inputs)
+ // note only need y to be random
+ [] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+ [] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+ [] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+ // choose x randomly from selection (have zy stimulated inputs)
+ [] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+ [] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+ [] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+ [] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+ // use nand gate
+ [] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
+ // [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ // + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
+
+ [] s=4 -> (s'=s);
+
+endmodule
+
+// rewards: final value of gate
+rewards
+ [] s=0 & (c=N) & (u=M) : z/N;
+endrewards
+
+label "target" = s=4 & z/N<0.1;
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 5c311c602..4c841acaa 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -24,6 +24,7 @@ namespace storm {
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::CuddSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GmmxxEquationSolverSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::NativeEquationSolverSettings(*this)));
+ this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::BisimulationSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GlpkSettings(*this)));
this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
}
@@ -495,6 +496,10 @@ namespace storm {
return dynamic_cast<storm::settings::modules::NativeEquationSolverSettings const&>(manager().getModule(storm::settings::modules::NativeEquationSolverSettings::moduleName));
}
+ storm::settings::modules::BisimulationSettings const& bisimulationSettings() {
+ return dynamic_cast<storm::settings::modules::BisimulationSettings const&>(manager().getModule(storm::settings::modules::BisimulationSettings::moduleName));
+ }
+
storm::settings::modules::GlpkSettings const& glpkSettings() {
return dynamic_cast<storm::settings::modules::GlpkSettings const&>(manager().getModule(storm::settings::modules::GlpkSettings::moduleName));
}
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 3daa43beb..9d597ca2e 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -25,6 +25,7 @@
#include "src/settings/modules/CuddSettings.h"
#include "src/settings/modules/GmmxxEquationSolverSettings.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
+#include "src/settings/modules/BisimulationSettings.h"
#include "src/settings/modules/GlpkSettings.h"
#include "src/settings/modules/GurobiSettings.h"
@@ -286,6 +287,13 @@ namespace storm {
* @return An object that allows accessing the settings of the native equation solver.
*/
storm::settings::modules::NativeEquationSolverSettings const& nativeEquationSolverSettings();
+
+ /*!
+ * Retrieves the settings of the native equation solver.
+ *
+ * @return An object that allows accessing the settings of the native equation solver.
+ */
+ storm::settings::modules::BisimulationSettings const& bisimulationSettings();
/*!
* Retrieves the settings of glpk.
diff --git a/src/settings/modules/BisimulationSettings.cpp b/src/settings/modules/BisimulationSettings.cpp
new file mode 100644
index 000000000..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<std::string> types = { "strong", "weak" };
+ this->addOption(storm::settings::OptionBuilder(moduleName, typeOptionName, true, "Sets the kind of bisimulation quotienting used. Available are: { strong, weak }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("strong").build()).build());
+ }
+
+ bool BisimulationSettings::isStrongBisimulationSet() const {
+ if (this->getOption(typeOptionName).getArgumentByName("name").getValueAsString() == "strong") {
+ return true;
+ }
+ return false;
+ }
+
+ bool BisimulationSettings::isWeakBisimulationSet() const {
+ if (this->getOption(typeOptionName).getArgumentByName("name").getValueAsString() == "weak") {
+ return true;
+ }
+ return false;
+ }
+
+ 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 <boost/container/flat_set.hpp>
+#include <iostream>
#include "src/storage/BitVector.h"
#include "src/exceptions/InvalidArgumentException.h"
@@ -96,6 +97,28 @@ namespace storm {
return *this;
}
+ bool BitVector::operator<(BitVector const& other) const {
+ if (this->size() < other.size()) {
+ return true;
+ } else if (this->size() > other.size()) {
+ return false;
+ }
+
+ std::vector<uint64_t>::const_iterator first1 = this->bucketVector.begin();
+ std::vector<uint64_t>::const_iterator last1 = this->bucketVector.end();
+ std::vector<uint64_t>::const_iterator first2 = other.bucketVector.begin();
+ std::vector<uint64_t>::const_iterator last2 = other.bucketVector.end();
+
+ for (; first1 != last1; ++first1, ++first2) {
+ if (*first1 < *first2) {
+ return true;
+ } else if (*first1 > *first2) {
+ return false;
+ }
+ }
+ return false;
+ }
+
BitVector& BitVector::operator=(BitVector&& other) {
// Only perform the assignment if the source and target are not identical.
if (this != &other) {
@@ -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<uint_fast64_t>(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..2f46baa55
--- /dev/null
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -0,0 +1,1302 @@
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+
+#include <algorithm>
+#include <unordered_map>
+#include <chrono>
+#include <iomanip>
+#include <boost/iterator/transform_iterator.hpp>
+
+#include "src/utility/graph.h"
+#include "src/exceptions/IllegalFunctionCallException.h"
+
+namespace storm {
+ namespace storage {
+
+ template<typename ValueType>
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::blockId = 0;
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) {
+ 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<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
+ std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl;
+ std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
+ std::cout << "states:" << std::endl;
+ 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<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
+ this->begin = begin;
+ this->markedPosition = begin;
+ STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
+ this->end = end;
+ STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementBegin() {
+ ++this->begin;
+ STORM_LOG_ASSERT(begin <= end, "Unable to resize block to illegal size.");
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getBegin() const {
+ return this->begin;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
+ if (this->hasPreviousBlock()) {
+ return this->getPreviousBlock().getEnd();
+ } else {
+ return 0;
+ }
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getEnd() const {
+ return this->end;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setIterator(iterator it) {
+ this->selfIt = it;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getIterator() const {
+ return this->selfIt;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
+ return this->getNextBlock().getIterator();
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
+ return this->getPreviousBlock().getIterator();
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() {
+ return *this->next;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
+ return *this->next;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
+ return this->next != nullptr;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
+ return *this->prev;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
+ return this->prev;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block* DeterministicModelBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
+ return this->next;
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
+ return *this->prev;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
+ return this->prev != nullptr;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::check() const {
+ assert(this->begin < this->end);
+ assert(this->prev == nullptr || this->prev->next == this);
+ assert(this->next == nullptr || this->next->prev == this);
+ return true;
+ }
+
+ template<typename ValueType>
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
+ // We need to take the original begin here, because the begin is temporarily moved.
+ return (this->end - this->getOriginalBegin());
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
+ return this->markedAsSplitter;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
+ this->markedAsSplitter = true;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
+ this->markedAsSplitter = false;
+ }
+
+ template<typename ValueType>
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Block::getId() const {
+ return this->id;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setAbsorbing(bool absorbing) {
+ this->absorbing = absorbing;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isAbsorbing() const {
+ return this->absorbing;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type DeterministicModelBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
+ return this->markedPosition;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
+ this->markedPosition = position;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
+ this->markedPosition = this->begin;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
+ ++this->markedPosition;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
+ this->markedAsPredecessorBlock = true;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
+ this->markedAsPredecessorBlock = false;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
+ return markedAsPredecessorBlock;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Block::hasLabel() const {
+ return this->label != nullptr;
+ }
+
+ template<typename ValueType>
+ std::string const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getLabel() const {
+ STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none.");
+ return *this->label;
+ }
+
+ template<typename ValueType>
+ std::shared_ptr<std::string> const& DeterministicModelBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
+ return this->label;
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
+ // Create the block and give it an iterator to itself.
+ typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
+ it->setIterator(it);
+
+ // 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<ValueType>());
+ positions[state] = state;
+ stateToBlockMapping[state] = &blocks.back();
+ }
+
+ // If we are requested to store silent probabilities, we need to prepare the vector.
+ if (this->keepSilentProbabilities) {
+ silentProbabilities = std::vector<ValueType>(numberOfStates);
+ }
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() {
+ typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
+ Block& firstBlock = *firstIt;
+ firstBlock.setIterator(firstIt);
+
+ storm::storage::sparse::state_type position = 0;
+ for (auto state : prob0States) {
+ statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
+ positions[state] = position;
+ stateToBlockMapping[state] = &firstBlock;
+ ++position;
+ }
+ firstBlock.setAbsorbing(true);
+
+ typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr<std::string>(new std::string(prob1Label)));
+ Block& secondBlock = *secondIt;
+ secondBlock.setIterator(secondIt);
+
+ for (auto state : prob1States) {
+ statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
+ positions[state] = position;
+ stateToBlockMapping[state] = &secondBlock;
+ ++position;
+ }
+ secondBlock.setAbsorbing(true);
+
+ typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
+ Block& thirdBlock = *thirdIt;
+ thirdBlock.setIterator(thirdIt);
+
+ storm::storage::BitVector otherStates = ~(prob0States | prob1States);
+ for (auto state : otherStates) {
+ statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
+ 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<ValueType>(numberOfStates);
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
+ std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]);
+ std::swap(this->positions[state1], this->positions[state2]);
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
+ storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first;
+ storm::storage::sparse::state_type state2 = this->statesAndValues[position2].first;
+
+ std::swap(this->statesAndValues[position1], this->statesAndValues[position2]);
+
+ this->positions[state1] = position2;
+ this->positions[state2] = position1;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
+ return this->positions[state];
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
+ this->positions[state] = position;
+ }
+
+ template<typename ValueType>
+ storm::storage::sparse::state_type const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
+ return this->statesAndValues[position].first;
+ }
+
+ template<typename ValueType>
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
+ return this->statesAndValues[this->positions[state]].second;
+ }
+
+ template<typename ValueType>
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
+ return this->statesAndValues[position].second;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
+ this->statesAndValues[this->positions[state]].second = value;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
+ this->statesAndValues[this->positions[state]].second += value;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ for (; first != last; ++first) {
+ this->stateToBlockMapping[first->first] = █
+ }
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getFirstBlock() {
+ return *this->blocks.begin();
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
+ return *this->stateToBlockMapping[state];
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
+ return *this->stateToBlockMapping[state];
+ }
+
+ template<typename ValueType>
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
+ return this->statesAndValues.begin() + block.getBegin();
+ }
+
+ template<typename ValueType>
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
+ return this->statesAndValues.begin() + block.getEnd();
+ }
+
+ template<typename ValueType>
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
+ return this->statesAndValues.begin() + block.getBegin();
+ }
+
+ template<typename ValueType>
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) const {
+ return this->statesAndValues.begin() + block.getEnd();
+ }
+
+ template<typename ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
+ // In case one of the resulting blocks would be empty, we simply return the current block and do not create
+ // a new one.
+ if (position == block.getBegin() || position == block.getEnd()) {
+ return block;
+ }
+
+ // Actually create the new block and insert it at the correct position.
+ typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
+ 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 ValueType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Block& DeterministicModelBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
+ // Find the beginning of the new block.
+ storm::storage::sparse::state_type begin;
+ if (block.hasPreviousBlock()) {
+ begin = block.getPreviousBlock().getEnd();
+ } else {
+ begin = 0;
+ }
+
+ // Actually insert the new block.
+ typename std::list<Block>::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<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
+ for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
+ Block& block = *blockIterator;
+
+ // 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<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> 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<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> 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<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked.");
+ return comparator.isOne(this->silentProbabilities[state]);
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silentness of state, because silent probabilities are not tracked.");
+ return !comparator.isZero(this->silentProbabilities[state]);
+ }
+
+ template<typename ValueType>
+ ValueType const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getSilentProbability(storm::storage::sparse::state_type state) const {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to retrieve silent probability of state, because silent probabilities are not tracked.");
+ return this->silentProbabilities[state];
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setSilentProbabilities(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
+ for (; first != last; ++first) {
+ this->silentProbabilities[first->first] = first->second;
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setSilentProbabilitiesToZero(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
+ for (; first != last; ++first) {
+ this->silentProbabilities[first->first] = storm::utility::zero<ValueType>();
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::Partition::setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value) {
+ STORM_LOG_ASSERT(this->keepSilentProbabilities, "Unable to set silent probability of state, because silent probabilities are not tracked.");
+ this->silentProbabilities[state] = value;
+ }
+
+ template<typename ValueType>
+ std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block> const& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
+ return this->blocks;
+ }
+
+ template<typename ValueType>
+ std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getStatesAndValues() {
+ return this->statesAndValues;
+ }
+
+ template<typename ValueType>
+ std::list<typename DeterministicModelBisimulationDecomposition<ValueType>::Block>& DeterministicModelBisimulationDecomposition<ValueType>::Partition::getBlocks() {
+ return this->blocks;
+ }
+
+ template<typename ValueType>
+ bool DeterministicModelBisimulationDecomposition<ValueType>::Partition::check() const {
+ for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
+ if (this->statesAndValues[this->positions[state]].first != state) {
+ assert(false);
+ }
+ }
+ 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<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::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<typename ValueType>
+ std::size_t DeterministicModelBisimulationDecomposition<ValueType>::Partition::size() const {
+ return this->blocks.size();
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak, bool buildQuotient) : comparator() {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
+ partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getLabelBasedInitialPartition(model, backwardTransitions, weak);
+ partitionRefinement(model, backwardTransitions, initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakDtmc : BisimulationType::Strong, buildQuotient);
+ }
+
+ template<typename ValueType>
+ DeterministicModelBisimulationDecomposition<ValueType>::DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient) {
+ STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
+ STORM_LOG_THROW(!weak || !bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation does not preserve bounded properties.");
+ storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+ Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, weak, bounded);
+ partitionRefinement(model, model.getBackwardTransitions(), initialPartition, weak ? BisimulationType::WeakCtmc : BisimulationType::Strong, buildQuotient);
+ }
+
+ template<typename ValueType>
+ std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelBisimulationDecomposition<ValueType>::getQuotient() const {
+ STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
+ return this->quotient;
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition, BisimulationType bisimulationType) {
+ // In order to create the quotient model, we need to construct
+ // (a) the new transition matrix,
+ // (b) the new labeling,
+ // (c) the new reward structures.
+
+ // Prepare a matrix builder for (a).
+ storm::storage::SparseMatrixBuilder<ValueType> builder(this->size(), this->size());
+
+ // Prepare the new state labeling for (b).
+ storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
+ std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
+ std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
+ for (auto const& ap : atomicPropositions) {
+ newLabeling.addAtomicProposition(ap);
+ }
+
+ // 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<ValueType>());
+
+ if (oldBlock.hasLabel()) {
+ newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
+ } else {
+ // Otherwise add all atomic propositions to the equivalence class that the representative state
+ // satisfies.
+ for (auto const& ap : atomicPropositions) {
+ if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
+ newLabeling.addAtomicPropositionToState(ap, blockIndex);
+ }
+ }
+ }
+ } else {
+ // Compute the outgoing transitions of the block.
+ std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
+ for (auto const& entry : model.getTransitionMatrix().getRow(representativeState)) {
+ storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId();
+
+ // If we are computing a weak bisimulation quotient, there is no need to add self-loops.
+ if ((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<ValueType>() - partition.getSilentProbability(representativeState)));
+ } else {
+ builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
+ }
+ }
+
+ // If the block has a special label, we only add that to the block.
+ 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<storm::models::AbstractDeterministicModel<ValueType>>(new ModelType(builder.build(), std::move(newLabeling)));
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, BisimulationType bisimulationType, bool buildQuotient) {
+ std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
+
+ // Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
+ std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
+ std::deque<Block*> splitterQueue;
+ std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); a.markAsSplitter(); });
+
+ // Then perform the actual splitting until there are no more splitters.
+ while (!splitterQueue.empty()) {
+ // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters).
+ std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
+
+ // 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<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.first < b.first; });
+
+ // Convert the state-value-pairs to states only.
+ auto lambda = [] (std::pair<storm::storage::sparse::state_type, ValueType> 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<std::chrono::milliseconds>(refinementTime).count() << "ms" << std::endl;
+ std::cout << " * time for extraction: " << std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime).count() << "ms" << std::endl;
+ std::cout << "------------------------------------------" << std::endl;
+ std::cout << " * total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms" << std::endl;
+ std::cout << std::endl;
+ }
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue) {
+ // Sort the states in the block based on their probabilities.
+ std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.second < b.second; } );
+
+ // 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<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
+ storm::storage::sparse::state_type currentIndex = block.getBegin();
+
+ // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
+ // first and the last state are different.
+ bool blockSplit = !comparator.isEqual(begin->second, end->second);
+ while (!comparator.isEqual(begin->second, end->second)) {
+ // Now we scan for the first state in the block that disagrees on the 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<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue) {
+ std::vector<uint_fast64_t> splitPoints = getSplitPointsWeak(block, partition);
+
+ // Restore the original begin of the block.
+ 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<storm::storage::BitVector> stateLabels(block.getEnd() - block.getBegin(), storm::storage::BitVector(splitPoints.size() - 1));
+
+ std::vector<storm::storage::sparse::state_type> stateStack;
+ stateStack.reserve(block.getEnd() - block.getBegin());
+ for (uint_fast64_t stateClassIndex = 0; stateClassIndex < splitPoints.size() - 1; ++stateClassIndex) {
+ for (auto stateIt = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex], stateIte = partition.getStatesAndValues().begin() + splitPoints[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) {
+
+ stateStack.push_back(stateIt->first);
+ stateLabels[partition.getPosition(stateIt->first) - block.getBegin()].set(stateClassIndex);
+ while (!stateStack.empty()) {
+ storm::storage::sparse::state_type currentState = stateStack.back();
+ stateStack.pop_back();
+
+ for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
+ if (comparator.isZero(predecessorEntry.getValue())) {
+ continue;
+ }
+
+ storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn();
+
+ // Only if the state is in the same block, is a silent state and it has not yet been
+ // labeled with the current label.
+ if (&partition.getBlock(predecessor) == &block && partition.isSilent(predecessor, comparator) && !stateLabels[partition.getPosition(predecessor) - block.getBegin()].get(stateClassIndex)) {
+ stateStack.push_back(predecessor);
+ stateLabels[partition.getPosition(predecessor) - block.getBegin()].set(stateClassIndex);
+ }
+ }
+ }
+ }
+ }
+
+ // Now that all states were appropriately labeled, we can sort the states according to their labels and then
+ // scan for ranges that agree on the label.
+ std::sort(partition.getBegin(block), partition.getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return stateLabels[partition.getPosition(a.first) - block.getBegin()] < stateLabels[partition.getPosition(b.first) - block.getBegin()]; });
+
+ // 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<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
+ storm::storage::sparse::state_type currentIndex = block.getBegin();
+
+ // Now we can check whether the block needs to be split, which is the case iff the 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<ValueType>();
+ 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<ValueType>();
+ 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<typename ValueType>
+ std::vector<uint_fast64_t> DeterministicModelBisimulationDecomposition<ValueType>::getSplitPointsWeak(Block& block, Partition& partition) {
+ std::vector<uint_fast64_t> result;
+ // We first scale all probabilities with (1-p[s]) where p[s] is the silent probability of state s.
+ std::for_each(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&] (std::pair<storm::storage::sparse::state_type, ValueType>& stateValuePair) {
+ ValueType const& silentProbability = partition.getSilentProbability(stateValuePair.first);
+ if (!comparator.isOne(silentProbability) && !comparator.isZero(silentProbability)) {
+ stateValuePair.second /= storm::utility::one<ValueType>() - silentProbability;
+ }
+ });
+
+ // Now sort the states based on their probabilities.
+ std::sort(partition.getStatesAndValues().begin() + block.getOriginalBegin(), partition.getStatesAndValues().begin() + block.getBegin(), [&partition] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.second < b.second; } );
+
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.getOriginalBegin();
+ for (auto stateIt = partition.getStatesAndValues().begin() + block.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + block.getBegin(); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(stateIt->first, position);
+ }
+
+ // Then, we scan for the ranges of states that agree on the probability.
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getStatesAndValues().begin() + block.getOriginalBegin();
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
+ typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getStatesAndValues().begin() + block.getBegin() - 1;
+ storm::storage::sparse::state_type currentIndex = block.getOriginalBegin();
+ result.push_back(currentIndex);
+
+ // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
+ // first and the last state are different.
+ while (!comparator.isEqual(begin->second, end->second)) {
+ // Now we scan for the first state in the block that disagrees on the probability value.
+ // Note that we do not have to check currentIndex for staying within bounds, because we know the matching
+ // state is within bounds.
+ ValueType const& currentValue = begin->second;
+
+ ++begin;
+ ++currentIndex;
+ while (begin != end && comparator.isEqual(begin->second, currentValue)) {
+ ++begin;
+ ++currentIndex;
+ }
+
+ // Remember the index at which the probabilities were different.
+ result.push_back(currentIndex);
+ }
+
+ // Push a sentinel element and return result.
+ result.push_back(block.getBegin());
+ return result;
+ }
+
+ template<typename ValueType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue) {
+ std::list<Block*> predecessorBlocks;
+
+ // Iterate over all states of the splitter and check its predecessors.
+ 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<Block*> blocksToSplit;
+
+ // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
+ // predecessors of the splitter.
+ for (auto blockPtr : predecessorBlocks) {
+ Block& block = *blockPtr;
+
+ 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<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded) {
+ std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel));
+ Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel);
+
+ // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
+ // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
+ if (weak) {
+ this->splitOffDivergentStates(model, backwardTransitions, partition);
+ this->initializeSilentProbabilities(model, partition);
+ }
+
+ return partition;
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition) {
+ std::vector<storm::storage::sparse::state_type> stateStack;
+ stateStack.reserve(model.getNumberOfStates());
+ storm::storage::BitVector nondivergentStates(model.getNumberOfStates());
+ for (auto& block : partition.getBlocks()) {
+ nondivergentStates.clear();
+
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
+ if (nondivergentStates.get(stateIt->first)) {
+ continue;
+ }
+
+ // 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<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return nondivergentStates.get(a.first) && !nondivergentStates.get(b.first); } );
+ // Update the positions vector.
+ storm::storage::sparse::state_type position = block.getBegin();
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) {
+ partition.setPosition(stateIt->first, position);
+ }
+
+ // Finally, split the block.
+ Block& nondivergentBlock = partition.splitBlock(block, block.getBegin() + nondivergentStates.getNumberOfSetBits());
+
+ // Since the remaining states in the block are divergent, we can mark the block as absorbing.
+ // This also guarantees that the self-loop will be added to the state of the quotient
+ // representing this block of states.
+ block.setAbsorbing(true);
+ } else if (nondivergentStates.getNumberOfSetBits() == 0) {
+ // If there are only diverging states in the block, we need to make it absorbing.
+ block.setAbsorbing(true);
+ }
+ }
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ typename DeterministicModelBisimulationDecomposition<ValueType>::Partition DeterministicModelBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak) {
+ Partition partition(model.getNumberOfStates(), weak);
+ for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
+ if (label == "init") {
+ continue;
+ }
+ partition.splitLabel(model.getLabeledStates(label));
+ }
+
+ // If we are creating the initial partition for weak bisimulation, we need to (a) split off all divergent
+ // states of each initial block and (b) initialize the vector of silent probabilities held by the partition.
+ if (weak) {
+ this->splitOffDivergentStates(model, backwardTransitions, partition);
+ this->initializeSilentProbabilities(model, partition);
+ }
+ return partition;
+ }
+
+ template<typename ValueType>
+ template<typename ModelType>
+ void DeterministicModelBisimulationDecomposition<ValueType>::initializeSilentProbabilities(ModelType const& model, Partition& partition) {
+ for (auto const& block : partition.getBlocks()) {
+ for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt) {
+ ValueType silentProbability = storm::utility::zero<ValueType>();
+
+ 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<double>;
+ }
+}
\ 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 <queue>
#include <deque>
@@ -19,23 +19,25 @@ namespace storm {
* This class represents the decomposition model into its (strong) bisimulation quotient.
*/
template <typename ValueType>
- class DeterministicModelStrongBisimulationDecomposition : public Decomposition<StateBlock> {
+ class DeterministicModelBisimulationDecomposition : public Decomposition<StateBlock> {
public:
/*!
- * Decomposes the given DTMC into equivalence classes under 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<ValueType> const& model, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
- * Decomposes the given CTMC into equivalence classes under strong bisimulation.
+ * Decomposes the given CTMC into equivalence classes under weak or strong bisimulation.
*
* @param model The model to decompose.
+ * @param weak A flag indication whether a weak bisimulation is to be computed.
* @param buildQuotient Sets whether or not the quotient model is to be built.
*/
- DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool weak = false, bool buildQuotient = false);
/*!
* Decomposes the given DTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -44,10 +46,11 @@ namespace storm {
* @param model The model to decompose.
* @param phiLabel The label that all phi states carry in the model.
* @param psiLabel The label that all psi states carry in the model.
+ * @param weak A flag indication whether a weak bisimulation is to be computed.
* @param bounded If set to true, also bounded until formulas are preserved.
* @param buildQuotient Sets whether or not the quotient model is to be built.
*/
- DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false);
/*!
* Decomposes the given CTMC into equivalence classes under strong bisimulation in a way that onle safely
@@ -56,10 +59,11 @@ namespace storm {
* @param model The model to decompose.
* @param phiLabel The label that all phi states carry in the model.
* @param psiLabel The label that all psi states carry in the model.
+ * @param weak A flag indication whether a weak bisimulation is to be computed.
* @param bounded If set to true, also bounded until formulas are preserved.
* @param buildQuotient Sets whether or not the quotient model is to be built.
*/
- DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient = false);
+ DeterministicModelBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded, bool buildQuotient = false);
/*!
* Retrieves the quotient of the model under the previously computed bisimulation.
@@ -69,6 +73,8 @@ namespace storm {
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> getQuotient() const;
private:
+ enum class BisimulationType { Strong, WeakDtmc, WeakCtmc };
+
class Partition;
class Block {
@@ -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<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator end);
+ void updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last);
// Retrieves the first block of the partition.
Block& getFirstBlock();
+
+ // Retrieves whether the given state is fully silent (only in case the silent probabilities are tracked).
+ bool isSilent(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+
+ // Retrieves whether the given state has a non-zero silent probability.
+ bool hasSilentProbability(storm::storage::sparse::state_type state, storm::utility::ConstantsComparator<ValueType> const& comparator) const;
+
+ // Retrieves the silent probability (i.e. the probability to stay within the own equivalence class).
+ ValueType const& getSilentProbability(storm::storage::sparse::state_type state) const;
+
+ // Sets the silent probabilities for all the states in the range to their values in the range.
+ void setSilentProbabilities(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last);
+
+ // Sets the silent probabilities for all states in the range to zero.
+ void setSilentProbabilitiesToZero(typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last);
+
+ // Sets the silent probability for the given state to the given value.
+ void setSilentProbability(storm::storage::sparse::state_type state, ValueType const& value);
+
private:
// The list of blocks in the partition.
std::list<Block> blocks;
@@ -355,6 +379,13 @@ namespace storm {
// This vector keeps track of the position of each state in the state vector.
std::vector<storm::storage::sparse::state_type> positions;
+
+ // A flag that indicates whether or not the vector with silent probabilities exists.
+ bool keepSilentProbabilities;
+
+ // This vector keeps track of the silent probabilities (i.e. the probabilities going into the very own
+ // equivalence class) of each state. This means that a state is silent iff its entry is non-zero.
+ std::vector<ValueType> silentProbabilities;
};
/*!
@@ -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<typename ModelType>
- void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient);
+ void partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, 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<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue);
+ void refinePartition(storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue);
/*!
* Refines the block based on their probability values (leading into the splitter).
*
* @param block The block to refine.
* @param partition The partition that contains the block.
+ * @param bisimulationType The kind of bisimulation that is to be computed.
* @param splitterQueue A queue into which all blocks that were split are inserted so they can be treated
* as splitters in the future.
*/
- void refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue);
+ void refineBlockProbabilities(Block& block, Partition& partition, BisimulationType bisimulationType, std::deque<Block*>& splitterQueue);
+
+ void refineBlockWeak(Block& block, Partition& partition, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::deque<Block*>& splitterQueue);
+
+ /*!
+ * Determines the split offsets in the given block.
+ *
+ * @param block The block that is to be analyzed for splits.
+ * @param partition The partition that contains the block.
+ */
+ std::vector<uint_fast64_t> getSplitPointsWeak(Block& block, Partition& partition);
/*!
* Builds the quotient model based on the previously computed equivalence classes (stored in the blocks
@@ -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<typename ModelType>
- 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<typename ModelType>
- Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded = false);
+ Partition getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool weak, bool bounded = false);
/*!
* Creates the initial partition based on all the labels in the given model.
*
* @param model The model whose state space is partitioned based on its labels.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param weak A flag indicating whether a weak bisimulation is to be computed.
* @return The resulting partition.
*/
template<typename ModelType>
- Partition getLabelBasedInitialPartition(ModelType const& model);
+ Partition getLabelBasedInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool weak);
+
+ /*!
+ * Splits all blocks of the given partition into a block that contains all divergent states and another block
+ * containing the non-divergent states.
+ *
+ * @param model The model from which to look-up the probabilities.
+ * @param backwardTransitions The backward transitions of the model.
+ * @param partition The partition that holds the silent probabilities.
+ */
+ template<typename ModelType>
+ void splitOffDivergentStates(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition);
+
+ /*!
+ * Initializes the silent probabilities by traversing all blocks and adding the probability of going to
+ * the very own equivalence class for each state.
+ *
+ * @param model The model from which to look-up the probabilities.
+ * @param partition The partition that holds the silent probabilities.
+ */
+ template<typename ModelType>
+ void initializeSilentProbabilities(ModelType const& model, Partition& partition);
// If required, a quotient model is built and stored in this member.
std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> quotient;
@@ -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 1c11a8107..000000000
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ /dev/null
@@ -1,899 +0,0 @@
-#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
-
-#include <algorithm>
-#include <unordered_map>
-#include <chrono>
-#include <iomanip>
-#include <boost/iterator/transform_iterator.hpp>
-
-#include "src/utility/graph.h"
-#include "src/exceptions/IllegalFunctionCallException.h"
-
-namespace storm {
- namespace storage {
-
- template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::blockId = 0;
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr<std::string> const& label) : next(next), prev(prev), begin(begin), end(end), markedAsSplitter(false), markedAsPredecessorBlock(false), markedPosition(begin), absorbing(false), id(blockId++), label(label) {
- 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<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::print(Partition const& partition) const {
- std::cout << "block " << this->getId() << " with marked position " << this->getMarkedPosition() << " and original begin " << this->getOriginalBegin() << std::endl;
- std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl;
- std::cout << "states:" << std::endl;
- 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<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
- this->begin = begin;
- this->markedPosition = begin;
- STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
- this->end = end;
- STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementBegin() {
- ++this->begin;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::decrementEnd() {
- ++this->begin;
- }
-
- template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getBegin() const {
- return this->begin;
- }
-
- template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getOriginalBegin() const {
- if (this->hasPreviousBlock()) {
- return this->getPreviousBlock().getEnd();
- } else {
- return 0;
- }
- }
-
- template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getEnd() const {
- return this->end;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setIterator(iterator it) {
- this->selfIt = it;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getIterator() const {
- return this->selfIt;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextIterator() const {
- return this->getNextBlock().getIterator();
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousIterator() const {
- return this->getPreviousBlock().getIterator();
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() {
- return *this->next;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlock() const {
- return *this->next;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasNextBlock() const {
- return this->next != nullptr;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() {
- return *this->prev;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlockPointer() {
- return this->prev;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block* DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNextBlockPointer() {
- return this->next;
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getPreviousBlock() const {
- return *this->prev;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasPreviousBlock() const {
- return this->prev != nullptr;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::check() const {
- if (this->begin >= this->end) {
- assert(false);
- }
- if (this->prev != nullptr) {
- assert (this->prev->next == this);
- }
- if (this->next != nullptr) {
- assert (this->next->prev == this);
- }
- return true;
- }
-
- template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getNumberOfStates() const {
- // We need to take the original begin here, because the begin is temporarily moved.
- return (this->end - this->getOriginalBegin());
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsSplitter() const {
- return this->markedAsSplitter;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsSplitter() {
- this->markedAsSplitter = true;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsSplitter() {
- this->markedAsSplitter = false;
- }
-
- template<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getId() const {
- return this->id;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setAbsorbing(bool absorbing) {
- this->absorbing = absorbing;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isAbsorbing() const {
- return this->absorbing;
- }
-
- template<typename ValueType>
- storm::storage::sparse::state_type DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getMarkedPosition() const {
- return this->markedPosition;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setMarkedPosition(storm::storage::sparse::state_type position) {
- this->markedPosition = position;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::resetMarkedPosition() {
- this->markedPosition = this->begin;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::incrementMarkedPosition() {
- ++this->markedPosition;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::markAsPredecessorBlock() {
- this->markedAsPredecessorBlock = true;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::unmarkAsPredecessorBlock() {
- this->markedAsPredecessorBlock = false;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::isMarkedAsPredecessor() const {
- return markedAsPredecessorBlock;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::hasLabel() const {
- return this->label != nullptr;
- }
-
- template<typename ValueType>
- std::string const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabel() const {
- STORM_LOG_THROW(this->label != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve label of block that has none.");
- return *this->label;
- }
-
- template<typename ValueType>
- std::shared_ptr<std::string> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::getLabelPtr() const {
- return this->label;
- }
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) {
- // Create the block and give it an iterator to itself.
- typename std::list<Block>::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr);
- it->setIterator(it);
-
- // 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<ValueType>());
- positions[state] = state;
- stateToBlockMapping[state] = &blocks.back();
- }
- }
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) {
- typename std::list<Block>::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr);
- Block& firstBlock = *firstIt;
- firstBlock.setIterator(firstIt);
-
- storm::storage::sparse::state_type position = 0;
- for (auto state : prob0States) {
- statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
- positions[state] = position;
- stateToBlockMapping[state] = &firstBlock;
- ++position;
- }
- firstBlock.setAbsorbing(true);
-
- typename std::list<Block>::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, std::shared_ptr<std::string>(new std::string(prob1Label)));
- Block& secondBlock = *secondIt;
- secondBlock.setIterator(secondIt);
-
- for (auto state : prob1States) {
- statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
- positions[state] = position;
- stateToBlockMapping[state] = &secondBlock;
- ++position;
- }
- secondBlock.setAbsorbing(true);
-
- typename std::list<Block>::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, otherLabel == "true" ? std::shared_ptr<std::string>(nullptr) : std::shared_ptr<std::string>(new std::string(otherLabel)));
- Block& thirdBlock = *thirdIt;
- thirdBlock.setIterator(thirdIt);
-
- storm::storage::BitVector otherStates = ~(prob0States | prob1States);
- for (auto state : otherStates) {
- statesAndValues[position] = std::make_pair(state, storm::utility::zero<ValueType>());
- positions[state] = position;
- stateToBlockMapping[state] = &thirdBlock;
- ++position;
- }
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) {
- std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]);
- std::swap(this->positions[state1], this->positions[state2]);
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) {
- 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<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getPosition(storm::storage::sparse::state_type state) const {
- return this->positions[state];
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) {
- this->positions[state] = position;
- }
-
- template<typename ValueType>
- storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getState(storm::storage::sparse::state_type position) const {
- return this->statesAndValues[position].first;
- }
-
- template<typename ValueType>
- ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValue(storm::storage::sparse::state_type state) const {
- return this->statesAndValues[this->positions[state]].second;
- }
-
- template<typename ValueType>
- ValueType const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const {
- return this->statesAndValues[position].second;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) {
- this->statesAndValues[this->positions[state]].second = value;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) {
- this->statesAndValues[this->positions[state]].second += value;
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::updateBlockMapping(Block& block, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator first, typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator last) {
- for (; first != last; ++first) {
- this->stateToBlockMapping[first->first] = █
- }
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getFirstBlock() {
- return *this->blocks.begin();
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) {
- return *this->stateToBlockMapping[state];
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlock(storm::storage::sparse::state_type state) const {
- return *this->stateToBlockMapping[state];
- }
-
- template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) {
- return this->statesAndValues.begin() + block.getBegin();
- }
-
- template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) {
- return this->statesAndValues.begin() + block.getEnd();
- }
-
- template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBegin(Block const& block) const {
- return this->statesAndValues.begin() + block.getBegin();
- }
-
- template<typename ValueType>
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getEnd(Block const& block) const {
- return this->statesAndValues.begin() + block.getEnd();
- }
-
- template<typename ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) {
- // 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<Block>::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 ValueType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::insertBlock(Block& block) {
- // Find the beginning of the new block.
- storm::storage::sparse::state_type begin;
- if (block.hasPreviousBlock()) {
- begin = block.getPreviousBlock().getEnd();
- } else {
- begin = 0;
- }
-
- // Actually insert the new block.
- typename std::list<Block>::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<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::splitLabel(storm::storage::BitVector const& statesWithLabel) {
- for (auto blockIterator = this->blocks.begin(), ite = this->blocks.end(); blockIterator != ite; ) { // The update of the loop was intentionally moved to the bottom of the loop.
- Block& block = *blockIterator;
-
- // 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<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> 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<std::pair<storm::storage::sparse::state_type, ValueType>>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair<storm::storage::sparse::state_type, ValueType> 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<typename ValueType>
- std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block> const& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() const {
- return this->blocks;
- }
-
- template<typename ValueType>
- std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getStatesAndValues() {
- return this->statesAndValues;
- }
-
- template<typename ValueType>
- std::list<typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Block>& DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::getBlocks() {
- return this->blocks;
- }
-
- template<typename ValueType>
- bool DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::check() const {
- for (uint_fast64_t state = 0; state < this->positions.size(); ++state) {
- if (this->statesAndValues[this->positions[state]].first != state) {
- assert(false);
- }
- }
- 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<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::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<typename ValueType>
- std::size_t DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition::size() const {
- return this->blocks.size();
- }
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, bool buildQuotient) {
- STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- Partition initialPartition = getLabelBasedInitialPartition(model);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
- }
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, bool buildQuotient) {
- STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- Partition initialPartition = getLabelBasedInitialPartition(model);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
- }
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Dtmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) {
- STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
- }
-
- template<typename ValueType>
- DeterministicModelStrongBisimulationDecomposition<ValueType>::DeterministicModelStrongBisimulationDecomposition(storm::models::Ctmc<ValueType> const& model, std::string const& phiLabel, std::string const& psiLabel, bool bounded, bool buildQuotient) {
- STORM_LOG_THROW(!model.hasStateRewards() && !model.hasTransitionRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently only supported for models without reward structures.");
- storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
- Partition initialPartition = getMeasureDrivenInitialPartition(model, backwardTransitions, phiLabel, psiLabel, bounded);
- partitionRefinement(model, model.getBackwardTransitions(), initialPartition, buildQuotient);
- }
-
- template<typename ValueType>
- std::shared_ptr<storm::models::AbstractDeterministicModel<ValueType>> DeterministicModelStrongBisimulationDecomposition<ValueType>::getQuotient() const {
- STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built.");
- return this->quotient;
- }
-
- template<typename ValueType>
- template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::buildQuotient(ModelType const& model, Partition const& partition) {
- // In order to create the quotient model, we need to construct
- // (a) the new transition matrix,
- // (b) the new labeling,
- // (c) the new reward structures.
-
- // Prepare a matrix builder for (a).
- storm::storage::SparseMatrixBuilder<ValueType> builder(this->size(), this->size());
-
- // Prepare the new state labeling for (b).
- storm::models::AtomicPropositionsLabeling newLabeling(this->size(), model.getStateLabeling().getNumberOfAtomicPropositions());
- std::set<std::string> atomicPropositionsSet = model.getStateLabeling().getAtomicPropositions();
- std::vector<std::string> atomicPropositions = std::vector<std::string>(atomicPropositionsSet.begin(), atomicPropositionsSet.end());
- for (auto const& ap : atomicPropositions) {
- newLabeling.addAtomicProposition(ap);
- }
-
- // 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<ValueType>());
-
- if (oldBlock.hasLabel()) {
- newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
- }
- } else {
- // Compute the outgoing transitions of the block.
- std::map<storm::storage::sparse::state_type, ValueType> blockProbability;
- for (auto const& entry : model.getTransitionMatrix().getRow(representativeState)) {
- storm::storage::sparse::state_type targetBlock = partition.getBlock(entry.getColumn()).getId();
- auto probIterator = blockProbability.find(targetBlock);
- if (probIterator != blockProbability.end()) {
- probIterator->second += entry.getValue();
- } else {
- blockProbability[targetBlock] = entry.getValue();
- }
- }
-
- // Now add them to the actual matrix.
- for (auto const& probabilityEntry : blockProbability) {
- builder.addNextValue(blockIndex, probabilityEntry.first, probabilityEntry.second);
- }
-
- // If the block has a special label, we only add that to the block.
- if (oldBlock.hasLabel()) {
- newLabeling.addAtomicPropositionToState(oldBlock.getLabel(), blockIndex);
- } else {
- // Otherwise add all atomic propositions to the equivalence class that the representative state
- // satisfies.
- for (auto const& ap : atomicPropositions) {
- if (model.getStateLabeling().getStateHasAtomicProposition(ap, representativeState)) {
- newLabeling.addAtomicPropositionToState(ap, blockIndex);
- }
- }
- }
- }
- }
-
- // Now check which of the blocks of the partition contain at least one initial state.
- for (auto initialState : 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<storm::models::AbstractDeterministicModel<ValueType>>(new ModelType(builder.build(), std::move(newLabeling)));
- }
-
- template<typename ValueType>
- template<typename ModelType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Partition& partition, bool buildQuotient) {
- std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now();
-
- // Initially, all blocks are potential splitter, so we insert them in the splitterQueue.
- std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now();
- std::deque<Block*> splitterQueue;
- std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); });
-
- // 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<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.first < b.first; });
-
- // Convert the state-value-pairs to states only.
- auto lambda = [] (std::pair<storm::storage::sparse::state_type, ValueType> 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<std::chrono::milliseconds>(refinementTime).count() << "ms" << std::endl;
- std::cout << " * time for extraction: " << std::chrono::duration_cast<std::chrono::milliseconds>(extractionTime).count() << "ms" << std::endl;
- std::cout << "------------------------------------------" << std::endl;
- std::cout << " * total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTime).count() << "ms" << std::endl;
- std::cout << std::endl;
- }
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refineBlockProbabilities(Block& block, Partition& partition, std::deque<Block*>& splitterQueue) {
- // Sort the states in the block based on their probabilities.
- std::sort(partition.getBegin(block), partition.getEnd(block), [&partition] (std::pair<storm::storage::sparse::state_type, ValueType> const& a, std::pair<storm::storage::sparse::state_type, ValueType> const& b) { return a.second < b.second; } );
-
- // 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<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator begin = partition.getBegin(block);
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator current = begin;
- typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
- storm::storage::sparse::state_type currentIndex = block.getBegin();
-
-
- // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
- // first and the last state are different.
- 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();
- }
- }
- }
-
- template<typename ValueType>
- void DeterministicModelStrongBisimulationDecomposition<ValueType>::refinePartition(storm::storage::SparseMatrix<ValueType> const& backwardTransitions, Block& splitter, Partition& partition, std::deque<Block*>& splitterQueue) {
- std::list<Block*> predecessorBlocks;
-
- // Iterate over all states of the splitter and check its predecessors.
- 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<Block*> blocksToSplit;
-
- // Now, we can iterate over the predecessor blocks and see whether we have to create a new block for
- // predecessors of the splitter.
- for (auto blockPtr : predecessorBlocks) {
- Block& block = *blockPtr;
-
- 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;
- }
-
- refineBlockProbabilities(*blockPtr, partition, splitterQueue);
- }
- }
-
- template<typename ValueType>
- template<typename ModelType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, bool bounded) {
- std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel));
- Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel);
- return partition;
- }
-
- template<typename ValueType>
- template<typename ModelType>
- typename DeterministicModelStrongBisimulationDecomposition<ValueType>::Partition DeterministicModelStrongBisimulationDecomposition<ValueType>::getLabelBasedInitialPartition(ModelType const& model) {
- Partition partition(model.getNumberOfStates());
- for (auto const& label : model.getStateLabeling().getAtomicPropositions()) {
- if (label == "init") {
- continue;
- }
- partition.splitLabel(model.getLabeledStates(label));
- }
- return partition;
- }
-
- template class DeterministicModelStrongBisimulationDecomposition<double>;
- }
-}
\ No newline at end of file
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 908d7dc52..df8aa248a 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -47,7 +47,11 @@ log4cplus::Logger logger;
// Headers for model processing.
#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
-#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h"
+#include "src/storage/DeterministicModelBisimulationDecomposition.h"
+
+// Headers for model checking.
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
// Headers for counterexample generation.
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
@@ -267,7 +271,7 @@ namespace storm {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = result->template as<storm::models::Dtmc<double>>();
STORM_PRINT(std::endl << "Performing bisimulation minimization..." << std::endl);
- storm::storage::DeterministicModelStrongBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, true);
+ storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
result = bisimulationDecomposition.getQuotient();
@@ -315,10 +319,16 @@ namespace storm {
STORM_LOG_THROW(settings.isPctlPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(settings.getPctlProperty());
generateCounterexample(model, filterFormula->getChild());
+ } else if (settings.isPctlPropertySet()) {
+ std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> filterFormula = storm::parser::PrctlParser::parsePrctlFormula(storm::settings::generalSettings().getPctlProperty());
+
+ if (model->getType() == storm::models::DTMC) {
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
+ modelchecker::prctl::SparseDtmcPrctlModelChecker<double> modelchecker(*dtmc);
+ filterFormula->check(modelchecker);
+ }
}
-
}
-
}
}
}