21#include <spot/twa/twagraph.hh>
22#include <spot/twaalgos/powerset.hh>
112 SPOT_API twa_graph_ptr
115 const_twa_graph_ptr aut_neg_f =
nullptr,
116 bool reject_bigger =
false,
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:44
bool minimize_obligation_guaranteed_to_work(const const_twa_graph_ptr &aut_f, formula f=nullptr)
Whether calling minimize_obligation is sure to work.
twa_graph_ptr minimize_monitor(const const_twa_graph_ptr &a)
Construct a minimal deterministic monitor.
twa_graph_ptr minimize_wdba(const const_twa_graph_ptr &a, const output_aborter *aborter=nullptr)
Minimize a Büchi automaton in the WDBA class.
twa_graph_ptr minimize_obligation(const const_twa_graph_ptr &aut_f, formula f=nullptr, const_twa_graph_ptr aut_neg_f=nullptr, bool reject_bigger=false, const output_aborter *aborter=nullptr)
Minimize an automaton if it represents an obligation property.
Definition: automata.hh:26