From 310db8a234c0ca1758e7565002361258577337e6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 1 Jun 2016 23:32:00 +0200 Subject: [PATCH] started to include reachability in JANI model generation Former-commit-id: d54f35b9995d6f681dab8b13f65e8d31d743eb3a --- src/builder/DdJaniModelBuilder.cpp | 143 ++++++++++++++---- src/builder/DdPrismModelBuilder.cpp | 51 ++----- src/builder/DdPrismModelBuilder.h | 2 - src/parser/JaniParser.cpp | 9 +- src/storage/jani/Exporter.cpp | 44 ++++-- src/storage/prism/Program.cpp | 35 ++++- src/utility/dd.cpp | 44 ++++++ src/utility/dd.h | 24 +++ .../builder/DdJaniModelBuilderTest.cpp | 24 +-- .../builder/DdPrismModelBuilderTest.cpp | 6 +- 10 files changed, 284 insertions(+), 98 deletions(-) create mode 100644 src/utility/dd.cpp create mode 100644 src/utility/dd.h diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 430cf658b..013f837dd 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -18,9 +18,14 @@ #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Ctmc.h" #include "src/models/symbolic/Mdp.h" +#include "src/models/symbolic/StandardRewardModel.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/MarkovChainSettings.h" #include "src/utility/macros.h" #include "src/utility/jani.h" +#include "src/utility/dd.h" #include "src/exceptions/InvalidArgumentException.h" namespace storm { @@ -164,7 +169,8 @@ namespace storm { std::map actionVariablesMap; // The meta variables used to encode the remaining nondeterminism. - std::vector nondeterminismVariables; + std::vector orderedNondeterminismVariables; + std::set nondeterminismVariables; // DDs representing the identity for each variable. std::map> variableToIdentityMap; @@ -242,7 +248,8 @@ namespace storm { } for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { std::pair variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i)); - result.nondeterminismVariables.push_back(variablePair.first); + result.orderedNondeterminismVariables.push_back(variablePair.first); + result.nondeterminismVariables.insert(variablePair.first); } // Create global variables. @@ -269,6 +276,10 @@ namespace storm { identity &= variableIdentity.toBdd(); range &= result.manager->getRange(variablePair.first); + // Add the location variable to the row/column variables. + result.rowMetaVariables.insert(variablePair.first); + result.columnMetaVariables.insert(variablePair.second); + // Then create variables for the variables of the automaton. for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { createVariable(variable, result); @@ -687,17 +698,17 @@ namespace storm { } template - storm::dd::Add encodeIndex(uint64_t index, std::vector const& nondeterminismVariables, CompositionVariables const& variables) { + storm::dd::Add encodeIndex(uint64_t index, std::vector const& orderedNondeterminismVariables, CompositionVariables const& variables) { storm::dd::Add result = variables.manager->template getAddZero(); - STORM_LOG_TRACE("Encoding " << index << " with " << nondeterminismVariables.size() << " binary variable(s)."); + STORM_LOG_TRACE("Encoding " << index << " with " << orderedNondeterminismVariables.size() << " binary variable(s)."); std::map metaVariableNameToValueMap; - for (uint_fast64_t i = 0; i < nondeterminismVariables.size(); ++i) { - if (index & (1ull << (nondeterminismVariables.size() - i - 1))) { - metaVariableNameToValueMap.emplace(nondeterminismVariables[i], 1); + for (uint_fast64_t i = 0; i < orderedNondeterminismVariables.size(); ++i) { + if (index & (1ull << (orderedNondeterminismVariables.size() - i - 1))) { + metaVariableNameToValueMap.emplace(orderedNondeterminismVariables[i], 1); } else { - metaVariableNameToValueMap.emplace(nondeterminismVariables[i], 0); + metaVariableNameToValueMap.emplace(orderedNondeterminismVariables[i], 0); } } @@ -717,21 +728,23 @@ namespace storm { }; template - SystemDd buildSystemDd(storm::jani::Model const& model, AutomatonDd const& automatonDd, CompositionVariables const& variables) { + SystemDd buildSystemDd(storm::jani::Model const& model, AutomatonDd const& automatonDd, CompositionVariables& variables) { // If the model is an MDP, we need to encode the nondeterminism using additional variables. if (model.getModelType() == storm::jani::ModelType::MDP) { // Determine how many nondeterminism variables we need. - std::vector actionVariables; + std::vector orderedActionVariables; + std::set actionVariables; std::map actionIndexToVariableIndex; uint64_t maximalNumberOfEdgesPerAction = 0; for (auto const& action : automatonDd.actionIndexToEdges) { - actionVariables.push_back(variables.actionVariablesMap.at(action.first)); - actionIndexToVariableIndex[action.first] = actionVariables.size() - 1; + orderedActionVariables.push_back(variables.actionVariablesMap.at(action.first)); + actionVariables.insert(orderedActionVariables.back()); + actionIndexToVariableIndex[action.first] = orderedActionVariables.size() - 1; maximalNumberOfEdgesPerAction = std::max(maximalNumberOfEdgesPerAction, static_cast(action.second.size())); } uint64_t numberOfNondeterminismVariables = static_cast(std::ceil(std::log2(maximalNumberOfEdgesPerAction))); - std::vector nondeterminismVariables(numberOfNondeterminismVariables); - std::copy(variables.nondeterminismVariables.begin(), variables.nondeterminismVariables.begin() + numberOfNondeterminismVariables, nondeterminismVariables.begin()); + std::vector orderedNondeterminismVariables(numberOfNondeterminismVariables); + std::copy(variables.orderedNondeterminismVariables.begin(), variables.orderedNondeterminismVariables.begin() + numberOfNondeterminismVariables, orderedNondeterminismVariables.begin()); // Prepare result. storm::dd::Add result = variables.manager->template getAddZero(); @@ -742,11 +755,11 @@ namespace storm { uint64_t edgeIndex = 0; for (auto const& edge : action.second) { - edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, nondeterminismVariables, variables); + edgesForAction += edge.transitionsDd * computeMissingGlobalVariableIdentities(edge, variables) * encodeIndex(edgeIndex, orderedNondeterminismVariables, variables); ++edgeIndex; } - result += edgesForAction * encodeAction(actionIndexToVariableIndex.at(action.first), actionVariables, variables); + result += edgesForAction * encodeAction(actionIndexToVariableIndex.at(action.first), orderedActionVariables, variables); } return SystemDd(result, result.sumAbstract(variables.columnMetaVariables), numberOfNondeterminismVariables); @@ -780,7 +793,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.allNondeterminismVariables, 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.nondeterminismVariables, std::map(), modelComponents.rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } @@ -788,13 +801,18 @@ namespace storm { } template - void postprocessSystemDd(storm::jani::Model const& model, SystemDd& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { + 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]); + } + variables.orderedNondeterminismVariables.resize(system.numberOfNondeterminismVariables); + // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { system.transitionsDd = system.transitionsDd / system.stateActionDd; } - // If we were asked to treat some states as terminal states, we cut away their transitions now. if (options.terminalStates || options.negatedTerminalStates) { std::map constantsSubstitution = model.getConstantsSubstitution(); @@ -811,21 +829,68 @@ namespace storm { terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); } - system.transitionMatrix *= (!terminalStatesBdd).template toAdd(); + system.transitionsDd *= (!terminalStatesBdd).template toAdd(); } } template - storm::dd::Bdd computeInitial(storm::jani::Model const& model, CompositionVariables const& variables) { - storm::dd::Bdd initialStates = variables.rowExpressionAdapter->translateExpression( generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd(); - - for (auto const& metaVariable : generationInfo.rowMetaVariables) { - initialStates &= generationInfo.manager->getRange(metaVariable); + storm::dd::Bdd computeInitialStates(storm::jani::Model const& model, CompositionVariables const& variables) { + storm::dd::Bdd initialStates = variables.rowExpressionAdapter->translateExpression(model.getInitialStatesExpression(true)).toBdd(); + for (auto const& automaton : model.getAutomata()) { + initialStates &= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, automaton.getInitialLocationIndex()); + } + for (auto const& metaVariable : variables.rowMetaVariables) { + initialStates &= variables.manager->getRange(metaVariable); } - return initialStates; } + template + void fixDeadlocks(storm::jani::ModelType const& modelType, storm::dd::Add& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& reachableStates, CompositionVariables const& variables) { + // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. + storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(variables.columnMetaVariables); + storm::dd::Add deadlockStates = (reachableStates && !statesWithTransition).template toAdd(); + + if (!deadlockStates.isZero()) { + // If we need to fix deadlocks, we do so now. + if (!storm::settings::getModule().isDontFixDeadlocksSet()) { + STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); + + uint_fast64_t count = 0; + for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) { + STORM_LOG_INFO((*it).first.toPrettyString(variables.rowMetaVariables) << std::endl); + } + + // Create a global identity DD. + storm::dd::Add globalIdentity = variables.manager->template getAddOne(); + for (auto const& identity : variables.automatonToIdentityMap) { + globalIdentity *= identity.second; + } + for (auto const& variable : variables.allGlobalVariables) { + globalIdentity *= variables.variableToIdentityMap.at(variable); + } + + if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) { + // For DTMCs, we can simply add the identity of the global module for all deadlock states. + transitionMatrix += deadlockStates * globalIdentity; + } else if (modelType == storm::jani::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::Add action = variables.manager->template getAddOne(); + for (auto const& variable : variables.actionVariablesMap) { + action *= variables.manager->template getIdentity(variable.second); + } + for (auto const& variable : variables.orderedNondeterminismVariables) { + action *= variables.manager->template getIdentity(variable); + } + transitionMatrix += deadlockStates * globalIdentity * action; + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); + } + } + } + template std::shared_ptr> DdJaniModelBuilder::translate() { // Create all necessary variables. @@ -840,12 +905,34 @@ namespace storm { SystemDd system = buildSystemDd(*this->model, globalAutomaton, variables); // Postprocess the system. This modifies the systemDd in place. - postprocessSystemDd(*this->model, system, variables, options); - + postprocessSystemAndVariables(*this->model, system, variables, options); + // Start creating the model components. ModelComponents modelComponents; + + // Build initial states. + modelComponents.initialStates = computeInitialStates(*this->model, variables); + // Perform reachability analysis to obtain reachable states. + storm::dd::Bdd transitionMatrixBdd = system.transitionsDd.notZero(); + if (this->model->getModelType() == storm::jani::ModelType::MDP) { + transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.nondeterminismVariables); + } + transitionMatrixBdd.template toAdd().exportToDot("trans_before_reach.dot"); + modelComponents.initialStates.template toAdd().exportToDot("initial.dot"); + modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables); + modelComponents.reachableStates.template toAdd().exportToDot("reach.dot"); + + // Cut transitions to reachable states. + storm::dd::Add reachableStatesAdd = modelComponents.reachableStates.template toAdd(); + modelComponents.transitionMatrix = system.transitionsDd * reachableStatesAdd; + system.transitionsDd.exportToDot("trans_full.dot"); + system.stateActionDd *= reachableStatesAdd; + + // Fix deadlocks if existing. + // fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables); + // Finally, create the model. return createModel(this->model->getModelType(), variables, modelComponents); } diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 371a3837a..ab9e01f93 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -7,7 +7,6 @@ #include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" -#include "src/storage/dd/DdManager.h" #include "src/settings/SettingsManager.h" #include "src/exceptions/InvalidStateException.h" @@ -16,9 +15,11 @@ #include "src/utility/prism.h" #include "src/utility/math.h" +#include "src/utility/dd.h" + +#include "src/storage/dd/DdManager.h" #include "src/storage/prism/Program.h" #include "src/storage/prism/Compositions.h" - #include "src/storage/dd/Add.h" #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/storage/dd/Bdd.h" @@ -1328,7 +1329,7 @@ namespace storm { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); } - storm::dd::Bdd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd); + storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionMatrixBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); storm::dd::Add reachableStatesAdd = reachableStates.template toAdd(); transitionMatrix *= reachableStatesAdd; stateActionDd *= reachableStatesAdd; @@ -1347,17 +1348,23 @@ namespace storm { STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl); } - if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { + if (program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC) { + storm::dd::Add identity = globalModule.identity; + + // Make sure that global variables do not change along the introduced self-loops. + for (auto const& var : generationInfo.allGlobalVariables) { + identity *= generationInfo.variableToIdentityMap.at(var); + } + // For DTMCs, we can simply add the identity of the global module for all deadlock states. - transitionMatrix += deadlockStates * globalModule.identity; + transitionMatrix += deadlockStates * identity; } 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::Add action = generationInfo.manager->template getAddOne(); - std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), - [&action, &generationInfo] (storm::expressions::Variable const& metaVariable) { - action *= generationInfo.manager->template getIdentity(metaVariable); - }); + for (auto const& metaVariable : generationInfo.allNondeterminismVariables) { + action *= generationInfo.manager->template getIdentity(metaVariable); + } // Make sure that global variables do not change along the introduced self-loops. for (auto const& var : generationInfo.allGlobalVariables) { action *= generationInfo.variableToIdentityMap.at(var); @@ -1421,32 +1428,6 @@ namespace storm { return initialStates; } - template - storm::dd::Bdd DdPrismModelBuilder::computeReachableStates(GenerationInformation& generationInfo, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionBdd) { - storm::dd::Bdd reachableStates = initialStates; - - // Perform the BFS to discover all reachable states. - bool changed = true; - uint_fast64_t iteration = 0; - do { - STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); - changed = false; - storm::dd::Bdd tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables); - storm::dd::Bdd newReachableStates = tmp && (!reachableStates); - - // Check whether new states were indeed discovered. - if (!newReachableStates.isZero()) { - changed = true; - } - - reachableStates |= newReachableStates; - - ++iteration; - } while (changed); - - return reachableStates; - } - // Explicitly instantiate the symbolic model builder. template class DdPrismModelBuilder; template class DdPrismModelBuilder; diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 9de5cf2df..22733ba29 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -256,8 +256,6 @@ namespace storm { static SystemResult createSystemDecisionDiagram(GenerationInformation& generationInfo); static storm::dd::Bdd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); - - static storm::dd::Bdd computeReachableStates(GenerationInformation& generationInfo, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions); // This member holds the program that was most recently translated (if any). boost::optional preparedProgram; diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index f23aa306c..72655906e 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -104,10 +104,12 @@ namespace storm { // TODO something. } else if(variableStructure.at("type") == "bool") { STORM_LOG_THROW(initExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for Boolean variable " << name << " (scope: " << scopeDescription << ") should have Boolean type."); - return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initExpr); + // TODO: reenable and put initExpr in the place where it belongs. +// return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initExpr); } else if(variableStructure.at("type") == "int") { STORM_LOG_THROW(initExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for interger variable " << name << " (scope: " << scopeDescription << ") should have integer type."); - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initExpr); + // TODO: reenable and put initExpr in the place where it belongs. +// return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initExpr); } else { // TODO clocks. STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); @@ -129,7 +131,8 @@ namespace storm { if(basictype == "int") { STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr, initExpr); + // TODO: reenable and put initExpr in the place where it belongs. +// return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr, initExpr); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); } diff --git a/src/storage/jani/Exporter.cpp b/src/storage/jani/Exporter.cpp index 643099b78..bf7eb6c00 100644 --- a/src/storage/jani/Exporter.cpp +++ b/src/storage/jani/Exporter.cpp @@ -88,10 +88,6 @@ namespace storm { out << ","; clearLine(out); appendIndent(out, indent); - appendField(out, "initial-value"); - appendValue(out, expressionToString(variable.getInitialValue())); - clearLine(out); - appendIndent(out, indent); out << "}"; } @@ -137,10 +133,6 @@ namespace storm { appendBoundedIntegerVariableType(out, variable, indent + 2); out << ","; clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "initial-value"); - appendValue(out, expressionToString(variable.getInitialValue())); - clearLine(out); appendIndent(out, indent); out << "}"; } @@ -159,10 +151,6 @@ namespace storm { appendValue(out, "int"); out << ","; clearLine(out); - appendIndent(out, indent + 1); - appendField(out, "initial-value"); - appendValue(out, expressionToString(variable.getInitialValue())); - clearLine(out); appendIndent(out, indent); out << "}"; } @@ -359,6 +347,21 @@ namespace storm { appendField(out, "initial-location"); appendValue(out, std::to_string(automaton.getInitialLocationIndex())); clearLine(out); + if (automaton.hasInitialStatesExpression()) { + appendIndent(out, indent + 1); + appendField(out, "initial-states"); + clearLine(out); + appendIndent(out, indent + 2); + out << "{"; + clearLine(out); + appendIndent(out, indent + 3); + appendField(out, "exp"); + appendValue(out, expressionToString(automaton.getInitialStatesExpression())); + clearLine(out); + appendIndent(out, indent + 2); + out << "}"; + clearLine(out); + } appendEdges(out, model, automaton, indent + 1); @@ -401,6 +404,23 @@ namespace storm { clearLine(out); appendVariables(out, model.getGlobalVariables(), 1); clearLine(out); + + if (model.hasInitialStatesExpression()) { + appendIndent(out, 1); + appendField(out, "initial-states"); + clearLine(out); + appendIndent(out, 2); + out << "{"; + clearLine(out); + appendIndent(out, 3); + appendField(out, "exp"); + appendValue(out, expressionToString(model.getInitialStatesExpression())); + clearLine(out); + appendIndent(out, 2); + out << "}"; + clearLine(out); + } + appendAutomata(out, model, 1); clearLine(out); out << "}" << std::endl; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 57d870b07..ef0b32909 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1494,7 +1494,8 @@ namespace storm { default: modelType = storm::jani::ModelType::UNDEFINED; } storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager); - + storm::expressions::Expression globalInitialStatesExpression; + // Add all constants of the PRISM program to the JANI model. for (auto const& constant : constants) { janiModel.addConstant(storm::jani::Constant(constant.getName(), constant.getExpressionVariable(), constant.isDefined() ? boost::optional(constant.getExpression()) : boost::none)); @@ -1502,10 +1503,14 @@ namespace storm { // Add all global variables of the PRISM program to the JANI model. for (auto const& variable : globalBooleanVariables) { - janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression())); + janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable())); + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; } for (auto const& variable : globalIntegerVariables) { - janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression(), variable.getInitialValueExpression())); + janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; } // Add all actions of the PRISM program to the JANI model. @@ -1545,29 +1550,42 @@ namespace storm { // previously built mapping to make variables global that are read by more than one module. for (auto const& module : modules) { storm::jani::Automaton automaton(module.getName()); + storm::expressions::Expression initialStatesExpression; + for (auto const& variable : module.getBooleanVariables()) { - storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression()); + storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable()); std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; // If there is exactly one module reading and writing the variable, we can make the variable local to this module. if (accessingModuleIndices.size() == 1) { automaton.addBooleanVariable(newBooleanVariable); - } else { // if (accessingModuleIndices.size() > 1) { + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; + } else if (accessingModuleIndices.size() > 1) { // Otherwise, we need to make it global. janiModel.addBooleanVariable(newBooleanVariable); + storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; } } for (auto const& variable : module.getIntegerVariables()) { - storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression(), variable.getInitialValueExpression()); + storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; // If there is exactly one module reading and writing the variable, we can make the variable local to this module. if (accessingModuleIndices.size() == 1) { automaton.addBoundedIntegerVariable(newIntegerVariable); - } else { //if (accessingModuleIndices.size() > 1) { + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; + } else if (accessingModuleIndices.size() > 1) { // Otherwise, we need to make it global. janiModel.addBoundedIntegerVariable(newIntegerVariable); + storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); + globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression; } } + // Set the proper expression characterizing the initial values of the automaton's variables. + automaton.setInitialStatesExpression(initialStatesExpression); + // Create a single location that will have all the edges. uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l")); automaton.setInitialLocation(onlyLocation); @@ -1603,6 +1621,9 @@ namespace storm { janiModel.addAutomaton(automaton); } + // Set the proper expression characterizing the initial values of the global variables. + janiModel.setInitialStatesExpression(globalInitialStatesExpression); + // Set the standard system composition. This is possible, because we reject non-standard compositions anyway. janiModel.setSystemComposition(janiModel.getStandardSystemComposition()); diff --git a/src/utility/dd.cpp b/src/utility/dd.cpp new file mode 100644 index 000000000..b50bc0031 --- /dev/null +++ b/src/utility/dd.cpp @@ -0,0 +1,44 @@ +#include "src/utility/dd.h" + +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Bdd.h" + +#include "src/utility/macros.h" + +namespace storm { + namespace utility { + namespace dd { + + template + storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables) { + storm::dd::Bdd reachableStates = initialStates; + + // Perform the BFS to discover all reachable states. + bool changed = true; + uint_fast64_t iteration = 0; + do { + STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis."); + changed = false; + storm::dd::Bdd tmp = reachableStates.relationalProduct(transitions, rowMetaVariables, columnMetaVariables); + storm::dd::Bdd newReachableStates = tmp && (!reachableStates); + + // Check whether new states were indeed discovered. + if (!newReachableStates.isZero()) { + changed = true; + } + + + reachableStates |= newReachableStates; + + ++iteration; + } while (changed); + + return reachableStates; + } + + template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + + } + } +} \ No newline at end of file diff --git a/src/utility/dd.h b/src/utility/dd.h new file mode 100644 index 000000000..f9af62f29 --- /dev/null +++ b/src/utility/dd.h @@ -0,0 +1,24 @@ +#pragma once + +#include + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace expressions { + class Variable; + } + namespace dd { + template + class Bdd; + } + + namespace utility { + namespace dd { + + template + storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + + } + } +} \ No newline at end of file diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 486a1b26e..732d2aae1 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -76,8 +76,12 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { auto t2 = std::chrono::high_resolution_clock::now(); std::cout << "die: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; - // EXPECT_EQ(13ul, model->getNumberOfStates()); - // EXPECT_EQ(20ul, model->getNumberOfTransitions()); + model->getTransitionMatrix().exportToDot("trans.dot"); + std::cout << "nnz: " << model->getTransitionMatrix().getNonZeroCount() << std::endl; + std::cout << "nodes: " << model->getTransitionMatrix().getNodeCount() << std::endl; + std::cout << "vars: " << model->getTransitionMatrix().getContainedMetaVariables().size() << std::endl; + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); janiModel = program.toJani(); @@ -86,8 +90,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "brp: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; - // EXPECT_EQ(677ul, model->getNumberOfStates()); - // EXPECT_EQ(867ul, model->getNumberOfTransitions()); + 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"); janiModel = program.toJani(); @@ -96,8 +100,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "crowds: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; - // EXPECT_EQ(8607ul, model->getNumberOfStates()); - // EXPECT_EQ(15113ul, model->getNumberOfTransitions()); + 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"); janiModel = program.toJani(); @@ -106,8 +110,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "lead: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; - // EXPECT_EQ(273ul, model->getNumberOfStates()); - // EXPECT_EQ(397ul, model->getNumberOfTransitions()); + 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"); janiModel = program.toJani(); @@ -116,8 +120,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Dtmc) { model = builder.translate(); t2 = std::chrono::high_resolution_clock::now(); std::cout << "nand: " << std::chrono::duration_cast(t2 - t1).count() << std::endl; - // EXPECT_EQ(1728ul, model->getNumberOfStates()); - // EXPECT_EQ(2505ul, model->getNumberOfTransitions()); + EXPECT_EQ(1728ul, model->getNumberOfStates()); + EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } //TEST(DdPrismModelBuilderTest_Cudd, Dtmc) { diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index e7c0f791f..4cd262a6f 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -57,9 +57,13 @@ 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); + model->getTransitionMatrix().exportToDot("trans_prism.dot"); + std::cout << "nnz: " << model->getTransitionMatrix().getNonZeroCount() << std::endl; + std::cout << "nodes: " << model->getTransitionMatrix().getNodeCount() << std::endl; + std::cout << "vars: " << model->getTransitionMatrix().getContainedMetaVariables().size() << std::endl; EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); - + 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());