22 #include <spot/twa/twagraph.hh>
23 #include <spot/twaalgos/game.hh>
57 SPOT_API twa_graph_ptr
59 const bdd& output_bdd,
bool complete_env =
true);
64 SPOT_API twa_graph_ptr
65 split_2step(
const const_twa_graph_ptr& aut,
bool complete_env =
true);
75 SPOT_API twa_graph_ptr
93 double total_time = 0.0;
94 double trans_time = 0.0;
95 double split_time = 0.0;
96 double paritize_time = 0.0;
97 double solve_time = 0.0;
98 double strat2aut_time = 0.0;
99 double simplify_strat_time = 0.0;
100 double aig_time = 0.0;
101 unsigned nb_states_arena = 0;
102 unsigned nb_states_arena_env = 0;
103 unsigned nb_strat_states = 0;
104 unsigned nb_strat_edges = 0;
105 unsigned nb_simpl_strat_states = 0;
106 unsigned nb_simpl_strat_edges = 0;
107 unsigned nb_latches = 0;
108 unsigned nb_gates = 0;
109 bool realizable =
false;
113 : force_sbacc{false},
117 verbose_stream{nullptr},
118 dict(make_bdd_dict())
125 std::optional<bench_var> bv;
126 std::ostream* verbose_stream;
133 SPOT_API std::ostream&
134 operator<<(std::ostream& os, synthesis_info::algo s);
138 SPOT_API std::ostream &
153 SPOT_API twa_graph_ptr
155 const std::vector<std::string>& all_outs,
157 SPOT_API twa_graph_ptr
159 const std::vector<std::string>& all_outs);
160 SPOT_API twa_graph_ptr
162 const std::vector<std::string>& all_outs,
164 SPOT_API twa_graph_ptr
166 const std::vector<std::string>& all_outs);
177 SPOT_API twa_graph_ptr
179 SPOT_API twa_graph_ptr
181 SPOT_API twa_graph_ptr
183 SPOT_API twa_graph_ptr
185 SPOT_API twa_graph_ptr
187 SPOT_API twa_graph_ptr
196 enum class realizability_code
205 realizability_code success;
223 SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
226 SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
228 const std::vector<std::string>& outs);
245 const std::vector<std::string>& output_aps,
Manage a map of options.
Definition: optionmap.hh:38
bool solve_game(const twa_graph_ptr &arena)
Generic interface for game solving.
twa_graph_ptr solved_game_to_split_mealy(twa_graph_ptr arena, synthesis_info &gi)
creates a mealy machine from a solved game arena taking into account the options given in gi....
twa_graph_ptr split_2step(const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env=true)
make each transition a 2-step transition, transforming the graph into an alternating arena
twa_graph_ptr solved_game_to_separated_mealy(twa_graph_ptr arena, synthesis_info &gi)
creates a mealy machine from a solved game arena taking into account the options given in gi....
twa_graph_ptr unsplit_2step(const const_twa_graph_ptr &aut)
the inverse of split_2step
twa_graph_ptr ltl_to_game(const formula &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
Creates a game from a specification and a set of output propositions.
std::pair< std::vector< formula >, std::vector< std::set< formula > > > split_independant_formulas(formula f, const std::vector< std::string > &outs)
Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-p...
twa_graph_ptr solved_game_to_mealy(twa_graph_ptr arena, synthesis_info &gi)
creates a mealy machine from a solved game arena taking into account the options given in gi....
mealy_like try_create_direct_strategy(formula f, const std::vector< std::string > &output_aps, synthesis_info &gi)
Creates a strategy for the formula given by calling all intermediate steps.
Definition: automata.hh:27
A struct that represents different types of mealy like objects.
Definition: synthesis.hh:195
Definition: synthesis.hh:92
Benchmarking data and options for synthesis.
Definition: synthesis.hh:81