ReachabilityMaxSet.hpp

//
// Created by shuzhu on 16/04/24.
//
 
#ifndef LYDIASYFT_REACHABILITYMAXSET_HPP
#define LYDIASYFT_REACHABILITYMAXSET_HPP
 
 
#include "game/DfaGameSynthesizer.h"
 
namespace Syft {
    class ReachabilityMaxSet : public DfaGameSynthesizer {
    private:
        CUDD::BDD goal_states_;
        CUDD::BDD state_space_;
 
    public:
 
        ReachabilityMaxSet(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player,
                           const CUDD::BDD &goal_states, const CUDD::BDD &state_space);
 
 
        MaxSetSynthesisResult run_maxset() const;
 
        SynthesisResult run() const final;
 
        void dump_dot(MaxSetSynthesisResult maxset, const std::string &def_filename,
                      const std::string &nondef_filename) const;
 
    };
}
 
 
#endif //LYDIASYFT_REACHABILITYMAXSET_HPP