more fixes to (JANI) game-based abstraction

src/storm/abstraction/AbstractionInformation.cpp

@@ -140,11 +140,12 @@ namespace storm {
         
         template<storm::dd::DdType DdType>
         std::vector<storm::expressions::Expression> AbstractionInformation<DdType>::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<storm::expressions::Expression> 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::dd::DdType DdType>
-        storm::expressions::Variable const& AbstractionInformation<DdType>::getDdLocationVariable(storm::expressions::Variable const& locationExpressionVariable, bool source) {
+        storm::expressions::Variable const& AbstractionInformation<DdType>::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 <storm::dd::DdType DdType>
+        uint64_t AbstractionInformation<DdType>::getNumberOfDdSourceLocationVariables() const {
+            uint64_t result = 0;
+            for (auto const& locationVariableToMetaVariablePair : locationExpressionToDdVariableMap) {
+                result += ddManager->getMetaVariable(locationVariableToMetaVariablePair.second.first).getNumberOfDdVariables();
+            }
+            return result;
+        }
+        
         template <storm::dd::DdType DdType>
         std::set<storm::expressions::Variable> const& AbstractionInformation<DdType>::getLocationExpressionVariables() const {
             return locationExpressionVariables;

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.

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<double>(abstractionInformation.get().getDdLocationVariable(expression.getVariable(), true));
+                return abstractionInformation.get().getDdManager().template getIdentity<double>(abstractionInformation.get().getDdLocationMetaVariable(expression.getVariable(), true));
             }
         }
         

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<storm::dd::DdType Type, typename ValueType>
         bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> 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<RefinementPredicates> kShortestPathPredicates = derivePredicatesFromInterpolationKShortestPaths(odd, transitionMatrix, player1Grouping, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, lower, upper, maxStrategyPair);
             

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<DdType> 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<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates && reachableStates.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs())).template toAdd<ValueType>();
 
                 transitionMatrix *= edgeDecoratorAdd;

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.");
                 }