Benchmarking variables tracking timing and counts for each step of synthesis. More...

#include <spot/twaalgos/synthesis.hh>

Collaboration diagram for spot::synthesis_info::bench_var:

Public Attributes
unsigned	sub_specs = 0
	Number of sub-specifications, after decomposition. More...

double	total_time = 0.0
	Total synthesis time. More...

double	sum_trans_time = 0.0
	Total LTL-to-automaton translation time. More...

double	sum_split_time = 0.0
	Total automaton splitting time. More...

double	sum_paritize_time = 0.0
	Total paritization time. More...

double	sum_solve_time = 0.0
	Total game solving time. More...

double	sum_strat2aut_time = 0.0
	Total strategy-to-automaton conversion time. More...

double	sum_simplify_strat_time = 0.0
	Total strategy simplification time. More...

double	aig_time = 0.0
	Total AIG encoding time. More...

unsigned	max_trans_states = 0
	Max translated automaton states. More...

unsigned	max_trans_edges = 0
	Max translated automaton edges. More...

unsigned	max_trans_colors = 0
	Max translated automaton colors. More...

unsigned	max_trans_ap = 0
	Max translated automaton APs. More...

unsigned	max_game_states = 0
	Max game states. More...

unsigned	max_game_colors = 0
	Max game colors. More...

unsigned	max_strat_states = 0
	Max strategy states. More...

unsigned	max_strat_edges = 0
	Max strategy edges. More...

unsigned	sum_strat_states = 0
	Total strategy states. More...

unsigned	sum_strat_edges = 0
	Total strategy edges. More...

unsigned	max_simpl_strat_states = 0
	Max simplified strategy states. More...

unsigned	max_simpl_strat_edges = 0
	Max simplified strategy edges. More...

unsigned	sum_simpl_strat_states = 0
	Total simplified strategy states. More...

unsigned	sum_simpl_strat_edges = 0
	Total simplified strategy edges. More...

unsigned	aig_latches = 0
	Number of AIG latches. More...

unsigned	aig_gates = 0
	Number of AIG gates. More...

bool	realizable = false
	Whether the specification is realizable. More...

Detailed Description

Benchmarking variables tracking timing and counts for each step of synthesis.

The sum_* and max_* variables make more sense when the specification is split into multiple sub-specifications. In this case, sum_*‍/max_* variables are sums/max over all sub-specifications.

Member Data Documentation

◆ aig_gates

unsigned spot::synthesis_info::bench_var::aig_gates = 0

Number of AIG gates.

◆ aig_latches

unsigned spot::synthesis_info::bench_var::aig_latches = 0

Number of AIG latches.

◆ aig_time

double spot::synthesis_info::bench_var::aig_time = 0.0

Total AIG encoding time.

◆ max_game_colors

unsigned spot::synthesis_info::bench_var::max_game_colors = 0

Max game colors.

◆ max_game_states

unsigned spot::synthesis_info::bench_var::max_game_states = 0

Max game states.

◆ max_simpl_strat_edges

unsigned spot::synthesis_info::bench_var::max_simpl_strat_edges = 0

Max simplified strategy edges.

◆ max_simpl_strat_states

unsigned spot::synthesis_info::bench_var::max_simpl_strat_states = 0

Max simplified strategy states.

◆ max_strat_edges

unsigned spot::synthesis_info::bench_var::max_strat_edges = 0

Max strategy edges.

◆ max_strat_states

unsigned spot::synthesis_info::bench_var::max_strat_states = 0

Max strategy states.

◆ max_trans_ap

unsigned spot::synthesis_info::bench_var::max_trans_ap = 0

Max translated automaton APs.

◆ max_trans_colors

unsigned spot::synthesis_info::bench_var::max_trans_colors = 0

Max translated automaton colors.

◆ max_trans_edges

unsigned spot::synthesis_info::bench_var::max_trans_edges = 0

Max translated automaton edges.

◆ max_trans_states

unsigned spot::synthesis_info::bench_var::max_trans_states = 0

Max translated automaton states.

◆ realizable

bool spot::synthesis_info::bench_var::realizable = false

Whether the specification is realizable.

◆ sub_specs

unsigned spot::synthesis_info::bench_var::sub_specs = 0

Number of sub-specifications, after decomposition.

◆ sum_paritize_time

double spot::synthesis_info::bench_var::sum_paritize_time = 0.0

Total paritization time.

◆ sum_simpl_strat_edges

unsigned spot::synthesis_info::bench_var::sum_simpl_strat_edges = 0

Total simplified strategy edges.

◆ sum_simpl_strat_states

unsigned spot::synthesis_info::bench_var::sum_simpl_strat_states = 0

Total simplified strategy states.

◆ sum_simplify_strat_time

double spot::synthesis_info::bench_var::sum_simplify_strat_time = 0.0

Total strategy simplification time.

◆ sum_solve_time

double spot::synthesis_info::bench_var::sum_solve_time = 0.0

Total game solving time.

◆ sum_split_time

double spot::synthesis_info::bench_var::sum_split_time = 0.0

Total automaton splitting time.

◆ sum_strat2aut_time

double spot::synthesis_info::bench_var::sum_strat2aut_time = 0.0

Total strategy-to-automaton conversion time.

◆ sum_strat_edges

unsigned spot::synthesis_info::bench_var::sum_strat_edges = 0

Total strategy edges.

◆ sum_strat_states

unsigned spot::synthesis_info::bench_var::sum_strat_states = 0

Total strategy states.

◆ sum_trans_time

double spot::synthesis_info::bench_var::sum_trans_time = 0.0

Total LTL-to-automaton translation time.

◆ total_time

double spot::synthesis_info::bench_var::total_time = 0.0

Total synthesis time.

The documentation for this struct was generated from the following file:

spot/twaalgos/synthesis.hh

Public Attributes