autfilt: add --remove-unused-ap

Part of #170.

* bin/autfilt.cc: Here.
* tests/core/remprop.test: Test it.
* NEWS: Mention it.

NEWS

@@ -10,6 +10,11 @@ New in spot 2.0a (not yet released)
     --rejecting-sccs=RANGE, trivial-sccs=RANGE, --terminal-sccs=RANGE,
     --weak-sccs=RANGE, --inherently-weak-sccs=RANGE).
 
+  * autfilt --remove-unused-ap can be used to remove atomic
+    proposition that are declared in the input automaton, but not
+    actually used.  This of course makes sense only for input/output
+    formats that declare atomic proposition (HOA & DSTAR).
+
   Library:
 
   * The print_hoa() function will now output version 1.1 of the HOA

bin/autfilt.cc

@@ -110,6 +110,7 @@ enum {
   OPT_REM_AP,
   OPT_REM_DEAD,
   OPT_REM_UNREACH,
+  OPT_REM_UNUSED_AP,
   OPT_REM_FIN,
   OPT_SAT_MINIMIZE,
   OPT_SCCS,
@@ -185,6 +186,8 @@ 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-unused-ap", OPT_REM_UNUSED_AP, nullptr, 0,
+      "remove declared atomic propositions that are not used", 0 },
     { "remove-unreachable-states", OPT_REM_UNREACH, nullptr, 0,
       "remove states that are unreachable from the initial state", 0 },
     { "remove-dead-states", OPT_REM_DEAD, nullptr, 0,
@@ -365,6 +368,7 @@ static unsigned int opt_keep_states_initial = 0;
 static bool opt_simplify_exclusive_ap = false;
 static bool opt_rem_dead = false;
 static bool opt_rem_unreach = false;
+static bool opt_rem_unused_ap = false;
 static bool opt_sep_sets = false;
 static const char* opt_sat_minimize = nullptr;
 
@@ -623,6 +627,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_REM_UNREACH:
       opt_rem_unreach = true;
       break;
+    case OPT_REM_UNUSED_AP:
+      opt_rem_unused_ap = true;
+      break;
     case OPT_SAT_MINIMIZE:
       opt_sat_minimize = arg ? arg : "";
       break;
@@ -873,7 +880,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);
+        aut = opt->excl_ap.constrain(aut, true);
+      else if (opt_rem_unused_ap) // constrain(aut, true) already does that
+        aut->remove_unused_ap();
 
       if (randomize_st || randomize_tr)
         spot::randomize(aut, randomize_st, randomize_tr);

tests/core/remprop.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.
@@ -95,3 +95,40 @@ diff out expected
 
 autfilt -H --remove-ap=a==1 automaton 2>stderr && exit 1
 grep "autfilt: unexpected '=' at position 2 in 'a==1'" stderr
+
+
+cat >automaton <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored
+properties: deterministic
+--BODY--
+State: 0 {0}
+[1] 0
+--END--
+EOF
+
+autfilt automaton > output
+diff automaton output
+
+cat >expect <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored
+properties: deterministic
+--BODY--
+State: 0 {0}
+[0] 0
+--END--
+EOF
+
+autfilt --remove-unused-ap automaton > output
+diff output expect