From 483212d27547bf3c7fa00ece9f77442d85c84acc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 25 Mar 2015 21:29:42 +0100
Subject: [PATCH] Make --keep-states more useful by actually removing states.

Fixes #70.

We don't modify the behavior of mask_keep_states(), because it is
actually useful in some algorithm to remove states without renumbering
all the other states.

* src/bin/autfilt.cc: Call purge_dead_states().
* src/tgbatest/maskkeep.test: Adjust.
---
 src/bin/autfilt.cc         |  5 ++++-
 src/tgbatest/maskkeep.test | 40 ++++++++------------------------------
 2 files changed, 12 insertions(+), 33 deletions(-)

diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index d17fa3aa8..837af8132 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -506,7 +506,10 @@ namespace
       // Postprocessing.
 
       if (!opt_keep_states.empty())
-	aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
+	{
+	  aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
+	  aut->purge_dead_states();
+	}
       if (opt_mask_acc)
 	aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
 
diff --git a/src/tgbatest/maskkeep.test b/src/tgbatest/maskkeep.test
index a5d966a5c..3ad825795 100755
--- a/src/tgbatest/maskkeep.test
+++ b/src/tgbatest/maskkeep.test
@@ -48,7 +48,7 @@ EOF
 
 cat >expect1 <<EOF
 HOA: v1
-States: 4
+States: 1
 Start: 0
 AP: 0
 acc-name: generalized-Buchi 2
@@ -56,25 +56,6 @@ Acceptance: 2 Inf(0)&Inf(1)
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0
-State: 1
-State: 2
-State: 3
---END--
-EOF
-
-cat >expect2 <<EOF
-HOA: v1
-States: 4
-Start: 1
-AP: 0
-acc-name: generalized-Buchi 2
-Acceptance: 2 Inf(0)&Inf(1)
-properties: trans-labels explicit-labels state-acc deterministic
---BODY--
-State: 0
-State: 1
-State: 2
-State: 3
 --END--
 EOF
 
@@ -82,11 +63,11 @@ run 0 ../../bin/autfilt --keep-states=0 input1 -H >output
 diff output expect1
 
 run 0 ../../bin/autfilt --keep-states=1 input1 -H >output
-diff output expect2
+diff output expect1
 
 cat >expect3 <<EOF
 HOA: v1
-States: 4
+States: 3
 Start: 0
 AP: 2 "a" "b"
 acc-name: generalized-Buchi 2
@@ -100,27 +81,22 @@ State: 1
 [0] 2
 State: 2
 [1] 1
-State: 3
 --END--
 EOF
 
 cat >expect4 <<EOF
 HOA: v1
-States: 4
-Start: 1
+States: 2
+Start: 0
 AP: 2 "a" "b"
 acc-name: generalized-Buchi 2
 Acceptance: 2 Inf(0)&Inf(1)
-properties: trans-labels explicit-labels trans-acc
+properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0
-[0] 1 {0}
-[1] 2 {1}
+[0] 1
 State: 1
-[0] 2
-State: 2
-[1] 1
-State: 3
+[1] 0
 --END--
 EOF