From 3dc084c4f6da24e0da99eabce8ca5dafc3648cdb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 18 Oct 2016 22:39:54 +0200
Subject: [PATCH] use mask_keep_accessible_states

* bin/autfilt.cc, spot/twaalgos/isweakscc.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sccinfo.cc: Use mask_keep_accessible_states instead of
mask_keep_states.
---
 bin/autfilt.cc             | 4 ++--
 spot/twaalgos/isweakscc.cc | 6 +++---
 spot/twaalgos/remfin.cc    | 4 ++--
 spot/twaalgos/sccinfo.cc   | 3 ++-
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index f2fdc796b..136ad3936 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -685,7 +685,6 @@ parse_opt(int key, char* arg, struct argp_state*)
               opt_keep_states.resize(res + 1, false);
             opt_keep_states[res] = true;
           }
-        opt_rem_unreach = true;
         break;
       }
     case OPT_MERGE:
@@ -1125,7 +1124,8 @@ namespace
         aut = spot::sl2(std::move(aut));
 
       if (!opt_keep_states.empty())
-        aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
+        aut = mask_keep_accessible_states(aut, opt_keep_states,
+                                          opt_keep_states_initial);
       if (opt_rem_dead)
         aut->purge_dead_states();
       else if (opt_rem_unreach)
diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc
index a6e1b636f..e7ab80ba1 100644
--- a/spot/twaalgos/isweakscc.cc
+++ b/spot/twaalgos/isweakscc.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-// Developpement de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// et Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -33,7 +33,7 @@ namespace spot
     auto& states = map.states_of(scc);
     for (auto s: states)
       keep[s] = true;
-    auto sccaut = mask_keep_states(aut, keep, states.front());
+    auto sccaut = mask_keep_accessible_states(aut, keep, states.front());
     sccaut->set_acceptance(sccaut->acc().num_sets(),
                            sccaut->get_acceptance().complement());
     return !sccaut->is_empty();
diff --git a/spot/twaalgos/remfin.cc b/spot/twaalgos/remfin.cc
index e10a19f37..1525fba41 100644
--- a/spot/twaalgos/remfin.cc
+++ b/spot/twaalgos/remfin.cc
@@ -82,10 +82,10 @@ namespace spot
           std::vector<bool> keep(aut->num_states(), false);
           for (auto s: states)
             keep[s] = true;
-          auto sccaut = mask_keep_states(aut, keep, states.front());
+          auto sccaut = mask_keep_accessible_states(aut, keep, states.front());
           // Force SBA to false.  It does not affect the emptiness
           // check result, however it prevent recurring into this
-          // procedure, because empty() will call to_tgba() wich will
+          // procedure, because empty() will call to_tgba() which will
           // call remove_fin()...
           sccaut->prop_state_acc(false);
           // If SCCAUT is empty, the SCC is BA-type (and none
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index ace20913b..c94935306 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -330,7 +330,8 @@ namespace spot
             k.resize(aut_->num_states());
           for (auto i: node.states_)
             k[i] = true;
-          if (mask_keep_states(aut_, k, node.states_.front())->is_empty())
+          if (mask_keep_accessible_states(aut_, k, node.states_.front())
+              ->is_empty())
             node.rejecting_ = true;
           else
             node.accepting_ = true;