alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: fix lar.old implementation

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2020-04-25 16:29:03 +02:00
parent a6da6ed95a
commit fe340ae8db
2 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
bin/ltlsynt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -286,7 +286,7 @@ namespace
spot::process_timer timer; spot::process_timer timer;
timer.start(); timer.start();
if (opt_solver == LAR) if (opt_solver == LAR || opt_solver == LAR_OLD)
{ {
trans_.set_type(spot::postprocessor::Generic); trans_.set_type(spot::postprocessor::Generic);
trans_.set_pref(spot::postprocessor::Deterministic); trans_.set_pref(spot::postprocessor::Deterministic);
@ -361,10 +361,17 @@ namespace
std::cerr << "split inputs and outputs done\nautomaton has " std::cerr << "split inputs and outputs done\nautomaton has "
<< dpa->num_states() << " states\n"; << dpa->num_states() << " states\n";
if (opt_solver == LAR) 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 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::change_parity_here(dpa, spot::parity_kind_max,
spot::parity_style_odd); spot::parity_style_odd);
if (verbose) if (verbose)

6
tests/core/ltlsynt.test
View file

@ -1,7 +1,7 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement # Copyright (C) 2017, 2019, 2020 Laboratoire de Recherche et
# de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # 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 ltl2tgba -f "!($F)" > negf_aut$i
# test ltlsynt # 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 ltlsynt -f "$F" --ins="$IN" --outs="$OUT" --algo=$algo > out$i || true
REAL=`head -1 out$i` REAL=`head -1 out$i`
test $REAL = $EXP test $REAL = $EXP