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
 
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::expressions::ExpressionManager& expressionManager, std::set<storm::expressions::Variable> const& abstractedVariables,
                           std::unique_ptr<storm::solver::SmtSolver>&& smtSolver,
                           AbstractionInformationOptions const& options = AbstractionInformationOptions(),
                           std::shared_ptr<storm::dd::DdManager<DdType>> ddManager = std::make_shared<storm::dd::DdManager<DdType>>());
 
    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