ModuleAbstractor.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/dd/DdType.h"
 
#include "storm-gamebased-ar/abstraction/prism/CommandAbstractor.h"
 
#include "storm/settings/modules/AbstractionSettings.h"
 
#include "storm/storage/expressions/Expression.h"
 
#include "storm/utility/solver.h"
 
namespace storm {
namespace prism {
// Forward-declare concrete module class.
class Module;
}  // namespace prism
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
template<storm::dd::DdType DdType>
class AbstractionInformation;
 
template<storm::dd::DdType DdType>
struct BottomStateResult;
 
template<storm::dd::DdType DdType>
struct GameBddResult;
 
namespace prism {
template<storm::dd::DdType DdType, typename ValueType>
class ModuleAbstractor {
   public:
    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;
    ModuleAbstractor(ModuleAbstractor&&) = default;
    ModuleAbstractor& operator=(ModuleAbstractor&&) = 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> getCommandUpdateProbabilitiesAdd() const;
 
    std::vector<CommandAbstractor<DdType, ValueType>> const& getCommands() const;
 
    std::vector<CommandAbstractor<DdType, ValueType>>& getCommands();
 
    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 commands of the abstract module.
    std::vector<CommandAbstractor<DdType, ValueType>> commands;
 
    // The concrete module this abstract module refers to.
    std::reference_wrapper<storm::prism::Module const> module;
};
}  // namespace prism
}  // namespace abstraction
}  // namespace storm::gbar