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

Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster. 

Former-commit-id: 07ffb5882d
tempestpy_adaptions
dehnert 10 years ago
parent
e79233bd7b
commit
706ea56963
17 changed files with 777 additions and 309 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. 4
      src/adapters/DdExpressionAdapter.cpp
  2. 87
      src/builder/DdPrismModelBuilder.cpp
  3. 19
      src/builder/DdPrismModelBuilder.h
  4. 20
      src/settings/modules/GeneralSettings.cpp
  5. 12
      src/settings/modules/GeneralSettings.h
  6. 589
      src/storage/dd/CuddDd.cpp
  7. 116
      src/storage/dd/CuddDd.h
  8. 26
      src/storage/dd/CuddDdForwardIterator.cpp
  9. 4
      src/storage/dd/CuddDdForwardIterator.h
  10. 64
      src/storage/dd/CuddDdManager.cpp
  11. 16
      src/storage/dd/CuddDdManager.h
  12. 15
      src/storage/dd/CuddDdMetaVariable.cpp
  13. 11
      src/storage/dd/CuddDdMetaVariable.h
  14. 12
      src/storage/dd/CuddOdd.cpp
  15. 7
      src/storage/dd/CuddOdd.h
  16. 34
      src/utility/cli.h
  17. 50
      test/functional/storage/CuddDdTest.cpp

4
src/adapters/DdExpressionAdapter.cpp
View File

@ -40,13 +40,13 @@ namespace storm {
result = leftResult || rightResult;
break;
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff:
result = leftResult.equals(rightResult);
result = leftResult.iff(rightResult);
break;
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies:
result = !leftResult || rightResult;
break;
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor:
result = (leftResult && !rightResult) || (!leftResult && rightResult);
result = leftResult.exclusiveOr(rightResult);
break;
}

87
src/builder/DdPrismModelBuilder.cpp
View File

@ -50,7 +50,7 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Update const& update) {
storm::dd::Dd<Type> updateDd = generationInfo.manager->getOne();
storm::dd::Dd<Type> updateDd = generationInfo.manager->getOne(true);
STORM_LOG_TRACE("Translating update " << update);
@ -77,7 +77,7 @@ namespace storm {
result *= guard;
// Restrict the transitions to the range of the written variable.
result = result * generationInfo.manager->getRange(primedMetaVariable);
result = result * generationInfo.manager->getRange(primedMetaVariable, true);
updateDd *= result;
}
@ -130,7 +130,7 @@ namespace storm {
STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable.");
if (!guardDd.isZero()) {
storm::dd::Dd<Type> commandDd = generationInfo.manager->getZero();
storm::dd::Dd<Type> commandDd = generationInfo.manager->getZero(true);
for (storm::prism::Update const& update : command.getUpdates()) {
storm::dd::Dd<Type> updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update);
@ -183,8 +183,8 @@ namespace storm {
template <storm::dd::DdType Type>
typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram> const& commandDds) {
storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero();
storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero();
storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero(true);
storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero(true);
storm::dd::Dd<Type> temporary;
for (auto const& commandDd : commandDds) {
@ -201,7 +201,7 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) {
storm::dd::Dd<Type> result = generationInfo.manager->getZero();
storm::dd::Dd<Type> result = generationInfo.manager->getZero(true);
STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << ".");
@ -220,11 +220,11 @@ namespace storm {
template <storm::dd::DdType Type>
typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram> const& commandDds, uint_fast64_t nondeterminismVariableOffset) {
storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero();
storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero();
storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero(true);
storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero(true);
// Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
storm::dd::Dd<Type> sumOfGuards = generationInfo.manager->getZero();
storm::dd::Dd<Type> sumOfGuards = generationInfo.manager->getZero(true);
for (auto const& commandDd : commandDds) {
sumOfGuards += commandDd.guardDd;
allGuards = allGuards || commandDd.guardDd;
@ -247,9 +247,9 @@ namespace storm {
// Calculate number of required variables to encode the nondeterminism.
uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
storm::dd::Dd<Type> equalsNumberOfChoicesDd = generationInfo.manager->getZero();
std::vector<storm::dd::Dd<Type>> choiceDds(maxChoices, generationInfo.manager->getZero());
std::vector<storm::dd::Dd<Type>> remainingDds(maxChoices, generationInfo.manager->getZero());
storm::dd::Dd<Type> equalsNumberOfChoicesDd = generationInfo.manager->getZero(true);
std::vector<storm::dd::Dd<Type>> choiceDds(maxChoices, generationInfo.manager->getZero(true));
std::vector<storm::dd::Dd<Type>> remainingDds(maxChoices, generationInfo.manager->getZero(true));
for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
// Determine the set of states with exactly currentChoices choices.
@ -262,7 +262,7 @@ namespace storm {
// Reset the previously used intermediate storage.
for (uint_fast64_t j = 0; j < currentChoices; ++j) {
choiceDds[j] = generationInfo.manager->getZero();
choiceDds[j] = generationInfo.manager->getZero(true);
remainingDds[j] = equalsNumberOfChoicesDd;
}
@ -335,23 +335,23 @@ namespace storm {
// Bring both choices to the same number of variables that encode the nondeterminism.
uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables);
if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) {
storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne(true);
for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) {
nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
}
action2Extended *= nondeterminisimEncoding;
} else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) {
storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne(true);
for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) {
nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
}
action1Extended *= nondeterminisimEncoding;
}
// Add a new variable that resolves the nondeterminism between the two choices.
storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended);
storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1, true).ite(action2Extended, action1Extended);
return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1);
} else {
@ -381,44 +381,44 @@ namespace storm {
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) {
// If the model is an MDP, we need to encode the nondeterminism using additional variables.
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
storm::dd::Dd<Type> result = generationInfo.manager->getZero();
storm::dd::Dd<Type> result = generationInfo.manager->getZero(true);
// First, determine the highest number of nondeterminism variables that is used in any action and make
// all actions use the same amout of nondeterminism variables.
uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables;
// Add variables to independent action DD.
storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne();
storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne(true);
for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
}
result = module.independentAction.transitionsDd * nondeterminismEncoding;
// Add variables to synchronized action DDs.
std::map<uint_fast64_t, storm::dd::Dd<Type>> synchronizingActionToDdMap;
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
nondeterminismEncoding = generationInfo.manager->getOne();
nondeterminismEncoding = generationInfo.manager->getOne(true);
for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
}
synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding);
}
// Add variables for synchronization.
storm::dd::Dd<Type> synchronization = generationInfo.manager->getOne();
storm::dd::Dd<Type> synchronization = generationInfo.manager->getOne(true);
for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0);
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true);
}
result *= synchronization;
for (auto& synchronizingAction : synchronizingActionToDdMap) {
synchronization = generationInfo.manager->getOne();
synchronization = generationInfo.manager->getOne(true);
for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
if (i == synchronizingAction.first) {
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1);
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1, true);
} else {
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0);
synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true);
}
}
@ -549,14 +549,24 @@ namespace storm {
// In particular, this creates the meta variables used to encode the model.
GenerationInformation generationInfo(preparedProgram);
auto clock = std::chrono::high_resolution_clock::now();
auto totalTimeStart = std::chrono::high_resolution_clock::now();
std::pair<storm::dd::Dd<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
auto totalTimeEnd = std::chrono::high_resolution_clock::now();
std::cout << "building matrix took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl;
storm::dd::Dd<Type> transitionMatrix = transitionMatrixModulePair.first;
ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
// Cut the transition matrix to the reachable fragment of the state space.
totalTimeStart = std::chrono::high_resolution_clock::now();
storm::dd::Dd<Type> reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix);
transitionMatrix *= reachableStates;
totalTimeEnd = std::chrono::high_resolution_clock::now();
std::cout << "reachability took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl;
totalTimeStart = std::chrono::high_resolution_clock::now();
transitionMatrix *= reachableStates.toMtbdd();
totalTimeEnd = std::chrono::high_resolution_clock::now();
std::cout << "cutting trans to reachable took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl;
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Dd<Type> statesWithTransition = transitionMatrix.notZero();
@ -564,7 +574,7 @@ namespace storm {
statesWithTransition = statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
}
statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables);
storm::dd::Dd<Type> deadlockStates = reachableStates * !statesWithTransition;
storm::dd::Dd<Type> deadlockStates = (reachableStates && !statesWithTransition).toMtbdd();
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
@ -577,7 +587,7 @@ namespace storm {
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
// For MDPs, however, we need to select an action associated with the self-loop, if we do not
// want to attach a lot of self-loops to the deadlock states.
storm::dd::Dd<Type> action = generationInfo.manager->getOne();
storm::dd::Dd<Type> action = generationInfo.manager->getOne(true);
std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->getIdentity(metaVariable); } );
transitionMatrix += deadlockStates * globalModule.identity * action;
}
@ -592,10 +602,10 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) {
storm::dd::Dd<Type> initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression());
storm::dd::Dd<Type> initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd();
for (auto const& metaVariable : generationInfo.rowMetaVariables) {
initialStates *= generationInfo.manager->getRange(metaVariable);
initialStates &= generationInfo.manager->getRange(metaVariable);
}
return initialStates;
@ -603,7 +613,7 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd<Type> const& initialStates, storm::dd::Dd<Type> const& transitions) {
storm::dd::Dd<Type> reachableStatesBdd = initialStates.notZero();
storm::dd::Dd<Type> reachableStatesBdd = initialStates.toBdd();
// If the model is an MDP, we can abstract from the variables encoding the nondeterminism in the model.
storm::dd::Dd<Type> transitionBdd = transitions.notZero();
@ -617,18 +627,17 @@ namespace storm {
do {
STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states.");
changed = false;
storm::dd::Dd<Type> tmp = reachableStatesBdd * transitionBdd;
tmp = tmp.existsAbstract(generationInfo.rowMetaVariables);
storm::dd::Dd<Type> tmp = reachableStatesBdd.andExists(transitionBdd, generationInfo.rowMetaVariables);
tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs);
storm::dd::Dd<Type> newReachableStates = tmp * (!reachableStatesBdd);
storm::dd::Dd<Type> newReachableStates = tmp && (!reachableStatesBdd);
// Check whether new states were indeed discovered.
if (!newReachableStates.isZero()) {
changed = true;
}
reachableStatesBdd += newReachableStates;
reachableStatesBdd |= newReachableStates;
++iteration;
} while (changed);

19
src/builder/DdPrismModelBuilder.h
View File

@ -68,7 +68,7 @@ namespace storm {
// Intentionally left empty.
}
ActionDecisionDiagram(storm::dd::DdManager<Type> const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero()), transitionsDd(manager.getZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) {
ActionDecisionDiagram(storm::dd::DdManager<Type> const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero(true)), transitionsDd(manager.getZero(true)), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) {
// Intentionally left empty.
}
@ -95,7 +95,7 @@ namespace storm {
// Intentionally left empty.
}
ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()), numberOfUsedNondeterminismVariables(0) {
ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero(true)), numberOfUsedNondeterminismVariables(0) {
// Intentionally left empty.
}
@ -209,7 +209,7 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
}
@ -230,8 +230,8 @@ namespace storm {
// Create meta variables for each of the modules' variables.
for (storm::prism::Module const& module : program.getModules()) {
storm::dd::Dd<Type> moduleIdentity = manager->getOne();
storm::dd::Dd<Type> moduleRange = manager->getOne();
storm::dd::Dd<Type> moduleIdentity = manager->getOne(true);
storm::dd::Dd<Type> moduleRange = manager->getOne(true);
for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) {
int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
@ -245,11 +245,10 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
variableIdentity.exportToDot(variablePair.first.getName() + "_ident.dot");
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
moduleIdentity *= variableIdentity;
moduleRange *= manager->getRange(variablePair.first);
moduleRange *= manager->getRange(variablePair.first, true);
rowColumnMetaVariablePairs.push_back(variablePair);
}
@ -263,10 +262,10 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
moduleIdentity *= variableIdentity;
moduleRange *= manager->getRange(variablePair.first);
moduleRange *= manager->getRange(variablePair.first, true);
rowColumnMetaVariablePairs.push_back(variablePair);
}

20
src/settings/modules/GeneralSettings.cpp
View File

@ -20,7 +20,7 @@ namespace storm {
const std::string GeneralSettings::configOptionName = "config";
const std::string GeneralSettings::configOptionShortName = "c";
const std::string GeneralSettings::explicitOptionName = "explicit";
const std::string GeneralSettings::explicitOptionShortName = "e";
const std::string GeneralSettings::explicitOptionShortName = "exp";
const std::string GeneralSettings::symbolicOptionName = "symbolic";
const std::string GeneralSettings::symbolicOptionShortName = "s";
const std::string GeneralSettings::propertyOptionName = "prop";
@ -41,6 +41,8 @@ namespace storm {
const std::string GeneralSettings::statisticsOptionShortName = "stats";
const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
const std::string GeneralSettings::engineOptionName = "engine";
const std::string GeneralSettings::engineOptionShortName = "e";
#ifdef STORM_HAVE_CARL
const std::string GeneralSettings::parametricOptionName = "parametric";
@ -76,6 +78,10 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
std::vector<std::string> engines = {"sparse", "dd"};
this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
@ -251,6 +257,16 @@ namespace storm {
return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
}
GeneralSettings::Engine GeneralSettings::getEngine() const {
std::string engine = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString();
if (engine == "sparse") {
return GeneralSettings::Engine::Sparse;
} else if (engine == "dd") {
return GeneralSettings::Engine::Dd;
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engine << "'.");
}
#ifdef STORM_HAVE_CARL
bool GeneralSettings::isParametricSet() const {
return this->getOption(parametricOptionName).getHasOptionBeenSet();
@ -265,6 +281,8 @@ namespace storm {
uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0);
STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both.");
STORM_LOG_THROW(this->getEngine() != Engine::Dd || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Decision-diagram engine can only be used with symbolic input models.");
return true;
}

12
src/settings/modules/GeneralSettings.h
View File

@ -13,6 +13,9 @@ namespace storm {
*/
class GeneralSettings : public ModuleSettings {
public:
// An enumeration of all engines.
enum class Engine { Sparse, Dd };
// An enumeration of all available LP solvers.
enum class LpSolver { Gurobi, glpk };
@ -287,6 +290,13 @@ namespace storm {
*/
bool isBisimulationSet() const;
/*!
* Retrieves the selected engine.
*
* @return The selecte engine.
*/
Engine getEngine() const;
#ifdef STORM_HAVE_CARL
/*!
* Retrieves whether the option enabling parametric model checking is set.
@ -335,6 +345,8 @@ namespace storm {
static const std::string statisticsOptionShortName;
static const std::string bisimulationOptionName;
static const std::string bisimulationOptionShortName;
static const std::string engineOptionName;
static const std::string engineOptionShortName;
#ifdef STORM_HAVE_CARL
static const std::string parametricOptionName;

589
src/storage/dd/CuddDd.cpp
View File

@ -7,29 +7,109 @@
#include "src/utility/vector.h"
#include "src/utility/macros.h"
#include "src/exceptions/IllegalFunctionCallException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace dd {
Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariables(containedMetaVariables) {
Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
// Intentionally left empty.
}
Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
// Intentionally left empty.
}
bool Dd<DdType::CUDD>::isBdd() const {
return this->cuddDd.which() == 0;
}
bool Dd<DdType::CUDD>::isMtbdd() const {
return this->cuddDd.which() == 1;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::toBdd() const {
if (this->isBdd()) {
return *this;
} else {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables);
}
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::toMtbdd() const {
if (this->isMtbdd()) {
return *this;
} else {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables);
}
}
BDD Dd<DdType::CUDD>::getCuddBdd() const {
if (this->isBdd()) {
return boost::get<BDD>(this->cuddDd);
} else {
STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD.");
return this->getCuddMtbdd().BddPattern();
}
}
ADD Dd<DdType::CUDD>::getCuddMtbdd() const {
if (this->isMtbdd()) {
return boost::get<ADD>(this->cuddDd);
} else {
STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD.");
return this->getCuddBdd().Add();
}
}
ABDD const& Dd<DdType::CUDD>::getCuddDd() const {
if (this->isBdd()) {
return static_cast<ABDD const&>(boost::get<BDD>(this->cuddDd));
} else {
return static_cast<ABDD const&>(boost::get<ADD>(this->cuddDd));
}
}
DdNode* Dd<DdType::CUDD>::getCuddDdNode() const {
if (this->isBdd()) {
return this->getCuddBdd().getNode();
} else {
return this->getCuddMtbdd().getNode();
}
}
bool Dd<DdType::CUDD>::operator==(Dd<DdType::CUDD> const& other) const {
return this->cuddAdd == other.getCuddAdd();
if (this->isBdd()) {
if (other.isBdd()) {
return this->getCuddBdd() == other.getCuddBdd();
} else {
return false;
}
} else {
if (other.isMtbdd()) {
return this->getCuddMtbdd() == other.getCuddMtbdd();
} else {
return false;
}
}
}
bool Dd<DdType::CUDD>::operator!=(Dd<DdType::CUDD> const& other) const {
return this->cuddAdd != other.getCuddAdd();
return !(*this == other);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const {
std::set<storm::expressions::Variable> metaVariableNames(this->getContainedMetaVariables());
metaVariableNames.insert(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end());
metaVariableNames.insert(elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames);
// If all involved DDs are BDDs, the result is also going to be a BDD.
if (this->isBdd() && thenDd.isBdd() && elseDd.isBdd()) {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
} else {
return Dd<DdType::CUDD>(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames);
}
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
@ -39,11 +119,9 @@ namespace storm {
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator+=(Dd<DdType::CUDD> const& other) {
this->cuddAdd += other.getCuddAdd();
// Join the variable sets of the two participating DDs.
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing addition on BDDs.");
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
this->cuddDd = this->getCuddMtbdd() + other.getCuddMtbdd();
return *this;
}
@ -54,45 +132,48 @@ namespace storm {
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator*=(Dd<DdType::CUDD> const& other) {
this->cuddAdd *= other.getCuddAdd();
// Join the variable sets of the two participating DDs.
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
if (this->isMtbdd() && other.isMtbdd()) {
this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd();
} else if (this->isBdd() && other.isBdd()) {
this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
} else {
STORM_LOG_WARN_COND(false, "Performing multiplication on two DDs of different type.");
this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd();
}
return *this;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
Dd<DdType::CUDD> result(*this);
result -= other;
return result;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-() const {
return this->getDdManager()->getZero() - *this;
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
return this->getDdManager()->getZero(true) - *this;
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator-=(Dd<DdType::CUDD> const& other) {
this->cuddAdd -= other.getCuddAdd();
// Join the variable sets of the two participating DDs.
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
this->cuddDd = this->getCuddMtbdd() - other.getCuddMtbdd();
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return *this;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::operator/(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
Dd<DdType::CUDD> result(*this);
result /= other;
return result;
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator/=(Dd<DdType::CUDD> const& other) {
this->cuddAdd = this->cuddAdd.Divide(other.getCuddAdd());
// Join the variable sets of the two participating DDs.
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
this->cuddDd = this->getCuddMtbdd().Divide(other.getCuddMtbdd());
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return *this;
}
@ -101,77 +182,155 @@ namespace storm {
result.complement();
return result;
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
if (this->isBdd()) {
this->cuddDd = ~this->getCuddBdd();
} else {
this->cuddDd = ~this->getCuddMtbdd();
}
return *this;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::operator&&(Dd<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
// Rewrite a and b to not((not a) or (not b)).
return Dd<DdType::CUDD>(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariables);
Dd<DdType::CUDD> result(*this);
result &= other;
return result;
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator&=(Dd<DdType::CUDD> const& other) {
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
if (this->isBdd() && other.isBdd()) {
this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
} else if (this->isMtbdd() && other.isMtbdd()) {
// We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
// the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
this->cuddDd = this->getCuddMtbdd() & other.getCuddMtbdd();
} else {
STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type.");
this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
}
return *this;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::operator||(Dd<DdType::CUDD> const& other) const {
Dd<DdType::CUDD> result(*this);
result |= other;
return result;
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator|=(Dd<DdType::CUDD> const& other) {
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
if (this->isBdd() && other.isBdd()) {
this->cuddDd = this->getCuddBdd() | other.getCuddBdd();
} else if (this->isMtbdd() && other.isMtbdd()) {
// We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
// the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
this->cuddDd = this->getCuddMtbdd() | other.getCuddMtbdd();
} else {
STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type.");
this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
}
return *this;
STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
this->cuddDd = this->getCuddBdd() | other.getCuddBdd();
this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return *this;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::iff(Dd<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariables);
if (this->isBdd() && other.isBdd()) {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
} else if (this->isMtbdd() && other.isMtbdd()) {
// We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
// the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables);
} else {
STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type.");
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
}
return *this;
}
Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
this->cuddAdd = ~this->cuddAdd;
Dd<DdType::CUDD> Dd<DdType::CUDD>::exclusiveOr(Dd<DdType::CUDD> const& other) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
if (this->isBdd() && other.isBdd()) {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
} else if (this->isMtbdd() && other.isMtbdd()) {
// We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
// the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables);
} else {
STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type.");
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
}
return *this;
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(false));
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
@ -179,15 +338,16 @@ namespace storm {
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeDd *= ddMetaVariable.getCube();
cubeDd &= ddMetaVariable.getCube();
}
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
@ -195,15 +355,16 @@ namespace storm {
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeDd *= ddMetaVariable.getCube();
cubeDd &= ddMetaVariable.getCube();
}
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
@ -211,15 +372,16 @@ namespace storm {
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeDd *= ddMetaVariable.getCube();
cubeDd *= ddMetaVariable.getCubeAsMtbdd();
}
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
@ -227,15 +389,16 @@ namespace storm {
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeDd *= ddMetaVariable.getCube();
cubeDd *= ddMetaVariable.getCubeAsMtbdd();
}
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
for (auto const& metaVariable : metaVariables) {
// First check whether the DD contains the meta variable and erase it, if this is the case.
@ -243,63 +406,102 @@ namespace storm {
newMetaVariables.erase(metaVariable);
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeDd *= ddMetaVariable.getCube();
cubeDd *= ddMetaVariable.getCubeAsMtbdd();
}
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
}
bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> const& other, double precision, bool relative) const {
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
if (relative) {
return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision);
return this->getCuddMtbdd().EqualSupNormRel(other.getCuddMtbdd(), precision);
} else {
return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision);
return this->getCuddMtbdd().EqualSupNorm(other.getCuddMtbdd(), precision);
}
}
void Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
std::vector<ADD> from;
std::vector<ADD> to;
for (auto const& metaVariablePair : metaVariablePairs) {
DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
// Check if it's legal so swap the meta variables.
if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
if (this->isBdd()) {
std::vector<BDD> from;
std::vector<BDD> to;
for (auto const& metaVariablePair : metaVariablePairs) {
DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
// Check if it's legal so swap the meta variables.
if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
}
// Keep track of the contained meta variables in the DD.
bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
if (containsVariable1 && !containsVariable2) {
this->removeContainedMetaVariable(metaVariablePair.first);
this->addContainedMetaVariable(metaVariablePair.second);
} else if (!containsVariable1 && containsVariable2) {
this->removeContainedMetaVariable(metaVariablePair.second);
this->addContainedMetaVariable(metaVariablePair.first);
}
// Add the variables to swap to the corresponding vectors.
for (auto const& ddVariable : variable1.getDdVariables()) {
from.push_back(ddVariable.getCuddBdd());
}
for (auto const& ddVariable : variable2.getDdVariables()) {
to.push_back(ddVariable.getCuddBdd());
}
}
// Keep track of the contained meta variables in the DD.
bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
if (containsVariable1 && !containsVariable2) {
this->removeContainedMetaVariable(metaVariablePair.first);
this->addContainedMetaVariable(metaVariablePair.second);
} else if (!containsVariable1 && containsVariable2) {
this->removeContainedMetaVariable(metaVariablePair.second);
this->addContainedMetaVariable(metaVariablePair.first);
// Finally, call CUDD to swap the variables.
this->cuddDd = this->getCuddBdd().SwapVariables(from, to);
} else {
std::vector<ADD> from;
std::vector<ADD> to;
for (auto const& metaVariablePair : metaVariablePairs) {
DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
// Check if it's legal so swap the meta variables.
if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
}
// Keep track of the contained meta variables in the DD.
bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
if (containsVariable1 && !containsVariable2) {
this->removeContainedMetaVariable(metaVariablePair.first);
this->addContainedMetaVariable(metaVariablePair.second);
} else if (!containsVariable1 && containsVariable2) {
this->removeContainedMetaVariable(metaVariablePair.second);
this->addContainedMetaVariable(metaVariablePair.first);
}
// Add the variables to swap to the corresponding vectors.
for (auto const& ddVariable : variable1.getDdVariables()) {
from.push_back(ddVariable.getCuddMtbdd());
}
for (auto const& ddVariable : variable2.getDdVariables()) {
to.push_back(ddVariable.getCuddMtbdd());
}
}
// Add the variables to swap to the corresponding vectors.
for (auto const& ddVariable : variable1.getDdVariables()) {
from.push_back(ddVariable.getCuddAdd());
}
for (auto const& ddVariable : variable2.getDdVariables()) {
to.push_back(ddVariable.getCuddAdd());
}
// Finally, call CUDD to swap the variables.
this->cuddDd = this->getCuddMtbdd().SwapVariables(from, to);
}
// Finally, call CUDD to swap the variables.
this->cuddAdd = this->cuddAdd.SwapVariables(from, to);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const {
std::vector<ADD> summationDdVariables;
STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s).");
// Create the CUDD summation variables.
std::vector<ADD> summationDdVariables;
for (auto const& metaVariable : summationMetaVariables) {
for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) {
summationDdVariables.push_back(ddVariable.getCuddAdd());
summationDdVariables.push_back(ddVariable.getCuddMtbdd());
}
}
@ -308,37 +510,68 @@ namespace storm {
std::set<storm::expressions::Variable> containedMetaVariables;
std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables);
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
for (auto const& metaVariable : existentialVariables) {
DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
cubeDd &= ddMetaVariable.getCube();
}
std::set<storm::expressions::Variable> unionOfMetaVariables;
std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
std::set<storm::expressions::Variable> containedMetaVariables;
std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables);
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(double value) const {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariables());
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables());
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(double value) const {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariables());
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables());
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::notZero() const {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables());
return this->toBdd();
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariables);
if (this->isBdd() && constraint.isBdd()) {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
} else {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables);
}
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const {
std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariables);
if (this->isBdd() && constraint.isBdd()) {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
} else {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables);
}
}
Dd<DdType::CUDD> Dd<DdType::CUDD>::getSupport() const {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariables());
if (this->isBdd()) {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
} else {
return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables());
}
}
uint_fast64_t Dd<DdType::CUDD>::getNonZeroCount() const {
@ -346,24 +579,40 @@ namespace storm {
for (auto const& metaVariable : this->getContainedMetaVariables()) {
numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
}
return static_cast<uint_fast64_t>(this->cuddAdd.CountMinterm(static_cast<int>(numberOfDdVariables)));
if (this->isBdd()) {
return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
} else {
return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
}
}
uint_fast64_t Dd<DdType::CUDD>::getLeafCount() const {
return static_cast<uint_fast64_t>(this->cuddAdd.CountLeaves());
if (this->isBdd()) {
return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
} else {
return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountLeaves());
}
}
uint_fast64_t Dd<DdType::CUDD>::getNodeCount() const {
return static_cast<uint_fast64_t>(this->cuddAdd.nodeCount());
if (this->isBdd()) {
return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
} else {
return static_cast<uint_fast64_t>(this->getCuddMtbdd().nodeCount());
}
}
double Dd<DdType::CUDD>::getMin() const {
ADD constantMinAdd = this->cuddAdd.FindMin();
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
ADD constantMinAdd = this->getCuddMtbdd().FindMin();
return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
}
double Dd<DdType::CUDD>::getMax() const {
ADD constantMaxAdd = this->cuddAdd.FindMax();
STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
ADD constantMaxAdd = this->getCuddMtbdd().FindMax();
return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
}
@ -381,65 +630,102 @@ namespace storm {
}
void Dd<DdType::CUDD>::setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap, double targetValue) {
Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
for (auto const& nameValuePair : metaVariableToValueMap) {
valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
// Also record that the DD now contains the meta variable.
this->addContainedMetaVariable(nameValuePair.first);
if (this->isBdd()) {
STORM_LOG_THROW(targetValue == storm::utility::zero<double>() || targetValue == storm::utility::one<double>(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD.");
Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
for (auto const& nameValuePair : metaVariableToValueMap) {
valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
// Also record that the DD now contains the meta variable.
this->addContainedMetaVariable(nameValuePair.first);
}
if (targetValue == storm::utility::one<double>()) {
this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getOne().getCuddBdd(), this->getCuddBdd());
} else {
this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getZero().getCuddBdd(), this->getCuddBdd());
}
} else {
Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
for (auto const& nameValuePair : metaVariableToValueMap) {
valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
// Also record that the DD now contains the meta variable.
this->addContainedMetaVariable(nameValuePair.first);
}
this->cuddDd = valueEncoding.toMtbdd().getCuddMtbdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddMtbdd(), this->getCuddMtbdd());
}
this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd);
}
double Dd<DdType::CUDD>::getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap) const {
std::set<storm::expressions::Variable> remainingMetaVariables(this->getContainedMetaVariables());
Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
for (auto const& nameValuePair : metaVariableToValueMap) {
valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
if (this->containsMetaVariable(nameValuePair.first)) {
remainingMetaVariables.erase(nameValuePair.first);
}
}
if (!remainingMetaVariables.empty()) {
throw storm::exceptions::InvalidArgumentException() << "Cannot evaluate function for which not all inputs were given.";
}
STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given.");
Dd<DdType::CUDD> value = *this * valueEncoding;
value = value.sumAbstract(this->getContainedMetaVariables());
return static_cast<double>(Cudd_V(value.getCuddAdd().getNode()));
if (this->isBdd()) {
Dd<DdType::CUDD> value = *this && valueEncoding;
return value.isZero() ? 0 : 1;
} else {
Dd<DdType::CUDD> value = *this * valueEncoding;
value = value.sumAbstract(this->getContainedMetaVariables());
return static_cast<double>(Cudd_V(value.getCuddMtbdd().getNode()));
}
}
bool Dd<DdType::CUDD>::isOne() const {
return *this == this->getDdManager()->getOne();
if (this->isBdd()) {
return this->getCuddBdd().IsOne();
} else {
return this->getCuddMtbdd().IsOne();
}
}
bool Dd<DdType::CUDD>::isZero() const {
return *this == this->getDdManager()->getZero();
if (this->isBdd()) {
return this->getCuddBdd().IsZero();
} else {
return this->getCuddMtbdd().IsZero();
}
}
bool Dd<DdType::CUDD>::isConstant() const {
return Cudd_IsConstant(this->cuddAdd.getNode());
if (this->isBdd()) {
return Cudd_IsConstant(this->getCuddBdd().getNode());
} else {
return Cudd_IsConstant(this->getCuddMtbdd().getNode());
}
}
uint_fast64_t Dd<DdType::CUDD>::getIndex() const {
return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
if (this->isBdd()) {
return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
} else {
return static_cast<uint_fast64_t>(this->getCuddMtbdd().NodeReadIndex());
}
}
template<typename ValueType>
std::vector<ValueType> Dd<DdType::CUDD>::toVector() const {
STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
return this->toVector<ValueType>(Odd<DdType::CUDD>(*this));
}
template<typename ValueType>
std::vector<ValueType> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const {
STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
std::vector<ValueType> result(rowOdd.getTotalOffset());
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
addToVectorRec(this->getCuddAdd().getNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result);
addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result);
return result;
}
storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix() const {
STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
std::set<storm::expressions::Variable> rowVariables;
std::set<storm::expressions::Variable> columnVariables;
@ -455,6 +741,7 @@ namespace storm {
}
storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
std::set<storm::expressions::Variable> rowMetaVariables;
std::set<storm::expressions::Variable> columnMetaVariables;
@ -470,6 +757,7 @@ namespace storm {
}
storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
@ -500,7 +788,7 @@ namespace storm {
// Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent
// it from actually generating the entries in the entry vector.
toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
// TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert
// the resulting (DD) vector to an explicit vector.
@ -516,7 +804,7 @@ namespace storm {
rowIndications[0] = 0;
// Now actually fill the entry vector.
toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
// Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
@ -529,6 +817,7 @@ namespace storm {
}
storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices;
@ -573,7 +862,7 @@ namespace storm {
// Next, we split the matrix into one for each group. This only works if the group variables are at the very
// top.
std::vector<Dd<DdType::CUDD>> groups;
splitGroupsRec(this->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
// Create the actual storage for the non-zero entries.
std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
@ -584,10 +873,10 @@ namespace storm {
for (uint_fast64_t i = 0; i < groups.size(); ++i) {
auto const& dd = groups[i];
toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables);
addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
}
// Since we modified the rowGroupIndices, we need to restore the correct values.
@ -610,9 +899,9 @@ namespace storm {
for (uint_fast64_t i = 0; i < groups.size(); ++i) {
auto const& dd = groups[i];
toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
}
// Since we modified the rowGroupIndices, we need to restore the correct values.
@ -632,7 +921,7 @@ namespace storm {
void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
// For the empty DD, we do not need to add any entries.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
return;
}
@ -684,7 +973,7 @@ namespace storm {
void Dd<DdType::CUDD>::splitGroupsRec(DdNode* dd, std::vector<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables) const {
// For the empty DD, we do not need to create a group.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
return;
}
@ -702,7 +991,7 @@ namespace storm {
template<typename ValueType>
void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const {
// For the empty DD, we do not need to add any entries.
if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
return;
}
@ -759,9 +1048,14 @@ namespace storm {
}
void Dd<DdType::CUDD>::exportToDot(std::string const& filename) const {
std::vector<ADD> cuddAddVector = { this->cuddAdd };
if (filename.empty()) {
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
if (this->isBdd()) {
std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector);
} else {
std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
}
} else {
// Build the name input of the DD.
std::vector<char*> ddNames;
@ -779,7 +1073,13 @@ namespace storm {
// Open the file, dump the DD and close it again.
FILE* filePointer = fopen(filename.c_str() , "w");
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer);
if (this->isBdd()) {
std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
} else {
std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer);
}
fclose(filePointer);
// Finally, delete the names.
@ -792,14 +1092,6 @@ namespace storm {
}
}
ADD Dd<DdType::CUDD>::getCuddAdd() {
return this->cuddAdd;
}
ADD const& Dd<DdType::CUDD>::getCuddAdd() const {
return this->cuddAdd;
}
void Dd<DdType::CUDD>::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) {
this->getContainedMetaVariables().insert(metaVariable);
}
@ -815,7 +1107,7 @@ namespace storm {
DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
int* cube;
double value;
DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
DdGen* generator = this->getCuddDd().FirstCube(&cube, &value);
return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
}
@ -824,14 +1116,13 @@ namespace storm {
}
storm::expressions::Expression Dd<DdType::CUDD>::toExpression() const {
return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariables());
return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables());
}
storm::expressions::Expression Dd<DdType::CUDD>::getMintermExpression() const {
// Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore
// make the DD more compact.
Dd<DdType::CUDD> tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables());
return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().getNode(), this->getDdManager()->getDdVariables());
return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->toBdd().getCuddDdNode(), this->getDdManager()->getDdVariables());
}
storm::expressions::Expression Dd<DdType::CUDD>::toExpressionRecur(DdNode const* dd, std::vector<storm::expressions::Variable> const& variables) {
@ -869,7 +1160,7 @@ namespace storm {
// }
}
std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
std::ostream& operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
dd.exportToDot();
return out;
}

116
src/storage/dd/CuddDd.h
View File

@ -5,6 +5,7 @@
#include <set>
#include <memory>
#include <iostream>
#include <boost/variant.hpp>
#include "src/storage/dd/Dd.h"
#include "src/storage/dd/CuddDdForwardIterator.h"
@ -65,17 +66,51 @@ namespace storm {
/*!
* Performs a logical or of the current and the given DD.
*
* @param other The second DD used for the operation.
* @return The logical or of the operands.
*/
Dd<DdType::CUDD> operator||(Dd<DdType::CUDD> const& other) const;
/*!
* Performs a logical or of the current and the given DD and assigns it to the current DD.
*
* @param other The second DD used for the operation.
* @return A reference to the current DD after the operation
*/
Dd<DdType::CUDD>& operator|=(Dd<DdType::CUDD> const& other);
/*!
* Performs a logical and of the current and the given DD.
*
* @param other The second DD used for the operation.
* @return The logical and of the operands.
*/
Dd<DdType::CUDD> operator&&(Dd<DdType::CUDD> const& other) const;
/*!
* Performs a logical and of the current and the given DD and assigns it to the current DD.
*
* @param other The second DD used for the operation.
* @return A reference to the current DD after the operation
*/
Dd<DdType::CUDD>& operator&=(Dd<DdType::CUDD> const& other);
/*!
* Performs a logical iff of the current and the given DD.
*
* @param other The second DD used for the operation.
* @return The logical iff of the operands.
*/
Dd<DdType::CUDD> iff(Dd<DdType::CUDD> const& other) const;
/*!
* Performs a logical exclusive-or of the current and the given DD.
*
* @param other The second DD used for the operation.
* @return The logical exclusive-or of the operands.
*/
Dd<DdType::CUDD> exclusiveOr(Dd<DdType::CUDD> const& other) const;
/*!
* Adds the two DDs.
*
@ -296,6 +331,16 @@ namespace storm {
*/
Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const;
/*!
* Computes the logical and of the current and the given DD and existentially abstracts from the given set
* of variables.
*
* @param other The second DD for the logical and.
* @param existentialVariables The variables from which to existentially abstract.
* @return A DD representing the result.
*/
Dd<DdType::CUDD> andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
/*!
* Computes a DD that represents the function in which all assignments with a function value strictly larger
* than the given value are mapped to one and all others to zero.
@ -605,20 +650,64 @@ namespace storm {
friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
/*!
* Converts an MTBDD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as
* a call to notZero().
*
* @return The corresponding BDD.
*/
Dd<DdType::CUDD> toBdd() const;
/*!
* Converts a BDD to an equivalent MTBDD.
*
* @return The corresponding MTBDD.
*/
Dd<DdType::CUDD> toMtbdd() const;
/*!
* Retrieves whether this DD is a BDD.
*
* @return True iff this DD is a BDD.
*/
bool isBdd() const;
/*!
* Retrieves whether this DD is an MTBDD. Even though MTBDDs technicall subsume BDDs, this will return false
* if the DD is actually a BDD.
*
* @return True iff this DD is an MTBDD.
*/
bool isMtbdd() const;
private:
/*!
* Retrieves a reference to the CUDD ADD object associated with this DD.
* Retrieves the CUDD BDD object associated with this DD.
*
* @return The CUDD ADD object associated with this DD.
* @return The CUDD BDD object associated with this DD.
*/
ADD getCuddAdd();
BDD getCuddBdd() const;
/*!
* Retrieves the CUDD ADD object associated with this DD.
* Retrieves the CUDD MTBDD object associated with this DD.
*
* @return The CUDD ADD object assoicated with this DD.
* @return The CUDD MTBDD object associated with this DD.
*/
ADD const& getCuddAdd() const;
ADD getCuddMtbdd() const;
/*!
* Retrieves the CUDD object associated with this DD.
*
* @return The CUDD object associated with this DD.
*/
ABDD const& getCuddDd() const;
/*!
* Retrieves the raw DD node of CUDD associated with this DD.
*
* @return The DD node of CUDD associated with this DD.
*/
DdNode* getCuddDdNode() const;
/*!
* Adds the given meta variable to the set of meta variables that are contained in this DD.
@ -657,10 +746,19 @@ namespace storm {
* Creates a DD that encapsulates the given CUDD ADD.
*
* @param ddManager The manager responsible for this DD.
* @param cuddAdd The CUDD ADD to store.
* @param cuddDd The CUDD ADD to store.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
* @param ddManager The manager responsible for this DD.
* @param cuddDd The CUDD ADD to store.
* @param containedMetaVariables The meta variables that appear in the DD.
*/
Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* Helper function to convert the DD into a (sparse) matrix.
@ -727,7 +825,7 @@ namespace storm {
std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
// The ADD created by CUDD.
ADD cuddAdd;
boost::variant<BDD, ADD> cuddDd;
// The meta variables that appear in this DD.
std::set<storm::expressions::Variable> containedMetaVariables;

26
src/storage/dd/CuddDdForwardIterator.cpp
View File

@ -80,19 +80,19 @@ namespace storm {
++this->cubeCounter;
for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) {
auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index]));
auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<0>(this->relevantDontCareDdVariables[index]));
if (ddMetaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
if ((this->cubeCounter & (1ull << index)) != 0) {
currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), true);
currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), true);
} else {
currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), false);
currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), false);
}
} else {
storm::expressions::Variable const& metaVariable = std::get<1>(this->relevantDontCareDdVariables[index]);
storm::expressions::Variable const& metaVariable = std::get<0>(this->relevantDontCareDdVariables[index]);
if ((this->cubeCounter & (1ull << index)) != 0) {
currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
} else {
currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
}
}
}
@ -106,31 +106,31 @@ namespace storm {
// valuations later.
for (auto const& metaVariable : *this->metaVariables) {
bool metaVariableAppearsInCube = false;
std::vector<std::tuple<ADD, storm::expressions::Variable, uint_fast64_t>> localRelenvantDontCareDdVariables;
std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> localRelenvantDontCareDdVariables;
auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable);
if (ddMetaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) {
if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) {
metaVariableAppearsInCube = true;
currentValuation.setBooleanValue(metaVariable, false);
} else if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) {
} else if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 1) {
metaVariableAppearsInCube = true;
currentValuation.setBooleanValue(metaVariable, true);
} else {
localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[0].getCuddAdd(), metaVariable, 0));
localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0));
}
} else {
int_fast64_t intValue = 0;
for (uint_fast64_t bitIndex = 0; bitIndex < ddMetaVariable.getNumberOfDdVariables(); ++bitIndex) {
if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) {
if (cube[ddMetaVariable.getDdVariables()[bitIndex].getIndex()] == 0) {
// Leave bit unset.
metaVariableAppearsInCube = true;
} else if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) {
} else if (cube[ddMetaVariable.getDdVariables()[bitIndex].getIndex()] == 1) {
intValue |= 1ull << (ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1);
metaVariableAppearsInCube = true;
} else {
// Temporarily leave bit unset so we can iterate trough the other option later.
// Add the bit to the relevant don't care bits.
localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
}
}
if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {

4
src/storage/dd/CuddDdForwardIterator.h
View File

@ -124,8 +124,8 @@ namespace storm {
// This is needed, because cubes may represent many assignments (if they have don't care variables).
uint_fast64_t cubeCounter;
// A vector of tuples of the form <variable, metaVariable, bitIndex>.
std::vector<std::tuple<ADD, storm::expressions::Variable, uint_fast64_t>> relevantDontCareDdVariables;
// A vector of tuples of the form <metaVariable, bitIndex>.
std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> relevantDontCareDdVariables;
// The current valuation of meta variables.
storm::expressions::SimpleValuation currentValuation;

64
src/storage/dd/CuddDdManager.cpp
View File

@ -37,19 +37,27 @@ namespace storm {
}
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne() const {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne(bool asMtbdd) const {
if (asMtbdd) {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
} else {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddOne());
}
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero() const {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero(bool asMtbdd) const {
if (asMtbdd) {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
} else {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddZero());
}
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getConstant(double value) const {
return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.constant(value));
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const {
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd) const {
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
@ -68,19 +76,23 @@ namespace storm {
for (std::size_t i = 1; i < ddVariables.size(); ++i) {
if (value & (1ull << (ddVariables.size() - i - 1))) {
result *= ddVariables[i];
result &= ddVariables[i];
} else {
result *= !ddVariables[i];
result &= !ddVariables[i];
}
}
return result;
if (asMtbdd) {
return result.toMtbdd();
} else {
return result;
}
}
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable) const {
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable, bool asMtbdd) const {
storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
Dd<DdType::CUDD> result = this->getZero();
Dd<DdType::CUDD> result = this->getZero(asMtbdd);
for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
result.setValue(variable, value, static_cast<double>(1));
@ -92,7 +104,7 @@ namespace storm {
Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) const {
storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
Dd<DdType::CUDD> result = this->getZero();
Dd<DdType::CUDD> result = this->getZero(true);
for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
result.setValue(variable, value, static_cast<double>(value));
}
@ -117,13 +129,13 @@ namespace storm {
std::vector<Dd<DdType::CUDD>> variables;
std::vector<Dd<DdType::CUDD>> variablesPrime;
for (std::size_t i = 0; i < numberOfBits; ++i) {
variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {unprimed}));
variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {primed}));
variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
}
// Now group the non-primed and primed variable.
for (uint_fast64_t i = 0; i < numberOfBits; ++i) {
this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
this->getCuddManager().MakeTreeNode(variables[i].getIndex(), 2, MTR_FIXED);
}
metaVariableMap.emplace(unprimed, DdMetaVariable<DdType::CUDD>(name, low, high, variables, this->shared_from_this()));
@ -144,11 +156,11 @@ namespace storm {
std::vector<Dd<DdType::CUDD>> variables;
std::vector<Dd<DdType::CUDD>> variablesPrime;
variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {unprimed}));
variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {primed}));
variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
// Now group the non-primed and primed variable.
this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED);
metaVariableMap.emplace(unprimed, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
metaVariableMap.emplace(primed, DdMetaVariable<DdType::CUDD>(name + "'", variablesPrime, this->shared_from_this()));
@ -199,22 +211,22 @@ namespace storm {
std::vector<std::string> DdManager<DdType::CUDD>::getDdVariableNames() const {
// First, we initialize a list DD variables and their names.
std::vector<std::pair<ADD, std::string>> variablePairs;
std::vector<std::pair<uint_fast64_t, std::string>> variablePairs;
for (auto const& variablePair : this->metaVariableMap) {
DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
// If the meta variable is of type bool, we don't need to suffix it with the bit number.
if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first.getName());
variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName());
} else {
// For integer-valued meta variables, we, however, have to add the suffix.
for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first.getName() + '.' + std::to_string(variableIndex));
variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex));
}
}
}
// Then, we sort this list according to the indices of the ADDs.
std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, std::string> const& a, std::pair<uint_fast64_t, std::string> const& b) { return a.first < b.first; });
// Now, we project the sorted vector to its second component.
std::vector<std::string> result;
@ -227,22 +239,22 @@ namespace storm {
std::vector<storm::expressions::Variable> DdManager<DdType::CUDD>::getDdVariables() const {
// First, we initialize a list DD variables and their names.
std::vector<std::pair<ADD, storm::expressions::Variable>> variablePairs;
std::vector<std::pair<uint_fast64_t, storm::expressions::Variable>> variablePairs;
for (auto const& variablePair : this->metaVariableMap) {
DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
// If the meta variable is of type bool, we don't need to suffix it with the bit number.
if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first);
variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first);
} else {
// For integer-valued meta variables, we, however, have to add the suffix.
for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first);
variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first);
}
}
}
// Then, we sort this list according to the indices of the ADDs.
std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, storm::expressions::Variable> const& a, std::pair<ADD, storm::expressions::Variable> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, storm::expressions::Variable> const& a, std::pair<uint_fast64_t, storm::expressions::Variable> const& b) { return a.first < b.first; });
// Now, we project the sorted vector to its second component.
std::vector<storm::expressions::Variable> result;

16
src/storage/dd/CuddDdManager.h
View File

@ -36,18 +36,20 @@ namespace storm {
#endif
/*!
* Retrieves a DD representing the constant one function.
* Retrieves a DD representing the constant one function. If the flag is set, the result will be given in
* terms of an MTBDD rather than a BDD.
*
* @return A DD representing the constant one function.
*/
Dd<DdType::CUDD> getOne() const;
Dd<DdType::CUDD> getOne(bool asMtbdd = false) const;
/*!
* Retrieves a DD representing the constant zero function.
* Retrieves a DD representing the constant zero function. If the flag is set, the result will be given in
* terms of an MTBDD rather than a BDD.
*
* @return A DD representing the constant zero function.
*/
Dd<DdType::CUDD> getZero() const;
Dd<DdType::CUDD> getZero(bool asMtbdd = false) const;
/*!
* Retrieves a DD representing the constant function with the given value.
@ -62,19 +64,21 @@ namespace storm {
*
* @param variable The expression variable associated with the meta variable.
* @param value The value the meta variable is supposed to have.
* @param asMtbdd If set to true, the result will be given in terms of an MTBDD.
* @return The DD representing the function that maps all inputs which have the given meta variable equal
* to the given value one.
*/
Dd<DdType::CUDD> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const;
Dd<DdType::CUDD> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd = false) const;
/*!
* Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values
* of the range of the meta variable to one.
*
* @param variable The expression variable associated with the meta variable.
* @param asMtbdd If set to true, the result will be given in terms of an MTBDD.
* @return The range of the meta variable.
*/
Dd<DdType::CUDD> getRange(storm::expressions::Variable const& variable) const;
Dd<DdType::CUDD> getRange(storm::expressions::Variable const& variable, bool asMtbdd = false) const;
/*!
* Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal

15
src/storage/dd/CuddDdMetaVariable.cpp
View File

@ -3,18 +3,20 @@
namespace storm {
namespace dd {
DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) {
// Create the cube of all variables of this meta variable.
for (auto const& ddVariable : this->ddVariables) {
this->cube *= ddVariable;
this->cube &= ddVariable;
}
this->cubeAsMtbdd = this->cube.toMtbdd();
}
DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) {
// Create the cube of all variables of this meta variable.
for (auto const& ddVariable : this->ddVariables) {
this->cube *= ddVariable;
this->cube &= ddVariable;
}
this->cubeAsMtbdd = this->cube.toMtbdd();
}
std::string const& DdMetaVariable<DdType::CUDD>::getName() const {
@ -48,5 +50,10 @@ namespace storm {
Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCube() const {
return this->cube;
}
Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCubeAsMtbdd() const {
return this->cubeAsMtbdd;
}
}
}

11
src/storage/dd/CuddDdMetaVariable.h
View File

@ -113,6 +113,13 @@ namespace storm {
*/
Dd<DdType::CUDD> const& getCube() const;
/*!
* Retrieves the cube of all variables that encode this meta variable represented as an MTBDD.
*
* @return The cube of all variables that encode this meta variable.
*/
Dd<DdType::CUDD> const& getCubeAsMtbdd() const;
// The name of the meta variable.
std::string name;
@ -131,6 +138,10 @@ namespace storm {
// The cube consisting of all variables that encode the meta variable.
Dd<DdType::CUDD> cube;
// The cube consisting of all variables that encode the meta variable represented by an MTBDD. This is
// used as a shortcut mainly for the abstraction methods.
Dd<DdType::CUDD> cubeAsMtbdd;
// A pointer to the manager responsible for this meta variable.
std::shared_ptr<DdManager<DdType::CUDD>> manager;
};

12
src/storage/dd/CuddOdd.cpp
View File

@ -17,17 +17,17 @@ namespace storm {
std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
// Now construct the ODD structure.
std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddRec(dd.getCuddAdd().getNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
// Currently, the DD needs to be an MTBDD, because complement edges are not supported.
std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddRec(dd.toMtbdd().getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
// Finally, move the children of the root ODD into this ODD.
this->dd = rootOdd->dd;
this->elseNode = std::move(rootOdd->elseNode);
this->thenNode = std::move(rootOdd->thenNode);
this->elseOffset = rootOdd->elseOffset;
this->thenOffset = rootOdd->thenOffset;
}
Odd<DdType::CUDD>::Odd(ADD dd, std::shared_ptr<Odd<DdType::CUDD>>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>>&& thenNode, uint_fast64_t thenOffset) : dd(dd), elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
Odd<DdType::CUDD>::Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
// Intentionally left empty.
}
@ -92,18 +92,18 @@ namespace storm {
thenOffset = 1;
}
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), nullptr, elseOffset, nullptr, thenOffset));
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(nullptr, elseOffset, nullptr, thenOffset));
} else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd<DdType::CUDD>> thenNode = elseNode;
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset()));
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset()));
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
}
}
}

7
src/storage/dd/CuddOdd.h
View File

@ -92,13 +92,13 @@ namespace storm {
/*!
* Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
*
* @param dd The DD associated with this ODD node.
* @param dd The DD node associated with this ODD node.
* @param elseNode The else-successor of thie ODD node.
* @param elseOffset The offset of the else-successor.
* @param thenNode The then-successor of thie ODD node.
* @param thenOffset The offset of the then-successor.
*/
Odd(ADD dd, std::shared_ptr<Odd<DdType::CUDD>>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>>&& thenNode, uint_fast64_t thenOffset);
Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset);
/*!
* Recursively builds the ODD.
@ -114,9 +114,6 @@ namespace storm {
*/
static std::shared_ptr<Odd<DdType::CUDD>> buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
// The DD associated with this ODD node.
ADD dd;
// The then- and else-nodes.
std::shared_ptr<Odd<DdType::CUDD>> elseNode;
std::shared_ptr<Odd<DdType::CUDD>> thenNode;

34
src/utility/cli.h
View File

@ -70,6 +70,7 @@ log4cplus::Logger printer;
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
// Headers related to exception handling.
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidTypeException.h"
@ -276,22 +277,25 @@ namespace storm {
}
// Customize model-building.
// typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
// if (formula) {
// options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
// }
// options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
//
// // Then, build the model from the symbolic description.
// result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
if (formula) {
options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
if (formula) {
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
}
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
// Then, build the model from the symbolic description.
result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd) {
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
if (formula) {
options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
}
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
}
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
return result;
}
@ -425,6 +429,8 @@ namespace storm {
STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
std::shared_ptr<storm::models::AbstractModel<ValueType>> model = buildSymbolicModel<ValueType>(program.get(), formula);
STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed.
model = preprocessModel<ValueType>(model, formula);

50
test/functional/storage/CuddDdTest.cpp
View File

@ -62,8 +62,15 @@ TEST(CuddDdManager, EncodingTest) {
ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4));
EXPECT_EQ(1, encoding.getNonZeroCount());
EXPECT_EQ(6, encoding.getNodeCount());
EXPECT_EQ(2, encoding.getLeafCount());
// As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less
// than the MTBDD.
EXPECT_EQ(5, encoding.getNodeCount());
EXPECT_EQ(1, encoding.getLeafCount());
// As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
EXPECT_EQ(6, encoding.toMtbdd().getNodeCount());
EXPECT_EQ(2, encoding.toMtbdd().getLeafCount());
}
TEST(CuddDdManager, RangeTest) {
@ -75,8 +82,8 @@ TEST(CuddDdManager, RangeTest) {
ASSERT_NO_THROW(range = manager->getRange(x.first));
EXPECT_EQ(9, range.getNonZeroCount());
EXPECT_EQ(2, range.getLeafCount());
EXPECT_EQ(6, range.getNodeCount());
EXPECT_EQ(1, range.getLeafCount());
EXPECT_EQ(5, range.getNodeCount());
}
TEST(CuddDdManager, IdentityTest) {
@ -100,17 +107,14 @@ TEST(CuddDd, OperatorTest) {
EXPECT_FALSE(manager->getZero() != manager->getZero());
EXPECT_TRUE(manager->getZero() != manager->getOne());
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne();
storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getOne();
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne(true);
storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getOne(true);
storm::dd::Dd<storm::dd::DdType::CUDD> dd3 = dd1 + dd2;
EXPECT_TRUE(dd3 == manager->getConstant(2));
dd3 += manager->getZero();
dd3 += manager->getZero(true);
EXPECT_TRUE(dd3 == manager->getConstant(2));
dd3 = dd1 && manager->getConstant(3);
EXPECT_TRUE(dd1 == manager->getOne());
dd3 = dd1 * manager->getConstant(3);
EXPECT_TRUE(dd3 == manager->getConstant(3));
@ -118,22 +122,22 @@ TEST(CuddDd, OperatorTest) {
EXPECT_TRUE(dd3 == manager->getConstant(6));
dd3 = dd1 - dd2;
EXPECT_TRUE(dd3 == manager->getZero());
EXPECT_TRUE(dd3.isZero());
dd3 -= manager->getConstant(-2);
EXPECT_TRUE(dd3 == manager->getConstant(2));
dd3 /= manager->getConstant(2);
EXPECT_TRUE(dd3 == manager->getOne());
EXPECT_TRUE(dd3.isOne());
dd3.complement();
EXPECT_TRUE(dd3 == manager->getZero());
dd3 = dd3.toBdd().complement();
EXPECT_TRUE(dd3.isZero());
dd1 = !dd3;
EXPECT_TRUE(dd1 == manager->getOne());
EXPECT_TRUE(dd1.isOne());
dd3 = dd1 || dd2;
EXPECT_TRUE(dd3 == manager->getOne());
dd3 = dd1 || dd2.toBdd();
EXPECT_TRUE(dd3.isOne());
dd1 = manager->getIdentity(x.first);
dd2 = manager->getConstant(5);
@ -142,7 +146,7 @@ TEST(CuddDd, OperatorTest) {
EXPECT_EQ(1, dd3.getNonZeroCount());
storm::dd::Dd<storm::dd::DdType::CUDD> dd4 = dd1.notEquals(dd2);
EXPECT_TRUE(dd4 == !dd3);
EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd());
dd3 = dd1.less(dd2);
EXPECT_EQ(11, dd3.getNonZeroCount());
@ -161,12 +165,12 @@ TEST(CuddDd, OperatorTest) {
EXPECT_EQ(10, dd4.getNonZeroCount());
dd4 = dd3.minimum(dd1);
dd4 *= manager->getEncoding(x.first, 2);
dd4 *= manager->getEncoding(x.first, 2, true);
dd4 = dd4.sumAbstract({x.first});
EXPECT_EQ(2, dd4.getValue());
dd4 = dd3.maximum(dd1);
dd4 *= manager->getEncoding(x.first, 2);
dd4 *= manager->getEncoding(x.first, 2, true);
dd4 = dd4.sumAbstract({x.first});
EXPECT_EQ(5, dd4.getValue());
@ -197,7 +201,7 @@ TEST(CuddDd, AbstractionTest) {
EXPECT_EQ(1, dd3.getNonZeroCount());
ASSERT_THROW(dd3 = dd3.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
ASSERT_NO_THROW(dd3 = dd3.existsAbstract({x.first}));
EXPECT_TRUE(dd3 == manager->getZero());
EXPECT_TRUE(dd3.isOne());
dd3 = dd1.equals(dd2);
dd3 *= manager->getConstant(3);
@ -253,7 +257,7 @@ TEST(CuddDd, GetSetValueTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne();
storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne(true);
ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2));
EXPECT_EQ(2, dd1.getLeafCount());
@ -397,7 +401,7 @@ TEST(CuddDd, OddTest) {
}
// Create a non-trivial matrix.
dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first);
dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first);
dd += manager->getEncoding(x.first, 1) * manager->getRange(x.second) + manager->getEncoding(x.second, 1) * manager->getRange(x.first);
// Create the ODDs.
Write Preview
Loading…
Cancel
Save