diff --git a/src/storm/abstraction/AbstractionInformation.cpp b/src/storm/abstraction/AbstractionInformation.cpp index d6d375544..5c5737f89 100644 --- a/src/storm/abstraction/AbstractionInformation.cpp +++ b/src/storm/abstraction/AbstractionInformation.cpp @@ -140,11 +140,12 @@ namespace storm { template std::vector AbstractionInformation::getPredicatesExcludingBottom(storm::storage::BitVector const& predicateValuation) const { - STORM_LOG_ASSERT(predicateValuation.size() == this->getNumberOfPredicates() + 1, "Size of predicate valuation does not match number of predicates."); + uint64_t offset = 1 + this->getNumberOfDdSourceLocationVariables(); + STORM_LOG_ASSERT(predicateValuation.size() == this->getNumberOfPredicates() + offset, "Size of predicate valuation does not match number of predicates."); std::vector result; for (uint64_t index = 0; index < this->getNumberOfPredicates(); ++index) { - if (predicateValuation[index + 1]) { + if (predicateValuation[index + offset]) { result.push_back(this->getPredicateByIndex(index)); } else { result.push_back(!this->getPredicateByIndex(index)); @@ -539,7 +540,7 @@ namespace storm { } template - storm::expressions::Variable const& AbstractionInformation::getDdLocationVariable(storm::expressions::Variable const& locationExpressionVariable, bool source) { + storm::expressions::Variable const& AbstractionInformation::getDdLocationMetaVariable(storm::expressions::Variable const& locationExpressionVariable, bool source) { auto const& metaVariablePair = locationExpressionToDdVariableMap.at(locationExpressionVariable); if (source) { return metaVariablePair.first; @@ -548,6 +549,15 @@ namespace storm { } } + template + uint64_t AbstractionInformation::getNumberOfDdSourceLocationVariables() const { + uint64_t result = 0; + for (auto const& locationVariableToMetaVariablePair : locationExpressionToDdVariableMap) { + result += ddManager->getMetaVariable(locationVariableToMetaVariablePair.second.first).getNumberOfDdVariables(); + } + return result; + } + template std::set const& AbstractionInformation::getLocationExpressionVariables() const { return locationExpressionVariables; diff --git a/src/storm/abstraction/AbstractionInformation.h b/src/storm/abstraction/AbstractionInformation.h index fa1a1927a..4256f2149 100644 --- a/src/storm/abstraction/AbstractionInformation.h +++ b/src/storm/abstraction/AbstractionInformation.h @@ -485,7 +485,12 @@ namespace storm { /*! * Retrieves the DD variable for the given location expression variable. */ - storm::expressions::Variable const& getDdLocationVariable(storm::expressions::Variable const& locationExpressionVariable, bool source); + storm::expressions::Variable const& getDdLocationMetaVariable(storm::expressions::Variable const& locationExpressionVariable, bool source); + + /*! + * Retrieves the number of DD variables associated with the source location variables. + */ + uint64_t getNumberOfDdSourceLocationVariables() const; /*! * Retrieves the source location variables. diff --git a/src/storm/abstraction/ExpressionTranslator.cpp b/src/storm/abstraction/ExpressionTranslator.cpp index 8bf792278..40e2b995d 100644 --- a/src/storm/abstraction/ExpressionTranslator.cpp +++ b/src/storm/abstraction/ExpressionTranslator.cpp @@ -136,7 +136,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expressions of this kind are currently not supported by the abstraction expression translator."); } else { - return abstractionInformation.get().getDdManager().template getIdentity(abstractionInformation.get().getDdLocationVariable(expression.getVariable(), true)); + return abstractionInformation.get().getDdManager().template getIdentity(abstractionInformation.get().getDdLocationMetaVariable(expression.getVariable(), true)); } } diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index b75a6380a..1bbdefd6a 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -594,9 +594,12 @@ namespace storm { auto pathIt = reversedPath.rbegin(); - // Decode initial state. The state valuation also includes the bottom state, so we need to reserve one more - // than the number of predicates here. - storm::storage::BitVector extendedPredicateValuation = odd.getEncoding(stateToOffset ? (*stateToOffset)[*pathIt] : *pathIt, abstractionInformation.getNumberOfPredicates() + 1); + // Decode initial state. The state valuation also includes + // * the bottom state, so we need to reserve one more, and + // * the location variables, + // so we need to reserve an appropriate size. + uint64_t predicateValuationOffset = abstractionInformation.getNumberOfDdSourceLocationVariables() + 1; + storm::storage::BitVector extendedPredicateValuation = odd.getEncoding(stateToOffset ? (*stateToOffset)[*pathIt] : *pathIt, abstractionInformation.getNumberOfPredicates() + predicateValuationOffset); ++pathIt; // Add all predicates of initial block. @@ -651,6 +654,9 @@ namespace storm { allVariableUpdateExpression = allVariableUpdateExpression || variableUpdateExpression; } + if (!allVariableUpdateExpression.isInitialized()) { + allVariableUpdateExpression = expressionManager.boolean(true); + } predicates.back().emplace_back(allVariableUpdateExpression); // Incorporate the new variables in the current substitution. @@ -659,7 +665,7 @@ namespace storm { } // Decode current state. - extendedPredicateValuation = odd.getEncoding(stateToOffset ? (*stateToOffset)[*pathIt] : *pathIt, abstractionInformation.getNumberOfPredicates() + 1); + extendedPredicateValuation = odd.getEncoding(stateToOffset ? (*stateToOffset)[*pathIt] : *pathIt, abstractionInformation.getNumberOfPredicates() + predicateValuationOffset); // Encode the predicates whose value might have changed. // FIXME: could be optimized by precomputation. @@ -687,7 +693,7 @@ namespace storm { if (containsAssignedVariables) { auto transformedPredicate = predicate.changeManager(expressionManager).substitute(currentSubstitution); - predicates.back().emplace_back(extendedPredicateValuation.get(predicateIndex + 1) ? transformedPredicate : !transformedPredicate); + predicates.back().emplace_back(extendedPredicateValuation.get(predicateIndex + predicateValuationOffset) ? transformedPredicate : !transformedPredicate); } } @@ -1231,8 +1237,8 @@ namespace storm { template bool MenuGameRefiner::refine(storm::abstraction::MenuGame const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& player1Grouping, std::vector const& player1Labeling, std::vector const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax const& quantitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const { - ValueType lower = quantitativeResult.getMin().getRange(initialStates).first; - ValueType upper = quantitativeResult.getMax().getRange(initialStates).second; +// ValueType lower = quantitativeResult.getMin().getRange(initialStates).first; +// ValueType upper = quantitativeResult.getMax().getRange(initialStates).second; // boost::optional kShortestPathPredicates = derivePredicatesFromInterpolationKShortestPaths(odd, transitionMatrix, player1Grouping, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, lower, upper, maxStrategyPair); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 3d0fec9c1..58d5e02f8 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -192,15 +192,19 @@ namespace storm { if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { // Get the target state BDD. storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); - + // In the presence of target states, we keep only states that can reach the target states. - reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; - + auto newReachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; + reachableStates = newReachableStates; + // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states. - reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + reachableStates |= (reachableStates && !targetStates).relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); relevantStatesWatch.stop(); + // Restrict transition relation to relevant fragment for computation of deadlock states. + transitionRelation &= reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); + STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); } @@ -222,7 +226,7 @@ namespace storm { // Construct the transition matrix by cutting away the transitions of unreachable states. // Note that we also restrict the successor states of transitions, because there might be successors - // that are not in the relevant we restrict to. + // that are not in the set of relevant states we restrict to. storm::dd::Add transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs())).template toAdd(); transitionMatrix *= edgeDecoratorAdd; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index c61f68833..167f437b6 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -191,8 +191,11 @@ namespace storm { // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states. - reachableStates = reachableStates || reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + reachableStates |= (reachableStates && !targetStates).relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + // Restrict transition relation to relevant fragment for computation of deadlock states. + transitionRelation &= reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs()); + relevantStatesWatch.stop(); STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); }