From fe340ae8db67a64011ffd0ae64c59f896a68648e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 25 Apr 2020 16:29:03 +0200
Subject: [PATCH] ltlsynt: fix lar.old implementation

* bin/ltlsynt.cc: Make sure to_parity_old() receive a deterministic
automaton, for correctness.   Also call reduce_parity() afterward,
to match what was done in 2.8.7.
* tests/core/ltlsynt.test: Include lar.old in the comparison of all
results to make sure it give the same result as the other 3
algorithms.
---
 bin/ltlsynt.cc          | 17 ++++++++++++-----
 tests/core/ltlsynt.test |  6 +++---
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 30d3d56db..3ca12960f 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -286,7 +286,7 @@ namespace
       spot::process_timer timer;
       timer.start();
 
-      if (opt_solver == LAR)
+      if (opt_solver == LAR || opt_solver == LAR_OLD)
         {
           trans_.set_type(spot::postprocessor::Generic);
           trans_.set_pref(spot::postprocessor::Deterministic);
@@ -361,10 +361,17 @@ namespace
                 std::cerr << "split inputs and outputs done\nautomaton has "
                           << dpa->num_states() << " states\n";
               if (opt_solver == LAR)
-                dpa = spot::to_parity(dpa);
+                {
+                  dpa = spot::to_parity(dpa);
+                  // reduce_parity is called by to_parity(),
+                  // but with colorization turned off.
+                  spot::colorize_parity_here(dpa, true);
+                }
               else
-                dpa = spot::to_parity_old(dpa);
-              spot::colorize_parity_here(dpa, true);
+                {
+                  dpa = spot::to_parity_old(dpa);
+                  dpa = reduce_parity_here(dpa, true);
+                }
               spot::change_parity_here(dpa, spot::parity_kind_max,
                                        spot::parity_style_odd);
               if (verbose)
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 5a1886e8c..e5915ce28 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2017, 2019, 2020 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -199,7 +199,7 @@ for i in 2 3 4 5 6 10; do
   ltl2tgba -f "!($F)" > negf_aut$i
 
   # test ltlsynt
-  for algo in sd ds lar; do
+  for algo in sd ds lar lar.old; do
     ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
     REAL=`head -1 out$i`
     test $REAL = $EXP