22#include <spot/twa/twagraph.hh>
23#include <spot/twaalgos/game.hh>
24#include <spot/twaalgos/relabel.hh>
58 SPOT_API twa_graph_ptr
60 const bdd& output_bdd,
bool complete_env =
true);
65 SPOT_API twa_graph_ptr
66 split_2step(
const const_twa_graph_ptr& aut,
bool complete_env =
true);
76 SPOT_API twa_graph_ptr
95 double total_time = 0.0;
96 double trans_time = 0.0;
97 double split_time = 0.0;
98 double paritize_time = 0.0;
99 double solve_time = 0.0;
100 double strat2aut_time = 0.0;
101 double simplify_strat_time = 0.0;
102 double aig_time = 0.0;
103 unsigned nb_states_arena = 0;
104 unsigned nb_states_arena_env = 0;
105 unsigned nb_strat_states = 0;
106 unsigned nb_strat_edges = 0;
107 unsigned nb_simpl_strat_states = 0;
108 unsigned nb_simpl_strat_edges = 0;
109 unsigned nb_latches = 0;
110 unsigned nb_gates = 0;
111 bool realizable =
false;
115 : force_sbacc{false},
119 verbose_stream{nullptr},
120 dict(make_bdd_dict())
127 std::optional<bench_var> bv;
128 std::ostream* verbose_stream;
135 SPOT_API std::ostream&
136 operator<<(std::ostream& os, synthesis_info::algo s);
140 SPOT_API std::ostream &
155 SPOT_API twa_graph_ptr
157 const std::vector<std::string>& all_outs,
159 SPOT_API twa_graph_ptr
161 const std::vector<std::string>& all_outs);
162 SPOT_API twa_graph_ptr
164 const std::vector<std::string>& all_outs,
166 SPOT_API twa_graph_ptr
168 const std::vector<std::string>& all_outs);
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
189 SPOT_API twa_graph_ptr
198 enum class realizability_code
207 realizability_code success;
225 SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
228 SPOT_API std::pair<std::vector<formula>, std::vector<std::set<formula>>>
230 const std::vector<std::string>& outs);
249 const std::vector<std::string>& output_aps,
262 relabeling_map env_map;
263 relabeling_map player_map;
282 bool split_env =
false,
283 bool split_play =
false,
284 unsigned max_letter = -1u,
285 unsigned max_letter_mult = -1u);
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
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_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
game_relabeling_map partitioned_game_relabel_here(twa_graph_ptr &arena, bool relabel_env, bool relabel_play, bool split_env=false, bool split_play=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u)
Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player dependi...
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.
mealy_like try_create_direct_strategy(formula f, const std::vector< std::string > &output_aps, synthesis_info &gi, bool want_strategy=false)
Creates a strategy for the formula given by calling all intermediate steps.
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....
void relabel_game_here(twa_graph_ptr &arena, game_relabeling_map &rel_maps)
Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order...
Definition automata.hh:27
Definition synthesis.hh:261
A struct that represents different types of mealy like objects.
Definition synthesis.hh:197
Definition synthesis.hh:94
Benchmarking data and options for synthesis.
Definition synthesis.hh:82