AutomatonAbstractor.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/dd/DdType.h"
 
#include "storm-gamebased-ar/abstraction/jani/EdgeAbstractor.h"
 
#include "storm/storage/expressions/Expression.h"
 
#include "storm/utility/solver.h"
 
namespace storm {
namespace jani {
// Forward-declare concrete automaton class.
class Automaton;
}  // namespace jani
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
template<storm::dd::DdType DdType>
class AbstractionInformation;
 
template<storm::dd::DdType DdType>
struct BottomStateResult;
 
namespace jani {
template<storm::dd::DdType DdType, typename ValueType>
class AutomatonAbstractor {
   public:
    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;
    AutomatonAbstractor(AutomatonAbstractor&&) = default;
    AutomatonAbstractor& operator=(AutomatonAbstractor&&) = default;

    void refine(std::vector<uint_fast64_t> const& predicates);

    storm::expressions::Expression const& getGuard(uint64_t player1Choice) const;

    uint64_t getNumberOfUpdates(uint64_t player1Choice) const;

    std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const;

    std::set<storm::expressions::Variable> const& getAssignedVariables(uint64_t player1Choice) const;

    GameBddResult<DdType> abstract();

    BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);

    storm::dd::Add<DdType, ValueType> getEdgeDecoratorAdd() const;

    storm::dd::Bdd<DdType> getInitialLocationsBdd() const;

    std::vector<EdgeAbstractor<DdType, ValueType>> const& getEdges() const;

    std::vector<EdgeAbstractor<DdType, ValueType>>& getEdges();

    std::size_t getNumberOfEdges() const;
 
    void notifyGuardsArePredicates();
 
   private:
    AbstractionInformation<DdType> const& getAbstractionInformation() const;
 
    // A factory that can be used to create new SMT solvers.
    std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
 
    // The DD-related information.
    std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
 
    // The abstract edge of the abstract automaton.
    std::vector<EdgeAbstractor<DdType, ValueType>> edges;
 
    // The concrete module this abstract automaton refers to.
    std::reference_wrapper<storm::jani::Automaton const> automaton;
 
    // If the automaton has more than one location, we need variables to encode that.
    boost::optional<std::pair<storm::expressions::Variable, storm::expressions::Variable>> locationVariables;
};
}  // namespace jani
}  // namespace abstraction
}  // namespace storm::gbar