BuchiReachability.hpp

//
// Created by shuzhu on 16/04/24.
//
 
#ifndef LYDIASYFT_BUCHIREACHABILITY_HPP
#define LYDIASYFT_BUCHIREACHABILITY_HPP
 
#include "game/DfaGameSynthesizer.h"
 
namespace Syft {
    class BuchiReachability : public DfaGameSynthesizer {
    private:
        CUDD::BDD goal_states_;
        CUDD::BDD state_space_;
        CUDD::BDD Buchi_;
 
    public:
 
        BuchiReachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player,
                          const CUDD::BDD &goal_states, const CUDD::BDD &Buchi, const CUDD::BDD &state_space);
 
 
        SynthesisResult run() const final;
 
    };
}
 
 
#endif //LYDIASYFT_BUCHIREACHABILITY_HPP