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

autfilt: fix simpification of exclusive AP

Browse source 
* bin/autfilt.cc: Here.
* tests/core/exclusive-tgba.test: Test it.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2016-04-29 12:08:32 +02:00
parent 188cb8e4ab
commit 1ceb0ed272
3 changed files with 25 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -33,6 +33,9 @@ New in spot 2.0a (not yet released)
* Typo in documentation of the -H option in --help output. * Typo in documentation of the -H option in --help output.
* The automaton parser would choke on comments like /******/. * The automaton parser would choke on comments like /******/.
* check_strength() should also set negated properties. * 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) New in spot 2.0 (2016-04-11)

11
bin/autfilt.cc
View file

@ -826,12 +826,14 @@ namespace
if (opt_mask_acc) if (opt_mask_acc)
aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); 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()) if (!opt->rem_ap.empty())
aut = opt->rem_ap.strip(aut); 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) if (opt_destut)
aut = spot::closure(std::move(aut)); aut = spot::closure(std::move(aut));
if (opt_instut == 1) if (opt_instut == 1)
@ -870,6 +872,9 @@ namespace
aut = post.run(aut, nullptr); 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) if (randomize_st || randomize_tr)
spot::randomize(aut, randomize_st, randomize_tr); spot::randomize(aut, randomize_st, randomize_tr);

15
tests/core/exclusive-tgba.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- 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). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # 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 --simplify-exclusive-ap automaton >out2
cat out2 cat out2
diff out2 expected-simpl 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`