twagraph: new kill_state method

This proceeds from a discussion with Michaël Cadilhac.
http://lists.lrde.epita.fr/pipermail/spot/2021q1/000356.html

* bin/autfilt.cc (--kill-states): New option.
* NEWS: Mention those.
* spot/twa/twagraph.hh, spot/twa/twagraph.cc: Add a kill_state()
method.
* tests/core/maskkeep.test: Test it.

NEWS

@@ -31,6 +31,8 @@ New in spot 2.9.6.dev (not yet released)
     --sbacc (an alias for --state-based-acceptance) cannot be
     abbreviated as --sba anymore.
 
+  - autfilt learned a --kill-states=NUM[,NUM...] option.
+
   Library:
 
   - Historically, Spot labels automata by Boolean formulas over
@@ -176,6 +178,10 @@ New in spot 2.9.6.dev (not yet released)
   - twa_graph::merge_edges() had its two passes swapped.  Doing so
     improves the determinism of some automata.
 
+  - twa_graph::kill_state(num) is a new method that removes the
+    outgoing edge of some state.  It can be used together with
+    purge_dead_states() to remove selected states.
+
   Python:
 
   - Bindings for functions related to games.

bin/autfilt.cc

@@ -130,6 +130,7 @@ enum {
   OPT_IS_VERY_WEAK,
   OPT_IS_WEAK,
   OPT_KEEP_STATES,
+  OPT_KILL_STATES,
   OPT_MASK_ACC,
   OPT_MERGE,
   OPT_NONDET_STATES,
@@ -297,6 +298,9 @@ static const argp_option options[] =
     { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
       "only keep specified states.  The first state will be the new "\
       "initial state.  Implies --remove-unreachable-states.", 0 },
+    { "kill-states", OPT_KILL_STATES, "NUM[,NUM...]", 0,
+      "mark the specified states as dead (no successor), and remove"
+      " them.  Implies --remove-dead-states.", 0 },
     { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0,
       "put the acceptance condition in Disjunctive Normal Form", 0 },
     { "streett-like", OPT_STREETT_LIKE, nullptr, 0,
@@ -656,6 +660,7 @@ static spot::acc_cond::mark_t opt_partial_degen = {};
 static spot::acc_cond::mark_t opt_mask_acc = {};
 static std::vector<bool> opt_keep_states = {};
 static unsigned int opt_keep_states_initial = 0;
+static std::vector<unsigned> opt_kill_states = {};
 static bool opt_simpl_acc = false;
 static bool opt_simplify_exclusive_ap = false;
 static bool opt_rem_dead = false;
@@ -1019,6 +1024,19 @@ parse_opt(int key, char* arg, struct argp_state*)
           }
         break;
       }
+    case OPT_KILL_STATES:
+      {
+        std::vector<long> values = to_longs(arg);
+        for (auto res : values)
+          {
+            if (res < 0)
+              error(2, 0, "state ids should be non-negative:"
+                    " --kill-states=%ld", res);
+            opt_kill_states.push_back(res);
+          }
+        opt_rem_dead = true;
+        break;
+      }
     case OPT_MERGE:
       opt_merge = true;
       break;
@@ -1527,6 +1545,13 @@ namespace
       else if (opt_instut == 2)
         aut = spot::sl2_inplace(std::move(aut));
 
+      if (!opt_kill_states.empty())
+        {
+          unsigned ns = aut->num_states();
+          for (unsigned s: opt_kill_states)
+            if (s < ns)
+              aut->kill_state(s);
+        }
       if (!opt_keep_states.empty())
         aut = mask_keep_accessible_states(aut, opt_keep_states,
                                           opt_keep_states_initial);

spot/twa/twagraph.cc

@@ -822,6 +822,35 @@ namespace spot
     set_named_prop("state-names", names.release());
   }
 
+  void twa_graph::kill_state(unsigned state)
+  {
+    auto t = g_.out_iteraser(state);
+    while (t)
+      t.erase();
+    // A complete automaton is unlikely to stay
+    // complete after killing a state.
+    if (prop_complete().is_true())
+      prop_complete(trival::maybe());
+    prop_stutter_invariant(trival::maybe());
+    // Many properties are preserved by state removal, and may even
+    // become true if they were false before and the appropriate
+    // states are removed.
+    if (prop_universal().is_false())
+      prop_universal(trival::maybe());
+    if (prop_inherently_weak().is_false())
+      prop_inherently_weak(trival::maybe());
+    if (prop_weak().is_false())
+      prop_weak(trival::maybe());
+    if (prop_very_weak().is_false())
+      prop_very_weak(trival::maybe());
+    if (prop_terminal().is_false())
+      prop_terminal(trival::maybe());
+    if (prop_unambiguous().is_false())
+      prop_unambiguous(trival::maybe());
+    if (prop_semi_deterministic().is_false())
+      prop_semi_deterministic(trival::maybe());
+  }
+
   void twa_graph::dump_storage_as_dot(std::ostream& out,
                                       const char* opt) const
   {

spot/twa/twagraph.hh

@@ -726,6 +726,15 @@ namespace spot
     ///@}
 #endif // SWIG
 
+    /// \brief Make a state dead.
+    ///
+    /// A state is dead if it has no successors.  So this function
+    /// simply erases all edges leaving \a state.
+    ///
+    /// It can be used together with purge_dead_states() to remove a
+    /// set of states from an automaton.
+    void kill_state(unsigned state);
+
     /// \brief Print the data structures used to represent the
     /// automaton in dot's format.
     ///

tests/core/maskkeep.test

@@ -100,14 +100,38 @@ State: 1
 --END--
 EOF
 
+cat >expect5 <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-invariant weak
+--BODY--
+State: 0
+--END--
+EOF
+
 run 0 autfilt --keep-states=0,1,2 input1 -H >output
 diff output expect3
 run 0 autfilt --keep-states=0,9999,1,2 input1 -H >output
 diff output expect3
+run 0 autfilt --kill-states=99,3 input1 -H >output
+diff output expect3
 
 run 0 autfilt --keep-states=1,2,0 input1 -H >output
 diff output expect4
 
+run 0 autfilt --kill-states=1,2 --kill-states=0 input1 -H >output
+diff output expect5
+run 0 autfilt --kill-states=0 input1 -H >output
+diff output expect5
+
+# make sure the complete property is reset
+ltl2tgba 'GF(a<->Xa)' | autfilt --kill-state=1 | grep -v complete
+
 # Errors
 run 2 autfilt --keep-states=a3 input1 2> error
 cat error
@@ -115,3 +139,10 @@ grep 'failed to parse' error
 run 2 autfilt --keep-states=3-2 input1 2> error
 cat error
 grep 'non-negative: --keep-states' error
+
+run 2 autfilt --kill-states=a3 input1 2> error
+cat error
+grep 'failed to parse' error
+run 2 autfilt --kill-states=3-2 input1 2> error
+cat error
+grep 'non-negative: --kill-states' error