autfilt: add a --remove-ap option

* src/tgbaalgos/remprop.cc, src/tgbaalgos/remprop.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/remprop.test: New test.
* src/tgbatest/Makefile.am: Add it.
* src/bin/autfilt.cc: Implement the option.
* doc/org/autfilt.org: Document it.

doc/org/autfilt.org

@@ -260,8 +260,11 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
       --product=FILENAME     build the product with the automaton in FILENAME
       --randomize[=s|t]      randomize states and transitions (specify 's' or
                              't' to randomize only states or transitions)
-      --remove-fin           rewrite the automaton without using Fin acceptance
-
+      --remove-ap=AP[=0|=1][,AP...]
+                             remove atomic propositions either by existential
+                             quantification, or by assigning them 0 or 1
+      --remove-fin           rewrite the automaton without using Fin
+                             acceptance
       --state-based-acceptance, --sbacc
                              define the acceptance using states
       --strip-acceptance     remove the acceptance condition and all acceptance
@@ -531,3 +534,117 @@ $txt
 
 #+RESULTS:
 [[file:autfilt-ex5.png]]
+
+
+Atomic propositions can be removed from an automaton in three ways:
+- use ~--remove-ap=a~ to remove =a= by existential quantification, i.e., both =a= and its negation will be replaced by true.
+  This does not remove any transition.
+- use ~--remove-ap=a=0~ to keep only transitions compatible with =!a= (i.e, transitions requiring =a= will be removed).
+- use ~--remove-ap=a=1~ to keep only transitions compatible with =a= (i.e, transitions requiring =!a= will be removed).
+
+Here are the results of these three options on our example:
+
+#+NAME: autfilt-ex6a
+#+BEGIN_SRC sh :results verbatim :export code
+autfilt --remove-ap=a aut-ex1.hoa --dot=.a
+#+END_SRC
+
+#+RESULTS: autfilt-ex6a
+#+begin_example
+digraph G {
+  rankdir=LR
+  label=<(Fin(<font color="#F17CB0">❶</font>) &amp; Fin(<font color="#B276B2">❸</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&amp;Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#F17CB0">❶</font>)>
+  labelloc="t"
+  fontname="Lato"
+  node [fontname="Lato"]
+  edge [fontname="Lato"]
+  node[style=filled, fillcolor="#ffffa0"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label=<1<br/><font color="#B276B2">❸</font>>]
+  0 -> 1 [label=<1<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
+  0 -> 2 [label=<1<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
+  1 [label="1"]
+  1 -> 0 [label=<b<br/><font color="#B276B2">❸</font>>]
+  1 -> 1 [label=<b<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
+  1 -> 2 [label=<b<br/><font color="#FAA43A">❷</font><font color="#B276B2">❸</font>>]
+  2 [label="2"]
+  2 -> 0 [label=<!b>]
+  2 -> 1 [label=<!b<br/><font color="#5DA5DA">⓿</font>>]
+  2 -> 2 [label=<!b<br/><font color="#5DA5DA">⓿</font>>]
+}
+#+end_example
+
+#+BEGIN_SRC dot :file autfilt-ex6a.png :cmdline -Tpng :var txt=autfilt-ex6a :exports results
+$txt
+#+END_SRC
+
+#+RESULTS:
+[[file:autfilt-ex6a.png]]
+
+#+NAME: autfilt-ex6b
+#+BEGIN_SRC sh :results verbatim :export code
+autfilt --remove-ap=a=0 aut-ex1.hoa --dot=.a
+#+END_SRC
+
+#+RESULTS: autfilt-ex6b
+#+begin_example
+digraph G {
+  rankdir=LR
+  label=<(Fin(<font color="#F17CB0">❶</font>) &amp; Fin(<font color="#B276B2">❸</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&amp;Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#F17CB0">❶</font>)>
+  labelloc="t"
+  fontname="Lato"
+  node [fontname="Lato"]
+  edge [fontname="Lato"]
+  node[style=filled, fillcolor="#ffffa0"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label=<1<br/><font color="#B276B2">❸</font>>]
+  0 -> 1 [label=<1<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
+  1 [label="1"]
+  1 -> 0 [label=<!b>]
+  1 -> 1 [label=<!b<br/><font color="#5DA5DA">⓿</font>>]
+}
+#+end_example
+
+#+BEGIN_SRC dot :file autfilt-ex6b.png :cmdline -Tpng :var txt=autfilt-ex6b :exports results
+$txt
+#+END_SRC
+
+#+RESULTS:
+[[file:autfilt-ex6b.png]]
+
+#+NAME: autfilt-ex6c
+#+BEGIN_SRC sh :results verbatim :export code
+autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a
+#+END_SRC
+
+#+RESULTS: autfilt-ex6c
+#+begin_example
+digraph G {
+  rankdir=LR
+  label=<(Fin(<font color="#F17CB0">❶</font>) &amp; Fin(<font color="#B276B2">❸</font>) &amp; Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&amp;Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#F17CB0">❶</font>)>
+  labelloc="t"
+  fontname="Lato"
+  node [fontname="Lato"]
+  edge [fontname="Lato"]
+  node[style=filled, fillcolor="#ffffa0"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label=<1<br/><font color="#B276B2">❸</font>>]
+  0 -> 1 [label=<1<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
+  1 [label="1"]
+  1 -> 0 [label=<b<br/><font color="#B276B2">❸</font>>]
+  1 -> 1 [label=<b<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
+}
+#+end_example
+
+#+BEGIN_SRC dot :file autfilt-ex6c.png :cmdline -Tpng :var txt=autfilt-ex6c :exports results
+$txt
+#+END_SRC
+
+#+RESULTS:
+[[file:autfilt-ex6c.png]]

src/bin/autfilt.cc

@@ -44,6 +44,7 @@
 #include "misc/random.hh"
 #include "hoaparse/public.hh"
 #include "ltlvisit/exclusive.hh"
+#include "tgbaalgos/remprop.hh"
 #include "tgbaalgos/randomize.hh"
 #include "tgbaalgos/are_isomorphic.hh"
 #include "tgbaalgos/canonicalize.hh"
@@ -83,6 +84,7 @@ enum {
   OPT_MERGE,
   OPT_PRODUCT,
   OPT_RANDOMIZE,
+  OPT_REM_AP,
   OPT_REM_FIN,
   OPT_SBACC,
   OPT_SEED,
@@ -145,6 +147,9 @@ static const argp_option options[] =
       "ensure two of them may not be true at the same time.  Use this option "
       "multiple times to declare independent groups of exclusive "
       "propositions.", 0 },
+    { "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 },
     /**************************************************/
     { 0, 0, 0, 0, "Filtering options:", 6 },
     { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
@@ -233,6 +238,7 @@ static spot::acc_cond::mark_t opt_mask_acc = 0U;
 static std::vector<bool> opt_keep_states = {};
 static unsigned int opt_keep_states_initial = 0;
 static spot::exclusive_ap excl_ap;
+static spot::remove_ap rem_ap;
 
 static int
 parse_opt(int key, char* arg, struct argp_state*)
@@ -385,6 +391,9 @@ parse_opt(int key, char* arg, struct argp_state*)
 	  randomize_st = true;
 	}
       break;
+    case OPT_REM_AP:
+      rem_ap.add_ap(arg);
+      break;
     case OPT_REM_FIN:
       opt_rem_fin = true;
       break;
@@ -504,6 +513,9 @@ namespace
       if (!excl_ap.empty())
 	aut = excl_ap.constrain(aut);
 
+      if (!rem_ap.empty())
+	aut = rem_ap.strip(aut);
+
       if (opt_destut)
 	aut = spot::closure(std::move(aut));
       if (opt_instut == 1)
@@ -586,38 +598,38 @@ main(int argc, char** argv)
   const argp ap = { options, parse_opt, "[FILENAMES...]",
 		    argp_program_doc, children, 0, 0 };
 
-  // This will ensure that all objects stored in this struct are
-  // destroyed before global variables.
-  opt_t o;
-  opt = &o;
+  try
+    {
+      // This will ensure that all objects stored in this struct are
+      // destroyed before global variables.
+      opt_t o;
+      opt = &o;
 
-  // Disable post-processing as much as possible by default.
-  level = spot::postprocessor::Low;
-  pref = spot::postprocessor::Any;
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
-    exit(err);
+      // Disable post-processing as much as possible by default.
+      level = spot::postprocessor::Low;
+      pref = spot::postprocessor::Any;
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
+	exit(err);
 
-  if (jobs.empty())
-    jobs.emplace_back("-", true);
+      if (jobs.empty())
+	jobs.emplace_back("-", true);
 
-  if (opt->are_isomorphic)
-    {
-      if (opt_merge)
-        opt->are_isomorphic->merge_transitions();
-      opt->isomorphism_checker = std::unique_ptr<spot::isomorphism_checker>
-	(new spot::isomorphism_checker(opt->are_isomorphic));
-    }
+      if (opt->are_isomorphic)
+	{
+	  if (opt_merge)
+	    opt->are_isomorphic->merge_transitions();
+	  opt->isomorphism_checker = std::unique_ptr<spot::isomorphism_checker>
+	    (new spot::isomorphism_checker(opt->are_isomorphic));
+	}
 
 
-  spot::srand(opt_seed);
+      spot::srand(opt_seed);
 
-  spot::postprocessor post(&extra_options);
-  post.set_pref(pref | comp);
-  post.set_type(type);
-  post.set_level(level);
+      spot::postprocessor post(&extra_options);
+      post.set_pref(pref | comp);
+      post.set_type(type);
+      post.set_level(level);
 
-  try
-    {
       hoa_processor processor(post);
       if (processor.run())
 	return 2;
@@ -626,6 +638,10 @@ main(int argc, char** argv)
     {
       error(2, 0, "%s", e.what());
     }
+  catch (const std::invalid_argument& e)
+    {
+      error(2, 0, "%s", e.what());
+    }
 
   if (automaton_format == Count)
     std::cout << match_count << std::endl;

src/tgbaalgos/Makefile.am

@@ -64,6 +64,7 @@ tgbaalgos_HEADERS = \
   reducerun.hh \
   relabel.hh \
   remfin.hh \
+  remprop.hh \
   replayrun.hh \
   safety.hh \
   sbacc.hh \
@@ -117,6 +118,7 @@ libtgbaalgos_la_SOURCES = \
   reachiter.cc \
   reducerun.cc \
   remfin.cc \
+  remprop.cc \
   replayrun.cc \
   relabel.cc \
   safety.cc \

src/tgbaalgos/remprop.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "remprop.hh"
+#include "ltlenv/defaultenv.hh"
+#include "tgbaalgos/mask.hh"
+#include "misc/casts.hh"
+#include "ltlvisit/tostring.hh"
+#include <ctype.h>
+#include <sstream>
+
+namespace spot
+{
+  remove_ap::~remove_ap()
+  {
+    for (auto& ap: props_exist)
+      ap->destroy();
+    for (auto& ap: props_pos)
+      ap->destroy();
+    for (auto& ap: props_neg)
+      ap->destroy();
+  }
+
+  namespace
+  {
+    static
+    void unexpected_char(const char* arg, const char* pos)
+    {
+      std::ostringstream out;
+      out << "unexpected ";
+      if (isprint(*pos))
+	out << '\'' << *pos << '\'';
+      else
+	out << "character";
+      out << " at position " << pos - arg << " in '";
+      out << arg << '\'';
+      throw std::invalid_argument(out.str());
+    }
+  }
+
+
+  void remove_ap::add_ap(const char* arg)
+  {
+    auto& env = spot::ltl::default_environment::instance();
+    std::vector<const spot::ltl::atomic_prop*> group;
+    auto start = arg;
+    while (*start)
+      {
+	while (*start == ' ' || *start == '\t')
+	  ++start;
+	if (!*start)
+	  break;
+	if (*start == ',' || *start == '=')
+	  unexpected_char(arg, start);
+	const spot::ltl::atomic_prop* the_ap = nullptr;
+
+	if (*start == '"')
+	  {
+	    auto end = ++start;
+	    while (*end && *end != '"')
+	      {
+		if (*end == '\\')
+		  ++end;
+		++end;
+	      }
+	    if (!*end)
+	      {
+		std::string s = "missing closing '\"' in ";
+		s += arg;
+		throw std::invalid_argument(s);
+	      }
+	    std::string ap(start, end - start);
+	    auto* t = env.require(ap);
+	    the_ap = down_cast<const spot::ltl::atomic_prop*>(t);
+	    do
+	      ++end;
+	    while (*end == ' ' || *end == '\t');
+	    start = end;
+	  }
+	else
+	  {
+	    auto end = start;
+	    while (*end && *end != ',' && *end != '=')
+	      ++end;
+	    auto rend = end;
+	    while (rend > start && (rend[-1] == ' ' || rend[-1] == '\t'))
+	      --rend;
+	    std::string ap(start, rend - start);
+	    auto* t = env.require(ap);
+	    the_ap = down_cast<const spot::ltl::atomic_prop*>(t);
+	    start = end;
+	  }
+	if (*start)
+	  {
+	    if (!(*start == ',' || *start == '='))
+	      unexpected_char(arg, start);
+	    if (*start == '=')
+	      {
+		do
+		  ++start;
+		while (*start == ' ' || *start == '\t');
+		if (*start == '0')
+		  props_neg.insert(the_ap);
+		else if (*start == '1')
+		  props_pos.insert(the_ap);
+		else
+		  unexpected_char(arg, start);
+		the_ap = nullptr;
+		do
+		  ++start;
+		while (*start == ' ' || *start == '\t');
+	      }
+	    if (*start)
+	      {
+		if (*start != ',')
+		  unexpected_char(arg, start);
+		++start;
+	      }
+	  }
+	if (the_ap)
+	  props_exist.insert(the_ap);
+      }
+  }
+
+  tgba_digraph_ptr remove_ap::strip(const_tgba_digraph_ptr aut) const
+  {
+    bdd restrict = bddtrue;
+    bdd exist = bddtrue;
+    auto d = aut->get_dict();
+
+    tgba_digraph_ptr res = make_tgba_digraph(d);
+    res->copy_ap_of(aut);
+    res->prop_copy(aut, { true, true, false, false });
+    res->copy_acceptance_of(aut);
+
+    for (auto ap: props_exist)
+      {
+	int v = d->has_registered_proposition(ap, aut);
+	if (v >= 0)
+	  {
+	    exist &= bdd_ithvar(v);
+	    d->unregister_variable(v, res);
+	  }
+      }
+    for (auto ap: props_pos)
+      {
+	int v = d->has_registered_proposition(ap, aut);
+	if (v >= 0)
+	  {
+	    restrict &= bdd_ithvar(v);
+	    d->unregister_variable(v, res);
+	  }
+      }
+    for (auto ap: props_neg)
+      {
+	int v = d->has_registered_proposition(ap, aut);
+	if (v >= 0)
+	  {
+	    restrict &= bdd_nithvar(v);
+	    d->unregister_variable(v, res);
+	  }
+      }
+
+    transform_accessible(aut, res, [&](unsigned, bdd& cond,
+				       acc_cond::mark_t&, unsigned)
+                         {
+			   cond = bdd_restrict(bdd_exist(cond, exist),
+					       restrict);
+                         });
+    return res;
+  }
+}

src/tgbaalgos/remprop.hh

+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include <vector>
+#include "ltlast/atomic_prop.hh"
+#include "tgba/tgbagraph.hh"
+
+namespace spot
+{
+  class SPOT_API remove_ap
+  {
+    std::set<const ltl::atomic_prop*> props_exist;
+    std::set<const ltl::atomic_prop*> props_pos;
+    std::set<const ltl::atomic_prop*> props_neg;
+  public:
+    ~remove_ap();
+    void add_ap(const char* ap_csv);
+
+    bool empty() const
+    {
+      return props_exist.empty() && props_pos.empty() && props_neg.empty();
+    }
+
+    tgba_digraph_ptr strip(const_tgba_digraph_ptr aut) const;
+  };
+}

src/tgbatest/Makefile.am

@@ -92,6 +92,7 @@ TESTS = \
   tripprod.test \
   dupexp.test \
   exclusive.test \
+  remprop.test \
   degendet.test \
   degenid.test \
   degenlskip.test \

src/tgbatest/remprop.test

+#! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2015 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs || exit 1
+
+set -e
+
+cat >automaton <<EOF
+HOA: v1
+States: 4
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 1
+State: 1
+[1] 2
+[2] 2
+State: 2 {0}
+[1] 2
+[0&1] 1
+[1&2] 3
+State: 3
+[t] 3
+--END--
+EOF
+
+cat >expected <<EOF
+HOA: v1
+States: 4
+Start: 0
+AP: 1 "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+--BODY--
+State: 0
+[t] 1
+State: 1
+[t] 2
+[0] 2
+State: 2 {0}
+[t] 2
+[t] 1
+[0] 3
+State: 3
+[t] 3
+--END--
+EOF
+
+run 0 ../../bin/autfilt -H --remove-ap=a,b automaton >out
+cat out
+diff out expected
+
+cat >expected <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[t] 1
+State: 1
+[0] 2
+State: 2
+--END--
+EOF
+
+run 0 ../../bin/autfilt -H --remove-ap=a=1,b=0 automaton >out
+cat out
+diff out expected
+
+../../bin/autfilt -H --remove-ap=a==1 automaton 2>stderr && exit 1
+grep "autfilt: unexpected '=' at position 2 in 'a==1'" stderr