FairnessLtlfSynthesizer.h

//
// Created by shuzhu on 20/01/24.
//
 
#ifndef LYDIASYFT_FAIRNESSLTLFSYNTHESIZER_H
#define LYDIASYFT_FAIRNESSLTLFSYNTHESIZER_H
 
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
 
#include "game/coGR1Reachability.hpp"
#include "game/coBuchiReachability.hpp"
 
namespace Syft {
 
    class FairnessLtlfSynthesizer {
    private:
        std::shared_ptr<VarMgr> var_mgr_;
        SymbolicStateDfa spec_;
        Player starting_player_;
        Player protagonist_player_;
        CUDD::BDD goal_states_;
        CUDD::BDD state_space_;
        CUDD::BDD assumption_;
 
    protected:
        CUDD::BDD load_CNF(const std::string &filename) const;
 
    public:
 
        FairnessLtlfSynthesizer(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player,
                                const CUDD::BDD &goal_states, const CUDD::BDD &state_space,
                                const std::string &assumption_filename);
 
        SynthesisResult run() const;
 
    };
 
}
 
#endif //LYDIASYFT_FAIRNESSLTLFSYNTHESIZER_H