StabilityLtlfSynthesizer.h

//
// Created by shuzhu on 21/01/24.
//
 
#ifndef LYDIASYFT_STABILITYLTLFSYNTHESIZER_H
#define LYDIASYFT_STABILITYLTLFSYNTHESIZER_H
 
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
#include "game/BuchiReachability.hpp"
 
namespace Syft {
 
 
    class StabilityLtlfSynthesizer {
    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:
 
        StabilityLtlfSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player,
                                 CUDD::BDD goal_states, CUDD::BDD state_space,
                                 const std::string &assumption_filename);
 
 
        SynthesisResult run() const;
 
    };
 
}
 
#endif //LYDIASYFT_STABILITYLTLFSYNTHESIZER_H