diff --git a/NEWS b/NEWS index b7488181b..212bd4dad 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,9 @@ New in spot 2.0.0a (not yet released) * Typo in documentation of the -H option in --help output. * The automaton parser would choke on comments like /******/. * check_strength() should also set negated properties. + * Fix autfilt to apply --simplify-exclusive-ap only after + the simplifications of (--small/--deterministic) have + been performed. New in spot 2.0 (2016-04-11) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 54c9128cf..6ef36513d 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -711,12 +711,14 @@ namespace if (opt_mask_acc) aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); - if (!opt->excl_ap.empty()) - aut = opt->excl_ap.constrain(aut, opt_simplify_exclusive_ap); - if (!opt->rem_ap.empty()) aut = opt->rem_ap.strip(aut); + // opt_simplify_exclusive_ap is handled only after + // post-processing. + if (!opt->excl_ap.empty()) + aut = opt->excl_ap.constrain(aut, false); + if (opt_destut) aut = spot::closure(std::move(aut)); if (opt_instut == 1) @@ -755,6 +757,9 @@ namespace aut = post.run(aut, nullptr); + if (opt_simplify_exclusive_ap && !opt->excl_ap.empty()) + aut = opt->excl_ap.constrain(aut, opt_simplify_exclusive_ap); + if (randomize_st || randomize_tr) spot::randomize(aut, randomize_st, randomize_tr); diff --git a/tests/core/exclusive-tgba.test b/tests/core/exclusive-tgba.test index eb7a74263..59e0093f0 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 Laboratoire de Recherche et Développement de +# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -160,3 +160,16 @@ run 0 autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ --simplify-exclusive-ap automaton >out2 cat out2 diff out2 expected-simpl + + +# Example from the paper +test "6,50,14" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' --stats='%s,%t,%e'` +test "6,24,12" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | + autfilt --exclusive-ap=a,b,c --stats='%s,%t,%e'` +test "5,22,10" = `ltl2tgba -B -f 'F(Ga | (GFb <-> GFc))' | + autfilt --small --exclusive-ap=a,b,c --stats='%s,%t,%e' --ap=3` +# The final automaton has 3 atomic propositions before +# simplifications, but only 2 after that. +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`