diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index 8889e0afb..52a409b28 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -441,6 +441,43 @@ namespace storm { return result; } + template + std::pair AbstractionInformation::decodeStateAndUpdate(storm::dd::Bdd const& state) const { + storm::storage::BitVector successor(this->getNumberOfPredicates()); + + storm::dd::Add stateAsAdd = state.template toAdd(); + uint_fast64_t updateIndex = 0; + for (auto const& stateValuePair : stateAsAdd) { + uint_fast64_t updateIndex = this->decodeAux(stateValuePair.first, 0, this->getAuxVariableCount()); + +#ifdef LOCAL_DEBUG + std::cout << "update idx: " << updateIndex << std::endl; +#endif + storm::storage::BitVector successor(this->getNumberOfPredicates()); + for (uint_fast64_t index = 0; index < this->getOrderedSuccessorVariables().size(); ++index) { + auto const& successorVariable = this->getOrderedSuccessorVariables()[index]; +#ifdef LOCAL_DEBUG + std::cout << successorVariable.getName() << " has value"; +#endif + if (stateValuePair.first.getBooleanValue(successorVariable)) { + successor.set(index); +#ifdef LOCAL_DEBUG + std::cout << " true"; +#endif + } else { +#ifdef LOCAL_DEBUG + std::cout << " false"; +#endif + } +#ifdef LOCAL_DEBUG + std::cout << std::endl; +#endif + } + } + + return std::make_pair(successors, updateIndex); + } + template class AbstractionInformation; template class AbstractionInformation; } diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index bfdefbcfb..6bfb728e1 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -435,10 +435,16 @@ namespace storm { std::vector> declareNewVariables(std::vector> const& oldPredicates, std::set const& newPredicates) const; /*! - * Decodes the choice in the form of a BDD over the source and + * Decodes the choice in the form of a BDD over the destination variables. */ std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + /*! + * Decodes the given state-and-update BDD (state as source variables) into a bit vector indicating the truth values of + * the predicates in the state and the update index. + */ + std::pair decodeStateAndUpdate(storm::dd::Bdd const& stateAndUpdate) const; + private: /*! * Encodes the given index with the given number of variables from the given variables. diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 51051415b..90ddd3f77 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -3,6 +3,7 @@ #include "storm/abstraction/AbstractionInformation.h" #include "storm/abstraction/MenuGameAbstractor.h" +#include "storm/storage/dd/DdManager.h" #include "storm/utility/dd.h" #include "storm/settings/SettingsManager.h" @@ -42,6 +43,41 @@ namespace storm { performRefinement(createGlobalRefinement(predicates)); } + template + storm::dd::Bdd getMostProbablePathSpanningTree(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& targetState, storm::dd::Bdd const& transitionFilter) { + storm::dd::Add maxProbabilities = game.getInitialStates().template toAdd(); + + storm::dd::Add border = game.getInitialStates().template toAdd(); + storm::dd::Bdd spanningTree = game.getManager().getBddZero(); + + storm::dd::Add transitionMatrix = ((transitionFilter && game.getExtendedTransitionMatrix().maxAbstractRepresentative(game.getProbabilisticBranchingVariables())).template toAdd() * game.getExtendedTransitionMatrix()); + transitionMatrix = transitionMatrix.sumAbstract(game.getNondeterminismVariables()); + + std::set variablesToAbstract(game.getRowVariables()); + variablesToAbstract.insert(game.getProbabilisticBranchingVariables().begin(), game.getProbabilisticBranchingVariables().end()); + while (!border.isZero() && (border && targetState).isZero()) { + // Determine the new maximal probabilities to all states. + storm::dd::Add tmp = border * transitionMatrix * maxProbabilities; + storm::dd::Bdd newMaxProbabilityChoices = tmp.maxAbstractRepresentative(variablesToAbstract); + storm::dd::Add newMaxProbabilities = tmp.maxAbstract(variablesToAbstract).swapVariables(game.getRowColumnMetaVariablePairs()); + + // Determine the probability values for which states strictly increased. + storm::dd::Bdd updateStates = newMaxProbabilities.greater(maxProbabilities); + maxProbabilities = updateStates.ite(newMaxProbabilities, maxProbabilities); + + // Delete all edges in the spanning tree that lead to states that need to be updated. + spanningTree &= ((!updateStates).swapVariables(game.getRowColumnMetaVariablePairs())); + + // Add all edges that achieve the new maximal value to the spanning tree. + spanningTree |= updateStates.swapVariables(game.getRowColumnMetaVariablePairs()) && newMaxProbabilityChoices; + + // Continue exploration from states that have been updated. + border = updateStates.template toAdd(); + } + + return spanningTree; + } + template std::pair, storm::OptimizationDirection> pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionsMin, storm::dd::Bdd const& transitionsMax, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { @@ -242,6 +278,21 @@ namespace storm { } } + template + storm::expressions::Expression MenuGameRefiner::buildTraceFormula(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& spanningTree, storm::dd::Bdd const& pivotState) const { + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); + + storm::dd::Bdd currentState = pivotState; + + while ((currentState && game.getInitialStates()).isZero()) { + storm::dd::Bdd predecessorTransition = currentState.swapVariables(game.getRowColumnMetaVariablePairs()) && spanningTree; + + + } + + return storm::expressions::Expression(); + } + template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, QualitativeResultMinMax const& qualitativeResult) const { STORM_LOG_TRACE("Trying refinement after qualitative check."); @@ -270,6 +321,12 @@ namespace storm { // Now that we have the pivot state candidates, we need to pick one. std::pair, storm::OptimizationDirection> pivotState = pickPivotState(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates); + // FIXME. + storm::dd::Bdd spanningTree = getMostProbablePathSpanningTree(game, pivotState.first, pivotState.second == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); + storm::expressions::Expression traceFormula = buildTraceFormula(game, spanningTree, pivotState.first); + + exit(-1); + // Derive predicate based on the selected pivot state. RefinementPredicates predicates = derivePredicatesFromPivotState(game, pivotState.first, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); std::vector preparedPredicates = preprocessPredicates(predicates.getPredicates(), (predicates.getSource() == RefinementPredicates::Source::Guard && splitGuards) || (predicates.getSource() == RefinementPredicates::Source::WeakestPrecondition && splitPredicates)); @@ -294,6 +351,10 @@ namespace storm { // Now that we have the pivot state candidates, we need to pick one. std::pair, storm::OptimizationDirection> pivotState = pickPivotState(game.getInitialStates(), pivotStateResult.reachableTransitionsMin, pivotStateResult.reachableTransitionsMax, game.getRowVariables(), game.getColumnVariables(), pivotStateResult.pivotStates); + // FIXME. + getMostProbablePathSpanningTree(game, pivotState.first, pivotState.second == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy); + exit(-1); + // Derive predicate based on the selected pivot state. RefinementPredicates predicates = derivePredicatesFromPivotState(game, pivotState.first, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); std::vector preparedPredicates = preprocessPredicates(predicates.getPredicates(), (predicates.getSource() == RefinementPredicates::Source::Guard && splitGuards) || (predicates.getSource() == RefinementPredicates::Source::WeakestPrecondition && splitPredicates)); @@ -304,10 +365,10 @@ namespace storm { template std::vector MenuGameRefiner::preprocessPredicates(std::vector const& predicates, bool split) const { if (split) { + AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); std::vector cleanedAtoms; for (auto const& predicate : predicates) { - AbstractionInformation const& abstractionInformation = abstractor.get().getAbstractionInformation(); // Split the predicates. std::vector atoms = splitter.split(predicate); diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h index 54c778ae2..c631ed3d8 100644 --- a/src/storm/abstraction/MenuGameRefiner.h +++ b/src/storm/abstraction/MenuGameRefiner.h @@ -82,6 +82,8 @@ namespace storm { */ std::vector createGlobalRefinement(std::vector const& predicates) const; + storm::expressions::Expression buildTraceFormula(storm::abstraction::MenuGame const& game, storm::dd::Bdd const& spanningTree, storm::dd::Bdd const& pivotState) const; + void performRefinement(std::vector const& refinementCommands) const; /// The underlying abstractor to refine.