sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

enabling changing value type in quotient extraction of dd-bisimulation

tempestpy_adaptions
dehnert 7 years ago
parent
5f7cd17789
commit
09866e4577
13 changed files with 204 additions and 141 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 50
      src/storm-cli-utilities/model-handling.h
  2. 10
      src/storm/api/bisimulation.h
  3. 4
      src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h
  4. 36
      src/storm/models/symbolic/Model.cpp
  5. 5
      src/storm/models/symbolic/Model.h
  6. 19
      src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
  7. 3
      src/storm/models/symbolic/StochasticTwoPlayerGame.h
  8. 51
      src/storm/storage/dd/BisimulationDecomposition.cpp
  9. 8
      src/storm/storage/dd/BisimulationDecomposition.h
  10. 22
      src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
  11. 6
      src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
  12. 119
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  13. 12
      src/storm/storage/dd/bisimulation/QuotientExtractor.h

50
src/storm-cli-utilities/model-handling.h
View File

@ -322,43 +322,47 @@ namespace storm {
}
}
template <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
std::shared_ptr<storm::models::Model<ExportValueType>> preprocessDdModelBisimulation(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) {
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), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
return storm::api::performBisimulationMinimization<DdType, ValueType, ExportValueType>(model, createFormulasToRespect(input.properties), storm::storage::BisimulationType::Strong, bisimulationSettings.getSignatureMode());
}
template <storm::dd::DdType DdType, typename ValueType>
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> result = std::make_pair(model, false);
std::pair<std::shared_ptr<storm::models::Model<ValueType>>, bool> intermediateResult = std::make_pair(model, false);
if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
result.first = preprocessDdMarkovAutomaton(result.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
result.second = true;
intermediateResult.first = preprocessDdMarkovAutomaton(intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>());
intermediateResult.second = true;
}
std::unique_ptr<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>> result;
auto symbolicModel = intermediateResult.first->template as<storm::models::symbolic::Model<DdType, ValueType>>();
if (generalSettings.isBisimulationSet()) {
result.first = preprocessDdModelBisimulation(model, input, bisimulationSettings);
result.second = true;
std::shared_ptr<storm::models::Model<ExportValueType>> newModel = preprocessDdModelBisimulation<DdType, ValueType, ExportValueType>(symbolicModel, input, bisimulationSettings);
result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(newModel, true);
} else {
result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
}
return result;
return *result;
}
template <storm::dd::DdType DdType, typename ValueType>
template <storm::dd::DdType DdType, typename BuildValueType, typename ExportValueType = BuildValueType>
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
storm::utility::Stopwatch preprocessingWatch(true);
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
if (model->isSparseModel()) {
result = preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input);
} else {
STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
result = preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
result = preprocessDdModel<DdType, BuildValueType, ExportValueType>(result.first->as<storm::models::symbolic::Model<DdType, BuildValueType>>(), input);
}
preprocessingWatch.stop();
@ -639,13 +643,13 @@ namespace storm {
}
}
template <storm::dd::DdType DdType, typename ValueType>
template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
std::shared_ptr<storm::models::ModelBase> model;
if (!buildSettings.isNoBuildModelSet()) {
model = buildModel<DdType, ValueType>(engine, input, ioSettings);
model = buildModel<DdType, BuildValueType>(engine, input, ioSettings);
}
if (model) {
@ -655,12 +659,12 @@ namespace storm {
STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model.");
if (model) {
auto preprocessingResult = preprocessModel<DdType, ValueType>(model, input);
auto preprocessingResult = preprocessModel<DdType, BuildValueType, VerificationValueType>(model, input);
if (preprocessingResult.second) {
model = preprocessingResult.first;
model->printModelInformationToStream(std::cout);
}
exportModel<DdType, ValueType>(model, input);
exportModel<DdType, BuildValueType>(model, input);
}
return model;
}
@ -678,17 +682,9 @@ namespace storm {
} else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
verifyWithExplorationEngine<VerificationValueType>(input);
} else {
std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType>(input, engine);
std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
if (model) {
if (!std::is_same<BuildValueType, VerificationValueType>::value) {
if (model->isSymbolicModel()) {
STORM_LOG_INFO("Converting symbolic model value type to fit the verification value type.");
auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, BuildValueType>>();
model = symbolicModel->template toValueType<VerificationValueType>();
}
}
if (coreSettings.isCounterexampleSet()) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
generateCounterexamples<VerificationValueType>(model, input);
@ -713,7 +709,7 @@ namespace storm {
STORM_LOG_INFO("Switching to DD library sylvan to allow for rational arithmetic.");
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber, double>(input);
} else if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);
processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, double>(input);
} else {
STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library.");
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, ValueType>(input);

10
src/storm/api/bisimulation.h
View File

@ -55,8 +55,8 @@ 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, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
typename std::enable_if<DdType == storm::dd::DdType::Sylvan || std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::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) || model->isOfType(storm::models::ModelType::Mdp) || model->isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs, CTMCs, MDPs and MAs.");
STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported.");
@ -64,13 +64,13 @@ namespace storm {
// Try to get rid of non state-rewards to easy bisimulation computation.
model->reduceToStateBasedRewards();
storm::dd::BisimulationDecomposition<DdType, ValueType> decomposition(*model, formulas, bisimulationType);
storm::dd::BisimulationDecomposition<DdType, ValueType, ExportValueType> 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, storm::storage::BisimulationType const& bisimulationType = storm::storage::BisimulationType::Strong, storm::dd::bisimulation::SignatureMode const& mode = storm::dd::bisimulation::SignatureMode::Eager) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
typename std::enable_if<DdType != storm::dd::DdType::Sylvan && !std::is_same<ValueType, double>::value, std::shared_ptr<storm::models::Model<ExportValueType>>>::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;
}

4
src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h
View File

@ -11,7 +11,7 @@ namespace storm {
}
namespace dd {
template<storm::dd::DdType DdType, typename ValueType>
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
class BisimulationDecomposition;
}
@ -47,7 +47,7 @@ namespace storm {
ModelType const& model;
/// The bisimulation object that maintains and refines the model.
std::unique_ptr<storm::dd::BisimulationDecomposition<DdType, ValueType>> bisimulation;
std::unique_ptr<storm::dd::BisimulationDecomposition<DdType, ValueType, ValueType>> bisimulation;
/// Maintains the last abstract model that was returned.
std::shared_ptr<storm::models::Model<ValueType>> lastAbstractModel;

36
src/storm/models/symbolic/Model.cpp
View File

@ -6,6 +6,7 @@
#include "storm/models/symbolic/Ctmc.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/MarkovAutomaton.h"
#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/exceptions/InvalidOperationException.h"
@ -384,7 +385,9 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType>
template<typename NewValueType>
std::shared_ptr<Model<Type, NewValueType>> Model<Type, ValueType>::toValueType() const {
typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType() const {
STORM_LOG_TRACE("Converting value type of symbolic model from " << typeid(ValueType).name() << " to " << typeid(NewValueType).name() << ".");
// Make a huge branching here as we cannot make a templated function virtual.
if (this->getType() == storm::models::ModelType::Dtmc) {
return this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>()->template toValueType<NewValueType>();
@ -394,6 +397,28 @@ namespace storm {
return this->template as<storm::models::symbolic::Mdp<Type, ValueType>>()->template toValueType<NewValueType>();
} else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
return this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>()->template toValueType<NewValueType>();
} else if (this->getType() == storm::models::ModelType::S2pg) {
return this->template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>()->template toValueType<NewValueType>();
}
STORM_LOG_WARN("Could not convert value type of model.");
return nullptr;
}
template<storm::dd::DdType Type, typename ValueType>
template<typename NewValueType>
typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type Model<Type, ValueType>::toValueType() const {
// Make a huge branching here as we cannot make a templated function virtual.
if (this->getType() == storm::models::ModelType::Dtmc) {
return std::make_shared<storm::models::symbolic::Dtmc<Type, ValueType>>(*this->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
} else if (this->getType() == storm::models::ModelType::Ctmc) {
return std::make_shared<storm::models::symbolic::Ctmc<Type, ValueType>>(*this->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
} else if (this->getType() == storm::models::ModelType::Mdp) {
return std::make_shared<storm::models::symbolic::Mdp<Type, ValueType>>(*this->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
} else if (this->getType() == storm::models::ModelType::MarkovAutomaton) {
return std::make_shared<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>(*this->template as<storm::models::symbolic::MarkovAutomaton<Type, ValueType>>());
} else if (this->getType() == storm::models::ModelType::S2pg) {
return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>(*this->template as<storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>>());
}
STORM_LOG_WARN("Could not convert value type of model.");
@ -403,9 +428,14 @@ namespace storm {
// Explicitly instantiate the template class.
template class Model<storm::dd::DdType::CUDD, double>;
template class Model<storm::dd::DdType::Sylvan, double>;
template typename std::enable_if<std::is_same<double, double>::value, std::shared_ptr<Model<storm::dd::DdType::CUDD, double>>>::type Model<storm::dd::DdType::CUDD, double>::toValueType<double>() const;
template class Model<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>> Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType() const;
template typename std::enable_if<std::is_same<double, double>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>>>::type Model<storm::dd::DdType::Sylvan, double>::toValueType<double>() const;
template typename std::enable_if<std::is_same<storm::RationalNumber, storm::RationalNumber>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, storm::RationalNumber>>>::type Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
template typename std::enable_if<std::is_same<storm::RationalFunction, storm::RationalFunction>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, storm::RationalFunction>>>::type Model<storm::dd::DdType::Sylvan, storm::RationalFunction>::toValueType<storm::RationalFunction>() const;
template typename std::enable_if<!std::is_same<storm::RationalNumber, double>::value, std::shared_ptr<Model<storm::dd::DdType::Sylvan, double>>>::type Model<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<double>() const;
template class Model<storm::dd::DdType::Sylvan, storm::RationalFunction>;
} // namespace symbolic
} // namespace models

5
src/storm/models/symbolic/Model.h
View File

@ -328,8 +328,11 @@ namespace storm {
std::set<storm::RationalFunctionVariable> const& getParameters() const;
template<typename NewValueType>
std::shared_ptr<Model<Type, NewValueType>> toValueType() const;
typename std::enable_if<!std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
template<typename NewValueType>
typename std::enable_if<std::is_same<ValueType, NewValueType>::value, std::shared_ptr<Model<Type, NewValueType>>>::type toValueType() const;
protected:
/*!
* Sets the transition matrix of the model.

19
src/storm/models/symbolic/StochasticTwoPlayerGame.cpp
View File

@ -82,11 +82,30 @@ namespace storm {
return player2Variables;
}
template<storm::dd::DdType Type, typename ValueType>
template<typename NewValueType>
std::shared_ptr<StochasticTwoPlayerGame<Type, NewValueType>> StochasticTwoPlayerGame<Type, ValueType>::toValueType() const {
typedef typename NondeterministicModel<Type, NewValueType>::RewardModelType NewRewardModelType;
std::unordered_map<std::string, NewRewardModelType> newRewardModels;
for (auto const& e : this->getRewardModels()) {
newRewardModels.emplace(e.first, e.second.template toValueType<NewValueType>());
}
auto newLabelToBddMap = this->getLabelToBddMap();
newLabelToBddMap.erase("init");
newLabelToBddMap.erase("deadlock");
return std::make_shared<StochasticTwoPlayerGame<Type, NewValueType>>(this->getManagerAsSharedPointer(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), this->getTransitionMatrix().template toValueType<NewValueType>(), this->getRowVariables(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), this->getPlayer1Variables(), this->getPlayer2Variables(), this->getNondeterminismVariables(), newLabelToBddMap, newRewardModels);
}
// Explicitly instantiate the template class.
template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>;
template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>;
#ifdef STORM_HAVE_CARL
template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template std::shared_ptr<StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>> StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<double>() const;
template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#endif

3
src/storm/models/symbolic/StochasticTwoPlayerGame.h
View File

@ -117,6 +117,9 @@ namespace storm {
*/
storm::dd::Bdd<Type> getIllegalPlayer2Mask() const;
template<typename NewValueType>
std::shared_ptr<StochasticTwoPlayerGame<Type, NewValueType>> toValueType() const;
private:
/*!
* Prepare all illegal masks.

51
src/storm/storage/dd/BisimulationDecomposition.cpp
View File

@ -31,31 +31,31 @@ namespace storm {
}
}
template <storm::dd::DdType DdType, typename ValueType>
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
this->initialize();
}
template <storm::dd::DdType DdType, typename ValueType>
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
this->initialize();
}
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, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, formulas))) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
BisimulationDecomposition<DdType, ValueType, ExportValueType>::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) : model(model), preservationInformation(model, formulas), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, formulas))) {
this->initialize();
}
template <storm::dd::DdType DdType, typename ValueType>
BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
BisimulationDecomposition<DdType, ValueType, ExportValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
this->initialize();
}
template <storm::dd::DdType DdType, typename ValueType>
BisimulationDecomposition<DdType, ValueType>::~BisimulationDecomposition() = default;
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
BisimulationDecomposition<DdType, ValueType, ExportValueType>::~BisimulationDecomposition() = default;
template <storm::dd::DdType DdType, typename ValueType>
void BisimulationDecomposition<DdType, ValueType>::initialize() {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
void BisimulationDecomposition<DdType, ValueType, ExportValueType>::initialize() {
auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
verboseProgress = generalSettings.isVerboseSet();
showProgressDelay = generalSettings.getShowProgressDelay();
@ -69,8 +69,8 @@ namespace storm {
STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
}
template <storm::dd::DdType DdType, typename ValueType>
void BisimulationDecomposition<DdType, ValueType>::compute(bisimulation::SignatureMode const& mode) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
void BisimulationDecomposition<DdType, ValueType, ExportValueType>::compute(bisimulation::SignatureMode const& mode) {
STORM_LOG_ASSERT(refiner, "No suitable refiner.");
STORM_LOG_ASSERT(this->refiner->getStatus() != Status::FixedPoint, "Can only proceed if no fixpoint has been reached yet.");
@ -96,8 +96,8 @@ namespace storm {
STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations, signature: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalRefinementTime()).count() << "ms).");
}
template <storm::dd::DdType DdType, typename ValueType>
bool BisimulationDecomposition<DdType, ValueType>::compute(uint64_t steps, bisimulation::SignatureMode const& mode) {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
bool BisimulationDecomposition<DdType, ValueType, ExportValueType>::compute(uint64_t steps, bisimulation::SignatureMode const& mode) {
STORM_LOG_ASSERT(refiner, "No suitable refiner.");
STORM_LOG_ASSERT(this->refiner->getStatus() != Status::FixedPoint, "Can only proceed if no fixpoint has been reached yet.");
STORM_LOG_ASSERT(steps > 0, "Can only perform positive number of steps.");
@ -123,24 +123,24 @@ namespace storm {
return !refined;
}
template <storm::dd::DdType DdType, typename ValueType>
bool BisimulationDecomposition<DdType, ValueType>::getReachedFixedPoint() const {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
bool BisimulationDecomposition<DdType, ValueType, ExportValueType>::getReachedFixedPoint() const {
return this->refiner->getStatus() == Status::FixedPoint;
}
template <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
std::shared_ptr<storm::models::Model<ValueType>> quotient;
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::Model<ExportValueType>> BisimulationDecomposition<DdType, ValueType, ExportValueType>::getQuotient() const {
std::shared_ptr<storm::models::Model<ExportValueType>> quotient;
if (this->refiner->getStatus() == Status::FixedPoint) {
STORM_LOG_INFO("Starting full quotient extraction.");
QuotientExtractor<DdType, ValueType> extractor;
QuotientExtractor<DdType, ValueType, ExportValueType> extractor;
quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
} else {
STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models.");
STORM_LOG_INFO("Starting partial quotient extraction.");
if (!partialQuotientExtractor) {
partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType>>(model);
partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType, ExportValueType>>(model);
}
quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
@ -150,8 +150,8 @@ namespace storm {
return quotient;
}
template <storm::dd::DdType DdType, typename ValueType>
void BisimulationDecomposition<DdType, ValueType>::refineWrtRewardModels() {
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
void BisimulationDecomposition<DdType, ValueType, ExportValueType>::refineWrtRewardModels() {
for (auto const& rewardModelName : this->preservationInformation.getRewardModelNames()) {
auto const& rewardModel = this->model.getRewardModel(rewardModelName);
refiner->refineWrtRewardModel(rewardModel);
@ -162,6 +162,7 @@ namespace storm {
template class BisimulationDecomposition<storm::dd::DdType::Sylvan, double>;
template class BisimulationDecomposition<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template class BisimulationDecomposition<storm::dd::DdType::Sylvan, storm::RationalNumber, double>;
template class BisimulationDecomposition<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}

8
src/storm/storage/dd/BisimulationDecomposition.h
View File

@ -29,11 +29,11 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
class PartitionRefiner;
template <storm::dd::DdType DdType, typename ValueType>
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
class PartialQuotientExtractor;
}
template <storm::dd::DdType DdType, typename ValueType>
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class BisimulationDecomposition {
public:
BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType);
@ -64,7 +64,7 @@ namespace storm {
/*!
* Retrieves the quotient model after the bisimulation decomposition was computed.
*/
std::shared_ptr<storm::models::Model<ValueType>> getQuotient() const;
std::shared_ptr<storm::models::Model<ExportValueType>> getQuotient() const;
private:
void initialize();
@ -80,7 +80,7 @@ namespace storm {
std::unique_ptr<bisimulation::PartitionRefiner<DdType, ValueType>> refiner;
// A quotient extractor that is used when the fixpoint has not been reached yet.
mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType>> partialQuotientExtractor;
mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType, ExportValueType>> partialQuotientExtractor;
// A flag indicating whether progress is reported.
bool verboseProgress;

22
src/storm/storage/dd/bisimulation/PartialQuotientExtractor.cpp
View File

@ -15,18 +15,18 @@ namespace storm {
namespace dd {
namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType>
PartialQuotientExtractor<DdType, ValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
PartialQuotientExtractor<DdType, ValueType, ExportValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) {
auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
this->quotientFormat = settings.getQuotientFormat();
STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> PartialQuotientExtractor<DdType, ValueType>::extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::Model<ExportValueType>> PartialQuotientExtractor<DdType, ValueType, ExportValueType>::extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto start = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::Model<ValueType>> result;
std::shared_ptr<storm::models::Model<ExportValueType>> result;
STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
result = extractDdQuotient(partition, preservationInformation);
@ -38,8 +38,8 @@ namespace storm {
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> PartialQuotientExtractor<DdType, ValueType>::extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> PartialQuotientExtractor<DdType, ValueType, ExportValueType>::extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto modelType = model.getType();
if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp) {
@ -122,16 +122,19 @@ namespace storm {
end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
if (modelType == storm::models::ModelType::Dtmc) {
return std::make_shared<storm::models::symbolic::Mdp<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), preservedLabelBdds, quotientRewardModels);
result = std::make_shared<storm::models::symbolic::Mdp<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), preservedLabelBdds, quotientRewardModels);
} else if (modelType == storm::models::ModelType::Mdp) {
std::set<storm::expressions::Variable> allNondeterminismVariables;
std::set_union(model.getRowVariables().begin(), model.getRowVariables().end(), model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end(), std::inserter(allNondeterminismVariables, allNondeterminismVariables.begin()));
return std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), model.getNondeterminismVariables(), allNondeterminismVariables, preservedLabelBdds, quotientRewardModels);
result = std::make_shared<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getRowVariables(), model.getNondeterminismVariables(), allNondeterminismVariables, preservedLabelBdds, quotientRewardModels);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type.");
}
return result->template toValueType<ExportValueType>();
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract partial quotient for this model type.");
}
@ -142,6 +145,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber, double>;
template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#endif

6
src/storm/storage/dd/bisimulation/PartialQuotientExtractor.h
View File

@ -16,15 +16,15 @@ namespace storm {
namespace dd {
namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType>
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class PartialQuotientExtractor {
public:
PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model);
std::shared_ptr<storm::models::Model<ValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::Model<ExportValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
private:
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
// The model for which to compute the partial quotient.
storm::models::symbolic::Model<DdType, ValueType> const& model;

119
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -222,10 +222,10 @@ namespace storm {
spp::sparse_hash_map<BDD, bool> visitedNodes;
};
template<storm::dd::DdType DdType, typename ValueType>
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class InternalSparseQuotientExtractor;
template<storm::dd::DdType DdType, typename ValueType>
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class InternalSparseQuotientExtractorBase {
public:
InternalSparseQuotientExtractorBase(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Bdd<DdType> const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd<DdType> const& representatives) : model(model), manager(model.getManager()), isNondeterministic(false), partitionBdd(partitionBdd), numberOfBlocks(numberOfBlocks), blockVariable(blockVariable), representatives(representatives), matrixEntriesCreated(false) {
@ -259,23 +259,23 @@ namespace storm {
virtual ~InternalSparseQuotientExtractorBase() = default;
storm::storage::SparseMatrix<ValueType> extractTransitionMatrix(storm::dd::Add<DdType, ValueType> const& transitionMatrix) {
storm::storage::SparseMatrix<ExportValueType> extractTransitionMatrix(storm::dd::Add<DdType, ValueType> const& transitionMatrix) {
return extractMatrixInternal(transitionMatrix);
}
std::vector<ValueType> extractStateVector(storm::dd::Add<DdType, ValueType> const& vector) {
std::vector<ExportValueType> extractStateVector(storm::dd::Add<DdType, ValueType> const& vector) {
return extractVectorInternal(vector, this->rowVariablesCube, this->odd);
}
std::vector<ValueType> extractStateActionVector(storm::dd::Add<DdType, ValueType> const& vector) {
std::vector<ExportValueType> extractStateActionVector(storm::dd::Add<DdType, ValueType> const& vector) {
if (!this->isNondeterministic) {
return extractStateVector(vector);
} else {
STORM_LOG_ASSERT(!this->rowPermutation.empty(), "Expected proper row permutation.");
std::vector<ValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd);
std::vector<ExportValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd);
// Reorder the values according to the known row permutation.
std::vector<ValueType> reorderedValues(valueVector.size());
std::vector<ExportValueType> reorderedValues(valueVector.size());
for (uint64_t pos = 0; pos < valueVector.size(); ++pos) {
reorderedValues[pos] = valueVector[rowPermutation[pos]];
}
@ -292,14 +292,14 @@ namespace storm {
}
protected:
virtual storm::storage::SparseMatrix<ValueType> extractMatrixInternal(storm::dd::Add<DdType, ValueType> const& matrix) = 0;
virtual storm::storage::SparseMatrix<ExportValueType> extractMatrixInternal(storm::dd::Add<DdType, ValueType> const& matrix) = 0;
virtual std::vector<ValueType> extractVectorInternal(storm::dd::Add<DdType, ValueType> const& vector, storm::dd::Bdd<DdType> const& variablesCube, storm::dd::Odd const& odd) = 0;
virtual std::vector<ExportValueType> extractVectorInternal(storm::dd::Add<DdType, ValueType> const& vector, storm::dd::Bdd<DdType> const& variablesCube, storm::dd::Odd const& odd) = 0;
storm::storage::SparseMatrix<ValueType> createMatrixFromEntries() {
storm::storage::SparseMatrix<ExportValueType> createMatrixFromEntries() {
for (auto& row : matrixEntries) {
std::sort(row.begin(), row.end(),
[] (storm::storage::MatrixEntry<uint_fast64_t, ValueType> const& a, storm::storage::MatrixEntry<uint_fast64_t, ValueType> const& b) {
[] (storm::storage::MatrixEntry<uint_fast64_t, ExportValueType> const& a, storm::storage::MatrixEntry<uint_fast64_t, ExportValueType> const& b) {
return a.getColumn() < b.getColumn();
});
}
@ -312,7 +312,7 @@ namespace storm {
uint64_t rowCounter = 0;
uint64_t lastState = this->isNondeterministic ? rowToState[rowPermutation.front()] : 0;
storm::storage::SparseMatrixBuilder<ValueType> builder(matrixEntries.size(), this->numberOfBlocks, 0, true, this->isNondeterministic);
storm::storage::SparseMatrixBuilder<ExportValueType> builder(matrixEntries.size(), this->numberOfBlocks, 0, true, this->isNondeterministic);
if (this->isNondeterministic) {
builder.newRowGroup(0);
}
@ -343,7 +343,7 @@ namespace storm {
return builder.build();
}
void addMatrixEntry(uint64_t row, uint64_t column, ValueType const& value) {
void addMatrixEntry(uint64_t row, uint64_t column, ExportValueType const& value) {
this->matrixEntries[row].emplace_back(column, value);
}
@ -390,7 +390,7 @@ namespace storm {
bool matrixEntriesCreated;
// The entries of the quotient matrix that is built.
std::vector<std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>> matrixEntries;
std::vector<std::vector<storm::storage::MatrixEntry<uint_fast64_t, ExportValueType>>> matrixEntries;
// A vector storing for each row which state it belongs to.
std::vector<uint64_t> rowToState;
@ -621,33 +621,33 @@ namespace storm {
spp::sparse_hash_map<DdNode const*, uint64_t> blockToOffset;
};
template<typename ValueType>
class InternalSparseQuotientExtractor<storm::dd::DdType::Sylvan, ValueType> : public InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType> {
template<typename ValueType, typename ExportValueType>
class InternalSparseQuotientExtractor<storm::dd::DdType::Sylvan, ValueType, ExportValueType> : public InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType, ExportValueType> {
public:
InternalSparseQuotientExtractor(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, ValueType> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& representatives) : InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType>(model, partitionBdd, blockVariable, numberOfBlocks, representatives) {
InternalSparseQuotientExtractor(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, ValueType> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& partitionBdd, storm::expressions::Variable const& blockVariable, uint64_t numberOfBlocks, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& representatives) : InternalSparseQuotientExtractorBase<storm::dd::DdType::Sylvan, ValueType, ExportValueType>(model, partitionBdd, blockVariable, numberOfBlocks, representatives) {
this->createBlockToOffsetMapping();
}
private:
virtual storm::storage::SparseMatrix<ValueType> extractMatrixInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& matrix) override {
virtual storm::storage::SparseMatrix<ExportValueType> extractMatrixInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& matrix) override {
this->createMatrixEntryStorage();
extractTransitionMatrixRec(matrix.getInternalAdd().getSylvanMtbdd().GetMTBDD(), this->isNondeterministic ? this->nondeterminismOdd : this->odd, 0, this->partitionBdd.getInternalBdd().getSylvanBdd().GetBDD(), this->representatives.getInternalBdd().getSylvanBdd().GetBDD(), this->allSourceVariablesCube.getInternalBdd().getSylvanBdd().GetBDD(), this->nondeterminismVariablesCube.getInternalBdd().getSylvanBdd().GetBDD(), this->isNondeterministic ? &this->odd : nullptr, 0);
return this->createMatrixFromEntries();
}
virtual std::vector<ValueType> extractVectorInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& vector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& variablesCube, storm::dd::Odd const& odd) override {
std::vector<ValueType> result(odd.getTotalOffset());
virtual std::vector<ExportValueType> extractVectorInternal(storm::dd::Add<storm::dd::DdType::Sylvan, ValueType> const& vector, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& variablesCube, storm::dd::Odd const& odd) override {
std::vector<ExportValueType> result(odd.getTotalOffset());
extractVectorRec(vector.getInternalAdd().getSylvanMtbdd().GetMTBDD(), this->representatives.getInternalBdd().getSylvanBdd().GetBDD(), variablesCube.getInternalBdd().getSylvanBdd().GetBDD(), odd, 0, result);
return result;
}
void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector<ValueType>& result) {
void extractVectorRec(MTBDD vector, BDD representativesNode, BDD variables, storm::dd::Odd const& odd, uint64_t offset, std::vector<ExportValueType>& result) {
if (representativesNode == sylvan_false || mtbdd_iszero(vector)) {
return;
}
if (sylvan_isconst(variables)) {
result[offset] = storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(vector);
result[offset] = storm::utility::convertNumber<ExportValueType>(storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(vector));
} else {
MTBDD vectorT;
MTBDD vectorE;
@ -723,7 +723,7 @@ namespace storm {
// If we have moved through all source variables, we must have arrived at a target block encoding.
if (sylvan_isconst(variables)) {
STORM_LOG_ASSERT(mtbdd_isleaf(transitionMatrixNode), "Expected constant node.");
this->addMatrixEntry(sourceOffset, blockToOffset.at(targetPartitionNode), storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode));
this->addMatrixEntry(sourceOffset, blockToOffset.at(targetPartitionNode), storm::utility::convertNumber<ExportValueType>(storm::dd::InternalAdd<storm::dd::DdType::Sylvan, ValueType>::getValue(transitionMatrixNode)));
if (stateOdd) {
this->assignRowToState(sourceOffset, stateOffset);
}
@ -817,18 +817,18 @@ namespace storm {
spp::sparse_hash_map<BDD, uint64_t> blockToOffset;
};
template<storm::dd::DdType DdType, typename ValueType>
QuotientExtractor<DdType, ValueType>::QuotientExtractor() : useRepresentatives(false) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
QuotientExtractor<DdType, ValueType, ExportValueType>::QuotientExtractor() : useRepresentatives(false) {
auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
this->useRepresentatives = settings.isUseRepresentativesSet();
this->useOriginalVariables = settings.isUseOriginalVariablesSet();
this->quotientFormat = settings.getQuotientFormat();
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> QuotientExtractor<DdType, ValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::Model<ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto start = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::Model<ValueType>> result;
std::shared_ptr<storm::models::Model<ExportValueType>> result;
if (quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Sparse) {
result = extractSparseQuotient(model, partition, preservationInformation);
} else {
@ -842,8 +842,8 @@ namespace storm {
return result;
}
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, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::sparse::Model<ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs());
storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd();
@ -853,8 +853,8 @@ namespace storm {
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
STORM_LOG_ASSERT(representatives.getNonZeroCount() == partition.getNumberOfBlocks(), "Representatives size does not match that of the partition: " << representatives.getNonZeroCount() << " vs. " << partition.getNumberOfBlocks() << ".");
STORM_LOG_ASSERT((representatives && partitionAsBdd).existsAbstract(model.getRowVariables()) == partitionAsBdd.existsAbstract(model.getRowVariables()), "Representatives do not cover all blocks.");
InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives);
storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
InternalSparseQuotientExtractor<DdType, ValueType, ExportValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives);
storm::storage::SparseMatrix<ExportValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
@ -881,47 +881,47 @@ namespace storm {
STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
start = std::chrono::high_resolution_clock::now();
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> quotientRewardModels;
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ExportValueType>> quotientRewardModels;
for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) {
auto const& rewardModel = model.getRewardModel(rewardModelName);
boost::optional<std::vector<ValueType>> quotientStateRewards;
boost::optional<std::vector<ExportValueType>> quotientStateRewards;
if (rewardModel.hasStateRewards()) {
quotientStateRewards = sparseExtractor.extractStateVector(rewardModel.getStateRewardVector());
}
boost::optional<std::vector<ValueType>> quotientStateActionRewards;
boost::optional<std::vector<ExportValueType>> quotientStateActionRewards;
if (rewardModel.hasStateActionRewards()) {
quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector());
}
quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ExportValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
}
end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
std::shared_ptr<storm::models::sparse::Model<ExportValueType>> result;
if (model.getType() == storm::models::ModelType::Dtmc) {
result = std::make_shared<storm::models::sparse::Dtmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
result = std::make_shared<storm::models::sparse::Dtmc<ExportValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
} else if (model.getType() == storm::models::ModelType::Ctmc) {
result = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
result = std::make_shared<storm::models::sparse::Ctmc<ExportValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
} else if (model.getType() == storm::models::ModelType::Mdp) {
result = std::make_shared<storm::models::sparse::Mdp<ValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
result = std::make_shared<storm::models::sparse::Mdp<ExportValueType>>(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels));
} else if (model.getType() == storm::models::ModelType::MarkovAutomaton) {
storm::models::symbolic::MarkovAutomaton<DdType, ValueType> const& markovAutomaton = *model.template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>();
boost::optional<storm::storage::BitVector> markovianStates = sparseExtractor.extractSetExists(markovAutomaton.getMarkovianStates());
storm::storage::sparse::ModelComponents<ValueType> modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates));
storm::storage::sparse::ModelComponents<ExportValueType> modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates));
modelComponents.exitRates = sparseExtractor.extractStateVector(markovAutomaton.getExitRateVector());
result = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(modelComponents));
result = std::make_shared<storm::models::sparse::MarkovAutomaton<ExportValueType>>(std::move(modelComponents));
}
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
if (this->useOriginalVariables) {
return extractQuotientUsingOriginalVariables(model, partition, preservationInformation);
@ -930,8 +930,8 @@ namespace storm {
}
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto modelType = model.getType();
bool useRepresentativesForThisExtraction = this->useRepresentatives;
@ -1028,22 +1028,25 @@ namespace storm {
end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Ctmc) {
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Mdp) {
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
} else {
return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
}
return result->template toValueType<ExportValueType>();
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
}
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> QuotientExtractor<DdType, ValueType, ExportValueType>::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto modelType = model.getType();
bool useRepresentativesForThisExtraction = this->useRepresentatives;
@ -1146,15 +1149,18 @@ namespace storm {
end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> result;
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Ctmc) {
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Mdp) {
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
} else {
return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
result = std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
}
return result->template toValueType<ExportValueType>();
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
}
@ -1164,6 +1170,7 @@ namespace storm {
template class QuotientExtractor<storm::dd::DdType::Sylvan, double>;
template class QuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber>;
template class QuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber, double>;
template class QuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
}

12
src/storm/storage/dd/bisimulation/QuotientExtractor.h
View File

@ -16,19 +16,19 @@ namespace storm {
namespace dd {
namespace bisimulation {
template<storm::dd::DdType DdType, typename ValueType>
template <storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class QuotientExtractor {
public:
QuotientExtractor();
std::shared_ptr<storm::models::Model<ValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::Model<ExportValueType>> extract(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
private:
std::shared_ptr<storm::models::sparse::Model<ValueType>> extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::sparse::Model<ExportValueType>> extractSparseQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
bool useRepresentatives;
bool useOriginalVariables;

Write Preview
Loading…
Cancel
Save