SymbolicStateDfa.h

#ifndef SYMBOLIC_STATE_DFA_H
#define SYMBOLIC_STATE_DFA_H
 
#include <memory>
#include <vector>
 
#include <cuddObj.hh>
 
#include "ExplicitStateDfaAdd.h"
 
namespace Syft {
 
    class SymbolicStateDfa {
    private:
 
        std::shared_ptr<VarMgr> var_mgr_;
        std::size_t automaton_id_;
 
        std::vector<int> initial_state_;
        CUDD::BDD final_states_;
        std::vector<CUDD::BDD> transition_function_;
 
        SymbolicStateDfa(std::shared_ptr<VarMgr> var_mgr);
 
        static std::pair<std::size_t, std::size_t> create_state_variables(
                std::shared_ptr<VarMgr> &mgr,
                std::size_t state_count);
 
        static CUDD::BDD state_to_bdd(const std::shared_ptr<VarMgr> &mgr,
                                      std::size_t automaton_id,
                                      std::size_t state);
 
        static CUDD::BDD state_set_to_bdd(
                const std::shared_ptr<VarMgr> &mgr,
                std::size_t automaton_id,
                const std::vector<size_t> &states);
 
        static std::vector<CUDD::BDD> symbolic_transition_function(
                const std::shared_ptr<VarMgr> &mgr,
                std::size_t automaton_id,
                const std::vector<CUDD::ADD> &transition_function);
 
    public:
 
 
        static SymbolicStateDfa from_explicit(const ExplicitStateDfaAdd &explicit_dfa);
 
        static SymbolicStateDfa from_predicates(std::shared_ptr<VarMgr> var_mgr,
                                                std::vector<CUDD::BDD> predicates);
 
        std::shared_ptr<VarMgr> var_mgr() const;
 
        std::size_t automaton_id() const;
 
        std::vector<int> initial_state() const;
 
        CUDD::BDD initial_state_bdd() const;
 
        CUDD::BDD final_states() const;
 
        std::vector<CUDD::BDD> transition_function() const;
 
        void restrict_dfa_with_states(const CUDD::BDD &valid_states);
 
        void restrict_dfa_with_transitions(const CUDD::BDD &feasible_moves);
 
        void dump_dot(const std::string &filename) const;
 
        static SymbolicStateDfa product_AND(const std::vector<SymbolicStateDfa> &dfa_vector);
 
        static std::vector<int> state_to_binary(std::size_t state,
                                                std::size_t bit_count);
 
        void new_sink_states(const CUDD::BDD &sink_states);
 
        static SymbolicStateDfa product_OR(const std::vector<SymbolicStateDfa> &dfa_vector);
 
        static SymbolicStateDfa complement(const SymbolicStateDfa dfa);
    };
 
}
 
#endif // SYMBOLIC_STATE_DFA_H