21#include <spot/twa/twa.hh>
22#include <spot/ta/taexplicit.hh>
23#include <spot/ta/tgtaexplicit.hh>
70 SPOT_API ta_explicit_ptr
71 tgba_to_ta(
const const_twa_ptr& tgba_to_convert, bdd atomic_propositions_set,
72 bool degeneralized =
true,
73 bool artificial_initial_state_mode =
true,
74 bool single_pass_emptiness_check =
false,
75 bool artificial_livelock_state_mode =
false,
76 bool no_livelock =
false);
87 SPOT_API tgta_explicit_ptr
89 bdd atomic_propositions_set);
tgta_explicit_ptr tgba_to_tgta(const const_twa_ptr &tgba_to_convert, bdd atomic_propositions_set)
Build a spot::tgta_explicit* (TGTA) from an LTL formula.
ta_explicit_ptr tgba_to_ta(const const_twa_ptr &tgba_to_convert, bdd atomic_propositions_set, bool degeneralized=true, bool artificial_initial_state_mode=true, bool single_pass_emptiness_check=false, bool artificial_livelock_state_mode=false, bool no_livelock=false)
Build a spot::ta_explicit* (TA) from an LTL formula.
Definition: automata.hh:26