diff --git a/NEWS b/NEWS index 9701c15ed..c962cd4ff 100644 --- a/NEWS +++ b/NEWS @@ -60,6 +60,12 @@ New in spot 2.6.1.dev (not yet released) colors 0-7, and that higher color numbers cycle into this 16-color palette. + Bugs fixed: + + - exclusive_ap::constrain() (called by autfilt --exclusive-ap=...) + would incorrectly copy the "universal" property of the input + automaton, causing print_hoa() to fail. + New in spot 2.6.1 (2018-08-04) Command-line tools: diff --git a/spot/tl/exclusive.cc b/spot/tl/exclusive.cc index 979b8fe94..4d863eaf0 100644 --- a/spot/tl/exclusive.cc +++ b/spot/tl/exclusive.cc @@ -178,7 +178,7 @@ namespace spot twa_graph_ptr res = make_twa_graph(aut->get_dict()); res->copy_ap_of(aut); - res->prop_copy(aut, { true, true, false, true, false, true }); + res->prop_copy(aut, { true, true, false, false, false, true }); res->copy_acceptance_of(aut); if (simplify_guards) { diff --git a/tests/core/exclusive-tgba.test b/tests/core/exclusive-tgba.test index 59e0093f0..9262546b7 100755 --- a/tests/core/exclusive-tgba.test +++ b/tests/core/exclusive-tgba.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -173,3 +173,9 @@ test "5,22,10" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | autfilt --small --exclusive-ap=a,b,c --simplify-ex --ap=3 > out test "5,21,10" = `autfilt out --stats='%s,%t,%e' --ap=2` + + +# Issue #363. +ltl2tgba 'a U b' | + autfilt --exclusive-ap=a,b,c --simplify-exclusive-ap > out +test "2,8,3" = `autfilt out --stats='%s,%t,%e' --ap=2`