DfaGameSynthesizer.h

#ifndef DFA_GAME_SYNTHESIZER_H
#define DFA_GAME_SYNTHESIZER_H
 
#include "Quantification.h"
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
#include "Transducer.h"
 
namespace Syft {
 
 
    class DfaGameSynthesizer : public Synthesizer<SymbolicStateDfa> {
    protected:
        std::shared_ptr<VarMgr> var_mgr_;
        Player starting_player_;
        Player protagonist_player_;
        std::vector<int> initial_vector_;
        std::vector<CUDD::BDD> transition_vector_;
        std::unique_ptr<Quantification> quantify_independent_variables_;
        std::unique_ptr<Quantification> quantify_non_state_variables_;
 
        CUDD::BDD preimage(const CUDD::BDD &winning_states) const;
 
        CUDD::BDD project_into_states(const CUDD::BDD &winning_moves) const;
 
        bool includes_initial_state(const CUDD::BDD &winning_states) const;
 
    public:
 
        DfaGameSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player);
 
 
        virtual SynthesisResult run()
        const override = 0;
 
 
        std::unique_ptr<Transducer> AbstractSingleStrategy(const SynthesisResult &result) const;
 
    private:
        std::unique_ptr<Transducer> abstract_single_strategy(const CUDD::BDD &winning_moves,
                                                             const std::shared_ptr<VarMgr> &var_mgr,
                                                             const std::vector<int> &initial_vector,
                                                             const std::vector<CUDD::BDD> &transition_vector,
                                                             Player starting_player) const;
 
        std::unordered_map<int, CUDD::BDD>
        synthesize_strategy(const CUDD::BDD &winning_moves, const std::shared_ptr<VarMgr> &var_mgr) const;
    };
 
}
 
#endif // DFA_GAME_SYNTHESIZER_H