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

* spot/twaalgos/postproc.cc: Improve to_parity() call.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2020-04-15 11:41:46 +02:00
parent d7ab8dbe13
commit 801d629a20
1 changed files with 18 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

33
spot/twaalgos/postproc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // Copyright (C) 2012-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.
@ -274,22 +274,25 @@ namespace spot
!(type_ == Generic && PREF_ == Any && level_ == Low)) !(type_ == Generic && PREF_ == Any && level_ == Low))
a = remove_alternation(a); a = remove_alternation(a);
if ((via_gba && !a->acc().is_generalized_buchi()) if ((via_gba || (want_parity && !a->acc().is_parity()))
|| (want_parity && !a->acc().is_parity())) && !a->acc().is_generalized_buchi())
{ {
twa_graph_ptr b = nullptr; // If we do want a parity automaton, we can use to_parity().
if (want_parity && is_deterministic(a) && // However (1) degeneralization is better if the input is
!a->acc().is_generalized_buchi()) // GBA, and (2) if we want a deterministic parity automaton and the
b = to_parity(a); // input is not deterministic, that is useless here. We need
// possible only if a was deterministic and (Rabin-like or Streett-like) // to determinize it first, and our deterministization
// and we want parity and a is not a TGBA // function only deal with TGBA as input.
// NB: on a TGBA, degeneralization is better than IAR if (want_parity && (PREF_ != Deterministic || is_deterministic(a)))
if (b) {
a = b; a = to_parity(a);
}
else else
a = to_generalized_buchi(a); {
if (PREF_ == Any && level_ == Low) a = to_generalized_buchi(a);
a = do_scc_filter(a, true); if (PREF_ == Any && level_ == Low)
a = do_scc_filter(a, true);
}
} }
if (PREF_ == Any && level_ == Low if (PREF_ == Any && level_ == Low