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

misc Doxygen fixes

Browse source 
* spot/misc/satsolver.hh, spot/tl/formula.hh, spot/twaalgos/hoa.hh,
spot/twaalgos/synthesis.hh, spot/twaalgos/zlktree.hh,
spot/twacube_algos/convert.hh: Typos in Doxygen comments.
This commit is contained in:
Alexandre Duret-Lutz 2022-11-08 15:52:02 +01:00
parent 0f4f7ec287
commit a6c65dff8d
6 changed files with 20 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/misc/satsolver.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2017-2018, 2020 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2013, 2017-2018, 2020, 2022 Laboratoire de Recherche
// et Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
@ -88,7 +88,7 @@ namespace spot
/// \brief Add a single lit. to the current clause.
void add(int v);
/// \breif Get the current number of clauses.
/// \brief Get the current number of clauses.
int get_nb_clauses() const;
/// \brief Get the current number of variables.

16
spot/tl/formula.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015-2021 Laboratoire de Recherche et Développement
// Copyright (C) 2015-2022 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -1227,12 +1227,12 @@ namespace spot
return bunop(op::Name, std::move(f), min, max); \
}
#endif
/// \brief Create SERE for f[*min..max]
/// \brief Create SERE for `f[*min..max]`
/// @{
SPOT_DEF_BUNOP(Star);
/// @}
/// \brief Create SERE for f[:*min..max]
/// \brief Create SERE for `f[:*min..max]`
///
/// This operator is a generalization of the (+) operator
/// defined by Dax et al. \cite dax.09.atva
@ -1259,24 +1259,24 @@ namespace spot
f.ptr_->clone()));
}
/// \brief Create a SERE equivalent to b[->min..max]
/// \brief Create a SERE equivalent to `b[->min..max]`
///
/// The operator does not exist: it is handled as syntactic sugar
/// by the parser and the printer. This function is used by the
/// parser to create the equivalent SERE.
static formula sugar_goto(const formula& b, unsigned min, unsigned max);
/// Create the SERE b[=min..max]
/// \brief Create the SERE `b[=min..max]`
///
/// The operator does not exist: it is handled as syntactic sugar
/// by the parser and the printer. This function is used by the
/// parser to create the equivalent SERE.
static formula sugar_equal(const formula& b, unsigned min, unsigned max);
/// Create the SERE a ##[n:m] b
/// \brief Create the SERE `a ##[n:m] b`
///
/// This ##[n:m] operator comes from SVA. When n=m, it is simply
/// written ##n.
/// This `##[n:m]` operator comes from SVA. When n=m, it is simply
/// written `##n`.
///
/// The operator does not exist in Spot it is handled as syntactic
/// sugar by the parser. This function is used by the parser to

4
spot/twaalgos/hoa.hh
View file

@ -95,7 +95,7 @@ namespace spot
/// registered in the automaton is not only ignored, but also
/// removed from the alias list stored in the automaton.
///
/// The \a or_str, \a and_str, and \ap_printer arguments are
/// The \a or_str, \a and_str, and \a ap_printer arguments are
/// used to print operators OR, AND, and to print atomic propositions
/// that are not aliases. \a lpar_str and \a rpar_str are used
/// to group conjuncts that appear in a disjunction.
@ -119,7 +119,7 @@ namespace spot
///
/// - If an alias A exists for \a label, `"@A"` is returned.
///
/// - If an alias A exists for the negation of \a label, `"!@A`
/// - If an alias A exists for the negation of \a label, `"!@A"`
/// is returned.
///
/// - If \a label is true or false, `true_str` or `false_str`

6
spot/twaalgos/synthesis.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2020-2021 Laboratoire de Recherche et
// Copyright (C) 2020-2022 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -36,8 +36,8 @@ namespace spot
/// p -- cond --> q cond in 2^2^AP
/// into a set of transitions of the form
/// p -- {a} --> (p,a) -- o --> q
/// for each a in cond \cap 2^2^I
/// and where o = (cond & a) \cap 2^2^(O)
/// for each a in cond ∪ 2^2^I
/// and where o = (cond & a) ∪ 2^2^O.
///
/// By definition, the states p are deterministic,
/// only the states of the form

2
spot/twaalgos/zlktree.hh
View file

@ -481,7 +481,7 @@ namespace spot
///
/// If \a colored is set, each output transition will have exactly
/// one color, and the output automaton will use at most n+1 colors
/// if the input has n colors. If \colored is unsed (the default),
/// if the input has n colors. If \a colored is unsed (the default),
/// output transitions will use at most one color, and output
/// automaton will use at most n colors.
///

6
spot/twacube_algos/convert.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016, 2020 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2015, 2016, 2020, 2022 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -51,7 +51,7 @@ namespace spot
twa_to_twacube(spot::const_twa_graph_ptr aut);
/// \brief Convert a twacube into a twa.
/// When \d is specified, the BDD_dict in parameter is used rather than
/// When \a d is specified, the BDD_dict in parameter is used rather than
/// creating a new one.
SPOT_API spot::twa_graph_ptr
twacube_to_twa(spot::twacube_ptr twacube,