ExplicitStateDfa.h

#ifndef EXPLICITSTATEDFA_H
#define EXPLICITSTATEDFA_H
 
extern "C" {
#include <mona/bdd.h>
#include <mona/dfa.h>
#include <mona/mem.h>
}
 
#include "lydia/logic/ltlf/base.hpp"
#include "lydia/dfa/mona_dfa.hpp"
#include "VarMgr.h"
 
namespace Syft {
 
    class ExplicitStateDfa : public whitemech::lydia::mona_dfa {
    public:
 
        ExplicitStateDfa(DFA *dfa, int nb_variables)
                : whitemech::lydia::mona_dfa(dfa, nb_variables) {
        }
 
        ExplicitStateDfa(DFA *dfa, const std::vector<std::string> &names)
                : whitemech::lydia::mona_dfa(dfa, names) {
        }
 
        ExplicitStateDfa(const ExplicitStateDfa &other)
                : whitemech::lydia::mona_dfa(dfaCopy(other.dfa_), other.names) {
 
        }
 
        ExplicitStateDfa &operator=(ExplicitStateDfa other) {
            this->names = other.names;
            this->dfa_ = dfaCopy(other.get_dfa());
            return *this;
        }
 
 
        ~ExplicitStateDfa() {
 
        }
 
        int get_nb_variables() {
            return this->names.size();
        }
 
        void dfa_print();
 
 
        static ExplicitStateDfa dfa_of_formula(const whitemech::lydia::LTLfFormula &formula);
 
        static ExplicitStateDfa dfa_product_and(const std::vector<ExplicitStateDfa> &dfa_vector);
 
        static ExplicitStateDfa dfa_product_or(const std::vector<ExplicitStateDfa> &dfa_vector);
 
        static ExplicitStateDfa dfa_minimize(const ExplicitStateDfa &d);
 
 
        static ExplicitStateDfa restrict_dfa_with_states(ExplicitStateDfa &d, std::vector<size_t> states);
 
        static ExplicitStateDfa
        restrict_dfa_with_transitions(ExplicitStateDfa &d, std::unordered_map<size_t, CUDD::BDD> transitions,
                                      std::shared_ptr<VarMgr> var_mgr);
 
        static ExplicitStateDfa dfa_complement(ExplicitStateDfa &d);
 
    private:
        static std::vector<std::string>
        traverse_bdd(CUDD::BDD dd, std::shared_ptr<VarMgr> var_mgr, std::vector<std::string> &names,
                     std::string guard_str);
    };
 
}
#endif //EXPLICITSTATEDFA_H