From de9041bb31557267d1085bc3a340617eb28bd944 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 6 Aug 2022 14:06:52 +0200
Subject: [PATCH] mealy: make output_assignment the default for reduce_mealy

* spot/twaalgos/mealy_machine.hh: Here. Also cite the FORTE paper.
* doc/spot.bib (renkin.22.forte): New entry.
---
 doc/spot.bib                   | 30 +++++++++++++++++++++++-------
 spot/twaalgos/mealy_machine.hh | 28 +++++++++++++++-------------
 2 files changed, 38 insertions(+), 20 deletions(-)

diff --git a/doc/spot.bib b/doc/spot.bib
index 9d5d6b235..2a58a3031 100644
--- a/doc/spot.bib
+++ b/doc/spot.bib
@@ -214,13 +214,13 @@
   doi		= {10.1109/DepCoS-RELCOMEX.2009.31}
 }
 
-@InProceedings{	cimatti.06.fmcad,
-  author	= {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone and
-		  Tonetta, Stefano},
-  title	= {From {PSL} to {NBA}: a Modular Symbolic Encoding},
-  booktitle	= {Proceedings of the 6th conference on Formal Methods in Computer
-		  Aided Design (FMCAD'06)},
-  pages	= {125--133},
+@InProceedings{	  cimatti.06.fmcad,
+  author	= {Cimatti, Alessandro and Roveri, Marco and Semprini, Simone
+		  and Tonetta, Stefano},
+  title		= {From {PSL} to {NBA}: a Modular Symbolic Encoding},
+  booktitle	= {Proceedings of the 6th conference on Formal Methods in
+		  Computer Aided Design (FMCAD'06)},
+  pages		= {125--133},
   year		= {2006},
   publisher	= {IEEE Computer Society},
   doi		= {10.1109/FMCAD.2006.19}
@@ -858,6 +858,22 @@
   doi		= {10.1007/978-3-030-59152-6_7}
 }
 
+@InProceedings{	  renkin.22.forte,
+  author	= {Florian Renkin and Philipp Schlehuber-Caissier and
+		  Alexandre Duret-Lutz and Adrien Pommellet},
+  title		= {Effective Reductions of {M}ealy Machines},
+  year		= 2022,
+  booktitle	= {Proceedings of the 42nd International Conference on Formal
+		  Techniques for Distributed Objects, Components, and Systems
+		  (FORTE'22)},
+  series	= {Lecture Notes in Computer Science},
+  volume	= 13273,
+  pages		= {170--187},
+  month		= jun,
+  publisher	= {Springer},
+  doi		= {10.1007/978-3-031-08679-3_8}
+}
+
 @InProceedings{	  rozier.07.spin,
   author	= {Kristin Y. Rozier and Moshe Y. Vardi},
   title		= {LTL Satisfiability Checking},
diff --git a/spot/twaalgos/mealy_machine.hh b/spot/twaalgos/mealy_machine.hh
index 7406cb61d..6da0f072a 100644
--- a/spot/twaalgos/mealy_machine.hh
+++ b/spot/twaalgos/mealy_machine.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2021 Laboratoire de Recherche et Développement
+// Copyright (C) 2021-2022 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -87,28 +87,30 @@ namespace spot
   unsplit_mealy(const const_twa_graph_ptr& m);
 
   /// \brief reduce an (in)completely specified mealy machine
-  ///        Based on signature inclusion or equality. This is not guaranteed
-  ///        to find the minimal number of states but is usually faster.
-  ///        This also comes at another drawback:
-  ///        All applicable sequences have to be infinite. Finite
-  ///        traces are disregarded
-  /// \param mm The mealy machine to be minimized, has to be unsplit
+  ///
+  /// This is a bisimulation based reduction, that optionally use
+  /// inclusion between signatures to force some output when there is
+  /// a choice in order to favor more reductions.  Only infinite
+  /// traces are considered.  See \cite renkin.22.forte for details.
+  ///
+  /// \param mm The mealy machine to be minimized, has to be unsplit.
   /// \param output_assignment Whether or not to use output assignment
   /// \return A specialization of \c mm. Note that if mm is separated,
   /// the returned machine is separated as well.
-  /// \note See todo TACAS22 Effective reductions of mealy machines
-  /// @{
+    /// @{
   SPOT_API twa_graph_ptr
   reduce_mealy(const const_twa_graph_ptr& mm,
-               bool output_assignment = false);
+               bool output_assignment = true);
 
   SPOT_API void
   reduce_mealy_here(twa_graph_ptr& mm,
-                    bool output_assignment = false);
+                    bool output_assignment = true);
   /// @}
 
   /// \brief Minimizes an (in)completely specified mealy machine
-  /// The approach is described in \todo TACAS
+  ///
+  /// The approach is described in \cite renkin.22.forte.
+  ///
   /// \param premin Use reduce_mealy before applying the
   ///               main algorithm if demanded AND
   ///               the original machine has no finite trace.
@@ -159,4 +161,4 @@ namespace spot
   SPOT_API void
   simplify_mealy_here(twa_graph_ptr& m, synthesis_info& si,
                       bool split_out);
-}
\ No newline at end of file
+}