diff --git a/NEWS b/NEWS index cad2abe75..a9504c67a 100644 --- a/NEWS +++ b/NEWS @@ -8,6 +8,10 @@ New in spot 2.3.2.dev (not yet released) - The output of 'genltl --r-left=1 --r-right=1 --format=%F' had typos. + - 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that + the output is "terminal" because dtwa_complement() failed to reset + that property. + New in spot 2.3.2 (2017-03-15) Tools: diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 03f9c24c4..9fff15ef6 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -18,7 +18,7 @@ // along with this program. If not, see . #include -#include +#include #include #include @@ -27,9 +27,19 @@ namespace spot twa_graph_ptr dtwa_complement(const const_twa_graph_ptr& aut) { + if (!is_deterministic(aut)) + throw + std::runtime_error("dtwa_complement() requires a deterministic input"); + // Simply complete the automaton, and complement its acceptance. auto res = cleanup_acceptance_here(complete(aut)); res->set_acceptance(res->num_sets(), res->get_acceptance().complement()); + // Complementing the acceptance is likely to break the terminal + // property, but not weakness. We make a useless call to + // prop_keep() just so we remember to update it in the future if a + // new argument is added. + res->prop_keep({true, true, true, true, true}); + res->prop_terminal(trival::maybe()); return res; } } diff --git a/tests/core/complement.test b/tests/core/complement.test index 2c03e0604..6a1f4c1c2 100755 --- a/tests/core/complement.test +++ b/tests/core/complement.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -22,12 +22,8 @@ set -e -autfilt=autfilt -ltl2tgba=ltl2tgba -randaut=randaut - -$randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut -run 0 $autfilt --complement -H aut >/dev/null +randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut +run 0 autfilt --complement -H aut >/dev/null cat >in <out +autfilt --complement -H in >out cat >expected <out +ltl2tgba -H 'GFa & GFb' Xa Fa | autfilt --complement -H >out cat >expected <out +ltl2tgba -H 'FGa' | autfilt --complement >out cat >expected <