21#include <spot/misc/common.hh>
22#include <spot/twa/fwd.hh>
24#include <spot/tl/nenoform.hh>
43 SPOT_API twa_graph_ptr
65 SPOT_API twa_graph_ptr
67 bool deterministic =
true,
bool state_based =
false);
74 SPOT_API twa_graph_ptr
76 bool deterministic =
true,
bool state_based =
false);
86 SPOT_API twa_graph_ptr
95 SPOT_API twa_graph_ptr
97 bool state_based =
false);
twa_graph_ptr gf_guarantee_to_ba(formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
Convert GF(φ) into a (D)BA if φ is a guarantee property.
twa_graph_ptr fg_safety_to_dca(formula fg, const bdd_dict_ptr &dict, bool state_based=false)
Convert FG(φ) into a DCA if φ is a safety property.
twa_graph_ptr fg_safety_to_dca_maybe(formula fg, const bdd_dict_ptr &dict, bool state_based)
Convert FG(φ) into a DCA if φ is a safety property.
twa_graph_ptr gf_guarantee_to_ba_maybe(formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
Convert GF(φ) into a (D)BA if φ is a guarantee property.
twa_graph_ptr g_f_terminal_inplace(twa_graph_ptr f_terminal, bool state_based=false)
Given a terminal automaton f_terminal recognizing some formula F(φ), modify it to recognize GF(φ).
Definition: automata.hh:26