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

enable representatives in quotient extraction also for MDP/MA

tempestpy_adaptions
dehnert 7 years ago
parent
66e08f9cd7
commit
d6f2261ca9
3 changed files with 74 additions and 13 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. 40
      src/storm/storage/dd/Bdd.cpp
  2. 13
      src/storm/storage/dd/Bdd.h
  3. 34
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

40
src/storm/storage/dd/Bdd.cpp
View File

@ -359,6 +359,46 @@ namespace storm {
}
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::renameVariablesConcretize(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const {
std::vector<InternalBdd<LibraryType>> fromBdds;
std::vector<InternalBdd<LibraryType>> toBdds;
for (auto const& metaVariable : from) {
STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
fromBdds.push_back(ddVariable.getInternalBdd());
}
}
std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
for (auto const& metaVariable : to) {
STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
toBdds.push_back(ddVariable.getInternalBdd());
}
}
std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
std::set<storm::expressions::Variable> newContainedMetaVariables = to;
std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin()));
STORM_LOG_ASSERT(toBdds.size() >= fromBdds.size(), "Unable to perform rename-concretize with mismatching sizes.");
if (fromBdds.size() == toBdds.size()) {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
} else {
InternalBdd<LibraryType> negatedCube = this->getDdManager().getBddOne().getInternalBdd();
for (uint64_t index = fromBdds.size(); index < toBdds.size(); ++index) {
negatedCube &= !toBdds[index];
}
toBdds.resize(fromBdds.size());
return Bdd<LibraryType>(this->getDdManager(), (internalBdd && negatedCube).swapVariables(fromBdds, toBdds), newContainedMetaVariables);
}
}
template<DdType LibraryType>
template<typename ValueType>
Add<LibraryType, ValueType> Bdd<LibraryType>::toAdd() const {

13
src/storm/storage/dd/Bdd.h
View File

@ -298,6 +298,19 @@ namespace storm {
*/
Bdd<LibraryType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
/*!
* Renames the given meta variables in the BDD. The number of the underlying DD variables of the from meta
* variable set needs to be at most as large as the to meta variable set. If the amount of variables coincide,
* this operation coincides with renameVariables. Otherwise, it first adds a unique encoding in terms of the
* superfluous variables and then performs the renaming.
*
* @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables.
* @param to The meta variables that are the target of the renaming process. The current ADD must not contain
* any of these meta variables.
* @return The resulting ADD.
*/
Bdd<LibraryType> renameVariablesConcretize(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
/*!
* Retrieves whether this DD represents the constant one function.
*

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

@ -936,10 +936,6 @@ namespace storm {
bool useRepresentativesForThisExtraction = this->useRepresentatives;
if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) {
if (modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) {
STORM_LOG_WARN_COND(!useRepresentativesForThisExtraction, "Using representatives is unsupported for MDPs, falling back to regular extraction.");
useRepresentativesForThisExtraction = false;
}
// Sanity checks.
STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size.");
@ -948,16 +944,20 @@ namespace storm {
std::set<storm::expressions::Variable> blockVariableSet = {partition.getBlockVariable()};
std::set<storm::expressions::Variable> blockPrimeVariableSet = {partition.getPrimedBlockVariable()};
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())};
auto start = std::chrono::high_resolution_clock::now();
// Compute representatives.
storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero();
partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
if (useRepresentativesForThisExtraction) {
storm::dd::Bdd<DdType> partitionAsBddOverPrimedBlockVariable = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet);
storm::dd::Bdd<DdType> representativePartition = partitionAsBddOverPrimedBlockVariable.existsAbstractRepresentative(model.getColumnVariables()).renameVariables(model.getColumnVariables(), blockVariableSet);
partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet);
storm::dd::Bdd<DdType> partitionAsBddOverPrimedBlockVariables = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet);
storm::dd::Bdd<DdType> tmp = (representatives && partitionAsBddOverPrimedBlockVariables).renameVariablesConcretize(model.getRowVariables(), blockVariableSet);
partitionAsBdd = (tmp && partitionAsBddOverPrimedBlockVariables).existsAbstract(blockPrimeVariableSet);
}
auto start = std::chrono::high_resolution_clock::now();
partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables());
@ -989,7 +989,6 @@ namespace storm {
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables());
// Pick a representative from each block.
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
partitionAsBdd &= representatives;
partitionAsAdd *= partitionAsBdd.template toAdd<ValueType>();
@ -1047,6 +1046,7 @@ namespace storm {
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) {
auto modelType = model.getType();
bool useRepresentativesForThisExtraction = this->useRepresentatives;
if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) {
STORM_LOG_WARN_COND(!this->useRepresentatives, "Using representatives is unsupported for this extraction, falling back to regular extraction.");
@ -1058,10 +1058,19 @@ namespace storm {
std::set<storm::expressions::Variable> blockPrimeVariableSet = {partition.getPrimedBlockVariable()};
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())};
storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero();
auto start = std::chrono::high_resolution_clock::now();
// Compute representatives.
storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero();
partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
if (useRepresentativesForThisExtraction) {
storm::dd::Bdd<DdType> partitionAsBddOverPrimedBlockVariables = partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet);
storm::dd::Bdd<DdType> tmp = (representatives && partitionAsBddOverPrimedBlockVariables).renameVariablesConcretize(model.getRowVariables(), blockVariableSet);
partitionAsBdd = (tmp && partitionAsBddOverPrimedBlockVariables).existsAbstract(blockPrimeVariableSet);
}
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
@ -1093,7 +1102,6 @@ namespace storm {
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()).renameVariablesAbstract(blockVariableSet, model.getColumnVariables());
// Pick a representative from each block.
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
partitionAsBdd &= representatives;
partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();

Write Preview
Loading…
Cancel
Save