CommandAbstractor.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <memory>
#include <set>
#include <vector>
 
#include "storm-gamebased-ar/abstraction/GameBddResult.h"
#include "storm-gamebased-ar/abstraction/LocalExpressionInformation.h"
#include "storm-gamebased-ar/abstraction/StateSetAbstractor.h"
 
#include "storm/storage/expressions/ExpressionEvaluator.h"
 
#include "storm/storage/dd/DdType.h"
#include "storm/storage/expressions/Expression.h"
 
#include "storm/solver/SmtSolver.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 prism {
// Forward-declare concrete command and assignment classes.
class Command;
class Assignment;
}  // namespace prism
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
template<storm::dd::DdType DdType>
class AbstractionInformation;
 
template<storm::dd::DdType DdType>
struct BottomStateResult;
 
namespace prism {
template<storm::dd::DdType DdType, typename ValueType>
class CommandAbstractor {
   public:
    CommandAbstractor(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation,
                      std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool useDecomposition,
                      bool addPredicatesForValidBlocks, bool debug);
 
    void refine(std::vector<uint_fast64_t> const& predicates);
 
    storm::expressions::Expression const& getGuard() const;
 
    uint64_t getNumberOfUpdates(uint64_t player1Choice) const;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t auxiliaryChoice) const;
 
    std::set<storm::expressions::Variable> const& getAssignedVariables() const;
 
    GameBddResult<DdType> abstract();
 
    BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);
 
    storm::dd::Add<DdType, ValueType> getCommandUpdateProbabilitiesAdd() const;
 
    storm::prism::Command const& getConcreteCommand() const;
 
    void notifyGuardIsPredicate();
 
   private:
    std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const;
 
    std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> computeRelevantPredicates() const;
 
    bool relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const;
 
    void addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates);
 
    storm::dd::Bdd<DdType> getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model,
                                             std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& variablePredicates) const;
 
    storm::dd::Bdd<DdType> getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model,
                                              std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>> const& variablePredicates) const;
 
    void recomputeCachedBdd();
 
    void recomputeCachedBddWithoutDecomposition();
 
    void recomputeCachedBddWithDecomposition();
 
    storm::dd::Bdd<DdType> computeMissingIdentities() const;
 
    storm::dd::Bdd<DdType> computeMissingUpdateIdentities() const;
 
    AbstractionInformation<DdType> const& getAbstractionInformation() const;
 
    AbstractionInformation<DdType>& getAbstractionInformation();
 
    // An SMT responsible for this abstract command.
    std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
    // The abstraction-related information.
    std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
 
    // The concrete command this abstract command refers to.
    std::reference_wrapper<storm::prism::Command const> command;
 
    // The variables to which this command assigns expressions.
    std::set<storm::expressions::Variable> assignedVariables;
 
    // The local expression-related information.
    LocalExpressionInformation<DdType> localExpressionInformation;
 
    // The evaluator used to translate the probability expressions.
    storm::expressions::ExpressionEvaluator<ValueType> evaluator;
 
    // The currently relevant source/successor predicates and the corresponding variables.
    std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>,
              std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>>
        relevantPredicatesAndVariables;
 
    // The set of all relevant predicates.
    std::set<uint64_t> allRelevantPredicates;
 
    // The most recent result of a call to computeDd. If nothing has changed regarding the relevant
    // predicates, this result may be reused.
    GameBddResult<DdType> cachedDd;
 
    // All relevant decision variables over which to perform AllSat.
    std::vector<storm::expressions::Variable> decisionVariables;
 
    // 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 guard of the command was added as a predicate. If this is true, there
    // is no need to compute bottom states.
    bool skipBottomStates;
 
    // A flag remembering whether we need to force recomputation of the BDD.
    bool forceRecomputation;
 
    // The abstract guard of the command. This is only used if the guard is not a predicate, because it can
    // then be used to constrain the bottom state abstractor.
    storm::dd::Bdd<DdType> abstractGuard;
 
    // A state-set abstractor used to determine the bottom states if not all guards were added.
    StateSetAbstractor<DdType, ValueType> bottomStateAbstractor;
 
    // A flag that indicates whether or not debug mode is enabled.
    bool debug;
};
}  // namespace prism
}  // namespace abstraction
}  // namespace storm::gbar