From 1ceb0ed2721b54e6d77cd119c013ce2a9be7e73d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 29 Apr 2016 12:08:32 +0200
Subject: [PATCH] autfilt: fix simpification of exclusive AP

* bin/autfilt.cc: Here.
* tests/core/exclusive-tgba.test: Test it.
* NEWS: Mention the fix.
---
 NEWS                           |  3 +++
 bin/autfilt.cc                 | 11 ++++++++---
 tests/core/exclusive-tgba.test | 15 ++++++++++++++-
 3 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index 2b0472c9a..fb63801c2 100644
--- a/NEWS
+++ b/NEWS
@@ -33,6 +33,9 @@ New in spot 2.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 5924bf642..528b2358e 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -826,12 +826,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)
@@ -870,6 +872,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`