StateSetAbstractor.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <memory>
#include <set>
 
#include "storm/utility/OsDetection.h"
 
#include "storm/storage/dd/DdType.h"
 
#include "storm/solver/SmtSolver.h"
#include "storm/utility/solver.h"
 
#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h"
 
namespace storm {
namespace utility {
namespace solver {
class SmtSolverFactory;
}
}  // namespace utility
 
namespace dd {
template<storm::dd::DdType DdType>
class Bdd;
 
template<storm::dd::DdType DdType, typename ValueType>
class Add;
}  // namespace dd
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
template<storm::dd::DdType DdType>
class AbstractionInformation;
 
template<storm::dd::DdType DdType, typename ValueType>
class StateSetAbstractor {
   public:
    StateSetAbstractor(StateSetAbstractor const& other) = default;
    StateSetAbstractor& operator=(StateSetAbstractor const& other) = default;
 
#ifndef WINDOWS
    StateSetAbstractor(StateSetAbstractor&& other) = default;
    StateSetAbstractor& operator=(StateSetAbstractor&& other) = default;
#endif
 
    StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::vector<storm::expressions::Expression> const& statePredicates,
                       std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory =
                           std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
 
    void refine(std::vector<uint_fast64_t> const& newPredicateIndices);
 
    void constrain(storm::expressions::Expression const& constraint);
 
    void constrain(storm::dd::Bdd<DdType> const& newConstraint);
 
    storm::dd::Bdd<DdType> getAbstractStates();
 
   private:
    void addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices);
 
    void pushConstraintBdd();
 
    void popConstraintBdd();
 
    void recomputeCachedBdd();
 
    storm::dd::Bdd<DdType> getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const;
 
    AbstractionInformation<DdType>& getAbstractionInformation();
 
    AbstractionInformation<DdType> const& getAbstractionInformation() const;
 
    // The SMT solver used for abstracting the set of states.
    std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
    // The abstraction-related information.
    std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
 
    // The local expression-related information.
    LocalExpressionInformation<DdType> localExpressionInformation;
 
    // The set of relevant predicates and the corresponding decision variables.
    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> relevantPredicatesAndVariables;
 
    // The set of all variables appearing in the concrete predicates.
    std::set<storm::expressions::Variable> concretePredicateVariables;
 
    // The set of all decision variables over which to perform the all-sat enumeration.
    std::vector<storm::expressions::Variable> decisionVariables;
 
    // A flag indicating whether the cached BDD needs recomputation.
    bool forceRecomputation;
 
    // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work
    // needed to be done).
    storm::dd::Bdd<DdType> cachedBdd;
 
    // This BDD currently constrains the search for solutions.
    storm::dd::Bdd<DdType> constraint;
};
}  // namespace abstraction
}  // namespace storm::gbar