diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index ccadd2a9b..acc7c5235 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -52,6 +52,8 @@ namespace storm { storm::dd::Dd DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update) { storm::dd::Dd updateDd = generationInfo.manager->getOne(); + STORM_LOG_TRACE("Translating update " << update); + // Iterate over all assignments (boolean and integer) and build the DD for it. std::vector assignments = update.getAssignments(); std::set assignedVariables; @@ -122,7 +124,7 @@ 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::Dd guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()); + storm::dd::Dd guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); if (!guardDd.isZero()) { @@ -138,9 +140,6 @@ 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); @@ -428,18 +427,20 @@ namespace storm { } return result; - } else { + } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { // Simply add all actions. storm::dd::Dd result = module.independentAction.transitionsDd; for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { result += synchronizingAction.second.transitionsDd; } return result; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type."); } } template - storm::dd::Dd DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { + std::pair, typename DdPrismModelBuilder::ModuleDecisionDiagram> DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { // Create the initial offset mapping. std::map synchronizingActionToOffsetMap; for (auto const& actionIndex : generationInfo.program.getActionIndices()) { @@ -467,9 +468,15 @@ namespace storm { // Combine the non-synchronizing action. system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, nextModule.independentAction, system.identity, nextModule.identity); + // For all synchronizing actions that the next module does not have, we need to multiply the identity of the next module. + for (auto& action : system.synchronizingActionToDecisionDiagramMap) { + if (!nextModule.hasSynchronizingAction(action.first)) { + action.second = combineUnsynchronizedActions(generationInfo, action.second, ActionDecisionDiagram(*generationInfo.manager), system.identity, nextModule.identity); + } + } + // 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 { @@ -488,11 +495,11 @@ namespace storm { result = result / result.sumAbstract(generationInfo.columnMetaVariables); } - return result; + return std::make_pair(result, system); } template - void DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { + std::pair, storm::dd::Dd> DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { // There might be nondeterministic variables. In that case the program must be prepared before translating. storm::prism::Program preparedProgram; if (options.constantDefinitions) { @@ -503,24 +510,42 @@ namespace storm { preparedProgram = preparedProgram.substituteConstants(); - std::cout << "translated prog: " << preparedProgram << std::endl; +// 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; - transitionMatrix.exportToDot("trans.dot"); - std::cout << "num transitions: " << transitionMatrix.getNonZeroCount() << std::endl; + std::pair, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo); + storm::dd::Dd transitionMatrix = transitionMatrixModulePair.first; + ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second; - storm::dd::Dd initialStates = createInitialStatesDecisionDiagram(generationInfo); - std::cout << "initial states: " << initialStates.getNonZeroCount() << std::endl; + // Cut the transition matrix to the reachable fragment of the state space. + storm::dd::Dd reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix); + transitionMatrix *= reachableStates; + + // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. + storm::dd::Dd statesWithTransition = transitionMatrix.notZero(); + if (program.getModelType() == storm::prism::Program::ModelType::MDP) { + statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables); + } + statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables); + storm::dd::Dd deadlockStates = reachableStates * !statesWithTransition; + + if (!deadlockStates.isZero()) { + // If we need to fix deadlocks, we do so now. + if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { + STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states."); + + // FIXME: For MDPs, we need to use an action encoding if we do not want to attach a lot of self-loops. + transitionMatrix += deadlockStates * globalModule.identity; + } 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."); + } + } - storm::dd::Dd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrix); - std::cout << "reachable states: " << reachableStates.getNonZeroCount() << std::endl; - exit(-1); + return std::make_pair(reachableStates, transitionMatrix * reachableStates); } template @@ -541,14 +566,9 @@ namespace storm { // 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 = transitionBdd.existsAbstract(generationInfo.allNondeterminismVariables); } - transitionBdd.exportToDot("trans.dot"); - reachableStatesBdd.exportToDot("reach.dot"); // Perform the BFS to discover all reachable states. bool changed = true; diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index c4caf3a9d..05f380060 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -59,7 +59,7 @@ namespace storm { * * @param program The program to translate. */ - static void translateProgram(storm::prism::Program const& program, Options const& options = Options()); + static std::pair, storm::dd::Dd> translateProgram(storm::prism::Program const& program, Options const& options = Options()); private: // This structure can store the decision diagrams representing a particular action. @@ -158,12 +158,19 @@ namespace storm { // The meta variables used to encode the synchronization. std::vector synchronizationMetaVariables; + // A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization + // variables). This is handy to abstract from this variable set. + std::set allNondeterminismVariables; + // DDs representing the identity for each variable. std::map> variableToIdentityMap; - // DDs representing the identity for each module (index). + // DDs representing the identity for each module. std::map> moduleToIdentityMap; + // DDs representing the valid ranges of the variables of each module. + std::map> moduleToRangeMap; + private: /*! * Creates the required meta variables and variable/module identities. @@ -173,6 +180,7 @@ namespace storm { for (uint_fast64_t i = 0; i < program.getActionIndices().size(); ++i) { std::pair variablePair = manager->addMetaVariable("sync" + std::to_string(i)); synchronizationMetaVariables.push_back(variablePair.first); + allNondeterminismVariables.insert(variablePair.first); } // Add nondeterminism variables (number of modules + number of commands). @@ -183,23 +191,10 @@ namespace storm { for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); nondeterminismMetaVariables.push_back(variablePair.first); + allNondeterminismVariables.insert(variablePair.first); } // Create meta variables for global program variables. - for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - 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(); int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); @@ -210,31 +205,30 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - + 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); + } for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { + std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + rowColumnMetaVariablePairs.push_back(variablePair); } // Create meta variables for each of the modules' variables. for (storm::prism::Module const& module : program.getModules()) { storm::dd::Dd moduleIdentity = manager->getOne(); - for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { - std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); - STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); - - rowMetaVariables.insert(variablePair.first); - variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); - - columnMetaVariables.insert(variablePair.second); - variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); - - 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); - } + storm::dd::Dd moduleRange = manager->getOne(); + for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); @@ -248,12 +242,32 @@ namespace storm { variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second); + variableIdentity.exportToDot(variablePair.first.getName() + "_ident.dot"); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); moduleIdentity *= variableIdentity; + moduleRange *= manager->getRange(variablePair.first); + + rowColumnMetaVariablePairs.push_back(variablePair); + } + for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { + std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + 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; + moduleRange *= manager->getRange(variablePair.first); rowColumnMetaVariablePairs.push_back(variablePair); } moduleToIdentityMap[module.getName()] = moduleIdentity; + moduleToRangeMap[module.getName()] = moduleRange; } } }; @@ -280,7 +294,7 @@ namespace storm { static storm::dd::Dd createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); - static storm::dd::Dd createSystemDecisionDiagram(GenerationInformation& generationInfo); + static std::pair, ModuleDecisionDiagram> createSystemDecisionDiagram(GenerationInformation& generationInfo); static storm::dd::Dd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp new file mode 100644 index 000000000..34edc67fd --- /dev/null +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -0,0 +1,36 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include + +#include "src/storage/dd/CuddDd.h" +#include "src/parser/PrismParser.h" +#include "src/builder/DdPrismModelBuilder.h" + +TEST(DdPrismModelBuilderTest, Dtmc) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::pair, storm::dd::Dd> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(13, model.first.getNonZeroCount()); + EXPECT_EQ(20, model.second.getNonZeroCount()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(677, model.first.getNonZeroCount()); + EXPECT_EQ(867, model.second.getNonZeroCount()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(8607, model.first.getNonZeroCount()); + EXPECT_EQ(15113, model.second.getNonZeroCount()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(273, model.first.getNonZeroCount()); + EXPECT_EQ(397, model.second.getNonZeroCount()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(1728, model.first.getNonZeroCount()); + EXPECT_EQ(2505, model.second.getNonZeroCount()); +} diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp new file mode 100644 index 000000000..4d3126997 --- /dev/null +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -0,0 +1,33 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/PrismParser.h" +#include "src/builder/ExplicitPrismModelBuilder.h" + +TEST(ExplicitPrismModelBuilderTest, Dtmc) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::unique_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(13, model->getNumberOfStates()); + EXPECT_EQ(20, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(677, model->getNumberOfStates()); + EXPECT_EQ(867, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(8607, model->getNumberOfStates()); + EXPECT_EQ(15113, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(273, model->getNumberOfStates()); + EXPECT_EQ(397, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(1728, model->getNumberOfStates()); + EXPECT_EQ(2505, model->getNumberOfTransitions()); +}