From 7d1829aefa40f1ec3f719af2d648d8463beb0e6c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Feb 2015 19:40:25 +0100 Subject: [PATCH] More work on DD-based model generation. Former-commit-id: f6f37bd52181e6a2d2ea0fe58318a6d973a7875d --- src/builder/DdPrismModelBuilder.cpp | 145 ++++++++++---------------- src/builder/DdPrismModelBuilder.h | 14 ++- src/storage/prism/BooleanVariable.cpp | 2 +- 3 files changed, 70 insertions(+), 91 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index cf6e42fb5..4f867f447 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -100,8 +100,8 @@ namespace storm { // All unassigned boolean variables need to keep their value. for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) { - storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable()); + storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable()); + if (assignedVariables.find(metaVariable) == assignedVariables.end()) { STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName()); updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable()); } @@ -138,6 +138,9 @@ namespace storm { commandDd += updateDd; } + guardDd.exportToDot(module.getName() + "_cmd_" + std::to_string(command.getGlobalIndex()) + "_grd.dot"); + commandDd.exportToDot(module.getName() + "_cmd_" + std::to_string(command.getGlobalIndex()) + ".dot"); + return ActionDecisionDiagram(guardDd, guardDd * commandDd); } else { return ActionDecisionDiagram(*generationInfo.manager); @@ -360,6 +363,7 @@ namespace storm { // Create module DD for all synchronizing actions of the module. std::map actionIndexToDdMap; for (auto const& actionIndex : module.getActionIndices()) { + STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'."); actionIndexToDdMap.emplace(actionIndex, createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex))); } @@ -443,15 +447,19 @@ namespace storm { } // Start by creating DDs for the first module. + STORM_LOG_TRACE("Translating (first) module '" << generationInfo.program.getModule(0).getName() << "'."); ModuleDecisionDiagram system = createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(0), synchronizingActionToOffsetMap); // No translate module by module and combine it with the system created thus far. for (uint_fast64_t i = 1; i < generationInfo.program.getNumberOfModules(); ++i) { storm::prism::Module const& currentModule = generationInfo.program.getModule(i); + STORM_LOG_TRACE("Translating module '" << currentModule.getName() << "'."); // Update the offset index. for (auto const& actionIndex : generationInfo.program.getActionIndices()) { - synchronizingActionToOffsetMap[actionIndex] = system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; + if (system.hasSynchronizingAction(actionIndex)) { + synchronizingActionToOffsetMap[actionIndex] = system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; + } } ModuleDecisionDiagram nextModule = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap); @@ -461,10 +469,11 @@ namespace storm { // Combine synchronizing actions. for (auto const& actionIndex : currentModule.getActionIndices()) { + std::cout << "treating action index " << actionIndex << std::endl; if (system.hasSynchronizingAction(actionIndex)) { system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]); } else { - system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, nextModule.identity); + system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, ActionDecisionDiagram(*generationInfo.manager), nextModule.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, nextModule.identity); } } @@ -494,11 +503,12 @@ namespace storm { preparedProgram = preparedProgram.substituteConstants(); + std::cout << "translated prog: " << preparedProgram << std::endl; + // Start by initializing the structure used for storing all information needed during the model generation. // In particular, this creates the meta variables used to encode the model. GenerationInformation generationInfo(preparedProgram); - auto clock = std::chrono::high_resolution_clock::now(); storm::dd::Dd transitionMatrix = createSystemDecisionDiagram(generationInfo); std::cout << "Built transition matrix in " << std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl; @@ -508,7 +518,9 @@ namespace storm { storm::dd::Dd initialStates = createInitialStatesDecisionDiagram(generationInfo); std::cout << "initial states: " << initialStates.getNonZeroCount() << std::endl; - + storm::dd::Dd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrix); + std::cout << "reachable states: " << reachableStates.getNonZeroCount() << std::endl; + exit(-1); } template @@ -522,88 +534,45 @@ namespace storm { return initialStates; } -// template -// storm::dd::Dd DdPrismModelBuilder::performReachability(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions) { -// storm::dd::Dd reachableStates = initialStates; -// -// // Copy current state -// storm::dd::Dd newReachableStates = reachableStates; -// -// std::set abstractVariables = std::set(); -// -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// // Synchronizing variables -// if (systemDd.containsMetaVariable("sync" + std::to_string(i))) { -// abstractVariables.insert("sync" + std::to_string(i)); -// } -// } -// for (uint_fast64_t i = 1; i <= generationInfo.numberOfNondetVariables; ++i) { -// // Nondet. variables -// if (systemDd.containsMetaVariable("nondet" + std::to_string(i))) { -// abstractVariables.insert("nondet" + std::to_string(i)); -// } -// } -// } -// -// // Create system BDD -// storm::dd::Dd systemBdd = systemDd.notZero(); -// -// // For MDPs, we need to abstract from the nondeterminism variables, but we can do so prior to the -// // reachability analysis. -// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { -// // Abstract from synchronizing and nondet. variables (MDPs) -// systemBdd = systemBdd.existsAbstract(abstractVariables); -// } -// -// // Initialize variables and choose option -// bool changed; -// int iter = 0; -// int option = storm::settings::adapterSettings().getReachabilityMethod(); -// -// //TODO: Name reachability options. -// std::cout << "Reachability option: " << option << std::endl; -// -// if (option == 3 || option == 4){ -// -// S = storm::dd::Dd(initialStateDd); -// U = storm::dd::Dd(initialStateDd); -// -// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.notZero(); -// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.existsAbstract(abstractVariables); -// -// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { -// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.notZero(); -// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.existsAbstract(abstractVariables); -// } -// } -// -// // Perform updates until nothing changes -// do { -// if (option == 1){ -// iter++; -// changed = true; -// -// newReachableStates = newReachableStates * systemBdd; -// -// // Abstract from row meta variables -// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames); -// -// // Swap column variables to row variables -// newReachableStates.swapVariables(generationInfo.metaVariablePairs); -// -// newReachableStates = newReachableStates * (!reachableStates); -// -// // Check if something has changed -// if (newReachableStates.isZero()) { -// changed = false; -// } -// -// // Update reachableStates DD -// reachableStates = reachableStates + newReachableStates; -// -// -// } + template + storm::dd::Dd DdPrismModelBuilder::computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions) { + storm::dd::Dd reachableStatesBdd = initialStates.notZero(); + + // If the model is an MDP, we can abstract from the variables encoding the nondeterminism in the model. + storm::dd::Dd transitionBdd = transitions.notZero(); + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + std::set abstractVariables; + abstractVariables.insert(generationInfo.synchronizationMetaVariables.begin(), generationInfo.synchronizationMetaVariables.end()); + abstractVariables.insert(generationInfo.nondeterminismMetaVariables.begin(), generationInfo.nondeterminismMetaVariables.end()); + transitionBdd = transitionBdd.existsAbstract(abstractVariables); + } + + transitionBdd.exportToDot("trans.dot"); + reachableStatesBdd.exportToDot("reach.dot"); + + // Perform the BFS to discover all reachable states. + bool changed = true; + uint_fast64_t iteration = 0; + do { + STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states."); + changed = false; + storm::dd::Dd tmp = reachableStatesBdd * transitionBdd; + tmp = tmp.existsAbstract(generationInfo.rowMetaVariables); + tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs); + + storm::dd::Dd newReachableStates = tmp * (!reachableStatesBdd); + + // Check whether new states were indeed discovered. + if (!newReachableStates.isZero()) { + changed = true; + } + + reachableStatesBdd += newReachableStates; + ++iteration; + } while (changed); + + return reachableStatesBdd; + } // template // storm::dd::Dd SymbolicModelAdapter::createSystemDecisionDiagramm(GenerationInformation & generationInfo){ diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index fa9ebf150..c4caf3a9d 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -125,7 +125,7 @@ namespace storm { */ class GenerationInformation { public: - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() { + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() { // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); @@ -149,6 +149,9 @@ namespace storm { std::map variableToColumnMetaVariableMap; std::unique_ptr> columnExpressionAdapter; + // All pairs of row/column meta variables. + std::vector> rowColumnMetaVariablePairs; + // The meta variables used to encode the nondeterminism. std::vector nondeterminismMetaVariables; @@ -194,6 +197,8 @@ namespace storm { storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + + rowColumnMetaVariablePairs.push_back(variablePair); } for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -208,6 +213,7 @@ namespace storm { storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); + rowColumnMetaVariablePairs.push_back(variablePair); } // Create meta variables for each of the modules' variables. @@ -226,6 +232,8 @@ namespace storm { storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second); variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; + + rowColumnMetaVariablePairs.push_back(variablePair); } for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -242,6 +250,8 @@ namespace storm { storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; + + rowColumnMetaVariablePairs.push_back(variablePair); } moduleToIdentityMap[module.getName()] = moduleIdentity; } @@ -274,7 +284,7 @@ namespace storm { static storm::dd::Dd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); - static storm::dd::Dd performReachability(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions); + static storm::dd::Dd computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions); // /*! // * Calculates the reachable states of the given transition matrix diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index 35df52356..c38812ec6 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -11,7 +11,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { - stream << variable.getName() << ": bool init" << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": bool init " << variable.getInitialValueExpression() << ";"; return stream; }