coGR1Reachability.hpp

//
// Created by shuzhu on 18/04/24.
//
 
#ifndef LYDIASYFT_COGR1REACHABILITY_HPP
#define LYDIASYFT_COGR1REACHABILITY_HPP
 
#include "GR1.h"
#include "automata/SymbolicStateDfa.h"
#include "Synthesizer.h"
 
namespace Syft {
    class coGR1Reachability {
    private:
        const std::shared_ptr<VarMgr> var_mgr_;
        const GR1 gr1_;
        const SymbolicStateDfa arena_;
        const CUDD::BDD state_space_;
        const CUDD::BDD initial_condition_;
        const std::string benchmark_name_;
        const std::string slugs_dir_;
 
        void print_variables(const std::string &filename) const;
 
        void print_initial_conditions(const CUDD::BDD &arena_initial_state_bdd, const std::string &filename) const;
 
        void print_transitions(const SymbolicStateDfa &arena, const CUDD::BDD &safe_states,
                               const std::string &filename) const;
 
        void print_liveness_constraints(const std::string &filename) const;
 
        std::string get_slugs_path() const;
 
 
    public:
 
        coGR1Reachability(const std::shared_ptr<VarMgr> &var_mgr, const GR1 &gr1,
                          const SymbolicStateDfa &arena,
                          const CUDD::BDD &state_space,
                          const CUDD::BDD &initial_condition,
                          const std::string &slugs_dir,
                          const std::string &benchmark_name);
 
        const std::string exec_slugs(const std::string &slugs, const std::string &slugs_input_file,
                                     const std::string &slugs_res_file, const std::string &slugs_strategy_file) const;
 
 
        SynthesisResult run() const;
 
        coGR1Reachability(SymbolicStateDfa dfa, Player player, Player player1, CUDD::BDD bdd, CUDD::BDD bdd1,
                          CUDD::BDD bdd2);
    };
}
 
 
#endif //LYDIASYFT_COGR1REACHABILITY_HPP