diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index a2d936cb3..30c55500a 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -490,6 +490,6 @@ namespace storm { template class AbstractionInformation; template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; - template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + template std::map> AbstractionInformation::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; } } diff --git a/src/storm/abstraction/LocalExpressionInformation.cpp b/src/storm/abstraction/LocalExpressionInformation.cpp index 4b6735407..0bb62e8d8 100644 --- a/src/storm/abstraction/LocalExpressionInformation.cpp +++ b/src/storm/abstraction/LocalExpressionInformation.cpp @@ -141,6 +141,15 @@ namespace storm { return this->variableToBlockMapping.find(variable)->second; } + template + std::set LocalExpressionInformation::getBlockIndicesOfVariables(std::set const& variables) const { + std::set result; + for (auto const& variable : variables) { + result.insert(getBlockIndexOfVariable(variable)); + } + return result; + } + template std::set const& LocalExpressionInformation::getRelatedExpressions(storm::expressions::Variable const& variable) const { return this->expressionBlocks[getBlockIndexOfVariable(variable)]; diff --git a/src/storm/abstraction/LocalExpressionInformation.h b/src/storm/abstraction/LocalExpressionInformation.h index cdae4a343..52827f8de 100644 --- a/src/storm/abstraction/LocalExpressionInformation.h +++ b/src/storm/abstraction/LocalExpressionInformation.h @@ -75,7 +75,15 @@ namespace storm { * @return The block index of the given variable. */ uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const; - + + /*! + * Retrieves the block indices of the given variables. + * + * @param variables The variables for which to retrieve the blocks. + * @return The block indices of the given variables. + */ + std::set getBlockIndicesOfVariables(std::set const& variables) const; + /*! * Retrieves the number of blocks of the variable partition. * diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 7ed477504..aa262e4e0 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -253,6 +253,10 @@ namespace storm { STORM_LOG_DEBUG("Derived new predicate (based on guard): " << newPredicate); } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); + +// player1Choice.template toAdd().exportToDot("choice.dot"); +// lowerChoice.template toAdd().exportToDot("lower.dot"); +// upperChoice.template toAdd().exportToDot("upper.dot"); // Decode both choices to explicit mappings. std::map> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(lowerChoice); diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index bbfe1baf9..1af0e8d12 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -69,6 +69,68 @@ namespace storm { std::map CommandAbstractor::getVariableUpdates(uint64_t auxiliaryChoice) const { return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap(); } + + template + void CommandAbstractor::recomputeCachedBddUsingDecomposition() { + STORM_LOG_TRACE("Recomputing BDD for command " << command.get() << " using the decomposition."); + auto start = std::chrono::high_resolution_clock::now(); + + // compute a decomposition of the command + // * start with all relevant blocks: blocks of assignment variables and variables in the rhs of assignments + // * go through all assignments of all updates and merge relevant blocks that are related via an assignment + // * repeat this until nothing changes anymore + // * the resulting blocks are the decomposition + + // Start by constructing the relevant blocks. + std::set allRelevantBlocks; + std::map variableToBlockIndex; + for (auto const& update : command.get().getUpdates()) { + for (auto const& assignment : update.getAssignments()) { + allRelevantBlocks.insert(localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable())); + + auto rhsVariableBlocks = localExpressionInformation.getBlockIndicesOfVariables(assignment.getExpression().getVariables()); + allRelevantBlocks.insert(rhsVariableBlocks.begin(), rhsVariableBlocks.end()); + } + } + STORM_LOG_TRACE("Found " << allRelevantBlocks.size() << " relevant block."); + + // Create a block partition. + std::vector> relevantBlockPartition; + std::map variableToLocalBlockIndex; + uint64_t index = 0; + for (auto const& blockIndex : allRelevantBlocks) { + relevantBlockPartition.emplace_back(std::set({blockIndex})); + for (auto const& variable : localExpressionInformation.getVariableBlockWithIndex(blockIndex)) { + variableToLocalBlockIndex[variable] = index; + } + ++index; + } + + // Proceed by relating the blocks via assignments until nothing changes anymore. + bool changed = false; + do { + for (auto const& update : command.get().getUpdates()) { + for (auto const& assignment : update.getAssignments()) { + std::set rhsVariables = assignment.getExpression().getVariables(); + + } + } + } while (changed); + + // if the decomposition has size 1, use the plain technique from before + + // otherwise, enumerate the abstract guard so we do this only once + + // then enumerate the solutions for each of the blocks of the decomposition + + // multiply the results + + // multiply with the abstract guard + + // multiply with missing identities + + // cache and return result + } template void CommandAbstractor::recomputeCachedBdd() { @@ -140,12 +202,12 @@ namespace storm { std::set assignedVariables; for (auto const& assignment : assignments) { // Also, variables appearing on the right-hand side of an assignment are relevant for source state. - auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getExpression().getVariables()); + auto const& rightHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignment.getExpression().getVariables()); result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end()); // Variables that are being assigned are relevant for the successor state. storm::expressions::Variable const& assignedVariable = assignment.getVariable(); - auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable); + auto const& leftHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignedVariable); result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); // Keep track of all assigned variables, so we can find the related predicates later. @@ -165,7 +227,7 @@ namespace storm { std::pair, std::vector>> result; // To start with, all predicates related to the guard are relevant source predicates. - result.first = localExpressionInformation.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables()); + result.first = localExpressionInformation.getRelatedExpressions(command.get().getGuardExpression().getVariables()); // Then, we add the predicates that become relevant, because of some update. for (auto const& update : command.get().getUpdates()) { @@ -223,13 +285,10 @@ namespace storm { template storm::dd::Bdd CommandAbstractor::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddOne(); -// std::cout << "new model ----------------" << std::endl; for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { if (model.getBooleanValue(variableIndexPair.first)) { -// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is true" << std::endl; result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } else { -// std::cout << this->getAbstractionInformation().getPredicateByIndex(variableIndexPair.second) << " is false" << std::endl; result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second); } } diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index 2b5d35845..c9eafce8f 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -161,6 +161,11 @@ namespace storm { * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. */ void recomputeCachedBdd(); + + /*! + * Recomputes the cached BDD using a decomposition. This needs to be triggered if any relevant predicates change. + */ + void recomputeCachedBddUsingDecomposition(); /*! * Computes the missing state identities. @@ -219,7 +224,7 @@ namespace storm { // The set of all relevant predicates. std::set allRelevantPredicates; - + // The most recent result of a call to computeDd. If nothing has changed regarding the relevant // predicates, this result may be reused. GameBddResult cachedDd; diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 939b9b7c4..dc70b13ec 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -39,7 +39,7 @@ namespace storm { std::vector invalidBlockStrategies = {"none", "local", "global"}; this->addOption(storm::settings::OptionBuilder(moduleName, invalidBlockStrategyOptionName, true, "Sets the strategy to detect invalid blocks.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("local").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build()); diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 4b6dc4a18..a9e4488b3 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -119,7 +119,6 @@ namespace storm { if (this->isJaniModel()) { std::map substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString); storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants(); - preparedModel = preparedModel.flattenComposition(); return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { std::map substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString); diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index f635e0aec..9ad1035b7 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -511,7 +511,17 @@ namespace storm { newAutomaton.changeAssignmentVariables(variableRemapping); // Finalize the flattened model. + storm::expressions::Expression initialStatesRestriction = getManager().boolean(true); + for (auto const& automaton : composedAutomata) { + if (automaton.get().hasInitialStatesRestriction()) { + initialStatesRestriction = initialStatesRestriction && automaton.get().getInitialStatesRestriction(); + } + } + newAutomaton.setInitialStatesRestriction(this->getInitialStatesExpression(composedAutomata)); + if (this->hasInitialStatesRestriction()) { + flattenedModel.setInitialStatesRestriction(this->getInitialStatesRestriction()); + } flattenedModel.addAutomaton(newAutomaton); flattenedModel.setStandardSystemComposition(); flattenedModel.finalize(); @@ -879,6 +889,10 @@ namespace storm { this->initialStatesRestriction = initialStatesRestriction; } + bool Model::hasInitialStatesRestriction() const { + return this->initialStatesRestriction.isInitialized(); + } + storm::expressions::Expression const& Model::getInitialStatesRestriction() const { return initialStatesRestriction; }