GR1LTLfSynthesizer.h

//
// Created by shuzhu on 21/01/24.
//
 
#ifndef LYDIASYFT_GR1LTLFSYNTHESIZER_H
#define LYDIASYFT_GR1LTLFSYNTHESIZER_H
 
#include "automata/ExplicitStateDfaAdd.h"
#include "GR1.h"
#include "Stopwatch.h"
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
#include "game/DfaGameSynthesizer.h"
 
 
namespace Syft {
    class GR1LTLfSynthesizer {
    private:
        const std::shared_ptr<VarMgr> var_mgr_;
        const GR1 gr1_;
        const SymbolicStateDfa env_safety_;
        const SymbolicStateDfa agn_safety_;
        const SymbolicStateDfa agn_reach_;
        const std::string benchmark_name_;
        const std::string slugs_dir_;
 
    public:
        GR1LTLfSynthesizer(const std::shared_ptr<VarMgr> &var_mgr, const GR1 &gr1,
                           const SymbolicStateDfa &env_safety,
                           const SymbolicStateDfa &agn_reach, const SymbolicStateDfa &agn_safety,
                           const std::string &slugs_dir,
                           const std::string &benchmark_name);
 
        SynthesisResult run() const;
 
    };
}
#endif //LYDIASYFT_GR1LTLFSYNTHESIZER_H