autfilt: add a --simplify-exclusive-ap option

* src/bin/autfilt.cc: Add option.
* src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh: implement it.
* src/tgbatest/exclusive.test: Test it.
* src/misc/minato.cc, src/misc/minato.hh: Add an interface to
simplify a Boolean function with don't care.

src/bin/autfilt.cc

@@ -88,6 +88,7 @@ enum {
   OPT_REM_FIN,
   OPT_SBACC,
   OPT_SEED,
+  OPT_SIMPLIFY_EXCLUSIVE_AP,
   OPT_STATES,
   OPT_STRIPACC,
   OPT_TGBA,
@@ -147,6 +148,10 @@ 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 },
+    { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, 0, 0,
+      "if --exclusive-ap is used, assume those AP groups are actually exclusive"
+      " in the system to simplify the expression of transition labels (implies "
+      "--merge-transitions)", 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 },
@@ -239,6 +244,7 @@ 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 bool opt_simplify_exclusive_ap = false;
 
 static int
 parse_opt(int key, char* arg, struct argp_state*)
@@ -403,6 +409,10 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_SEED:
       opt_seed = to_int(arg);
       break;
+    case OPT_SIMPLIFY_EXCLUSIVE_AP:
+      opt_simplify_exclusive_ap = true;
+      opt_merge = true;
+      break;
     case OPT_STATES:
       opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
@@ -514,7 +524,7 @@ namespace
 	aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets());
 
       if (!excl_ap.empty())
-	aut = excl_ap.constrain(aut);
+	aut = excl_ap.constrain(aut, opt_simplify_exclusive_ap);
 
       if (!rem_ap.empty())
 	aut = rem_ap.strip(aut);

src/ltlvisit/exclusive.cc

@@ -24,6 +24,7 @@
 #include "ltlast/constant.hh"
 #include "tgbaalgos/mask.hh"
 #include "misc/casts.hh"
+#include "misc/minato.hh"
 #include "apcollect.hh"
 
 namespace spot
@@ -160,7 +161,8 @@ namespace spot
     return ltl::multop::instance(ltl::multop::And, f->clone(), c);
   }
 
-  tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut) const
+  tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut,
+					   bool simplify_guards) const
   {
     // Compute the support of the automaton.
     bdd support = bddtrue;
@@ -196,11 +198,29 @@ namespace spot
     res->copy_ap_of(aut);
     res->prop_copy(aut, { true, true, true, true });
     res->copy_acceptance_of(aut);
+    if (simplify_guards)
+      {
+	transform_accessible(aut, res, [&](unsigned, bdd& cond,
+					   acc_cond::mark_t&, unsigned)
+			     {
+			       minato_isop isop(cond & restrict,
+						cond | !restrict,
+						true);
+			       bdd res = bddfalse;
+			       bdd cube = bddfalse;
+			       while ((cube = isop.next()) != bddfalse)
+				 res |= cube;
+			       cond = res;
+			     });
+      }
+    else
+      {
 	transform_accessible(aut, res, [&](unsigned, bdd& cond,
 					   acc_cond::mark_t&, unsigned)
 			     {
 			       cond &= restrict;
 			     });
+      }
     return res;
   }
 }

src/ltlvisit/exclusive.hh

@@ -42,6 +42,7 @@ namespace spot
     }
 
     const ltl::formula* constrain(const ltl::formula* f) const;
-    tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut) const;
+    tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut,
+			       bool simplify_guards = false) const;
   };
 }

src/misc/minato.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -28,8 +28,12 @@ namespace spot
 {
 
   minato_isop::minato_isop(bdd input)
-    : ret_(bddfalse)
+    : minato_isop(input, bdd_support(input))
+  {
+  }
 
+  minato_isop::minato_isop(bdd input, bdd vars)
+    : ret_(bddfalse)
   {
     // If INPUT has the form a&b&c&(binary function) we want to
     // compute the ISOP of the only binary and prepend a&b&c latter.
@@ -39,14 +43,23 @@ namespace spot
     // original algorithm, because in many cases we are trying to
     // build ISOPs out of formulae that are already cubes.
     cube_.push(bdd_satprefix(input));
-    todo_.emplace(input, input, bdd_support(input));
+    todo_.emplace(input, input, vars);
   }
 
-  minato_isop::minato_isop(bdd input, bdd vars)
+  minato_isop::minato_isop(bdd input_min, bdd input_max, bool)
     : ret_(bddfalse)
   {
-    cube_.push(bdd_satprefix(input));
-    todo_.emplace(input, input, vars);
+    if (input_min == input_max)
+      {
+	cube_.push(bdd_satprefix(input_min));
+	input_max = input_min;
+      }
+    else
+      {
+	cube_.push(bddtrue);
+      }
+    bdd common = input_min & input_max;
+    todo_.emplace(input_min, input_max, bdd_support(common));
   }
 
   bdd

src/misc/minato.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -58,6 +58,13 @@ namespace spot
     /// \arg input The BDD function to translate in ISOP.
     /// \arg vars  The set of BDD variables to factorize in \a input.
     minato_isop(bdd input, bdd vars);
+    /// \brief Conctructor.
+    ///
+    /// This version allow some flexibility in computing the ISOP.
+    /// the result must be within \a input_min and \a input_max.
+    /// \arg input_min The minimum BDD function to translate in ISOP.
+    /// \arg input_max The maximum BDD function to translate in ISOP.
+    minato_isop(bdd input_min, bdd input_max, bool);
     /// \brief Compute the next sum term of the ISOP form.
     /// Return \c bddfalse when all terms have been output.
     bdd next();

src/tgbatest/exclusive.test

@@ -35,7 +35,7 @@ State: 0
 [0] 1
 State: 1
 [1] 2
-[2] 2
+[2&!1] 2
 State: 2 {0}
 [1] 2
 [0&1] 1
@@ -64,11 +64,34 @@ State: 2 {0}
 --END--
 EOF
 
+cat >expected-simpl <<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
+State: 1
+[1 | 2] 2
+State: 2 {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
 
+run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \
+    --simplify-exclusive-ap automaton >out2
+cat out2
+diff out2 expected-simpl
+
 cat >automaton <<EOF
 HOA: v1
 States: 4
@@ -81,7 +104,7 @@ State: 0
 [0] 1
 State: 1
 [1] 2
-[0] 2
+[0&!1] 2
 State: 2 {0}
 [1] 2
 [0&1] 1
@@ -110,7 +133,30 @@ State: 2 {0}
 --END--
 EOF
 
+cat >expected-simpl <<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
+State: 1
+[0 | 1] 2
+State: 2 {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
+
+run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \
+    --simplify-exclusive-ap automaton >out2
+cat out2
+diff out2 expected-simpl