LTLfMaxSetSynthesizer.h

//
// Created by shuzhu on 20/01/24.
//
 
#ifndef SYFT_REACHABILITYMAXSETSYNTHESIZER_H
#define SYFT_REACHABILITYMAXSETSYNTHESIZER_H
 
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
#include "game/ReachabilityMaxSet.hpp"
 
namespace Syft {
 
    class LTLfMaxSetSynthesizer {
    private:
        std::shared_ptr<VarMgr> var_mgr_;
        SymbolicStateDfa spec_;
        Player starting_player_;
        Player protagonist_player_;
        CUDD::BDD goal_states_;
        CUDD::BDD state_space_;
 
    public:
 
        LTLfMaxSetSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player,
                              CUDD::BDD goal_states, CUDD::BDD state_space);
 
        MaxSetSynthesisResult run() const;
 
        void dump_dot(MaxSetSynthesisResult maxset, const std::string &def_filename,
                      const std::string &nondef_filename) const;
 
    };
 
}
 
#endif //SYFT_REACHABILITYMAXSETSYNTHESIZER_H