From de5704049d2de88cb20e44f34531e77ca831dc52 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 16 Feb 2020 08:20:21 +0100
Subject: [PATCH] tgba_determinize: improve citations in doc

* doc/spot.bib (klein.07.ciaa, redziejowski.12.fi): Add two entries.
* spot/twaalgos/determinize.hh: Use them.
---
 doc/spot.bib                 | 27 +++++++++++++++++++++++++++
 spot/twaalgos/determinize.hh | 20 ++++++++++----------
 2 files changed, 37 insertions(+), 10 deletions(-)

diff --git a/doc/spot.bib b/doc/spot.bib
index bcb1452d4..027ec695a 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
@@ -384,6 +385,21 @@
   doi		= {10.4204/EPTCS.229.10}
 }
 
+@InCollection{	  klein.07.ciaa,
+  year		= {2007},
+  booktitle	= {Proceedings of the 12th International Conference on the
+		  Implementation and Application of Automata (CIAA'07)},
+  volume	= {4783},
+  series	= {Lecture Notes in Computer Science},
+  editor	= {Jan Holub and Jan Žďárek},
+  doi		= {10.1007/978-3-540-76336-9_7},
+  title		= {On-the-Fly Stuttering in the Construction of Deterministic
+		  $\omega$-Automata},
+  publisher	= {Springer},
+  author	= {Joachim Klein and Christel Baier},
+  pages		= {51--61}
+}
+
 @InProceedings{	  kretisnky.12.cav,
   author	= {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza},
   title		= {Deterministic Automata for the {(F,G)}-Fragment of {LTL}},
@@ -585,6 +601,17 @@
   url		= {http://www.eda.org/vfv/}
 }
 
+@Article{	  redziejowski.12.fi,
+  author	= {Roman Redziejowski},
+  title		= {An improved construction of deterministic omega-automaton
+		  using derivatives},
+  journal	= {Fundamenta Informaticae},
+  year		= {2012},
+  volume	= {119},
+  number	= {3-4},
+  pages		= {393--496}
+}
+
 @InProceedings{	  renault.13.tacas,
   author	= {Etienne Renault and Alexandre Duret-Lutz and Fabrice
 		  Kordon and Denis Poitrenaud},
diff --git a/spot/twaalgos/determinize.hh b/spot/twaalgos/determinize.hh
index ab0c993a5..c588ff9aa 100644
--- a/spot/twaalgos/determinize.hh
+++ b/spot/twaalgos/determinize.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015, 2016, 2019 Laboratoire de Recherche et
+// Copyright (C) 2015-2016, 2019-2020 Laboratoire de Recherche et
 // Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -34,20 +34,20 @@ namespace spot
   /// The output will be a deterministic automaton using parity acceptance.
   ///
   /// This procedure is based on an algorithm by Roman Redziejowski
-  /// (Fundamenta Informaticae 119, 3-4 (2012)).  Redziejowski's
-  /// algorithm is similar to Piterman's improvement of Safra's
-  /// algorithm, except it is presented on transition-based acceptance
-  /// and use simpler notations.  We implement three additional
-  /// optimizations (they can be individually disabled) based on
+  /// \cite redziejowski.12.fi .  Redziejowski's algorithm is similar
+  /// to Piterman's improvement of Safra's algorithm, except it is
+  /// presented on transition-based acceptance and use simpler
+  /// notations.  We implement three additional optimizations (they
+  /// can be individually disabled) based on
   ///
   ///   - knowledge about SCCs of the input automaton
   ///   - knowledge about simulation relations in the input automaton
   ///   - knowledge about stutter-invariance of the input automaton
   ///
-  /// The last optimization is an idea described by Joachim Klein &
-  /// Christel Baier (CIAA'07) and implemented in ltl2dstar.  In fact,
-  /// ltl2dstar even has a finer version (letter-based stuttering)
-  /// that is not implemented here.
+  /// The last optimization is an idea implemented in
+  /// [`ltl2dstar`](https://www.ltl2dstar.fr) \cite klein.07.ciaa .  In
+  /// fact, `ltl2dstar` even has a finer version (letter-based
+  /// stuttering) that is not implemented here.
   ///
   /// \param aut the automaton to determinize
   ///