From e43bdfaaaa3e246208d1f86616cb4ab4f13bd00f Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 1 Dec 2015 17:31:04 +0100 Subject: [PATCH] more work on the dd stuff *sigh* Former-commit-id: df8e227336a1941db6e1b8ac6b2225a76c009ddb --- .../3rdparty/cudd-2.5.0/src/cudd/cuddExport.c | 9 +- .../3rdparty/sylvan/src/sylvan_storm_custom.c | 2 +- resources/3rdparty/xercesc-3.1.2/Makefile | 4 +- .../3rdparty/xercesc-3.1.2/config.status | 6 +- resources/3rdparty/xercesc-3.1.2/libtool | 2 +- .../3rdparty/xercesc-3.1.2/samples/Makefile | 4 +- resources/3rdparty/xercesc-3.1.2/src/Makefile | 4 +- .../util/MsgLoaders/MsgCatalog/Makefile | 2 +- .../3rdparty/xercesc-3.1.2/tests/Makefile | 4 +- src/adapters/AddExpressionAdapter.cpp | 38 +++-- src/adapters/AddExpressionAdapter.h | 4 +- src/builder/DdPrismModelBuilder.cpp | 51 +++---- src/models/symbolic/Ctmc.cpp | 1 + src/models/symbolic/DeterministicModel.cpp | 1 + src/models/symbolic/Dtmc.cpp | 1 + src/models/symbolic/Mdp.cpp | 3 +- src/models/symbolic/Model.cpp | 4 +- src/models/symbolic/NondeterministicModel.cpp | 1 + src/models/symbolic/StandardRewardModel.cpp | 1 + .../symbolic/StochasticTwoPlayerGame.cpp | 3 +- src/storage/dd/Bdd.cpp | 17 +++ src/storage/dd/Bdd.h | 9 ++ src/storage/dd/cudd/InternalCuddBdd.cpp | 20 +++ src/storage/dd/cudd/InternalCuddBdd.h | 9 ++ src/storage/dd/sylvan/InternalSylvanAdd.cpp | 4 +- src/storage/dd/sylvan/InternalSylvanBdd.cpp | 9 ++ src/storage/dd/sylvan/InternalSylvanBdd.h | 9 ++ .../builder/DdPrismModelBuilderTest.cpp | 135 +++++++++++++++++- 28 files changed, 293 insertions(+), 64 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c index 2392da36a..affbfd53b 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c @@ -543,10 +543,17 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { - retval = fprintf(fp, + if (inames != NULL) { + retval = fprintf(fp, "\"%p\" [label = \"%s\"];\n", (void *) ((mask & (ptrint) scan) / sizeof(DdNode)), inames[dd->invperm[i]]); + } else { + retval = fprintf(fp, + "\"%p\" [label = \"%i\"];\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), i); + } if (retval == EOF) goto failure; if (cuddT(scan) != Cudd_ReadZero(dd)) { retval = fprintf(fp, diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c index 55b16ac32..45283ae09 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c @@ -43,7 +43,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) int nega = mtbdd_isnegated(a); int negb = mtbdd_isnegated(b); - result = mtbdd_double(a / b); + result = mtbdd_double(vval_a / vval_b); if (nega ^ negb) return mtbdd_negate(result); else return result; } diff --git a/resources/3rdparty/xercesc-3.1.2/Makefile b/resources/3rdparty/xercesc-3.1.2/Makefile index 2068ff63d..111646ba8 100644 --- a/resources/3rdparty/xercesc-3.1.2/Makefile +++ b/resources/3rdparty/xercesc-3.1.2/Makefile @@ -305,7 +305,7 @@ ICU_FLAGS = ICU_LIBS = -licuuc -licudata ICU_PRESENT = no ICU_SBIN = -INSTALL = /usr/local/bin/ginstall -c +INSTALL = /usr/bin/install -c INSTALL_DATA = ${INSTALL} -m 644 INSTALL_PROGRAM = ${INSTALL} INSTALL_SCRIPT = ${INSTALL} @@ -322,7 +322,7 @@ LT_SYS_LIBRARY_PATH = MAINT = # MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo MANIFEST_TOOL = : -MKDIR_P = /usr/local/bin/gmkdir -p +MKDIR_P = config/install-sh -c -d NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm NMEDIT = nmedit OBJDUMP = objdump diff --git a/resources/3rdparty/xercesc-3.1.2/config.status b/resources/3rdparty/xercesc-3.1.2/config.status index 94ec90984..1fa77926e 100755 --- a/resources/3rdparty/xercesc-3.1.2/config.status +++ b/resources/3rdparty/xercesc-3.1.2/config.status @@ -439,8 +439,8 @@ gives unlimited permission to copy, distribute and modify it." ac_pwd='/Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2' srcdir='.' -INSTALL='/usr/local/bin/ginstall -c' -MKDIR_P='/usr/local/bin/gmkdir -p' +INSTALL='/usr/bin/install -c' +MKDIR_P='config/install-sh -c -d' AWK='awk' test -n "$AWK" || AWK=awk # The default lists apply if the user does not specify any file. @@ -998,7 +998,7 @@ S["am__leading_dot"]="." S["SET_MAKE"]="" S["AWK"]="awk" S["mkdir_p"]="$(MKDIR_P)" -S["MKDIR_P"]="/usr/local/bin/gmkdir -p" +S["MKDIR_P"]="config/install-sh -c -d" S["INSTALL_STRIP_PROGRAM"]="$(install_sh) -c -s" S["STRIP"]="strip" S["install_sh"]="${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/install-sh" diff --git a/resources/3rdparty/xercesc-3.1.2/libtool b/resources/3rdparty/xercesc-3.1.2/libtool index 66f79e8c2..78a06db0c 100755 --- a/resources/3rdparty/xercesc-3.1.2/libtool +++ b/resources/3rdparty/xercesc-3.1.2/libtool @@ -1,6 +1,6 @@ #! /bin/sh # Generated automatically by config.status (xerces-c) 3.1.2 -# Libtool was configured on host Christians-iMac.fritz.box: +# Libtool was configured on host tartaros.informatik.rwth-aachen.de: # NOTE: Changes made to this file will be lost: look at ltmain.sh. # Provide generalized library-building support services. diff --git a/resources/3rdparty/xercesc-3.1.2/samples/Makefile b/resources/3rdparty/xercesc-3.1.2/samples/Makefile index a64154cc9..32de166c6 100644 --- a/resources/3rdparty/xercesc-3.1.2/samples/Makefile +++ b/resources/3rdparty/xercesc-3.1.2/samples/Makefile @@ -358,7 +358,7 @@ ICU_FLAGS = ICU_LIBS = -licuuc -licudata ICU_PRESENT = no ICU_SBIN = -INSTALL = /usr/local/bin/ginstall -c +INSTALL = /usr/bin/install -c INSTALL_DATA = ${INSTALL} -m 644 INSTALL_PROGRAM = ${INSTALL} INSTALL_SCRIPT = ${INSTALL} @@ -375,7 +375,7 @@ LT_SYS_LIBRARY_PATH = MAINT = # MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo MANIFEST_TOOL = : -MKDIR_P = /usr/local/bin/gmkdir -p +MKDIR_P = ../config/install-sh -c -d NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm NMEDIT = nmedit OBJDUMP = objdump diff --git a/resources/3rdparty/xercesc-3.1.2/src/Makefile b/resources/3rdparty/xercesc-3.1.2/src/Makefile index b1b3f31c9..3bc3efd99 100644 --- a/resources/3rdparty/xercesc-3.1.2/src/Makefile +++ b/resources/3rdparty/xercesc-3.1.2/src/Makefile @@ -1426,7 +1426,7 @@ ICU_FLAGS = ICU_LIBS = -licuuc -licudata ICU_PRESENT = no ICU_SBIN = -INSTALL = /usr/local/bin/ginstall -c +INSTALL = /usr/bin/install -c INSTALL_DATA = ${INSTALL} -m 644 INSTALL_PROGRAM = ${INSTALL} INSTALL_SCRIPT = ${INSTALL} @@ -1443,7 +1443,7 @@ LT_SYS_LIBRARY_PATH = MAINT = # MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo MANIFEST_TOOL = : -MKDIR_P = /usr/local/bin/gmkdir -p +MKDIR_P = ../config/install-sh -c -d NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm NMEDIT = nmedit OBJDUMP = objdump diff --git a/resources/3rdparty/xercesc-3.1.2/src/xercesc/util/MsgLoaders/MsgCatalog/Makefile b/resources/3rdparty/xercesc-3.1.2/src/xercesc/util/MsgLoaders/MsgCatalog/Makefile index 3b8b4770c..cfab1c354 100644 --- a/resources/3rdparty/xercesc-3.1.2/src/xercesc/util/MsgLoaders/MsgCatalog/Makefile +++ b/resources/3rdparty/xercesc-3.1.2/src/xercesc/util/MsgLoaders/MsgCatalog/Makefile @@ -3,7 +3,7 @@ srcdir = . top_srcdir = ../../../../.. top_builddir = ../../../../.. prefix = /Users/chris/work/storm/build_xcode/resources/3rdparty/xercesc-3.1.2 -INSTALL = /usr/local/bin/ginstall -c +INSTALL = /usr/bin/install -c INSTALL_PROGRAM = ${INSTALL} mkdir_p = $(MKDIR_P) diff --git a/resources/3rdparty/xercesc-3.1.2/tests/Makefile b/resources/3rdparty/xercesc-3.1.2/tests/Makefile index ac7344726..b86d1d65c 100644 --- a/resources/3rdparty/xercesc-3.1.2/tests/Makefile +++ b/resources/3rdparty/xercesc-3.1.2/tests/Makefile @@ -342,7 +342,7 @@ ICU_FLAGS = ICU_LIBS = -licuuc -licudata ICU_PRESENT = no ICU_SBIN = -INSTALL = /usr/local/bin/ginstall -c +INSTALL = /usr/bin/install -c INSTALL_DATA = ${INSTALL} -m 644 INSTALL_PROGRAM = ${INSTALL} INSTALL_SCRIPT = ${INSTALL} @@ -359,7 +359,7 @@ LT_SYS_LIBRARY_PATH = MAINT = # MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo MANIFEST_TOOL = : -MKDIR_P = /usr/local/bin/gmkdir -p +MKDIR_P = ../config/install-sh -c -d NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm NMEDIT = nmedit OBJDUMP = objdump diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index c86f9dca0..0a561a1eb 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -17,20 +17,33 @@ namespace storm { } template - storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { + storm::dd::Add AddExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { if (expression.hasBooleanType()) { return boost::any_cast>(expression.accept(*this)).template toAdd(); } else { - return boost::any_cast>(expression.accept(*this)); + return boost::any_cast>(expression.accept(*this)); } } + template + storm::dd::Bdd AddExpressionAdapter::translateBooleanExpression(storm::expressions::Expression const& expression) { + STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected expression of boolean type."); + return boost::any_cast>(expression.accept(*this)); + } + template boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { - storm::dd::Add elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); - storm::dd::Add thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); - storm::dd::Add conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); - return conditionDd.ite(thenDd, elseDd); + if (expression.hasBooleanType()) { + storm::dd::Bdd elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); + storm::dd::Bdd thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); + storm::dd::Bdd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); + return conditionDd.ite(thenDd, elseDd); + } else { + storm::dd::Add elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); + storm::dd::Add thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); + storm::dd::Add conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); + return conditionDd.ite(thenDd, elseDd); + } } template @@ -62,10 +75,10 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { - storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); + storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - storm::dd::Add result; + storm::dd::Add result; switch (expression.getOperatorType()) { case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus: result = leftResult + rightResult; @@ -97,8 +110,8 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { - storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); - storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); + storm::dd::Add leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); + storm::dd::Add rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); storm::dd::Bdd result; switch (expression.getRelationType()) { @@ -151,7 +164,7 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { - storm::dd::Add result = boost::any_cast>(expression.getOperand()->accept(*this)); + storm::dd::Add result = boost::any_cast>(expression.getOperand()->accept(*this)); switch (expression.getOperatorType()) { case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus: @@ -187,6 +200,7 @@ namespace storm { // Explicitly instantiate the symbolic expression adapter template class AddExpressionAdapter; + template class AddExpressionAdapter; } // namespace adapters } // namespace storm diff --git a/src/adapters/AddExpressionAdapter.h b/src/adapters/AddExpressionAdapter.h index a8a8d43c6..9e74fd49d 100644 --- a/src/adapters/AddExpressionAdapter.h +++ b/src/adapters/AddExpressionAdapter.h @@ -6,6 +6,7 @@ #include "storage/expressions/ExpressionVisitor.h" #include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" #include "src/storage/dd/DdManager.h" namespace storm { @@ -16,7 +17,8 @@ namespace storm { public: AddExpressionAdapter(std::shared_ptr> ddManager, std::map const& variableMapping); - storm::dd::Add translateExpression(storm::expressions::Expression const& expression); + storm::dd::Add translateExpression(storm::expressions::Expression const& expression); + storm::dd::Bdd translateBooleanExpression(storm::expressions::Expression const& expression); virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override; virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override; diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 3a897c1db..aa55fbcbd 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -144,8 +144,8 @@ namespace storm { // Create meta variables for each of the modules' variables. for (storm::prism::Module const& module : program.getModules()) { - storm::dd::Add moduleIdentity = manager->template getAddOne(); - storm::dd::Add moduleRange = manager->template getAddOne(); + storm::dd::Bdd moduleIdentity = manager->getBddOne(); + storm::dd::Bdd moduleRange = manager->getBddOne(); for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -159,10 +159,10 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); - variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); - moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first).template toAdd(); + storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd()); + moduleIdentity &= variableIdentity; + moduleRange &= manager->getRange(variablePair.first); rowColumnMetaVariablePairs.push_back(variablePair); } @@ -176,15 +176,15 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)).template toAdd() * manager->getRange(variablePair.first).template toAdd() * manager->getRange(variablePair.second).template toAdd(); - variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); - moduleIdentity *= variableIdentity; - moduleRange *= manager->getRange(variablePair.first).template toAdd(); + storm::dd::Bdd variableIdentity = manager->template getIdentity(variablePair.first).equals(manager->template getIdentity(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd()); + moduleIdentity &= variableIdentity; + moduleRange &= manager->getRange(variablePair.first); rowColumnMetaVariablePairs.push_back(variablePair); } - moduleToIdentityMap[module.getName()] = moduleIdentity; - moduleToRangeMap[module.getName()] = moduleRange; + moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd(); + moduleToRangeMap[module.getName()] = moduleRange.template toAdd(); } } }; @@ -347,6 +347,7 @@ namespace storm { std::set assignedGlobalVariables; std::set_intersection(assignedVariables.begin(), assignedVariables.end(), generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); + int index = 0; // All unassigned boolean variables need to keep their value. for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) { @@ -369,14 +370,14 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) { STORM_LOG_TRACE("Translating guard " << command.getGuardExpression()); - storm::dd::Add guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; - STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); + storm::dd::Add guard = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; + STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); - if (!guardDd.isZero()) { + if (!guard.isZero()) { // Create the DDs representing the individual updates. std::vector updateResults; for (storm::prism::Update const& update : command.getUpdates()) { - updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guardDd, update)); + updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guard, update)); STORM_LOG_WARN_COND(!updateResults.back().updateDd.isZero(), "Update '" << update << "' does not have any effect."); } @@ -412,7 +413,7 @@ namespace storm { commandDd += updateResultsIt->updateDd * probabilityDd; } - return ActionDecisionDiagram(guardDd, guardDd * commandDd, globalVariablesInSomeUpdate); + return ActionDecisionDiagram(guard, guard * commandDd, globalVariablesInSomeUpdate); } else { return ActionDecisionDiagram(*generationInfo.manager); } @@ -516,7 +517,7 @@ namespace storm { STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards."); allGuards += commandDd.guardDd; - allCommands += commandDd.guardDd * commandDd.transitionsDd ; + allCommands += commandDd.guardDd * commandDd.transitionsDd; } return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables); @@ -1028,6 +1029,7 @@ namespace storm { SystemResult system = createSystemDecisionDiagram(generationInfo); storm::dd::Add transitionMatrix = system.allTransitionsDd; + ModuleDecisionDiagram const& globalModule = system.globalModule; storm::dd::Add stateActionDd = system.stateActionDd; @@ -1073,7 +1075,7 @@ namespace storm { storm::dd::Add reachableStatesAdd = reachableStates.template toAdd(); transitionMatrix *= reachableStatesAdd; stateActionDd *= reachableStatesAdd; - + // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); storm::dd::Add deadlockStates = (reachableStates && !statesWithTransition).template toAdd(); @@ -1172,11 +1174,9 @@ namespace storm { do { STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); changed = false; - storm::dd::Bdd tmp = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables); - tmp = tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); - + storm::dd::Bdd tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables); storm::dd::Bdd newReachableStates = tmp && (!reachableStates); - + // Check whether new states were indeed discovered. if (!newReachableStates.isZero()) { changed = true; @@ -1189,9 +1189,10 @@ namespace storm { return reachableStates; } - // Explicitly instantiate the symbolic expression adapter + // Explicitly instantiate the symbolic model builder. template class DdPrismModelBuilder; - + template class DdPrismModelBuilder; + } // namespace adapters } // namespace storm diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp index 0dadb25c7..64c3868d3 100644 --- a/src/models/symbolic/Ctmc.cpp +++ b/src/models/symbolic/Ctmc.cpp @@ -33,6 +33,7 @@ namespace storm { // Explicitly instantiate the template class. template class Ctmc; + template class Ctmc; } // namespace symbolic } // namespace models diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp index 5fbf90d77..ed6ff3f4a 100644 --- a/src/models/symbolic/DeterministicModel.cpp +++ b/src/models/symbolic/DeterministicModel.cpp @@ -29,6 +29,7 @@ namespace storm { // Explicitly instantiate the template class. template class DeterministicModel; + template class DeterministicModel; } // namespace symbolic } // namespace models diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp index 598112aa5..443577dae 100644 --- a/src/models/symbolic/Dtmc.cpp +++ b/src/models/symbolic/Dtmc.cpp @@ -28,6 +28,7 @@ namespace storm { // Explicitly instantiate the template class. template class Dtmc; + template class Dtmc; } // namespace symbolic } // namespace models diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp index a6559ce44..4c68e0f44 100644 --- a/src/models/symbolic/Mdp.cpp +++ b/src/models/symbolic/Mdp.cpp @@ -28,7 +28,8 @@ namespace storm { } // Explicitly instantiate the template class. - template class Mdp; + template class Mdp; + template class Mdp; } // namespace symbolic } // namespace models diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 3d73aed35..9840a3188 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -228,7 +228,9 @@ namespace storm { } // Explicitly instantiate the template class. - template class Model; + template class Model; + template class Model; + } // namespace symbolic } // namespace models } // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index 2c8ff52f5..2eac2ccf5 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -69,6 +69,7 @@ namespace storm { // Explicitly instantiate the template class. template class NondeterministicModel; + template class NondeterministicModel; } // namespace symbolic } // namespace models diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp index dfef2a2a9..f97caf293 100644 --- a/src/models/symbolic/StandardRewardModel.cpp +++ b/src/models/symbolic/StandardRewardModel.cpp @@ -152,6 +152,7 @@ namespace storm { } template class StandardRewardModel; + template class StandardRewardModel; } } } \ No newline at end of file diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index 5986e9ce7..6d8183a61 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -40,7 +40,8 @@ namespace storm { } // Explicitly instantiate the template class. - template class StochasticTwoPlayerGame; + template class StochasticTwoPlayerGame; + template class StochasticTwoPlayerGame; } // namespace symbolic } // namespace models diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 882471d8c..c37b3b223 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -142,6 +142,23 @@ namespace storm { return Bdd(this->getDdManager(), internalBdd.restrict(constraint), Dd::joinMetaVariables(*this, constraint)); } + template + Bdd Bdd::relationalProduct(Bdd const& relation, std::set const& rowMetaVariables) const { + std::set tmpMetaVariables = Dd::joinMetaVariables(*this, relation); + std::set newMetaVariables; + std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin())); + + std::vector> rowVariables; + for (auto const& metaVariable : rowMetaVariables) { + DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + for (auto const& ddVariable : variable.getDdVariables()) { + rowVariables.push_back(ddVariable); + } + } + + return Bdd(this->getDdManager(), internalBdd.relationalProduct(relation, rowVariables), newMetaVariables); + } + template Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 85504708c..3ce2b295a 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -186,6 +186,15 @@ namespace storm { */ Bdd restrict(Bdd const& constraint) const; + /*! + * Computes the relational product of the current BDD and the given BDD representing a relation. + * + * @param relation The relation to use. + * @param rowMetaVariables The row meta variables used in the relation. + * @return The ralational product. + */ + Bdd relationalProduct(Bdd const& relation, std::set const& rowMetaVariables) const; + /*! * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have * the same number of underlying BDD variables. diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 2c39523a5..21250df39 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -7,6 +7,8 @@ #include "src/storage/BitVector.h" +#include + namespace storm { namespace dd { InternalBdd::InternalBdd(InternalDdManager const* ddManager, cudd::BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) { @@ -27,6 +29,24 @@ namespace storm { return !(*this == other); } + InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const { + InternalBdd cube = ddManager->getBddOne(); + for (auto const& variable : rowVariables) { + cube &= variable; + } + + InternalBdd result = this->andExists(relation, cube); + + // Create the corresponding "from" vector for the variable swap. + std::vector> columnVariables; + for (auto const& variable : rowVariables) { + columnVariables.push_back(InternalBdd(ddManager, ddManager->getCuddManager().bddVar(variable.getIndex() + 1))); + } + result = result.swapVariables(rowVariables, columnVariables); + + return result; + } + InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { return InternalBdd(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd())); } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 7d446e2ab..8a904424f 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -76,6 +76,15 @@ namespace storm { */ bool operator!=(InternalBdd const& other) const; + /*! + * Computes the relational product of the current BDD and the given BDD representing a relation. + * + * @param relation The relation to use. + * @param rowVariables The row variables of the relation represented as individual BDDs. + * @return The ralational product. + */ + InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const; + /*! * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero * function value to the function values specified by the first DD and all others to the function values diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index da1064dd5..1c30f59b5 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -166,11 +166,11 @@ namespace storm { InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromIndices; std::vector toIndices; - uint_fast64_t var = 0; for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromIndices.push_back(it1->getIndex()); + fromIndices.push_back(it2->getIndex()); toIndices.push_back(it2->getIndex()); - ++var; + toIndices.push_back(it1->getIndex()); } return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices)); } diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 6f4cc610c..4b1e089c6 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -8,6 +8,9 @@ #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" + +#include + namespace storm { namespace dd { InternalBdd::InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) { @@ -27,6 +30,10 @@ namespace storm { return sylvanBdd != other.sylvanBdd; } + InternalBdd InternalBdd::relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { return InternalBdd(ddManager, this->sylvanBdd.Ite(thenDd.sylvanBdd, elseDd.sylvanBdd)); } @@ -95,7 +102,9 @@ namespace storm { std::vector toIndices; for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { fromIndices.push_back(it1->getIndex()); + fromIndices.push_back(it2->getIndex()); toIndices.push_back(it2->getIndex()); + toIndices.push_back(it1->getIndex()); } return InternalBdd(ddManager, this->sylvanBdd.Permute(fromIndices, toIndices)); } diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index 3e294d031..610b678c0 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -65,6 +65,15 @@ namespace storm { */ bool operator!=(InternalBdd const& other) const; + /*! + * Computes the relational product of the current BDD and the given BDD representing a relation. + * + * @param relation The relation to use. + * @param rowVariables The row variables of the relation represented as individual BDDs. + * @return The ralational product. + */ + InternalBdd relationalProduct(InternalBdd const& relation, std::vector> const& rowVariables) const; + /*! * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero * function value to the function values specified by the first DD and all others to the function values diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index dbf8c60d6..030226d69 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -10,7 +10,36 @@ #include "src/parser/PrismParser.h" #include "src/builder/DdPrismModelBuilder.h" -TEST(DdPrismModelBuilderTest, Dtmc) { +TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + + // FIXME: re-enable as soon as sylvan ADD-iterator is done. +// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); +// model = storm::builder::DdPrismModelBuilder::translateProgram(program); +// EXPECT_EQ(677ul, model->getNumberOfStates()); +// EXPECT_EQ(867ul, model->getNumberOfTransitions()); + +// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); +// model = storm::builder::DdPrismModelBuilder::translateProgram(program); +// EXPECT_EQ(8607ul, model->getNumberOfStates()); +// EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(273ul, model->getNumberOfStates()); + EXPECT_EQ(397ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(1728ul, model->getNumberOfStates()); + EXPECT_EQ(2505ul, model->getNumberOfTransitions()); +} + +TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); @@ -21,24 +50,55 @@ TEST(DdPrismModelBuilderTest, Dtmc) { model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } -TEST(DdPrismModelBuilderTest, Ctmc) { +TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { + // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. + std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); + + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(276ul, model->getNumberOfStates()); + EXPECT_EQ(1120ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(3478ul, model->getNumberOfStates()); + EXPECT_EQ(14639ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(22ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(810ul, model->getNumberOfStates()); + EXPECT_EQ(3699ul, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(66ul, model->getNumberOfStates()); + EXPECT_EQ(189ul, model->getNumberOfTransitions()); +} + +TEST(DdPrismModelBuilderTest_Cudd, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); @@ -69,7 +129,70 @@ TEST(DdPrismModelBuilderTest, Ctmc) { EXPECT_EQ(189ul, model->getNumberOfTransitions()); } -TEST(DdPrismModelBuilderTest, Mdp) { +TEST(DdPrismModelBuilderTest_Sylvan, Mdp) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(169ul, mdp->getNumberOfStates()); + EXPECT_EQ(436ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(254ul, mdp->getNumberOfChoices()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(364ul, mdp->getNumberOfStates()); + EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(573ul, mdp->getNumberOfChoices()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(272ul, mdp->getNumberOfStates()); + EXPECT_EQ(492ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(400ul, mdp->getNumberOfChoices()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(1038ul, mdp->getNumberOfStates()); + EXPECT_EQ(1282ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(1054ul, mdp->getNumberOfChoices()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + + EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); + mdp = model->as>(); + + EXPECT_EQ(4093ul, mdp->getNumberOfStates()); + EXPECT_EQ(5585ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(5519ul, mdp->getNumberOfChoices()); + + // FIXME: re-enable after Sylvan ADD iterator is done. +// program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); +// model = storm::builder::DdPrismModelBuilder::translateProgram(program); +// +// EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp); +// mdp = model->as>(); +// +// EXPECT_EQ(37ul, mdp->getNumberOfStates()); +// EXPECT_EQ(59ul, mdp->getNumberOfTransitions()); +// EXPECT_EQ(59ul, mdp->getNumberOfChoices()); +} + +TEST(DdPrismModelBuilderTest_Cudd, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program);