From 28a6471efbae8ebea5568bb650f0c4d3b4501168 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 5 Sep 2023 11:39:13 +0200
Subject: [PATCH] forq: fix bib entry and bind the doxygen doc to a group

* doc/spot.bib: Reformat the FORQ reference in the style of the
rest of the bibliographic file.
* spot/twaalgos/forq_contains.hh: Adjust, and add missing \ingroup.
---
 doc/spot.bib                   | 29 +++++++++++++++--------------
 spot/twaalgos/forq_contains.hh | 34 ++++++++++++++++++----------------
 2 files changed, 33 insertions(+), 30 deletions(-)

diff --git a/doc/spot.bib b/doc/spot.bib
index 2ca89c721..c645c8156 100644
--- a/doc/spot.bib
+++ b/doc/spot.bib
@@ -1,3 +1,4 @@
+
 @InProceedings{	  babiak.12.tacas,
   author	= {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r
 		  K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k
@@ -185,7 +186,7 @@
   month		= apr,
   volume	= {13244},
   pages		= {99--117},
-  doi		= {10.1007/978-3-030-99527-0_6},
+  doi		= {10.1007/978-3-030-99527-0_6}
 }
 
 @InProceedings{	  cerna.03.mfcs,
@@ -336,17 +337,17 @@
   month		= aug
 }
 
-@inproceedings{doveriFORQBasedLanguageInclusion2022,
-  title = {{{FORQ-Based Language Inclusion Formal Testing}}},
-  booktitle = {{{CAV}}'22: {{Proc}}. 32nd {{Int}}. {{Conf}}. on {{Computer Aided Verification}}},
-  author = {Doveri, Kyveli and Ganty, Pierre and Mazzocchi, Nicolas},
-  year = {2022},
-  volume = {13372},
-  pages = {109--129},
-  publisher = {{Springer International Publishing}},
-  doi = {10.1007/978-3-031-13188-2_6},
-  urldate = {2022-09-15},
-  isbn = {978-3-031-13187-5 978-3-031-13188-2}
+@InProceedings{	  doveri.22.cav,
+  title		= {{FORQ}-Based Language Inclusion Formal Testing},
+  booktitle	= {Proceedings of the 32nd International Conference on
+		  Computer Aided Verification (CAV'22)},
+  author	= {Kyveli Doveri and Pierre Ganty and Nicolas Mazzocchi},
+  year		= {2022},
+  volume	= {13372},
+  pages		= {109--129},
+  publisher	= {Springer International Publishing},
+  doi		= {10.1007/978-3-031-13188-2_6},
+  month		= aug
 }
 
 @InProceedings{	  duret.11.vecos,
@@ -1099,7 +1100,8 @@
   publisher	= {Elsevier},
   editor	= {Rance Cleaveland and Hubert Garavel},
   year		= {2002},
-  month		= jul,  pdf		= {adl/duret.16.atva.pdf},
+  month		= jul,
+  pdf		= {adl/duret.16.atva.pdf},
   abstract	= {Checking liveness properties with partial-order reductions
 		  requires a cycle proviso to ensure that an action cannot be
 		  postponed forever. The proviso forces each cycle to contain
@@ -1111,7 +1113,6 @@
 		  the source of this edge, while this paper also explores the
 		  expansion of the destination and the use of SCC-based
 		  information.},
-
   address	= {M{\'a}laga, Spain},
   doi		= {10.1016/S1571-0661(04)80409-2}
 }
diff --git a/spot/twaalgos/forq_contains.hh b/spot/twaalgos/forq_contains.hh
index 24e2e8065..3d49c5498 100644
--- a/spot/twaalgos/forq_contains.hh
+++ b/spot/twaalgos/forq_contains.hh
@@ -23,29 +23,31 @@
 
 namespace spot
 {
+  /// \ingroup containment
   /// \brief Returns a word accepted by \a left that is rejected by \a right,
   /// or nullptr.
   ///
-  /// This implements the language containment algorithm from
-  /// \cite{doveriFORQBasedLanguageInclusion2022}
-  /// to check whether L(left)⊆L(right), in which case, it returns nullptr.
-  /// Otherwise, it returns a counterexample, i.e., a word that is accepted
-  /// by $L(left)\setminus L(right)$, hence the name of the function.
+  /// This implements a FORQ-based language containment algorithm
+  /// \cite doveri.22.cav to check whether L(left)⊆L(right), in which
+  /// case, it returns nullptr.  Otherwise, it returns a
+  /// counterexample, i.e., a word that is accepted by
+  /// $L(left)\setminus L(right)$, hence the name of the function.
   ///
-  /// \pre Automata \a left and \a right should be
-  /// non-alternating state-based Büchi-automata.
-  SPOT_API twa_word_ptr difference_word_forq(
-    const_twa_graph_ptr left, spot::const_twa_graph_ptr right);
+  /// \pre Automata \a left and \a right should be non-alternating
+  /// Büchi-automata.
+  SPOT_API
+  twa_word_ptr difference_word_forq(const_twa_graph_ptr left,
+                                    const_twa_graph_ptr right);
 
+  /// \ingroup containment
   /// \brief Returns a boolean value indicating
   /// whether \a left is included in the language of \a right.
   ///
-  /// This implements the language containment algorithm from
-  /// \cite{doveriFORQBasedLanguageInclusion2022}
-  /// to check whether L(left)⊆L(right).
+  /// This implements a FORQ-based language containment algorithm
+  /// to check whether L(left)⊆L(right). \cite doveri.22.cav
   ///
-  /// \pre Automata \a left and \a right should be
-  /// non-alternating state-based Büchi-automata.
-  SPOT_API bool contains_forq(
-    const_twa_graph_ptr left, const_twa_graph_ptr right);
+  /// \pre Automata \a left and \a right should be non-alternating
+  /// Büchi-automata.
+  SPOT_API
+  bool contains_forq(const_twa_graph_ptr left, const_twa_graph_ptr right);
 }