From b25ef3f09c7d98116926e39a9b76830530db6334 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 31 Jul 2017 10:19:06 +0200
Subject: [PATCH] introduced symbolic bisimulation modes lazy and eager, fixed
bug in sparse quotient extraction
---
src/storm/api/bisimulation.h | 10 ++--
src/storm/cli/cli.cpp | 2 +-
src/storm/models/symbolic/Model.cpp | 2 +-
src/storm/models/symbolic/Model.h | 3 +-
.../models/symbolic/NondeterministicModel.cpp | 9 ++++
.../models/symbolic/NondeterministicModel.h | 9 ++++
.../settings/modules/BisimulationSettings.cpp | 14 ++++++
.../settings/modules/BisimulationSettings.h | 8 +++
.../bisimulation/BisimulationDecomposition.h | 18 +++----
.../storage/bisimulation/BisimulationType.h | 10 ++++
.../storage/dd/BisimulationDecomposition.cpp | 50 +++++++++++--------
.../storage/dd/BisimulationDecomposition.h | 9 ++--
src/storm/storage/dd/DdMetaVariable.cpp | 1 +
.../storage/dd/bisimulation/Partition.cpp | 41 +++++++++++----
src/storm/storage/dd/bisimulation/Partition.h | 14 ++++--
.../dd/bisimulation/QuotientExtractor.cpp | 27 +++++++---
.../dd/bisimulation/SignatureComputer.cpp | 34 ++++++++++++-
.../dd/bisimulation/SignatureComputer.h | 18 ++++++-
.../storage/dd/bisimulation/SignatureMode.h | 11 ++++
19 files changed, 222 insertions(+), 68 deletions(-)
create mode 100644 src/storm/storage/bisimulation/BisimulationType.h
create mode 100644 src/storm/storage/dd/bisimulation/SignatureMode.h
diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h
index ac8797fc8..c59c62b09 100644
--- a/src/storm/api/bisimulation.h
+++ b/src/storm/api/bisimulation.h
@@ -55,16 +55,18 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
+
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs and CTMCs.");
+ STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported.");
- storm::dd::BisimulationDecomposition<DdType, ValueType> decomposition(*model, formulas);
- decomposition.compute();
+ storm::dd::BisimulationDecomposition<DdType, ValueType> decomposition(*model, formulas, bisimulationType);
+ decomposition.compute(mode);
return decomposition.getQuotient();
}
template <storm::dd::DdType DdType, typename ValueType>
- typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ValueType>>>::type performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is not supported for this combination of DD library and value type.");
return nullptr;
}
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 7a1ef8066..5bab54a87 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -485,7 +485,7 @@ namespace storm {
STORM_LOG_WARN_COND(!bisimulationSettings.isWeakBisimulationSet(), "Weak bisimulation is currently not supported on DDs. Falling back to strong bisimulation.");
STORM_LOG_INFO("Performing bisimulation minimization...");
- return storm::api::performBisimulationMinimization<DdType, ValueType>(model, createFormulasToRespect(input.properties));
+ return storm::api::performBisimulationMinimization<DdType, ValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
}
template <storm::dd::DdType DdType, typename ValueType>
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 2a6804618..27a37534f 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -162,7 +162,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ValueType>
- storm::dd::Bdd<Type> Model<Type, ValueType>::getQualitativeTransitionMatrix() const {
+ storm::dd::Bdd<Type> Model<Type, ValueType>::getQualitativeTransitionMatrix(bool) const {
return this->getTransitionMatrix().notZero();
}
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index c9a628ff4..dbd74634c 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -204,9 +204,10 @@ namespace storm {
* Retrieves the matrix qualitatively (i.e. without probabilities) representing the transitions of the
* model.
*
+ * @param keepNondeterminism If false, the matrix will abstract from the nondeterminism variables.
* @return A matrix representing the qualitative transitions of the model.
*/
- storm::dd::Bdd<Type> getQualitativeTransitionMatrix() const;
+ virtual storm::dd::Bdd<Type> getQualitativeTransitionMatrix(bool keepNondeterminism = true) const;
/*!
* Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices.
diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp
index 71a334a1a..6545e27c0 100644
--- a/src/storm/models/symbolic/NondeterministicModel.cpp
+++ b/src/storm/models/symbolic/NondeterministicModel.cpp
@@ -96,6 +96,15 @@ namespace storm {
illegalMask = !(this->getTransitionMatrix().notZero().existsAbstract(this->getColumnVariables())) && this->getReachableStates();
}
+ template<storm::dd::DdType Type, typename ValueType>
+ storm::dd::Bdd<Type> NondeterministicModel<Type, ValueType>::getQualitativeTransitionMatrix(bool keepNondeterminism) const {
+ if (!keepNondeterminism) {
+ return this->getTransitionMatrix().notZero().existsAbstract(this->getNondeterminismVariables());
+ } else {
+ return Model<Type, ValueType>::getQualitativeTransitionMatrix(keepNondeterminism);
+ }
+ }
+
// Explicitly instantiate the template class.
template class NondeterministicModel<storm::dd::DdType::CUDD, double>;
template class NondeterministicModel<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h
index e97347c44..45dc27b0a 100644
--- a/src/storm/models/symbolic/NondeterministicModel.h
+++ b/src/storm/models/symbolic/NondeterministicModel.h
@@ -113,6 +113,15 @@ namespace storm {
*/
storm::dd::Bdd<Type> getIllegalSuccessorMask() const;
+ /*!
+ * Retrieves the matrix qualitatively (i.e. without probabilities) representing the transitions of the
+ * model.
+ *
+ * @param keepNondeterminism If false, the matrix will abstract from the nondeterminism variables.
+ * @return A matrix representing the qualitative transitions of the model.
+ */
+ virtual storm::dd::Bdd<Type> getQualitativeTransitionMatrix(bool keepNondeterminism = true) const override;
+
virtual void printModelInformationToStream(std::ostream& out) const override;
protected:
diff --git a/src/storm/settings/modules/BisimulationSettings.cpp b/src/storm/settings/modules/BisimulationSettings.cpp
index 2c1db8a39..679daa54d 100644
--- a/src/storm/settings/modules/BisimulationSettings.cpp
+++ b/src/storm/settings/modules/BisimulationSettings.cpp
@@ -16,6 +16,7 @@ namespace storm {
const std::string BisimulationSettings::typeOptionName = "type";
const std::string BisimulationSettings::representativeOptionName = "repr";
const std::string BisimulationSettings::quotientFormatOptionName = "quot";
+ const std::string BisimulationSettings::signatureModeOptionName = "sigmode";
BisimulationSettings::BisimulationSettings() : ModuleSettings(moduleName) {
std::vector<std::string> types = { "strong", "weak" };
@@ -25,6 +26,9 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build());
+
+ std::vector<std::string> signatureModes = { "eager", "lazy" };
+ this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
}
bool BisimulationSettings::isStrongBisimulationSet() const {
@@ -53,6 +57,16 @@ namespace storm {
return this->getOption(representativeOptionName).getHasOptionBeenSet();
}
+ storm::dd::bisimulation::SignatureMode BisimulationSettings::getSignatureMode() const {
+ std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString();
+ if (modeAsString == "eager") {
+ return storm::dd::bisimulation::SignatureMode::Eager;
+ } else if (modeAsString == "lazy") {
+ return storm::dd::bisimulation::SignatureMode::Lazy;
+ }
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unknown signature mode '" << modeAsString << ".");
+ }
+
bool BisimulationSettings::check() const {
bool optionsSet = this->getOption(typeOptionName).getHasOptionBeenSet();
STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet() || !optionsSet, "Bisimulation minimization is not selected, so setting options for bisimulation has no effect.");
diff --git a/src/storm/settings/modules/BisimulationSettings.h b/src/storm/settings/modules/BisimulationSettings.h
index ccdea9e5d..0d71baa86 100644
--- a/src/storm/settings/modules/BisimulationSettings.h
+++ b/src/storm/settings/modules/BisimulationSettings.h
@@ -3,6 +3,8 @@
#include "storm/settings/modules/ModuleSettings.h"
+#include "storm/storage/dd/bisimulation/SignatureMode.h"
+
namespace storm {
namespace settings {
namespace modules {
@@ -48,6 +50,11 @@ namespace storm {
*/
bool isUseRepresentativesSet() const;
+ /*!
+ * Retrieves the mode to compute signatures.
+ */
+ storm::dd::bisimulation::SignatureMode getSignatureMode() const;
+
virtual bool check() const override;
// The name of the module.
@@ -58,6 +65,7 @@ namespace storm {
static const std::string typeOptionName;
static const std::string representativeOptionName;
static const std::string quotientFormatOptionName;
+ static const std::string signatureModeOptionName;
};
} // namespace modules
} // namespace settings
diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.h b/src/storm/storage/bisimulation/BisimulationDecomposition.h
index 49089063a..6aa56345c 100644
--- a/src/storm/storage/bisimulation/BisimulationDecomposition.h
+++ b/src/storm/storage/bisimulation/BisimulationDecomposition.h
@@ -7,6 +7,7 @@
#include "storm/storage/Decomposition.h"
#include "storm/storage/StateBlock.h"
#include "storm/storage/bisimulation/Partition.h"
+#include "storm/storage/bisimulation/BisimulationType.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/logic/Formulas.h"
@@ -18,15 +19,12 @@ namespace storm {
namespace utility {
template <typename ValueType> class ConstantsComparator;
}
-
+
namespace logic {
class Formula;
}
namespace storage {
-
- enum class BisimulationType { Strong, Weak };
- enum class BisimulationTypeChoice { Strong, Weak, FromSettings };
inline BisimulationType resolveBisimulationTypeChoice(BisimulationTypeChoice c) {
switch(c) {
@@ -40,8 +38,8 @@ namespace storm {
} else {
return BisimulationType::Strong;
}
-
}
+ return BisimulationType::Strong;
}
/*!
@@ -89,7 +87,7 @@ namespace storm {
/**
* Sets the bisimulation type. If the bisimulation type is set to weak,
- * we also change the bounded flag (as bounded properties are not preserved under
+ * we also change the bounded flag (as bounded properties are not preserved under
* weak bisimulation).
*/
void setType(BisimulationType t) {
@@ -136,7 +134,7 @@ namespace storm {
private:
boost::optional<OptimizationDirection> optimalityType;
-
+
/// A flag that indicates whether or not the state-rewards of the model are to be respected (and should
/// be kept in the quotient model, if one is built).
bool keepRewards;
@@ -155,7 +153,7 @@ namespace storm {
* @param formula The only formula to check.
*/
void preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula);
-
+
/*!
* Adds the given expressions and labels to the set of respected atomic propositions.
*
@@ -189,7 +187,7 @@ namespace storm {
* @return The quotient model.
*/
std::shared_ptr<ModelType> getQuotient() const;
-
+
/*!
* Computes the decomposition of the model into bisimulation equivalence classes. If requested, a quotient
* model is built.
@@ -263,7 +261,7 @@ namespace storm {
// The model to decompose.
ModelType const& model;
-
+
// The backward transitions of the model.
storm::storage::SparseMatrix<ValueType> backwardTransitions;
diff --git a/src/storm/storage/bisimulation/BisimulationType.h b/src/storm/storage/bisimulation/BisimulationType.h
new file mode 100644
index 000000000..fc9dba9b2
--- /dev/null
+++ b/src/storm/storage/bisimulation/BisimulationType.h
@@ -0,0 +1,10 @@
+#pragma once
+
+namespace storm {
+ namespace storage {
+
+ enum class BisimulationType { Strong, Weak };
+ enum class BisimulationTypeChoice { Strong, Weak, FromSettings };
+
+ }
+}
diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp
index 81ad026af..89746b5e9 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.cpp
+++ b/src/storm/storage/dd/BisimulationDecomposition.cpp
@@ -8,22 +8,18 @@
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/NotSupportedException.h"
-#include <sylvan_table.h>
-
-extern llmsset_t nodes;
-
namespace storm {
namespace dd {
using namespace bisimulation;
template <storm::dd::DdType DdType, typename ValueType>
- BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model) : BisimulationDecomposition(model, bisimulation::Partition<DdType, ValueType>::create(model)) {
+ BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : BisimulationDecomposition(model, bisimulation::Partition<DdType, ValueType>::create(model, bisimulationType)) {
// Intentionally left empty.
}
template <storm::dd::DdType DdType, typename ValueType>
- BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : BisimulationDecomposition(model, bisimulation::Partition<DdType, ValueType>::create(model, formulas)) {
+ BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : BisimulationDecomposition(model, bisimulation::Partition<DdType, ValueType>::create(model, formulas, bisimulationType)) {
// Intentionally left empty.
}
@@ -33,7 +29,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- void BisimulationDecomposition<DdType, ValueType>::compute() {
+ void BisimulationDecomposition<DdType, ValueType>::compute(bisimulation::SignatureMode const& mode) {
this->status = Status::InComputation;
auto start = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::duration totalSignatureTime(0);
@@ -45,27 +41,41 @@ namespace storm {
#endif
SignatureRefiner<DdType, ValueType> refiner(model.getManager(), currentPartition.getBlockVariable(), model.getRowVariables());
- SignatureComputer<DdType, ValueType> signatureComputer(model);
+ SignatureComputer<DdType, ValueType> signatureComputer(model, mode);
bool done = false;
uint64_t iterations = 0;
while (!done) {
++iterations;
auto iterationStart = std::chrono::high_resolution_clock::now();
- auto signatureStart = std::chrono::high_resolution_clock::now();
- Signature<DdType, ValueType> signature = signatureComputer.compute(currentPartition);
- auto signatureEnd = std::chrono::high_resolution_clock::now();
- totalSignatureTime += (signatureEnd - signatureStart);
+ std::chrono::milliseconds::rep signatureTime = 0;
+ std::chrono::milliseconds::rep refinementTime = 0;
- auto refinementStart = std::chrono::high_resolution_clock::now();
- Partition<DdType, ValueType> newPartition = refiner.refine(currentPartition, signature);
- auto refinementEnd = std::chrono::high_resolution_clock::now();
- totalRefinementTime += (refinementEnd - refinementStart);
-
- auto signatureTime = std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
- auto refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
+ Partition<DdType, ValueType> newPartition;
+ for (uint64_t index = 0, end = signatureComputer.getNumberOfSignatures(); index < end; ++index) {
+ auto signatureStart = std::chrono::high_resolution_clock::now();
+ Signature<DdType, ValueType> signature = signatureComputer.compute(currentPartition, index);
+ auto signatureEnd = std::chrono::high_resolution_clock::now();
+ totalSignatureTime += (signatureEnd - signatureStart);
+ STORM_LOG_DEBUG("Signature " << iterations << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes and partition DD has " << currentPartition.getNodeCount() << " nodes.");
+
+ auto refinementStart = std::chrono::high_resolution_clock::now();
+ newPartition = refiner.refine(currentPartition, signature);
+ auto refinementEnd = std::chrono::high_resolution_clock::now();
+ totalRefinementTime += (refinementEnd - refinementStart);
+
+ signatureTime += std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
+ refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
+
+ // Potentially exit early in case we have refined the partition already.
+ if (newPartition.getNumberOfBlocks() > currentPartition.getNumberOfBlocks()) {
+ break;
+ }
+ }
+
auto iterationTime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - iterationStart).count();
- STORM_LOG_DEBUG("Iteration " << iterations << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << iterationTime << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms). Signature DD has " << signature.getSignatureAdd().getNodeCount() << " nodes and partition DD has " << currentPartition.getNodeCount() << " nodes.");
+
+ STORM_LOG_DEBUG("Iteration " << iterations << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << iterationTime << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
if (currentPartition == newPartition) {
done = true;
diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h
index d13d6a114..3650c58ed 100644
--- a/src/storm/storage/dd/BisimulationDecomposition.h
+++ b/src/storm/storage/dd/BisimulationDecomposition.h
@@ -4,8 +4,9 @@
#include <vector>
#include "storm/storage/dd/DdType.h"
-
+#include "storm/storage/bisimulation/BisimulationType.h"
#include "storm/storage/dd/bisimulation/Partition.h"
+#include "storm/storage/dd/bisimulation/SignatureMode.h"
#include "storm/models/symbolic/Model.h"
@@ -21,14 +22,14 @@ namespace storm {
Initialized, InComputation, FixedPoint
};
- BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model);
- BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+ BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
+ BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType);
BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, bisimulation::Partition<DdType, ValueType> const& initialPartition);
/*!
* Computes the decomposition.
*/
- void compute();
+ void compute(bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager);
/*!
* Retrieves the quotient model after the bisimulation decomposition was computed.
diff --git a/src/storm/storage/dd/DdMetaVariable.cpp b/src/storm/storage/dd/DdMetaVariable.cpp
index fda284391..9cebd15cb 100644
--- a/src/storm/storage/dd/DdMetaVariable.cpp
+++ b/src/storm/storage/dd/DdMetaVariable.cpp
@@ -68,6 +68,7 @@ namespace storm {
for (auto const& v : ddVariables) {
indicesAndLevels.emplace_back(v.getIndex(), v.getLevel());
}
+
return indicesAndLevels;
}
diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp
index 6e71074eb..7c434f653 100644
--- a/src/storm/storage/dd/bisimulation/Partition.cpp
+++ b/src/storm/storage/dd/bisimulation/Partition.cpp
@@ -8,7 +8,11 @@
#include "storm/logic/AtomicExpressionFormula.h"
#include "storm/logic/AtomicLabelFormula.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/BisimulationSettings.h"
+
#include "storm/utility/macros.h"
+#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/InvalidPropertyException.h"
namespace storm {
@@ -41,34 +45,34 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
- Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model) {
- return create(model, model.getLabels());
+ Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) {
+ return create(model, model.getLabels(), bisimulationType);
}
template<storm::dd::DdType DdType, typename ValueType>
- Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels) {
+ Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const& bisimulationType) {
std::shared_ptr<PreservationInformation> preservationInformation = std::make_shared<PreservationInformation>();
std::vector<storm::expressions::Expression> expressions;
for (auto const& label : labels) {
preservationInformation->addLabel(label);
expressions.push_back(model.getExpression(label));
}
- return create(model, expressions, preservationInformation);
+ return create(model, expressions, preservationInformation, bisimulationType);
}
template<storm::dd::DdType DdType, typename ValueType>
- Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions) {
+ Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const& bisimulationType) {
std::shared_ptr<PreservationInformation> preservationInformation = std::make_shared<PreservationInformation>();
for (auto const& expression : expressions) {
preservationInformation->addExpression(expression);
}
- return create(model, expressions, preservationInformation);
+ return create(model, expressions, preservationInformation, bisimulationType);
}
template<storm::dd::DdType DdType, typename ValueType>
- Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) {
if (formulas.empty()) {
- return create(model);
+ return create(model, bisimulationType);
}
std::shared_ptr<PreservationInformation> preservationInformation = std::make_shared<PreservationInformation>();
@@ -93,11 +97,14 @@ namespace storm {
expressionVector.emplace_back(expression);
}
- return create(model, expressionVector, preservationInformation);
+ return create(model, expressionVector, preservationInformation, bisimulationType);
}
template<storm::dd::DdType DdType, typename ValueType>
- Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, std::shared_ptr<PreservationInformation> const& preservationInformation) {
+ Partition<DdType, ValueType> Partition<DdType, ValueType>::create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, std::shared_ptr<PreservationInformation> const& preservationInformation, storm::storage::BisimulationType const& bisimulationType) {
+
+ STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported.");
+
storm::dd::DdManager<DdType>& manager = model.getManager();
std::vector<storm::dd::Bdd<DdType>> stateSets;
@@ -122,6 +129,20 @@ namespace storm {
}
}
+ template<storm::dd::DdType DdType, typename ValueType>
+ uint64_t Partition<DdType, ValueType>::getNumberOfStates() const {
+ return this->getStates().getNonZeroCount();
+ }
+
+ template<storm::dd::DdType DdType, typename ValueType>
+ storm::dd::Bdd<DdType> Partition<DdType, ValueType>::getStates() const {
+ if (this->storedAsAdd()) {
+ return this->asAdd().notZero().existsAbstract({this->getBlockVariable()});
+ } else {
+ return this->asBdd().existsAbstract({this->getBlockVariable()});
+ }
+ }
+
template<storm::dd::DdType DdType, typename ValueType>
uint64_t Partition<DdType, ValueType>::getNumberOfBlocks() const {
return nextFreeBlockIndex;
diff --git a/src/storm/storage/dd/bisimulation/Partition.h b/src/storm/storage/dd/bisimulation/Partition.h
index f52c827cb..80d882645 100644
--- a/src/storm/storage/dd/bisimulation/Partition.h
+++ b/src/storm/storage/dd/bisimulation/Partition.h
@@ -8,6 +8,7 @@
#include "storm/storage/dd/DdType.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
+#include "storm/storage/bisimulation/BisimulationType.h"
#include "storm/models/symbolic/Model.h"
@@ -35,23 +36,24 @@ namespace storm {
/*!
* Creates a partition from the given model that respects all labels.
*/
- static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model);
+ static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
/*!
* Creates a partition from the given model that respects the given labels.
*/
- static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels);
+ static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::string> const& labels, storm::storage::BisimulationType const& bisimulationType);
/*!
* Creates a partition from the given model that respects the given expressions.
*/
- static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions);
+ static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, storm::storage::BisimulationType const& bisimulationType);
/*!
* Creates a partition from the given model that preserves the given formulas.
*/
- static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+ static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType);
+ uint64_t getNumberOfStates() const;
uint64_t getNumberOfBlocks() const;
bool storedAsAdd() const;
@@ -66,6 +68,8 @@ namespace storm {
uint64_t getNextFreeBlockIndex() const;
uint64_t getNodeCount() const;
+ storm::dd::Bdd<DdType> getStates() const;
+
PreservationInformation const& getPreservationInformation() const;
private:
@@ -98,7 +102,7 @@ namespace storm {
/*!
* Creates a partition from the given model that respects the given expressions.
*/
- static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, std::shared_ptr<PreservationInformation> const& preservationInformation);
+ static Partition create(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::expressions::Expression> const& expressions, std::shared_ptr<PreservationInformation> const& preservationInformation, storm::storage::BisimulationType const& bisimulationType);
static std::pair<storm::dd::Bdd<DdType>, uint64_t> createPartitionBdd(storm::dd::DdManager<DdType> const& manager, storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<storm::dd::Bdd<DdType>> const& stateSets, storm::expressions::Variable const& blockVariable);
diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index aee570395..2fb31b2d1 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -83,6 +83,7 @@ namespace storm {
// Create the number of rows necessary for the matrix.
this->entries.resize(partition.getNumberOfBlocks());
+ STORM_LOG_TRACE("Partition has " << partition.getNumberOfStates() << " states in " << partition.getNumberOfBlocks() << " blocks.");
storm::storage::BitVector encoding(this->stateVariablesIndicesAndLevels.size());
extractTransitionMatrixRec(transitionMatrix.getInternalAdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), partition.asAdd().getInternalAdd().getCuddDdNode(), 0, encoding);
@@ -106,11 +107,16 @@ namespace storm {
return *blockCacheEntry;
}
+// FILE* fp = fopen("block.dot" , "w");
+// Cudd_DumpDot(ddman, 1, &blockEncoding, nullptr, nullptr, fp);
+// fclose(fp);
+
uint64_t result = 0;
uint64_t offset = 0;
while (blockEncoding != Cudd_ReadOne(ddman)) {
- if (Cudd_T(blockEncoding) != Cudd_ReadZero(ddman)) {
- blockEncoding = Cudd_T(blockEncoding);
+ DdNode* then = Cudd_T(blockEncoding);
+ if (then != Cudd_ReadZero(ddman)) {
+ blockEncoding = then;
result |= 1ull << offset;
} else {
blockEncoding = Cudd_E(blockEncoding);
@@ -205,6 +211,7 @@ namespace storm {
DdNode* te = transitionMatrixNode;
DdNode* et = transitionMatrixNode;
DdNode* ee = transitionMatrixNode;
+ STORM_LOG_ASSERT(transitionMatrixVariable >= this->stateVariablesIndicesAndLevels[currentIndex].first, "Illegal top variable of transition matrix.");
if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
DdNode* t = Cudd_T(transitionMatrixNode);
DdNode* e = Cudd_E(transitionMatrixNode);
@@ -226,16 +233,17 @@ namespace storm {
}
} else {
if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
- tt = Cudd_T(transitionMatrixNode);
- te = Cudd_E(transitionMatrixNode);
+ tt = et = Cudd_T(transitionMatrixNode);
+ te = ee = Cudd_E(transitionMatrixNode);
} else {
- tt = te = transitionMatrixNode;
+ tt = te = et = ee = transitionMatrixNode;
}
}
// Move through partition (for source state).
DdNode* sourceT;
DdNode* sourceE;
+ STORM_LOG_ASSERT(sourcePartitionVariable >= this->stateVariablesIndicesAndLevels[currentIndex].first, "Illegal top variable of source partition.");
if (sourcePartitionVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
sourceT = Cudd_T(sourcePartitionNode);
sourceE = Cudd_E(sourcePartitionNode);
@@ -246,6 +254,7 @@ namespace storm {
// Move through partition (for target state).
DdNode* targetT;
DdNode* targetE;
+ STORM_LOG_ASSERT(targetPartitionVariable >= this->stateVariablesIndicesAndLevels[currentIndex].first, "Illegal top variable of source partition.");
if (targetPartitionVariable == this->stateVariablesIndicesAndLevels[currentIndex].first) {
targetT = Cudd_T(targetPartitionNode);
targetE = Cudd_E(targetPartitionNode);
@@ -422,10 +431,10 @@ namespace storm {
}
} else {
if (transitionMatrixVariable == this->stateVariablesIndicesAndLevels[currentIndex].first + 1) {
- tt = sylvan_high(transitionMatrixNode);
- te = sylvan_low(transitionMatrixNode);
+ tt = et = sylvan_high(transitionMatrixNode);
+ te = ee = sylvan_low(transitionMatrixNode);
} else {
- tt = te = transitionMatrixNode;
+ tt = te = et = ee = transitionMatrixNode;
}
}
@@ -490,6 +499,8 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> QuotientExtractor<DdType, ValueType>::extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition) {
InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model.getManager(), model.getRowVariables());
+ auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs());
+
storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix(), partition);
storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks());
diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp
index 873d81608..f7606115f 100644
--- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp
+++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp
@@ -7,14 +7,35 @@ namespace storm {
namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType>
- SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model), transitionMatrix(model.getTransitionMatrix()) {
+ SignatureComputer<DdType, ValueType>::SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode) : model(model), transitionMatrix(model.getTransitionMatrix()), mode(mode) {
if (DdType == storm::dd::DdType::Sylvan) {
this->transitionMatrix = this->transitionMatrix.notZero().ite(this->transitionMatrix, this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
}
+ if (mode == SignatureMode::Lazy) {
+ if (DdType == storm::dd::DdType::Sylvan) {
+ this->transitionMatrix01 = model.getQualitativeTransitionMatrix().ite(this->transitionMatrix.getDdManager().template getAddOne<ValueType>(), this->transitionMatrix.getDdManager().template getAddUndefined<ValueType>());
+ } else {
+ this->transitionMatrix01 = model.getQualitativeTransitionMatrix().template toAdd<ValueType>();
+ }
+ }
}
template<storm::dd::DdType DdType, typename ValueType>
- Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::compute(Partition<DdType, ValueType> const& partition) {
+ uint64_t SignatureComputer<DdType, ValueType>::getNumberOfSignatures() const {
+ return this->mode == SignatureMode::Lazy ? 2 : 1;
+ }
+
+ template<storm::dd::DdType DdType, typename ValueType>
+ Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::compute(Partition<DdType, ValueType> const& partition, uint64_t index) {
+ if (mode == SignatureMode::Lazy && index == 1) {
+ return getQualitativeSignature(partition);
+ } else {
+ return getFullSignature(partition);
+ }
+ }
+
+ template<storm::dd::DdType DdType, typename ValueType>
+ Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::getFullSignature(Partition<DdType, ValueType> const& partition) const {
if (partition.storedAsBdd()) {
return Signature<DdType, ValueType>(this->transitionMatrix.multiplyMatrix(partition.asBdd(), model.getColumnVariables()));
} else {
@@ -22,6 +43,15 @@ namespace storm {
}
}
+ template<storm::dd::DdType DdType, typename ValueType>
+ Signature<DdType, ValueType> SignatureComputer<DdType, ValueType>::getQualitativeSignature(Partition<DdType, ValueType> const& partition) const {
+ if (partition.storedAsBdd()) {
+ return Signature<DdType, ValueType>(this->transitionMatrix01.multiplyMatrix(partition.asBdd(), model.getColumnVariables()));
+ } else {
+ return Signature<DdType, ValueType>(this->transitionMatrix01.multiplyMatrix(partition.asAdd(), model.getColumnVariables()));
+ }
+ }
+
template class SignatureComputer<storm::dd::DdType::CUDD, double>;
template class SignatureComputer<storm::dd::DdType::Sylvan, double>;
diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.h b/src/storm/storage/dd/bisimulation/SignatureComputer.h
index f2de03f49..9b6177c1e 100644
--- a/src/storm/storage/dd/bisimulation/SignatureComputer.h
+++ b/src/storm/storage/dd/bisimulation/SignatureComputer.h
@@ -4,6 +4,7 @@
#include "storm/storage/dd/bisimulation/Signature.h"
#include "storm/storage/dd/bisimulation/Partition.h"
+#include "storm/storage/dd/bisimulation/SignatureMode.h"
#include "storm/models/symbolic/Model.h"
@@ -14,14 +15,27 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
class SignatureComputer {
public:
- SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model);
+ SignatureComputer(storm::models::symbolic::Model<DdType, ValueType> const& model, SignatureMode const& mode = SignatureMode::Eager);
- Signature<DdType, ValueType> compute(Partition<DdType, ValueType> const& partition);
+ Signature<DdType, ValueType> compute(Partition<DdType, ValueType> const& partition, uint64_t index = 0);
+
+ uint64_t getNumberOfSignatures() const;
private:
+ Signature<DdType, ValueType> getFullSignature(Partition<DdType, ValueType> const& partition) const;
+
+ Signature<DdType, ValueType> getQualitativeSignature(Partition<DdType, ValueType> const& partition) const;
+
storm::models::symbolic::Model<DdType, ValueType> const& model;
+ // The transition matrix to use for the signature computation.
storm::dd::Add<DdType, ValueType> transitionMatrix;
+
+ // The mode to use for signature computation.
+ SignatureMode mode;
+
+ // Only used when using lazy signatures is enabled.
+ storm::dd::Add<DdType, ValueType> transitionMatrix01;
};
}
diff --git a/src/storm/storage/dd/bisimulation/SignatureMode.h b/src/storm/storage/dd/bisimulation/SignatureMode.h
new file mode 100644
index 000000000..bcec54b6f
--- /dev/null
+++ b/src/storm/storage/dd/bisimulation/SignatureMode.h
@@ -0,0 +1,11 @@
+#pragma once
+
+namespace storm {
+ namespace dd {
+ namespace bisimulation {
+
+ enum class SignatureMode { Eager, Lazy };
+
+ }
+ }
+}