diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index a5500092b..d033be86b 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -152,6 +152,10 @@ namespace storm { auxVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } STORM_LOG_DEBUG("Created " << auxVariableCount << " auxiliary variables."); + + bottomStateVariables = ddManager->addMetaVariable("bot"); + bottomStateBdds = std::make_pair(ddManager->getEncoding(bottomStateVariables.first, 1), ddManager->getEncoding(bottomStateVariables.second, 1)); + extendedPredicateDdVariables.push_back(bottomStateVariables); } template @@ -204,6 +208,11 @@ namespace storm { return auxVariables; } + template + storm::expressions::Variable const& AbstractionInformation::getAuxVariable(uint_fast64_t index) const { + return auxVariables[index]; + } + template std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const { return std::set(auxVariables.begin() + start, auxVariables.begin() + end); @@ -255,6 +264,37 @@ namespace storm { return predicateDdVariables; } + template + std::vector> const& AbstractionInformation::getExtendedSourceSuccessorVariablePairs() const { + return extendedPredicateDdVariables; + } + + template + storm::expressions::Variable const& AbstractionInformation::getBottomStateVariable(bool source) const { + if (source) { + return bottomStateVariables.first; + } else { + return bottomStateVariables.second; + } + } + + template + storm::dd::Bdd AbstractionInformation::getBottomStateBdd(bool source, bool negated) const { + if (source) { + if (negated) { + return !bottomStateBdds.first; + } else { + return bottomStateBdds.first; + } + } else { + if (negated) { + return !bottomStateBdds.second; + } else { + return bottomStateBdds.second; + } + } + } + template storm::dd::Bdd const& AbstractionInformation::encodePredicateAsSource(uint_fast64_t predicateIndex) const { return predicateBdds[predicateIndex].first; diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index fab9c1526..4be327e4e 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -258,6 +258,14 @@ namespace storm { * @return The meta variables associated with auxiliary information. */ std::vector const& getAuxVariables() const; + + /*! + * Retrieves the auxiliary variable with the given index. + * + * @param index The index of the auxiliary variable to retrieve. + * @return The auxiliary variable with the given index. + */ + storm::expressions::Variable const& getAuxVariable(uint_fast64_t index) const; /*! * Retrieves the requested set of auxiliary variables. @@ -309,6 +317,30 @@ namespace storm { * @return The meta variable pairs for all predicates. */ std::vector> const& getSourceSuccessorVariablePairs() const; + + /*! + * Retrieves the meta variables pairs for all predicates together with the meta variables marking the bottom states. + * + * @return The meta variable pairs for all predicates and bottom states. + */ + std::vector> const& getExtendedSourceSuccessorVariablePairs() const; + + /*! + * Retrieves the meta variable marking the bottom states. + * + * @param source A flag indicating whether the source or successor meta variable is to be returned. + * @return The meta variable marking the bottom states. + */ + storm::expressions::Variable const& getBottomStateVariable(bool source) const; + + /*! + * Retrieves the BDD that can be used to mark the bottom states. + * + * @param source A flag indicating whether the source or successor BDD is to be returned. + * @param negated A flag indicating whether the BDD should encode the bottom states or the non-bottom states. + * @return The BDD that can be used to mark bottom states. + */ + storm::dd::Bdd getBottomStateBdd(bool source, bool negated) const; /*! * Retrieves the BDD for the predicate with the given index over the source variables. @@ -388,6 +420,9 @@ namespace storm { /// The DD variables corresponding to the predicates. std::vector> predicateDdVariables; + /// The DD variables corresponding to the predicates together with the DD variables marking the bottom states. + std::vector> extendedPredicateDdVariables; + /// The set of all source variables. std::set sourceVariables; @@ -403,6 +438,12 @@ namespace storm { /// A BDD that represents the identity of all predicate variables. storm::dd::Bdd allPredicateIdentities; + /// A meta variable pair that marks bottom states. + std::pair bottomStateVariables; + + /// The BDDs associated with the bottom state variable pair. + std::pair, storm::dd::Bdd> bottomStateBdds; + /// A mapping from DD variable indices to the predicate index they represent. std::unordered_map ddVariableIndexToPredicateIndexMap; diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index 723d67b41..071a3a9c0 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -90,7 +90,7 @@ namespace storm { } // We now compute how many variables we need to encode the choices. We add one to the maximal number of - // choices to + // choices to account for a possible transition to a bottom state. uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices + 1))); // Finally, build overall result. @@ -241,7 +241,7 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } result |= updateBdd; @@ -280,7 +280,7 @@ namespace storm { } } - result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } return result; } @@ -316,13 +316,13 @@ namespace storm { result.states = bottomStateAbstractor.getAbstractStates(); // Now equip all these states with an actual transition to a bottom state. - result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities(); + result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false); - // Add the command encoding and the next free player 2 encoding. - result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables); + // Mark the states as bottom states. + result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); - result.states.template toAdd().exportToDot("bottom_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - result.transitions.template toAdd().exportToDot("bottom_trans_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + // Add the command encoding and the next free player 2 encoding. + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); return result; } @@ -331,7 +331,7 @@ namespace storm { storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - result += this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); + result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index ee76febf4..30a60928e 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -45,7 +45,7 @@ namespace storm { // DDs use the same amount DD variable encoding the choices of player 2. storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { - result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.numberOfPlayer2Variables); + result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); } return GameBddResult(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index); } diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index c0fd0459b..07b3078c8 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -56,7 +56,7 @@ namespace storm { // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible // choices. If for some reason this should not be enough, we could grow this vector dynamically, but // odds are that it's impossible to treat such models in any event. - abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount))) + 1); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // Now that we have created all other DD variables, we create the DD variables for the predicates. std::vector allPredicateIndices; @@ -129,12 +129,8 @@ namespace storm { std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); - auto auxVariables = abstractionInformation.getAuxVariableSet(1, abstractionInformation.getAuxVariableCount()); + auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); - std::cout << "vars" << std::endl; - for (auto const& var : auxVariables) { - std::cout << var.getName() << std::endl; - } // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); @@ -154,20 +150,38 @@ namespace storm { // Compute bottom states and the appropriate transitions if necessary. BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); + bool hasBottomStates = false; if (!addedAllGuards) { bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + hasBottomStates = !bottomStateResult.states.isZero(); } // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;// + bottomStateResult.transitions.template toAdd(); - transitionMatrix.exportToDot("trans_upd.dot"); + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + + // If there are bottom states, we need to mark all other states as non-bottom now. + if (hasBottomStates) { + transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); + transitionMatrix += bottomStateResult.transitions.template toAdd(); + reachableStates &= abstractionInformation.getBottomStateBdd(true, true); + reachableStates |= bottomStateResult.states; + } std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); + std::set allSourceVariables(abstractionInformation.getSourceVariables()); + if (hasBottomStates) { + allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); + } + std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); + if (hasBottomStates) { + allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); + } + + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, hasBottomStates ? abstractionInformation.getExtendedSourceSuccessorVariablePairs() : abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template