LTLfSynthesizer.h

#ifndef SYFT_REACHABILITYSYNTHESIZER_H
#define SYFT_REACHABILITYSYNTHESIZER_H
 
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
#include "game/Reachability.hpp"
 
namespace Syft {
 
    class LTLfSynthesizer {
    private:
        std::shared_ptr<VarMgr> var_mgr_;
        SymbolicStateDfa spec_;
        Player starting_player_;
        Player protagonist_player_;
        CUDD::BDD goal_states_;
        CUDD::BDD state_space_;
 
    public:
 
        LTLfSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player,
                        CUDD::BDD goal_states, CUDD::BDD state_space);
 
        SynthesisResult run() const;
 
        std::unique_ptr<Transducer> AbstractSingleStrategy(const SynthesisResult &result) const;
 
    };
 
}
 
#endif //SYFT_REACHABILITYSYNTHESIZER_H