slight polishing of valid-block-mode treatment, also for JANI

src/storm/abstraction/jani/AutomatonAbstractor.cpp

@@ -24,12 +24,12 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) {
+            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) {
                 
                 // For each concrete command, we create an abstract counterpart.
                 uint64_t edgeId = 0;
                 for (auto const& edge : automaton.getEdges()) {
-                    edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition, debug);
+                    edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug);
                     ++edgeId;
                 }
                 

src/storm/abstraction/jani/AutomatonAbstractor.h

@@ -35,7 +35,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param useDecomposition A flag indicating whether to use the decomposition during abstraction.
                  */
-                AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug);
+                AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug);
                 
                 AutomatonAbstractor(AutomatonAbstractor const&) = default;
                 AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default;

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -23,7 +23,7 @@ namespace storm {
     namespace abstraction {
         namespace jani {
             template <storm::dd::DdType DdType, typename ValueType>
-            EdgeAbstractor<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory), debug(debug) {
+            EdgeAbstractor<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), addPredicatesForValidBlocks(addPredicatesForValidBlocks), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory), debug(debug) {
                 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations());
@@ -43,6 +43,11 @@ namespace storm {
                         assignedVariables.insert(assignment.getExpressionVariable());
                     }
                 }
+                
+                // Log whether or not predicates are added to ensure valid blocks.
+                if (this->addPredicatesForValidBlocks) {
+                    STORM_LOG_DEBUG("Adding more predicates to ensure valid blocks.");
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -489,6 +494,12 @@ namespace storm {
                     storm::expressions::Variable const& assignedVariable = assignment.getExpressionVariable();
                     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->addPredicatesForValidBlocks) {
+                        auto const& assignedVariableBlock = localExpressionInformation.getRelatedExpressions(assignedVariable);
+                        result.first.insert(assignedVariableBlock.begin(), assignedVariableBlock.end());
+                    }
                 }
                 
                 return result;

src/storm/abstraction/jani/EdgeAbstractor.h

@@ -58,7 +58,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param useDecomposition A flag indicating whether to use an edge decomposition during abstraction.
                  */
-                EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug);
+                EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug);
                                
                 /*!
                  * Refines the abstract edge with the given predicates.
@@ -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 addPredicatesForValidBlocks;
+
                 // A flag indicating whether the computation of bottom states can be skipped (for example, if the bottom
                 // states become empty at some point).
                 bool skipBottomStates;

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -35,7 +35,7 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, MenuGameAbstractorOptions const& options) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager()), AbstractionInformationOptions(options.constraints)), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
+            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, MenuGameAbstractorOptions const& options) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager()), AbstractionInformationOptions(options.constraints)), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), restrictToValidBlocks(false), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
                 
                 // Check whether the model is linear as the abstraction requires this.
                 STORM_LOG_WARN_COND(model.isLinear(), "The model appears to contain non-linear expressions, which may cause malfunctioning of the abstraction.");
@@ -70,9 +70,11 @@ 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 addPredicatesForValidBlocks = !restrictToValidBlocks;
                 bool debug = settings.isDebugSet();
                 for (auto const& automaton : model.getAutomata()) {
-                    automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition, debug);
+                    automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug);
                 }
                 
                 // Retrieve global BDDs/ADDs so we can multiply them in the abstraction process.
@@ -97,8 +99,10 @@ namespace storm {
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(predicateIndices);
                 
+                if (this->restrictToValidBlocks) {
                     // Refine the valid blocks.
                     validBlockAbstractor.refine(predicateIndices);
+                }
 
                 refinementPerformed |= !command.getPredicates().empty();
             }
@@ -183,15 +187,22 @@ namespace storm {
                 }
                 relevantStatesWatch.stop();
 
+                storm::dd::Bdd<DdType> extendedTransitionRelation = nonTerminalStates && game.bdd;
+                storm::dd::Bdd<DdType> initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates();
+                if (this->restrictToValidBlocks) {
+                    STORM_LOG_DEBUG("Restricting to valid blocks.");
                     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);
                     
+                    // 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 = initialLocationsBdd && 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/jani/JaniMenuGameAbstractor.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/abstraction/prism/CommandAbstractor.cpp

@@ -13,9 +13,6 @@
 #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"
 
@@ -26,7 +23,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), addAssignmentRelatedVariablesToSourcePredicates(false), 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 addPredicatesForValidBlocks, 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), addPredicatesForValidBlocks(addPredicatesForValidBlocks), 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());
@@ -47,8 +44,10 @@ namespace storm {
                     }
                 }
                 
-                auto const& abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
-                addAssignmentRelatedVariablesToSourcePredicates = abstractionSettings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::MorePredicates;
+                // Log whether or not predicates are added to ensure valid blocks.
+                if (this->addPredicatesForValidBlocks) {
+                    STORM_LOG_DEBUG("Adding more predicates to ensure valid blocks.");
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -497,7 +496,7 @@ namespace storm {
                     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) {
+                    if (this->addPredicatesForValidBlocks) {
                         auto const& assignedVariableBlock = localExpressionInformation.getRelatedExpressions(assignedVariable);
                         result.first.insert(assignedVariableBlock.begin(), assignedVariableBlock.end());
                     }

src/storm/abstraction/prism/CommandAbstractor.h

@@ -56,7 +56,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param useDecomposition A flag indicating whether to use the decomposition during abstraction.
                  */
-                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug);
+                CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug);
                                
                 /*!
                  * Refines the abstract command with the given predicates.
@@ -248,7 +248,7 @@ namespace storm {
                 bool useDecomposition;
                 
                 // Whether or not to add predicates indirectly related to assignment variables to relevant source predicates.
-                bool addAssignmentRelatedVariablesToSourcePredicates;
+                bool addPredicatesForValidBlocks;
                 
                 // 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.

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -23,11 +23,11 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
+            ModuleAbstractor<DdType, ValueType>::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) {
                 
                 // For each concrete command, we create an abstract counterpart.
                 for (auto const& command : module.getCommands()) {
-                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, debug);
+                    commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug);
                 }
             }
             

src/storm/abstraction/prism/ModuleAbstractor.h

@@ -38,7 +38,7 @@ namespace storm {
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  * @param useDecomposition A flag that governs whether to use the decomposition in the abstraction.
                  */
-                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool debug);
+                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug);
                 
                 ModuleAbstractor(ModuleAbstractor const&) = default;
                 ModuleAbstractor& operator=(ModuleAbstractor const&) = default;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -67,9 +67,10 @@ namespace storm {
                 auto const& settings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
                 bool useDecomposition = settings.isUseDecompositionSet();
                 restrictToValidBlocks = settings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::BlockEnumeration;
+                bool addPredicatesForValidBlocks = !restrictToValidBlocks;
                 bool debug = settings.isDebugSet();
                 for (auto const& module : program.getModules()) {
-                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, debug);
+                    this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug);
                 }
                 
                 // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later.
@@ -181,6 +182,7 @@ namespace storm {
                 storm::dd::Bdd<DdType> extendedTransitionRelation = nonTerminalStates && game.bdd;
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
                 if (restrictToValidBlocks) {
+                    STORM_LOG_DEBUG("Restricting to valid blocks.");
                     storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
 
                     // Compute the choices with only valid successors so we can restrict the game to these.