adding a corrected valid-block-mode for game-based abstraction

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -13,6 +13,9 @@
 #include "storm/storage/prism/Command.h"
 #include "storm/storage/prism/Update.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/AbstractionSettings.h"
+
 #include "storm/utility/solver.h"
 #include "storm/utility/macros.h"
 
@@ -23,7 +26,7 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
-            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory), debug(debug) {
+            CommandAbstractor<DdType, ValueType>::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), addAssignmentRelatedVariablesToSourcePredicates(false), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory), debug(debug) {
                 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
@@ -43,6 +46,9 @@ namespace storm {
                         assignedVariables.insert(assignment.getVariable());
                     }
                 }
+                
+                auto const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
+                addAssignmentRelatedVariablesToSourcePredicates = abstractionSettings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::MorePredicates;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -283,7 +289,7 @@ namespace storm {
                     }
                 }
                 
-                // Then enumerate the solutions for each of the blocks of the decomposition
+                // Then enumerate the solutions for each of the blocks of the decomposition.
                 uint64_t usedNondeterminismVariables = 0;
                 uint64_t blockCounter = 0;
                 std::vector<storm::dd::Bdd<DdType>> blockBdds;
@@ -489,6 +495,12 @@ namespace storm {
                     storm::expressions::Variable const& assignedVariable = assignment.getVariable();
                     auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable);
                     result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end());
+                    
+                    // Predicates that are indirectly related to the assigned variables are relevant for the source state (if requested).
+                    if (this->addAssignmentRelatedVariablesToSourcePredicates) {
+                        auto const& assignedVariableBlock = localExpressionInformation.getRelatedExpressions(assignedVariable);
+                        result.first.insert(assignedVariableBlock.begin(), assignedVariableBlock.end());
+                    }
                 }
                 
                 return result;
@@ -508,6 +520,18 @@ namespace storm {
                     result.second.push_back(relevantUpdatePredicates.second);
                 }
                 
+//                std::cout << "relevant predicates for command " << command.get().getGlobalIndex() << std::endl;
+//                std::cout << "source predicates" << std::endl;
+//                for (auto const& i : result.first) {
+//                    std::cout << this->getAbstractionInformation().getPredicateByIndex(i) << std::endl;
+//                }
+//                for (uint64_t i = 0; i < result.second.size(); ++i) {
+//                    std::cout << "destination " << i << std::endl;
+//                    for (auto const& j : result.second[i]) {
+//                        std::cout << this->getAbstractionInformation().getPredicateByIndex(j) << std::endl;
+//                    }
+//                }
+                
                 return result;
             }
             

src/storm/abstraction/prism/CommandAbstractor.h

@@ -247,6 +247,9 @@ namespace storm {
                 // A flag indicating whether to use the decomposition when abstracting.
                 bool useDecomposition;
                 
+                // Whether or not to add predicates indirectly related to assignment variables to relevant source predicates.
+                bool addAssignmentRelatedVariablesToSourcePredicates;
+                
                 // A flag indicating whether the guard of the command was added as a predicate. If this is true, there
                 // is no need to compute bottom states.
                 bool skipBottomStates;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -66,6 +66,7 @@ namespace storm {
                 // For each module of the concrete program, we create an abstract counterpart.
                 auto const& settings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
                 bool useDecomposition = settings.isUseDecompositionSet();
+                restrictToValidBlocks = settings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::BlockEnumeration;
                 bool debug = settings.isDebugSet();
                 for (auto const& module : program.getModules()) {
                     this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, debug);
@@ -92,8 +93,10 @@ namespace storm {
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(predicateIndices);
                 
-                // Refine the valid blocks.
-                validBlockAbstractor.refine(predicateIndices);
+                if (restrictToValidBlocks) {
+                    // Refine the valid blocks.
+                    validBlockAbstractor.refine(predicateIndices);
+                }
 
                 refinementPerformed |= !command.getPredicates().empty();
             }
@@ -175,15 +178,21 @@ namespace storm {
                 }
                 relevantStatesWatch.stop();
                 
-                storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
+                storm::dd::Bdd<DdType> extendedTransitionRelation = nonTerminalStates && game.bdd;
+                storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
+                if (restrictToValidBlocks) {
+                    storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
 
-                // Compute the choices with only valid successors so we can restrict the game to these.
-                auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables);
+                    // Compute the choices with only valid successors so we can restrict the game to these.
+                    auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables);
+                    
+                    // Restrict the proper parts.
+                    extendedTransitionRelation &= validBlocks && choicesWithOnlyValidSuccessors;
+                    initialStates &= validBlocks;
+                }
                 
                 // Do a reachability analysis on the raw transition relation.
-                storm::dd::Bdd<DdType> extendedTransitionRelation = validBlocks && nonTerminalStates && game.bdd && choicesWithOnlyValidSuccessors;
                 storm::dd::Bdd<DdType> transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract);
-                storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates() && validBlocks;
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
 

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -159,6 +159,9 @@ namespace storm {
                 // A state-set abstractor used to determine the initial states of the abstraction.
                 StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
                 
+                // A flag indicating whether the valid blocks need to be computed and the game restricted to these.
+                bool restrictToValidBlocks;
+                
                 // An object that is used to compute the valid blocks.
                 ValidBlockAbstractor<DdType> validBlockAbstractor;
                                 

src/storm/logic/BoundedUntilFormula.cpp

@@ -99,10 +99,10 @@ namespace storm {
             } else {
                 this->getLeftSubformula().gatherUsedVariables(usedVariables);
                 this->getRightSubformula().gatherUsedVariables(usedVariables);
-                if (this->hasLowerBound()) {
+                if (this->hasLowerBound(0)) {
                     this->getLowerBound().gatherVariables(usedVariables);
                 }
-                if (this->hasUpperBound()) {
+                if (this->hasUpperBound(0)) {
                     this->getUpperBound().gatherVariables(usedVariables);
                 }
             }
@@ -189,7 +189,7 @@ namespace storm {
         }
 
         bool BoundedUntilFormula::hasUpperBound() const {
-            for(auto const& ub : upperBound) {
+            for (auto const& ub : upperBound) {
                 if (static_cast<bool>(ub)) {
                     return true;
                 }

src/storm/settings/modules/AbstractionSettings.cpp

@@ -33,6 +33,7 @@ namespace storm {
             const std::string AbstractionSettings::injectRefinementPredicatesOptionName = "injectref";
             const std::string AbstractionSettings::fixPlayer1StrategyOptionName = "fixpl1strat";
             const std::string AbstractionSettings::fixPlayer2StrategyOptionName = "fixpl2strat";
+            const std::string AbstractionSettings::validBlockModeOptionName = "validmode";
             
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@@ -132,6 +133,13 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
                                              .setDefaultValueString("off").build())
                                 .build());
+                
+                std::vector<std::string> validModes = {"morepreds", "blockenum"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, validBlockModeOptionName, true, "Sets the mode to guarantee valid blocks only.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(validModes))
+                                             .setDefaultValueString("morepreds").build())
+                                .build());
+
             }
             
             AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const {
@@ -266,6 +274,16 @@ namespace storm {
                 return this->getOption(fixPlayer2StrategyOptionName).getArgumentByName("value").getValueAsString() == "on";
             }
             
+            AbstractionSettings::ValidBlockMode AbstractionSettings::getValidBlockMode() const {
+                std::string modeAsString = this->getOption(validBlockModeOptionName).getArgumentByName("mode").getValueAsString();
+                if (modeAsString == "morepreds") {
+                    return ValidBlockMode::MorePredicates;
+                } else if (modeAsString == "blockenum") {
+                    return ValidBlockMode::BlockEnumeration;
+                }
+                return ValidBlockMode::MorePredicates;
+            }
+            
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -31,6 +31,10 @@ namespace storm {
                     Dd, Sparse
                 };
                 
+                enum class ValidBlockMode {
+                    MorePredicates, BlockEnumeration
+                };
+                
                 /*!
                  * Creates a new set of abstraction settings.
                  */
@@ -186,6 +190,11 @@ namespace storm {
                  */
                 bool isFixPlayer2StrategySet() const;
 
+                /*!
+                 * Retrieves the selected mode to guarantee valid blocks.
+                 */
+                ValidBlockMode getValidBlockMode() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -209,6 +218,7 @@ namespace storm {
                 const static std::string injectRefinementPredicatesOptionName;
                 const static std::string fixPlayer1StrategyOptionName;
                 const static std::string fixPlayer2StrategyOptionName;
+                const static std::string validBlockModeOptionName;
             };
             
         }