diff --git a/NEWS b/NEWS index 73f9b9cb9..39d078500 100644 --- a/NEWS +++ b/NEWS @@ -24,6 +24,11 @@ New in spot 2.7.2.dev (not yet released) acc_cond::acc_code::top_conjuncts() can be used to split an acceptance condition on the top-level & or |. + - minimize_obligation() learned to work on very weak automata even + if the formula or negated automaton are not supplied. (This + allows "autfilt [-D] --small" to minimize very-weak automata + whenever they are found to represent obligation properties.) + Bugs fixed: - When processing CSV files with MSDOS-style \r\n line endings, diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 42aed0b12..c024d204b 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2010-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -45,6 +45,7 @@ #include #include #include +#include #include namespace spot @@ -570,8 +571,12 @@ namespace spot ("minimize_obligation() does not support alternation"); // FIXME: We should build scc_info once, pass it to minimize_wdba - // and reuse it for is_terminal_automaton(), and - // is_weak_automaton(). + // and reuse it for is_terminal_automaton(), + // is_weak_automaton(), and is_very_weak_automaton(). + // FIXME: we should postpone the call to minimize_wdba() until + // we know for sure that we can verify (or that we do not need + // to verify) its output, rather than computing in cases where + // we may discard it. auto min_aut_f = minimize_wdba(aut_f); if (reject_bigger) @@ -614,9 +619,15 @@ namespace spot // Remove useless SCCs. aut_neg_f = scc_filter(aut_neg_f, true); } + else if (is_very_weak_automaton(aut_f)) + { + // Very weak automata are easy to complement. + aut_neg_f = remove_alternation(dualize(aut_f)); + } else { - // Otherwise, we cannot check if the minimization is safe. + // Otherwise, we don't try to complement the automaton and + // therefore we cannot check if the minimization is safe. return nullptr; } } diff --git a/tests/core/optba.test b/tests/core/optba.test index 65ce06824..52b52e725 100755 --- a/tests/core/optba.test +++ b/tests/core/optba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017, 2019 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -160,3 +160,14 @@ test `autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18 # But we should have 19 with Büchi acceptance, not 20. test `autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19 + + +# This should be reduced to a 3-state minimal WDBA if we +# correctly recognize that this is an obligation. Issue #379. +cat >in <