22 #include <spot/twaalgos/postproc.hh>
23 #include <spot/tl/simplify.hh>
78 build_simplifier(dict);
85 build_simplifier(make_bdd_dict());
94 using postprocessor::output_type;
97 set_type(output_type type)
102 using postprocessor::output_pref;
105 set_pref(output_pref pref)
110 using postprocessor::optimization_level;
113 set_level(optimization_level level)
118 auto d = simpl_owned_->get_dict();
122 if (!gf_guarantee_set_)
123 gf_guarantee_ = level != Low;
142 void build_simplifier(
const bdd_dict_ptr& dict);
143 twa_graph_ptr run_aux(
formula f);
154 bool gf_guarantee_ =
true;
155 bool gf_guarantee_set_ =
false;
157 int branchpost_ = -1;
158 unsigned tls_max_states_ = 64;
159 unsigned tls_max_ops_ = 16;
Manage a map of options.
Definition: optionmap.hh:38
Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface.
Definition: postproc.hh:67
void set_pref(output_pref pref)
Select the desired characteristics of the output automaton.
Definition: postproc.hh:197
void set_type(output_type type)
Select the desired output type.
Definition: postproc.hh:139
Rewrite or simplify f in various ways.
Definition: simplify.hh:110
Translate an LTL formula into an optimized spot::tgba.
Definition: translate.hh:65
twa_graph_ptr run(formula f)
Convert f into an automaton.
void clear_caches()
Clear the LTL simplification caches.
twa_graph_ptr run(formula *f)
Convert f into an automaton, and update f.
Definition: automata.hh:27