autfilt: add a --exclusive-ap option

* src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh: Implement
constrain() for automata.
* src/bin/autfilt.cc: Add --exclusive-ap option.
* src/tgba/bdddict.cc, src/tgba/bdddict.hh: Add a
has_registered_proposition() method.
* src/tgbatest/exclusive.test: New file.
* src/tgbatest/Makefile.am: Add it.

src/bin/autfilt.cc

@@ -43,6 +43,7 @@
 #include "misc/timer.hh"
 #include "misc/random.hh"
 #include "hoaparse/public.hh"
+#include "ltlvisit/exclusive.hh"
 #include "tgbaalgos/randomize.hh"
 #include "tgbaalgos/are_isomorphic.hh"
 #include "tgbaalgos/canonicalize.hh"
@@ -71,6 +72,7 @@ enum {
   OPT_DESTUT,
   OPT_DNF_ACC,
   OPT_EDGES,
+  OPT_EXCLUSIVE_AP,
   OPT_INSTUT,
   OPT_INTERSECT,
   OPT_IS_COMPLETE,
@@ -138,6 +140,11 @@ static const argp_option options[] =
     { "complement-acceptance", OPT_COMPLEMENT_ACC, 0, 0,
       "complement the acceptance condition (without touching the automaton)",
       0 },
+    { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0,
+      "if any of those APs occur in the automaton, restrict all edges to "
+      "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 },
     /**************************************************/
     { 0, 0, 0, 0, "Filtering options:", 6 },
     { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
@@ -225,6 +232,7 @@ static bool opt_complement_acc = false;
 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 int
 parse_opt(int key, char* arg, struct argp_state*)
@@ -287,6 +295,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_EDGES:
       opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
+    case OPT_EXCLUSIVE_AP:
+      excl_ap.add_group(arg);
+      break;
     case OPT_INSTUT:
       if (!arg || (arg[0] == '1' && arg[1] == 0))
 	opt_instut = 1;
@@ -490,6 +501,9 @@ namespace
       if (opt_mask_acc)
 	aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
 
+      if (!excl_ap.empty())
+	aut = excl_ap.constrain(aut);
+
       if (opt_destut)
 	aut = spot::closure(std::move(aut));
       if (opt_instut == 1)

src/ltlvisit/exclusive.cc

@@ -22,6 +22,7 @@
 #include "ltlast/multop.hh"
 #include "ltlast/unop.hh"
 #include "ltlast/constant.hh"
+#include "tgbaalgos/mask.hh"
 #include "misc/casts.hh"
 #include "apcollect.hh"
 
@@ -158,4 +159,48 @@ namespace spot
 				  ltl::multop::instance(ltl::multop::And, v));
     return ltl::multop::instance(ltl::multop::And, f->clone(), c);
   }
+
+  tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut) const
+  {
+    // Compute the support of the automaton.
+    bdd support = bddtrue;
+    {
+      std::set<int> bdd_seen;
+      for (auto& t: aut->transitions())
+	if (bdd_seen.insert(t.cond.id()).second)
+	  support &= bdd_support(t.cond);
+    }
+
+    bdd restrict = bddtrue;
+    auto d = aut->get_dict();
+
+    std::vector<bdd> group;
+    for (auto& g: groups)
+      {
+	group.clear();
+
+	for (auto ap: g)
+	  {
+	    int v = d->has_registered_proposition(ap, aut);
+	    if (v >= 0)
+	      group.push_back(bdd_nithvar(v));
+	  }
+
+	unsigned s = group.size();
+	for (unsigned j = 0; j < s; ++j)
+	  for (unsigned k = j + 1; k < s; ++k)
+	    restrict &= group[j] | group[k];
+      }
+
+    tgba_digraph_ptr res = make_tgba_digraph(aut->get_dict());
+    res->copy_ap_of(aut);
+    res->prop_copy(aut, { true, true, true, true });
+    res->copy_acceptance_of(aut);
+    transform_accessible(aut, res, [&](unsigned, bdd& cond,
+				       acc_cond::mark_t&, unsigned)
+                         {
+			   cond &= restrict;
+                         });
+    return res;
+  }
 }

src/ltlvisit/exclusive.hh

@@ -22,6 +22,7 @@
 #include <vector>
 #include "ltlast/atomic_prop.hh"
 #include "ltlast/formula.hh"
+#include "tgba/tgbagraph.hh"
 
 namespace spot
 {
@@ -41,5 +42,6 @@ namespace spot
     }
 
     const ltl::formula* constrain(const ltl::formula* f) const;
+    tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut) const;
   };
 }

src/tgba/bdddict.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2012, 2013, 2014, 2015 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -118,6 +118,20 @@ namespace spot
     return num;
   }
 
+  int
+  bdd_dict::has_registered_proposition(const ltl::formula* f,
+				       const void* me)
+  {
+    auto ssi = var_map.find(f);
+    if (ssi == var_map.end())
+      return -1;
+    int num = ssi->second;
+    auto& r = bdd_map[num].refs;
+    if (r.find(me) == r.end())
+      return -1;
+    return num;
+  }
+
   void
   bdd_dict::register_propositions(bdd f, const void* for_me)
   {

src/tgba/bdddict.hh

@@ -1,9 +1,9 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
-// Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
+// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
+// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -126,7 +126,23 @@ namespace spot
     }
     /// @}
 
-    /// \brief Register an atomic proposition.
+    /// \brief whether a proposition has already been registered
+    ///
+    /// If \a f has been registered for \a me, this returns
+    /// a non-negative value that is the BDD variable number.
+    /// Otherwise this returns -1.
+    /// @{
+    int has_registered_proposition(const ltl::formula* f,
+				   const void* me);
+    template <typename T>
+    int has_registered_proposition(const ltl::formula* f,
+				   std::shared_ptr<T> for_me)
+    {
+      return has_registered_proposition(f, for_me.get());
+    }
+    /// @}
+
+    /// \brief Register an acceptance variable.
     ///
     /// Return (and maybe allocate) a BDD variable designating an
     /// acceptance set associated to formula \a f.  The \a for_me

src/tgbatest/Makefile.am

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

src/tgbatest/exclusive.test

@@ -0,0 +1,116 @@
+#! /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: 3
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0&!1&!2] 1
+State: 1
+[!0&1&!2] 2
+[!0&!1&2] 2
+State: 2 {0}
+[!0&1&!2] 2
+--END--
+EOF
+
+run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \
+    automaton >out
+cat out
+diff out expected
+
+cat >automaton <<EOF
+HOA: v1
+States: 4
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 1
+State: 1
+[1] 2
+[0] 2
+State: 2 {0}
+[1] 2
+[0&1] 1
+[1&0] 3
+State: 3
+[t] 3
+--END--
+EOF
+
+cat >expected <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[0&!1] 1
+State: 1
+[!0&1] 2
+[0&!1] 2
+State: 2 {0}
+[!0&1] 2
+--END--
+EOF
+
+run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \
+    automaton >out
+cat out
+diff out expected