AbstractionInformation.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <set>
#include <vector>
 
#include "storm/storage/dd/DdType.h"
 
#include "storm/storage/dd/Bdd.h"
 
#include "storm/solver/SmtSolver.h"
 
#include "storm/storage/expressions/EquivalenceChecker.h"
 
namespace storm {
namespace expressions {
class ExpressionManager;
class Expression;
class Variable;
}  // namespace expressions
 
class Environment;
 
namespace dd {
template<storm::dd::DdType DdType>
class DdManager;
}
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
 
struct AbstractionInformationOptions {
    AbstractionInformationOptions() = default;
 
    AbstractionInformationOptions(std::vector<storm::expressions::Expression> const& constraints) : constraints(constraints) {
        // Intentionally left empty.
    }
 
    std::vector<storm::expressions::Expression> constraints;
};
 
template<storm::dd::DdType DdType>
class AbstractionInformation {
   public:
    AbstractionInformation(storm::Environment const& env, storm::expressions::ExpressionManager& expressionManager,
                           std::set<storm::expressions::Variable> const& abstractedVariables, std::unique_ptr<storm::solver::SmtSolver>&& smtSolver,
                           AbstractionInformationOptions const& options = AbstractionInformationOptions());

    void addExpressionVariable(storm::expressions::Variable const& variable);

    void addExpressionVariable(storm::expressions::Variable const& variable, storm::expressions::Expression const& constraint);

    void addConstraint(storm::expressions::Expression const& constraint);

    std::vector<storm::expressions::Expression> const& getConstraints() const;

    uint_fast64_t getOrAddPredicate(storm::expressions::Expression const& predicate);

    std::vector<uint_fast64_t> addPredicates(std::vector<storm::expressions::Expression> const& predicates);

    storm::expressions::ExpressionManager& getExpressionManager();

    storm::expressions::ExpressionManager const& getExpressionManager() const;

    storm::dd::DdManager<DdType>& getDdManager();

    storm::dd::DdManager<DdType> const& getDdManager() const;

    std::shared_ptr<storm::dd::DdManager<DdType>> getDdManagerAsSharedPointer();

    std::shared_ptr<storm::dd::DdManager<DdType> const> getDdManagerAsSharedPointer() const;

    std::vector<storm::expressions::Expression> const& getPredicates() const;

    std::vector<storm::expressions::Expression> getPredicates(storm::storage::BitVector const& predicateValuation) const;

    std::vector<storm::expressions::Expression> getPredicatesExcludingBottom(storm::storage::BitVector const& predicateValuation) const;

    storm::expressions::Expression const& getPredicateByIndex(uint_fast64_t index) const;

    storm::dd::Bdd<DdType> getPredicateSourceVariable(storm::expressions::Expression const& predicate) const;

    bool hasPredicate(storm::expressions::Expression const& predicate) const;

    std::size_t getNumberOfPredicates() const;

    std::set<storm::expressions::Variable> const& getAbstractedVariables() const;

    void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t auxVariableCount);

    storm::dd::Bdd<DdType> encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const;

    uint_fast64_t decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const;

    storm::dd::Bdd<DdType> encodePlayer2Choice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const;

    uint_fast64_t decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const;

    storm::dd::Bdd<DdType> encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const;

    uint_fast64_t decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const;

    std::vector<storm::expressions::Variable> const& getPlayer1Variables() const;

    std::set<storm::expressions::Variable> getPlayer1VariableSet(uint_fast64_t count) const;

    std::size_t getPlayer1VariableCount() const;

    std::vector<storm::expressions::Variable> const& getPlayer2Variables() const;

    std::size_t getPlayer2VariableCount() const;

    std::set<storm::expressions::Variable> getPlayer2VariableSet(uint_fast64_t count) const;

    std::vector<storm::expressions::Variable> const& getAuxVariables() const;

    storm::expressions::Variable const& getAuxVariable(uint_fast64_t index) const;

    std::set<storm::expressions::Variable> getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const;

    std::size_t getAuxVariableCount() const;

    std::set<storm::expressions::Variable> const& getSourceVariables() const;

    std::set<storm::expressions::Variable> const& getSuccessorVariables() const;

    std::set<storm::expressions::Variable> const& getSourcePredicateVariables() const;

    std::set<storm::expressions::Variable> const& getSuccessorPredicateVariables() const;

    storm::dd::Bdd<DdType> const& getAllPredicateIdentities() const;

    storm::dd::Bdd<DdType> const& getAllLocationIdentities() const;

    std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> const& getPredicateToBddMap() const;

    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getSourceSuccessorVariablePairs() const;

    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getExtendedSourceSuccessorVariablePairs() const;

    storm::expressions::Variable const& getBottomStateVariable(bool source) const;

    storm::dd::Bdd<DdType> getBottomStateBdd(bool source, bool negated) const;

    storm::dd::Bdd<DdType> const& encodePredicateAsSource(uint_fast64_t predicateIndex) const;

    storm::dd::Bdd<DdType> const& encodePredicateAsSuccessor(uint_fast64_t predicateIndex) const;

    storm::dd::Bdd<DdType> const& getPredicateIdentity(uint_fast64_t predicateIndex) const;

    storm::expressions::Expression const& getPredicateForDdVariableIndex(uint_fast64_t ddVariableIndex) const;

    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> declareNewVariables(
        std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& oldPredicates, std::set<uint_fast64_t> const& newPredicates) const;

    storm::storage::BitVector decodeState(storm::dd::Bdd<DdType> const& state) const;

    template<typename ValueType>
    std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;

    template<typename ValueType>
    std::vector<std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>>> decodeChoicesToUpdateSuccessorMapping(
        std::set<storm::expressions::Variable> const& player2Variables, storm::dd::Bdd<DdType> const& choices) const;

    std::tuple<storm::storage::BitVector, uint64_t, uint64_t> decodeStatePlayer1ChoiceAndUpdate(storm::dd::Bdd<DdType> const& stateChoiceAndUpdate) const;

    std::pair<std::pair<storm::expressions::Variable, storm::expressions::Variable>, uint64_t> addLocationVariables(
        storm::expressions::Variable const& locationExpressionVariable, uint64_t highestLocationIndex);

    storm::expressions::Variable getLocationVariable(uint64_t locationVariableIndex, bool source) const;

    std::set<storm::expressions::Variable> const& getSourceLocationVariables() const;

    std::set<storm::expressions::Variable> const& getSuccessorLocationVariables() const;

    storm::expressions::Variable const& getDdLocationMetaVariable(storm::expressions::Variable const& locationExpressionVariable, bool source);

    uint64_t getNumberOfDdSourceLocationVariables() const;

    std::set<storm::expressions::Variable> const& getLocationExpressionVariables() const;

    storm::dd::Bdd<DdType> encodeLocation(storm::expressions::Variable const& locationVariable, uint64_t locationIndex) const;
 
   protected:
    std::vector<storm::expressions::Variable> const& getOrderedSourcePredicateVariables() const;

    std::vector<storm::expressions::Variable> const& getOrderedSuccessorPredicateVariables() const;

    storm::dd::Bdd<DdType> encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end,
                                        std::vector<storm::dd::Bdd<DdType>> const& variables) const;

    uint_fast64_t decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end,
                               std::vector<storm::expressions::Variable> const& variables) const;
 
    // The expression related data.

    std::reference_wrapper<storm::expressions::ExpressionManager> expressionManager;

    std::unordered_map<storm::expressions::Expression, uint64_t> predicateToIndexMap;

    storm::expressions::EquivalenceChecker equivalenceChecker;

    std::vector<storm::expressions::Expression> predicates;

    std::set<storm::expressions::Variable> abstractedVariables;

    std::vector<storm::expressions::Expression> constraints;
 
    // The DD-related data.

    std::shared_ptr<storm::dd::DdManager<DdType>> ddManager;

    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;

    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> extendedPredicateDdVariables;

    std::set<storm::expressions::Variable> sourceVariables;

    std::set<storm::expressions::Variable> successorVariables;

    std::set<storm::expressions::Variable> sourcePredicateVariables;

    std::set<storm::expressions::Variable> successorPredicateVariables;

    std::vector<storm::expressions::Variable> orderedSourcePredicateVariables;

    std::vector<storm::expressions::Variable> orderedSuccessorPredicateVariables;

    std::vector<std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>>> predicateBdds;

    std::vector<storm::dd::Bdd<DdType>> predicateIdentities;

    storm::dd::Bdd<DdType> allPredicateIdentities;

    storm::dd::Bdd<DdType> allLocationIdentities;

    std::pair<storm::expressions::Variable, storm::expressions::Variable> bottomStateVariables;

    std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> bottomStateBdds;

    std::unordered_map<uint_fast64_t, uint_fast64_t> ddVariableIndexToPredicateIndexMap;

    std::vector<storm::expressions::Variable> player1Variables;

    std::vector<storm::dd::Bdd<DdType>> player1VariableBdds;

    std::vector<storm::expressions::Variable> player2Variables;

    std::vector<storm::dd::Bdd<DdType>> player2VariableBdds;

    std::vector<storm::expressions::Variable> auxVariables;

    std::vector<storm::dd::Bdd<DdType>> auxVariableBdds;

    std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> expressionToBddMap;

    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> locationVariablePairs;

    std::map<storm::expressions::Variable, std::pair<storm::expressions::Variable, storm::expressions::Variable>> locationExpressionToDdVariableMap;

    std::set<storm::expressions::Variable> locationExpressionVariables;
 
    // All source location variables.
    std::set<storm::expressions::Variable> allSourceLocationVariables;
 
    // All successor location variables.
    std::set<storm::expressions::Variable> allSuccessorLocationVariables;
};
 
}  // namespace abstraction
}  // namespace storm::gbar