alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twaalgos: more doxygen comments

Browse source 
* spot/twaalgos/product.hh, spot/twaalgos/remfin.hh,
spot/twaalgos/sum.hh, spot/twaalgos/totgba.hh: Improve documentation.
This commit is contained in:
Alexandre Duret-Lutz 2018-01-15 22:18:22 +01:00
parent c920825fad
commit d94fb07168
4 changed files with 89 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

60
spot/twaalgos/product.hh
View file

@ -26,24 +26,80 @@
namespace spot
{
// The tgba constructed by product() below contain property named
// "product-states" with type product_states.
/// \brief Automata constructed by product() contain a property
/// named "product-states" with this type
typedef std::vector<std::pair<unsigned, unsigned>> product_states;
/// \ingroup twa_algorithms
/// \brief Intersect two automata using a synchronous product
///
/// The resulting automaton will accept the intersection of both
/// languages and have an acceptance condition that is the
/// conjunction of the acceptance conditions of the two input
/// automata.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
/// the pair of original state numbers associated to each state of
/// the product.
SPOT_API
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \ingroup twa_algorithms
/// \brief Intersect two automata using a synchronous product
///
/// These variant allow changing the initial state of both automata
/// in case you want to start the product at a different place.
///
/// The resulting automaton will accept the intersection of the
/// languages recognized by each input automaton (with its initial
/// state changed) and have an acceptance condition that is the
/// conjunction of the acceptance conditions of the two input
/// automata.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
/// the pair of original state numbers associated to each state of
/// the product.
SPOT_API
twa_graph_ptr product(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,
unsigned left_state,
unsigned right_state);
/// \ingroup twa_algorithms
/// \brief Sum two automata using a synchronous product
///
/// The resulting automaton will accept the union of both
/// languages and have an acceptance condition that is the
/// disjunction of the acceptance conditions of the two input
/// automata.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
/// the pair of original state numbers associated to each state of
/// the product.
SPOT_API
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \ingroup twa_algorithms
/// \brief Sum two automata using a synchronous product
///
/// These variant allow changing the initial state of both automata
/// in case you want to start the product at a different place.
///
/// The resulting automaton will accept the sum of the languages
/// recognized by each input automaton (with its initial state
/// changed) and have an acceptance condition that is the
/// disjunction of the acceptance conditions of the two input
/// automata.
///
/// The algorithm also defines a named property called
/// "product-states" with type spot::product_states. This stores
/// the pair of original state numbers associated to each state of
/// the product.
SPOT_API
twa_graph_ptr product_or(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right,

15
spot/twaalgos/remfin.hh
View file

@ -23,11 +23,12 @@
namespace spot
{
/// \brief Convert a state-based Rabin automaton to Büchi automaton,
/// preserving determinism when possible.
/// \ingroup twa_algorithms
/// \brief Convert a Rabin automaton to Büchi automaton, preserving
/// determinism when possible.
///
/// Return nullptr if the input is not a Rabin automaton, or is not
/// state-based.
/// Return nullptr if the input is not a Rabin (or Rabin-like)
/// automaton.
///
/// This essentially applies the algorithm from "Deterministic
/// ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan,
@ -39,7 +40,13 @@ namespace spot
SPOT_API twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut);
/// \ingroup twa_algorithms
/// \brief Rewrite an automaton without Fin acceptance.
///
/// This algorithm dispatches between many strategies. It has
/// dedicated algorithms for weak automata, automata with Rabin-like
/// acceptance, automata with Streett-like acceptance, and some
/// generic code that will work on any kind of acceptance condition.
SPOT_API twa_graph_ptr
remove_fin(const const_twa_graph_ptr& aut);
}

4
spot/twaalgos/sum.hh
View file

@ -24,6 +24,7 @@
namespace spot
{
/// \ingroup twa_algorithms
/// \brief Sum two twa into a new twa, performing the union of the two input
/// automata.
///
@ -34,6 +35,7 @@ namespace spot
twa_graph_ptr sum(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \ingroup twa_algorithms
/// \brief Sum two twa into a new twa, performing the union of the two input
/// automata.
///
@ -48,6 +50,7 @@ namespace spot
unsigned left_state,
unsigned right_state);
/// \ingroup twa_algorithms
/// \brief Sum two twa into a new twa, using a universal initial transition,
/// performing the intersection of the two languages of the input automata.
///
@ -58,6 +61,7 @@ namespace spot
twa_graph_ptr sum_and(const const_twa_graph_ptr& left,
const const_twa_graph_ptr& right);
/// \ingroup twa_algorithms
/// \brief Sum two twa into a new twa, using a universal initial transition,
/// performing the intersection of the two languages of the input automata.
///

18
spot/twaalgos/totgba.hh
View file

@ -25,22 +25,35 @@
namespace spot
{
/// \ingroup twa_algorithms
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Büchi automaton.
///
/// This dispatch between many algorithms. If the input has Streett
/// (or Streett-like) acceptance,
/// spot::streett_to_generalized_buchi() is called right away and
/// produces a TGBA. Otherwise, it calls spot::remove_in() which
/// returns a TBA.
SPOT_API twa_graph_ptr
to_generalized_buchi(const const_twa_graph_ptr& aut);
/// \ingroup twa_algorithms
/// \brief Convert Streett acceptance into generalized Büchi
/// acceptance.
SPOT_API twa_graph_ptr
streett_to_generalized_buchi(const const_twa_graph_ptr& in);
/// \ingroup twa_algorithms
/// \brief Convert Streett acceptance into generalized Büchi
/// only if SPOT_STREET_CONF_MIN is set to a number of pairs
/// less than the number of pairs used by IN.
///
/// This version only works SPOT_STREET_CONF_MIN is set to a number
/// of pairs less than the number of pairs used by \a in. The
/// default is 3. It returns nullptr of that condition is not met,
/// or if the input automaton does not have Streett-like acceptance.
SPOT_API twa_graph_ptr
streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in);
/// \ingroup twa_algorithms
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Rabin automaton.
///
@ -55,6 +68,7 @@ namespace spot
to_generalized_rabin(const const_twa_graph_ptr& aut,
bool share_inf = false);
/// \ingroup twa_algorithms
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Streett automaton.
///