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