From a6c65dff8d026bdacf373fb738b9adb9a1b71fd5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Nov 2022 15:52:02 +0100 Subject: [PATCH] misc Doxygen fixes * 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. --- spot/misc/satsolver.hh | 6 +++--- spot/tl/formula.hh | 16 ++++++++-------- spot/twaalgos/hoa.hh | 4 ++-- spot/twaalgos/synthesis.hh | 6 +++--- spot/twaalgos/zlktree.hh | 2 +- spot/twacube_algos/convert.hh | 6 +++--- 6 files changed, 20 insertions(+), 20 deletions(-) diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh index 03a75fa02..3b5bedccd 100644 --- a/spot/misc/satsolver.hh +++ b/spot/misc/satsolver.hh @@ -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. diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index c52ed3e39..d01b8379c 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -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 diff --git a/spot/twaalgos/hoa.hh b/spot/twaalgos/hoa.hh index 74e97b567..441b9ed16 100644 --- a/spot/twaalgos/hoa.hh +++ b/spot/twaalgos/hoa.hh @@ -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` diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 115b8097c..b1b7fdf1d 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -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 diff --git a/spot/twaalgos/zlktree.hh b/spot/twaalgos/zlktree.hh index d210033e3..6d8b3270c 100644 --- a/spot/twaalgos/zlktree.hh +++ b/spot/twaalgos/zlktree.hh @@ -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. /// diff --git a/spot/twacube_algos/convert.hh b/spot/twacube_algos/convert.hh index f21aaec3f..ba739f470 100644 --- a/spot/twacube_algos/convert.hh +++ b/spot/twacube_algos/convert.hh @@ -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,