autfilt: --remove-unreachable-states, --remove-dead-states

Add these two options as an answer to comments in
https://github.com/adl/hoaf/issues/39

* src/bin/autfilt.cc: Add those options.  Also
make --keep-state use --remove-unreachable-states
instead of the less efficient --remove-dead-states
by default.
* src/tgbatest/readsave.test: Test them.

src/bin/autfilt.cc

@@ -86,6 +86,8 @@ enum {
   OPT_PRODUCT,
   OPT_RANDOMIZE,
   OPT_REM_AP,
+  OPT_REM_DEAD,
+  OPT_REM_UNREACH,
   OPT_REM_FIN,
   OPT_SBACC,
   OPT_SEED,
@@ -134,7 +136,7 @@ static const argp_option options[] =
       "remove the acceptance condition and all acceptance sets", 0 },
     { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0,
       "only keep specified states.  The first state will be the new "\
-      "initial state", 0 },
+      "initial state.  Implies --remove-unreachable-states.", 0 },
     { "dnf-acceptance", OPT_DNF_ACC, 0, 0,
       "put the acceptance condition in Disjunctive Normal Form", 0 },
     { "cnf-acceptance", OPT_CNF_ACC, 0, 0,
@@ -158,6 +160,11 @@ static const argp_option options[] =
     { "remove-ap", OPT_REM_AP, "AP[=0|=1][,AP...]", 0,
       "remove atomic propositions either by existential quantification, or "
       "by assigning them 0 or 1", 0 },
+    { "remove-unreachable-states", OPT_REM_UNREACH, 0, 0,
+      "remove states that are unreachable from the initial state", 0 },
+    { "remove-dead-states", OPT_REM_DEAD, 0, 0,
+      "remove states that are unreachable, or that cannot belong to an "
+      "infinite path", 0 },
     /**************************************************/
     { 0, 0, 0, 0, "Filtering options:", 6 },
     { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
@@ -248,6 +255,8 @@ static unsigned int opt_keep_states_initial = 0;
 static spot::exclusive_ap excl_ap;
 static spot::remove_ap rem_ap;
 static bool opt_simplify_exclusive_ap = false;
+static bool opt_rem_dead = false;
+static bool opt_rem_unreach = false;
 
 static int
 parse_opt(int key, char* arg, struct argp_state*)
@@ -368,6 +377,7 @@ 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_PRODUCT:
@@ -405,9 +415,15 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_REM_AP:
       rem_ap.add_ap(arg);
       break;
+    case OPT_REM_DEAD:
+      opt_rem_dead = true;
+      break;
     case OPT_REM_FIN:
       opt_rem_fin = true;
       break;
+    case OPT_REM_UNREACH:
+      opt_rem_unreach = true;
+      break;
     case OPT_SBACC:
       opt_sbacc = true;
       break;
@@ -521,11 +537,6 @@ namespace
 
       // Postprocessing.
 
-      if (!opt_keep_states.empty())
-	{
-	  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());
 
@@ -542,6 +553,13 @@ namespace
       else if (opt_instut == 2)
 	aut = spot::sl2(std::move(aut));
 
+      if (!opt_keep_states.empty())
+	aut = mask_keep_states(aut, opt_keep_states, opt_keep_states_initial);
+      if (opt_rem_dead)
+	aut->purge_dead_states();
+      else if (opt_rem_unreach)
+	aut->purge_unreachable_states();
+
       if (opt->product)
 	aut = spot::product(std::move(aut), opt->product);
 

src/tgbatest/readsave.test

@@ -509,3 +509,165 @@ EOF
 
 $autfilt --dot=bao in >out
 diff out expected
+
+
+# Let's pretend that this is some used supplied input, as discussed in
+# the comments of https://github.com/adl/hoaf/issues/39
+
+cat >input <<EOF
+HOA: v1
+States: 7
+Start: 1
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 1
+[!0&1] 0
+[!0&!1] 4
+State: 3
+[!0&!1] 2
+State: 4
+[0&1] 6
+[0&1] 5
+[0&1] 2
+[!0&1] 3
+State: 6
+[!0&!1] 1
+[!0&!1] 3
+[0&1] 7
+--END--
+EOF
+
+# autfilt should complain about the input (we only check the exit
+# status here, because the actual error messages are tested in
+# hoaparse.test) and produce a valid output with the number of states
+# fixed, and the missing state definitions.
+$autfilt -H input >output1 && exit 1
+
+cat >expect1 <<EOF
+HOA: v1
+States: 8
+Start: 1
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+State: 1
+[!0&1] 0
+[!0&!1] 4
+State: 2
+State: 3
+[!0&!1] 2
+State: 4
+[0&1] 6
+[0&1] 5
+[0&1] 2
+[!0&1] 3
+State: 5
+State: 6
+[!0&!1] 1
+[!0&!1] 3
+[0&1] 7
+State: 7
+--END--
+EOF
+
+diff output1 expect1
+# Make sure the output is valid.
+$autfilt -H output1 > output1b
+diff output1 output1b
+
+# Here is the scenario where the undefined states are actually states
+# we wanted to remove.  So we tell autfilt to fix the automaton using
+# --remove-dead-states
+$autfilt -H --remove-dead input >output2 && exit 1
+
+cat >expect2 <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[!0&!1] 1
+State: 1
+[0&1] 2
+State: 2
+[!0&!1] 0
+--END--
+EOF
+
+diff output2 expect2
+
+
+
+# Check the difference between --remove-unreach and --remove-dead
+cat >input <<EOF
+HOA: v1
+States: 6
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+--BODY--
+State: 0
+[!0&!1] 1
+State: 1
+[0&1] 2
+State: 2
+[!0&!1] 0
+[t] 5
+State: 3
+[t] 4
+State: 4
+[t] 3
+State: 5
+--END--
+EOF
+
+$autfilt -H --remove-unreach input >output3
+$autfilt -H --remove-dead input >>output3
+
+cat >expect3 <<EOF
+HOA: v1
+States: 4
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[!0&!1] 1
+State: 1
+[0&1] 2
+State: 2
+[!0&!1] 0
+[t] 3
+State: 3
+--END--
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[!0&!1] 1
+State: 1
+[0&1] 2
+State: 2
+[!0&!1] 0
+--END--
+EOF
+
+diff output3 expect3