From 3919f90712151af52d484b3d6a5f5f5f8a4876dd Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 2 Jun 2016 23:09:42 +0200 Subject: [PATCH] started debugging JANI MDP building Former-commit-id: b122d605be42e7e13659ba8f441922e725888061 --- src/builder/DdJaniModelBuilder.cpp | 104 +++++++----- src/builder/DdPrismModelBuilder.cpp | 5 + src/storage/prism/Program.cpp | 4 +- .../builder/DdJaniModelBuilderTest.cpp | 150 ++++++++++++++++++ .../builder/DdPrismModelBuilderTest.cpp | 2 + 5 files changed, 224 insertions(+), 41 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index b2c76e174..d76da2f74 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -169,8 +169,10 @@ namespace storm { std::map actionVariablesMap; // The meta variables used to encode the remaining nondeterminism. - std::vector orderedNondeterminismVariables; - std::set nondeterminismVariables; + std::vector localNondeterminismVariables; + + // The meta variables used to encode the actions and nondeterminism. + std::set allNondeterminismVariables; // DDs representing the identity for each variable. std::map> variableToIdentityMap; @@ -234,10 +236,21 @@ namespace storm { CompositionVariables createVariables() { CompositionVariables result; + for (auto const& automaton : this->model.getAutomata()) { + // Start by creating a meta variable for the location of the automaton. + std::pair variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); + result.automatonToLocationVariableMap[automaton.getName()] = variablePair; + + // Add the location variable to the row/column variables. + result.rowMetaVariables.insert(variablePair.first); + result.columnMetaVariables.insert(variablePair.second); + } + for (auto const& action : this->model.getActions()) { if (this->model.getActionIndex(action.getName()) != this->model.getSilentActionIndex()) { std::pair variablePair = result.manager->addMetaVariable(action.getName()); result.actionVariablesMap[this->model.getActionIndex(action.getName())] = variablePair.first; + result.allNondeterminismVariables.insert(variablePair.first); } } @@ -248,18 +261,8 @@ namespace storm { } for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { std::pair variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i)); - result.orderedNondeterminismVariables.push_back(variablePair.first); - result.nondeterminismVariables.insert(variablePair.first); - } - - for (auto const& automaton : this->model.getAutomata()) { - // Start by creating a meta variable for the location of the automaton. - std::pair variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1); - result.automatonToLocationVariableMap[automaton.getName()] = variablePair; - - // Add the location variable to the row/column variables. - result.rowMetaVariables.insert(variablePair.first); - result.columnMetaVariables.insert(variablePair.second); + result.localNondeterminismVariables.push_back(variablePair.first); + result.allNondeterminismVariables.insert(variablePair.first); } // Create global variables. @@ -652,11 +655,16 @@ namespace storm { // Add the source location and the guard. transitionsDd *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationId()).template toAdd() * guard; - // If we Multiply the ranges of global variables if we wrote at least one to make sure everything stays within its bounds. + // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeUpdate.empty()) { transitionsDd *= variables.globalVariableRanges; } + // If the edge has a rate, we multiply it to the DD. + if (edge.hasRate()) { + transitionsDd *= variables.rowExpressionAdapter->translateExpression(edge.getRate()); + } + return EdgeDd(guard, transitionsDd, globalVariablesInSomeUpdate); } else { return EdgeDd(variables.manager->template getAddZero(), variables.manager->template getAddZero()); @@ -689,13 +697,15 @@ namespace storm { }; template - storm::dd::Add encodeAction(uint64_t trueIndex, std::vector const& actionVariables, CompositionVariables const& variables) { - storm::dd::Add encoding = variables.manager->template getAddZero(); - - trueIndex = actionVariables.size() - (trueIndex + 1); + storm::dd::Add encodeAction(boost::optional trueIndex, std::vector const& actionVariables, CompositionVariables const& variables) { + storm::dd::Add encoding = variables.manager->template getAddOne(); + + if (trueIndex) { + *trueIndex = actionVariables.size() - (*trueIndex + 1); + } uint64_t index = 0; for (auto it = actionVariables.rbegin(), ite = actionVariables.rend(); it != ite; ++it, ++index) { - if (index == trueIndex) { + if (trueIndex && index == trueIndex) { encoding *= variables.manager->getEncoding(*it, 1).template toAdd(); } else { encoding *= variables.manager->getEncoding(*it, 0).template toAdd(); @@ -717,17 +727,17 @@ namespace storm { } template - storm::dd::Add encodeIndex(uint64_t index, std::vector const& orderedNondeterminismVariables, CompositionVariables const& variables) { + storm::dd::Add encodeIndex(uint64_t index, std::vector const& localNondeterminismVariables, CompositionVariables const& variables) { storm::dd::Add result = variables.manager->template getAddZero(); - STORM_LOG_TRACE("Encoding " << index << " with " << orderedNondeterminismVariables.size() << " binary variable(s)."); + STORM_LOG_TRACE("Encoding " << index << " with " << localNondeterminismVariables.size() << " binary variable(s)."); std::map metaVariableNameToValueMap; - for (uint_fast64_t i = 0; i < orderedNondeterminismVariables.size(); ++i) { - if (index & (1ull << (orderedNondeterminismVariables.size() - i - 1))) { - metaVariableNameToValueMap.emplace(orderedNondeterminismVariables[i], 1); + for (uint_fast64_t i = 0; i < localNondeterminismVariables.size(); ++i) { + if (index & (1ull << (localNondeterminismVariables.size() - i - 1))) { + metaVariableNameToValueMap.emplace(localNondeterminismVariables[i], 1); } else { - metaVariableNameToValueMap.emplace(orderedNondeterminismVariables[i], 0); + metaVariableNameToValueMap.emplace(localNondeterminismVariables[i], 0); } } @@ -753,17 +763,28 @@ namespace storm { // Determine how many nondeterminism variables we need. std::vector orderedActionVariables; std::set actionVariables; - std::map actionIndexToVariableIndex; + std::map> actionIndexToVariableIndex; uint64_t maximalNumberOfEdgesPerAction = 0; for (auto const& action : automatonDd.actionIndexToEdges) { - orderedActionVariables.push_back(variables.actionVariablesMap.at(action.first)); - actionVariables.insert(orderedActionVariables.back()); - actionIndexToVariableIndex[action.first] = orderedActionVariables.size() - 1; + if (action.first != model.getSilentActionIndex()) { + orderedActionVariables.push_back(variables.actionVariablesMap.at(action.first)); + actionVariables.insert(orderedActionVariables.back()); + actionIndexToVariableIndex[action.first] = orderedActionVariables.size() - 1; + } else { + actionIndexToVariableIndex[action.first] = boost::none; + } maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast(action.second.size())); } + + // If the maximal number of edges per action is zero, which can happen if the model only has unsatisfiable guards, + // then we must not compute the number of variables. + if (maximalNumberOfEdgesPerAction == 0) { + return SystemDd(variables.manager->template getAddZero(), variables.manager->template getAddZero(), 0); + } + uint64_t numberOfNondeterminismVariables = static_cast(std::ceil(std::log2(maximalNumberOfEdgesPerAction))); - std::vector orderedNondeterminismVariables(numberOfNondeterminismVariables); - std::copy(variables.orderedNondeterminismVariables.begin(), variables.orderedNondeterminismVariables.begin() + numberOfNondeterminismVariables, orderedNondeterminismVariables.begin()); + std::vector localNondeterminismVariables(numberOfNondeterminismVariables); + std::copy(variables.localNondeterminismVariables.begin(), variables.localNondeterminismVariables.begin() + numberOfNondeterminismVariables, localNondeterminismVariables.begin()); // Prepare result. storm::dd::Add result = variables.manager->template getAddZero(); @@ -774,7 +795,9 @@ namespace storm { uint64_t edgeIndex = 0; for (auto const& edge : action.second) { - edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, orderedNondeterminismVariables, variables); + storm::dd::Add dd = edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, localNondeterminismVariables, variables); + dd.exportToDot("add" + std::to_string(edgeIndex) + ".dot"); + edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, localNondeterminismVariables, variables); ++edgeIndex; } @@ -812,7 +835,7 @@ namespace storm { } else if (modelType == storm::jani::ModelType::CTMC) { return std::shared_ptr>(new storm::models::symbolic::Ctmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); } else if (modelType == storm::jani::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.nondeterminismVariables, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map(), modelComponents.rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } @@ -822,10 +845,10 @@ namespace storm { template void postprocessSystemAndVariables(storm::jani::Model const& model, SystemDd& system, CompositionVariables& variables, typename DdJaniModelBuilder::Options const& options) { // Get rid of the nondeterminism variables that were not used. - for (uint64_t index = system.numberOfNondeterminismVariables; index < variables.orderedNondeterminismVariables.size(); ++index) { - variables.nondeterminismVariables.erase(variables.orderedNondeterminismVariables[index]); + for (uint64_t index = system.numberOfNondeterminismVariables; index < variables.localNondeterminismVariables.size(); ++index) { + variables.allNondeterminismVariables.erase(variables.localNondeterminismVariables[index]); } - variables.orderedNondeterminismVariables.resize(system.numberOfNondeterminismVariables); + variables.localNondeterminismVariables.resize(system.numberOfNondeterminismVariables); // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { @@ -899,7 +922,7 @@ namespace storm { for (auto const& variable : variables.actionVariablesMap) { action *= variables.manager->template getIdentity(variable.second); } - for (auto const& variable : variables.orderedNondeterminismVariables) { + for (auto const& variable : variables.localNondeterminismVariables) { action *= variables.manager->template getIdentity(variable); } transitionMatrix += deadlockStates * globalIdentity * action; @@ -933,9 +956,12 @@ namespace storm { modelComponents.initialStates = computeInitialStates(*this->model, variables); // Perform reachability analysis to obtain reachable states. + system.transitionsDd.exportToDot("trans.dot"); + std::cout << "nnz: " << system.transitionsDd.getNonZeroCount() << std::endl; + std::cout << "size: " << system.transitionsDd.getNodeCount() << std::endl; storm::dd::Bdd transitionMatrixBdd = system.transitionsDd.notZero(); if (this->model->getModelType() == storm::jani::ModelType::MDP) { - transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.nondeterminismVariables); + transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables); } modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index ab9e01f93..db2567e2c 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1324,6 +1324,11 @@ namespace storm { // Cut the transitions and rewards to the reachable fragment of the state space. storm::dd::Bdd initialStates = createInitialStatesDecisionDiagram(generationInfo); + + transitionMatrix.exportToDot("trans_prism.dot"); + std::cout << "nnz: " << transitionMatrix.getNonZeroCount() << std::endl; + std::cout << "size: " << transitionMatrix.getNodeCount() << std::endl; + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); if (program.getModelType() == storm::prism::Program::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 66758a72e..b7b080a48 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1560,7 +1560,7 @@ namespace storm { automaton.addBoundedIntegerVariable(newIntegerVariable); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; - } else if (!accessingModuleIndices.empty()) { + } else { //if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. janiModel.addBoundedIntegerVariable(newIntegerVariable); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); @@ -1575,7 +1575,7 @@ namespace storm { automaton.addBooleanVariable(newBooleanVariable); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; - } else if (!accessingModuleIndices.empty()) { + } else { //if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. janiModel.addBooleanVariable(newBooleanVariable); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 9d05bae3c..24c372693 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -170,4 +170,154 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) { model = builder.translate(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); +} + +TEST(DdJaniModelBuilderTest_Sylvan, Mdp) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::jani::Model janiModel = program.toJani(true); + storm::builder::DdJaniModelBuilder builder(janiModel); + std::shared_ptr> model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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(DdJaniModelBuilderTest_Cudd, Mdp) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + storm::jani::Model janiModel = program.toJani(true); + storm::builder::DdJaniModelBuilder builder(janiModel); + std::shared_ptr> model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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()); + + exit(-1); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); + janiModel = program.toJani(true); + builder = storm::builder::DdJaniModelBuilder(janiModel); + model = builder.translate(); + + 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()); } \ No newline at end of file diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index ccf16c1ff..bfaffc1f3 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -210,6 +210,8 @@ TEST(DdPrismModelBuilderTest_Cudd, Mdp) { EXPECT_EQ(364ul, mdp->getNumberOfStates()); EXPECT_EQ(654ul, mdp->getNumberOfTransitions()); EXPECT_EQ(573ul, mdp->getNumberOfChoices()); + + exit(-1); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); model = storm::builder::DdPrismModelBuilder().translateProgram(program);