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

more doxygen

Browse source 
This introduce some section for acceptance transformation, and add
more comments in a few places.

* spot/taalgos/emptinessta.hh, spot/twa/twa.hh, spot/twa/twagraph.hh,
spot/twaalgos/bfssteps.hh, spot/twaalgos/cleanacc.hh,
spot/twaalgos/degen.hh, spot/twaalgos/dualize.hh,
spot/twaalgos/parity.hh, spot/twaalgos/rabin2parity.hh,
spot/twaalgos/remfin.hh, spot/twaalgos/sccinfo.hh,
spot/twaalgos/sepsets.hh, spot/twaalgos/split.hh,
spot/twaalgos/totgba.hh: More doxygen.
* spot/twa/twagraph.cc: Typos in comments.
This commit is contained in:
Alexandre Duret-Lutz 2018-01-18 18:00:11 +01:00
parent 7e02aae366
commit 1a0fa3b722
15 changed files with 115 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

10
spot/taalgos/emptinessta.hh
View file

@ -1,9 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2012, 2013, 2014, 2016 Laboratoire de Recherche
// Copyright (C) 2012-2014, 2016, 2018 Laboratoire de Recherche
// et Dévelopment de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -39,7 +36,8 @@ namespace spot
/// \addtogroup ta_emptiness_check Emptiness-checks
/// \ingroup ta_algorithms
///
/// \ingroup ta_emptiness_check
/// \brief Check whether the language of a product (spot::ta_product) between
/// a Kripke structure and a TA is empty. It works also for the product
/// using Generalized TA (GTA and SGTA).
@ -156,6 +154,4 @@ namespace spot
/// @}
/// \addtogroup ta_emptiness_check_algorithms Emptiness-check algorithms
/// \ingroup ta_emptiness_check
}

3
spot/twa/twa.hh
View file

@ -1690,6 +1690,9 @@ namespace spot
/// \addtogroup stutter_inv Stutter-invariance checks
/// \ingroup twa_algorithms
/// \addtogroup twa_acc_transform Conversion between acceptance conditions
/// \ingroup twa_algorithms
/// \addtogroup twa_ltl Translating LTL formulas into TωA
/// \ingroup twa_algorithms

8
spot/twa/twagraph.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -494,8 +494,8 @@ namespace spot
// #3 get rid of the unused universal destinations
// #4 merge identical universal destinations
//
// graph::degrag_states() actually does only #1. It it could
// do #2, but that would prevent use from doing #3 and #4. It
// graph::degrag_states() actually does only #1. It could
// do #2, but that would prevent us from doing #3 and #4. It
// cannot do #3 and #4 because the graph object does not know
// what an initial state is, and our initial state might be
// universal.

68
spot/twa/twagraph.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement de l'Epita.
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -29,6 +29,12 @@
namespace spot
{
/// \ingroup twa_representation
/// \brief Graph-based representation of a TωA
///
/// In a twa_graph, states are usually denoted by their number. However
/// if the on-the-fly interface is used, it returns pointer to instances
/// of the twa_graph_state class.
struct SPOT_API twa_graph_state: public spot::state
{
public:
@ -69,6 +75,13 @@ namespace spot
}
};
/// \ingroup twa_representation
/// \brief Data attached to edges of a twa_graph
///
/// Each edge of the graph has to additional data that are \a cond
/// (a BDD representing the Boolean formula labeling the edge), and
/// \a acc a set of acceptance marks representing the membership of
/// the each to each acceptance set.
struct SPOT_API twa_graph_edge_data
{
bdd cond;
@ -101,6 +114,11 @@ namespace spot
};
/// \ingroup twa_representation
/// \brief Iterator used by the on-the-fly interface of twa_graph.
///
/// Instances of this class are returned by twa_graph::succ_iter().
template<class Graph>
class SPOT_API twa_graph_succ_iterator final:
public twa_succ_iterator
@ -165,6 +183,8 @@ namespace spot
};
/// \ingroup twa_representation
/// \brief Graph-based representation of a TωA
class SPOT_API twa_graph final: public twa
{
public:
@ -505,11 +525,25 @@ namespace spot
SPOT_RETURN(g_.is_dead_edge(t));
#endif
/// Iterate over all edges, and merge those with compatible
/// extremities and acceptance.
/// \brief Merge edges that can be merged.
///
/// This makes two passes over the automaton to reduce the number
/// of edges with an identical pair of source and destination.
///
/// In the first pass, edges that share their source, destination,
/// and acceptance marks are merged into a single edge whose condition
/// is the conjunction of the conditions of the original edges.
///
/// In the second pass, which is performed only on automata with
/// Fin-less acceptance, edges with the same source, destination,
/// and conditions are merged into a single edge whose set of
/// acceptance marks is the intersection of the sets of the edges.
///
/// If the automaton uses some universal edges, the method
/// merge_univ_dests() is also called.
void merge_edges();
/// \brief marge common universal destination
/// \brief Merge common universal destinations.
///
/// This is already called by merge_edges().
void merge_univ_dests();
@ -559,6 +593,8 @@ namespace spot
/// assumed.
void copy_state_names_from(const const_twa_graph_ptr& other);
/// \brief Return the marks associated to a state if the
/// acceptance is state-based.
acc_cond::mark_t state_acc_sets(unsigned s) const
{
if (SPOT_UNLIKELY(!(bool)prop_state_acc()))
@ -572,6 +608,12 @@ namespace spot
return 0U;
}
/// \brief Tell if a state is acceptince.
///
/// This makes only sense for automata using state-based
/// acceptance, and a simple acceptance condition like Büchi or
/// co-Büchi.
///@{
bool state_is_accepting(unsigned s) const
{
if (SPOT_UNLIKELY(!(bool)prop_state_acc()))
@ -589,6 +631,7 @@ namespace spot
{
return state_is_accepting(state_number(s));
}
///@}
bool operator==(const twa_graph& aut) const
{
@ -608,17 +651,26 @@ namespace spot
dests2.begin());
}
/// \brief Renumber all states, and drop some.
///
/// This semi-internal function is a wrapper around
/// digraph::defrag_state() that additionally deals with universal
/// branching.
///
/// \param newst A vector indicating how each state should be renumbered.
/// Use -1U to erase a state.
/// \param used_states the number of states used (after renumbering)
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
};
/// \ingroup twa
/// \ingroup twa_representation
/// \brief Build an explicit automaton from all states of \a aut,
inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict)
{
return std::make_shared<twa_graph>(dict);
}
/// \ingroup twa
/// \ingroup twa_representation
/// \brief Build an explicit automaton from all states of \a aut,
inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut,
twa::prop_set p)
@ -626,7 +678,7 @@ namespace spot
return std::make_shared<twa_graph>(aut, p);
}
/// \ingroup twa
/// \ingroup twa_representation
/// \brief Build an explicit automaton from all states of \a aut,
inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut,
twa::prop_set p)
@ -634,7 +686,7 @@ namespace spot
return std::make_shared<twa_graph>(aut, p);
}
/// \ingroup twa
/// \ingroup twa_representation
/// \brief Build an explicit automaton from all states of \a aut,
///
/// This overload works using the abstract interface for automata.

6
spot/twaalgos/bfssteps.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2011, 2013, 2014, 2018 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -27,7 +27,7 @@
namespace spot
{
/// \ingroup twa_misc
/// \ingroup twa_generic
/// \brief Make a BFS in a spot::tgba to compute a twa_run::steps.
///
/// This class should be used to compute the shortest path

10
spot/twaalgos/cleanacc.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -23,7 +23,7 @@
namespace spot
{
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Remove useless acceptance sets
///
/// This removes from the automaton the acceptance marks that are
@ -37,7 +37,7 @@ namespace spot
SPOT_API twa_graph_ptr
cleanup_acceptance_here(twa_graph_ptr aut, bool strip = true);
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Remove useless acceptance sets
///
/// This removes from the automaton the acceptance marks that are
@ -49,7 +49,7 @@ namespace spot
cleanup_acceptance(const_twa_graph_ptr aut);
/// @{
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Simplify an acceptance condition
///
/// Does evereything cleanup_acceptance() does, but additionally:

6
spot/twaalgos/degen.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 2015, 2017, Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2012-2015, 2017, 2018 Laboratoire de
// Recherche et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -23,7 +23,7 @@
namespace spot
{
/// \ingroup twa_misc
/// \ingroup twa_acc_transform
/// \brief Degeneralize a spot::tgba into an equivalent sba with
/// only one acceptance condition.
///

5
spot/twaalgos/dualize.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -24,6 +24,7 @@
namespace spot
{
/// \ingroup twa_misc
/// \brief Complement an automaton by dualizing it.
///
/// Given an automaton \a aut of any type, produces the dual as output. The

2
spot/twaalgos/parity.hh
View file

@ -25,7 +25,7 @@
namespace spot
{
/// \addtogroup parity_algorithms Algorithms for parity acceptance
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \ingroup parity_algorithms
/// @{

11
spot/twaalgos/rabin2parity.hh
View file

@ -22,6 +22,7 @@
namespace spot
{
/// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like automaton into a parity automaton based on the
/// index appearence record (IAR)
///
@ -34,12 +35,18 @@ namespace spot
/// acceptance condition.
/// Details on the algorithm can be found in:
/// https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
///
/// Throws an std::runtime_error if the input is not Rabin-like.
SPOT_API
twa_graph_ptr
iar(const const_twa_graph_ptr& aut);
/// Return nullptr if the input automaton is not Rabin-like, and calls iar()
/// otherwise.
/// \ingroup twa_acc_transform
/// \brief Turn a Rabin-like automaton into a parity automaton based on the
/// index appearence record (IAR)
///
/// Return nullptr if the input automaton is not Rabin-like, and
/// calls spot::iar() otherwise.
SPOT_API
twa_graph_ptr
iar_maybe(const const_twa_graph_ptr& aut);

8
spot/twaalgos/remfin.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
// de l'Epita.
// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -23,7 +23,7 @@
namespace spot
{
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Convert a Rabin automaton to Büchi automaton, preserving
/// determinism when possible.
///
@ -40,7 +40,7 @@ namespace spot
SPOT_API twa_graph_ptr
rabin_to_buchi_maybe(const const_twa_graph_ptr& aut);
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Rewrite an automaton without Fin acceptance.
///
/// This algorithm dispatches between many strategies. It has

9
spot/twaalgos/sccinfo.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2017 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -211,7 +211,8 @@ namespace spot
}
/// Storage for SCC related information.
/// \ingroup twa_misc
/// \brief Storage for SCC related information.
class SPOT_API scc_info_node
{
public:
@ -298,7 +299,8 @@ namespace spot
}
};
/// Options to alter the behavior of scc_info
/// \ingroup twa_misc
/// \brief Options to alter the behavior of scc_info
enum class scc_info_options
{
/// Stop exploring when an accepting SCC is found, and do not track
@ -347,6 +349,7 @@ namespace spot
| static_cast<ut>(right));
}
/// \ingroup twa_misc
/// \brief Compute an SCC map and gather assorted information.
///
/// This takes twa_graph as input and compute its SCCs. This

4
spot/twaalgos/sepsets.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -23,10 +23,12 @@
namespace spot
{
/// \ingroup twa_acc_transform
/// \brief Whether the Inf and Fin numbers are disjoints
SPOT_API bool
has_separate_sets(const const_twa_graph_ptr& aut);
/// \ingroup twa_acc_transform
/// \brief Separate the Fin and Inf sets used by an automaton
///
/// This makes sure that the numbers used a Fin and Inf are

3
spot/twaalgos/split.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2017 Laboratoire de Recherche et Développement
// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -23,6 +23,7 @@
namespace spot
{
/// \ingroup twa_misc
/// \brief transform edges into transitions
///
/// Create a new version of the automaton where all edges are split

11
spot/twaalgos/totgba.hh
View file

@ -25,7 +25,7 @@
namespace spot
{
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Büchi automaton.
///
@ -37,13 +37,13 @@ namespace spot
SPOT_API twa_graph_ptr
to_generalized_buchi(const const_twa_graph_ptr& aut);
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \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
/// \ingroup twa_acc_transform
/// \brief Convert Streett acceptance into generalized Büchi
///
/// This version only works SPOT_STREET_CONF_MIN is set to a number
@ -53,7 +53,7 @@ namespace spot
SPOT_API twa_graph_ptr
streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in);
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Rabin automaton.
///
@ -68,7 +68,7 @@ namespace spot
to_generalized_rabin(const const_twa_graph_ptr& aut,
bool share_inf = false);
/// \ingroup twa_algorithms
/// \ingroup twa_acc_transform
/// \brief Take an automaton with any acceptance condition and return
/// an equivalent Generalized Streett automaton.
///
@ -83,6 +83,7 @@ namespace spot
to_generalized_streett(const const_twa_graph_ptr& aut,
bool share_fin = false);
/// \ingroup twa_acc_transform
/// \brief Converts any DNF acceptance condition into Streett-like.
///
/// This function is an optimized version of the construction described