22#include <spot/twa/twagraph.hh>
23#include <spot/tl/apcollect.hh>
24#include <spot/tl/simplify.hh>
25#include <spot/twaalgos/powerset.hh>
78 SPOT_API twa_graph_ptr
80 bool exprop =
false,
bool symb_merge =
true,
81 bool branching_postponement =
false,
82 bool fair_loop_approx =
false,
85 bool unambiguous =
false,
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:44
Rewrite or simplify f in various ways.
Definition: simplify.hh:109
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition: apcollect.hh:33
twa_graph_ptr ltl_to_tgba_fm(formula f, const bdd_dict_ptr &dict, bool exprop=false, bool symb_merge=true, bool branching_postponement=false, bool fair_loop_approx=false, const atomic_prop_set *unobs=nullptr, tl_simplifier *simplifier=nullptr, bool unambiguous=false, const output_aborter *aborter=nullptr)
Build a spot::twa_graph_ptr from an LTL or PSL formula.
Definition: automata.hh:26