Make it easy to complement an acceptance condition

* src/tgba/acc.cc, src/tgba/acc.hh (complement): New method.
* src/bin/autfilt.cc: Add a --complement-acceptance option.
* src/tgbatest/acc2.test: Test it.

src/bin/autfilt.cc

@@ -84,6 +84,7 @@ Exit status:\n\
 #define OPT_DNF_ACC 21
 #define OPT_REM_FIN 22
 #define OPT_CLEAN_ACC 23
+#define OPT_COMPLEMENT_ACC 24
 
 static const argp_option options[] =
   {
@@ -119,7 +120,7 @@ static const argp_option options[] =
       "define the acceptance using states", 0 },
     { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 },
     { "strip-acceptance", OPT_STRIPACC, 0, 0,
-      "remove the acceptance conditions and all acceptance sets", 0 },
+      "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 },
@@ -129,6 +130,9 @@ static const argp_option options[] =
       "rewrite the automaton without using Fin acceptance", 0 },
     { "cleanup-acceptance", OPT_CLEAN_ACC, 0, 0,
       "remove unused acceptance sets from the automaton", 0 },
+    { "complement-acceptance", OPT_COMPLEMENT_ACC, 0, 0,
+      "complement the acceptance condition (without touching the automaton)",
+      0 },
     /**************************************************/
     { 0, 0, 0, 0, "Filtering options:", 6 },
     { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
@@ -211,6 +215,7 @@ static bool opt_stripacc = false;
 static bool opt_dnf_acc = false;
 static bool opt_rem_fin = false;
 static bool opt_clean_acc = false;
+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;
@@ -259,6 +264,15 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_CLEAN_ACC:
       opt_clean_acc = true;
       break;
+    case OPT_COMPLEMENT_ACC:
+      opt_complement_acc = true;
+      break;
+    case OPT_DESTUT:
+      opt_destut = true;
+      break;
+    case OPT_DNF_ACC:
+      opt_dnf_acc = true;
+      break;
     case OPT_EDGES:
       opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
@@ -273,12 +287,6 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_INTERSECT:
       opt->intersect = read_automaton(arg, opt->dict);
       break;
-    case OPT_DESTUT:
-      opt_destut = true;
-      break;
-    case OPT_DNF_ACC:
-      opt_dnf_acc = true;
-      break;
     case OPT_IS_COMPLETE:
       opt_is_complete = true;
       break;
@@ -426,13 +434,16 @@ namespace
 	spot::strip_acceptance_here(aut);
       if (opt_merge)
 	aut->merge_transitions();
+      if (opt_clean_acc || opt_rem_fin)
+	cleanup_acceptance(aut);
+      if (opt_complement_acc)
+	aut->set_acceptance(aut->acc().num_sets(),
+			    aut->get_acceptance().complement());
+      if (opt_rem_fin)
+	aut = remove_fin(aut);
       if (opt_dnf_acc)
 	aut->set_acceptance(aut->acc().num_sets(),
 			    aut->get_acceptance().to_dnf());
-      if (opt_clean_acc && !opt_rem_fin)
-	cleanup_acceptance(aut);
-      if (opt_rem_fin)
-	aut = remove_fin(aut);
 
       // Filters.
 

src/tgba/acc.cc

@@ -353,6 +353,84 @@ namespace spot
     return true;
   }
 
+  namespace
+  {
+    acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos)
+    {
+      auto start = pos - pos->size;
+
+      acc_cond::acc_code res;
+      res.resize(2);
+      res[0].mark = 0U;
+      res[1].size = 1;
+
+      switch (pos->op)
+	{
+	case acc_cond::acc_op::And:
+	  {
+	    --pos;
+	    res[1].op = acc_cond::acc_op::Fin; // f
+	    do
+	      {
+		auto tmp = complement_rec(pos);
+		tmp.append_or(std::move(res));
+		std::swap(tmp, res);
+		pos -= pos->size + 1;
+	      }
+	    while (pos > start);
+	    return res;
+	  }
+	case acc_cond::acc_op::Or:
+	  {
+	    --pos;
+	    res[1].op = acc_cond::acc_op::Inf; // t
+	    do
+	      {
+		auto tmp = complement_rec(pos);
+		tmp.append_and(std::move(res));
+		std::swap(tmp, res);
+		pos -= pos->size + 1;
+	      }
+	    while (pos > start);
+	    return res;
+	  }
+	case acc_cond::acc_op::Fin:
+	  res[0].mark = pos[-1].mark;
+	  res[1].op = acc_cond::acc_op::Inf;
+	  return res;
+	case acc_cond::acc_op::Inf:
+	  res[0].mark = pos[-1].mark;
+	  res[1].op = acc_cond::acc_op::Fin;
+	  return res;
+	case acc_cond::acc_op::FinNeg:
+	  res[0].mark = pos[-1].mark;
+	  res[1].op = acc_cond::acc_op::InfNeg;
+	  return res;
+	case acc_cond::acc_op::InfNeg:
+	  res[0].mark = pos[-1].mark;
+	  res[1].op = acc_cond::acc_op::FinNeg;
+	  return res;
+	}
+      SPOT_UNREACHABLE();
+      return acc_cond::acc_code{};
+    }
+
+  }
+
+
+  acc_cond::acc_code acc_cond::acc_code::complement() const
+  {
+    if (empty())
+      {
+	acc_cond::acc_code res;
+	res.resize(2);
+	res[0].mark = 0U;
+	res[1].op = acc_cond::acc_op::Fin;
+	res[1].size = 1;
+	return res;
+      }
+    return complement_rec(&back());
+  }
 
   std::ostream& operator<<(std::ostream& os,
 			   const spot::acc_cond::acc_code& code)

src/tgba/acc.hh

@@ -560,6 +560,8 @@ namespace spot
 
       acc_code to_dnf() const;
 
+      acc_code complement() const;
+
       SPOT_API
       friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
     };

src/tgbatest/acc2.test

@@ -68,3 +68,24 @@ do
 done < acceptances > output
 
 diff acceptances output
+
+a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)"
+b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)"
+cat >acceptances<<EOF
+2 Inf(0)&Inf(1), 2 Fin(0)|Fin(1)
+2 Fin(0) & Inf(1), 2 Inf(0) | Fin(1)
+2 t, 2 f
+2 f, 2 t
+3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(1) & Inf(2)) | Fin(0)
+4 $a, 4 $b
+4 $b, 4 (Inf(1) | Fin(2)) & (Inf(3) | Fin(1)) & Inf(0)
+3 (Fin(0)|Fin(1)) & Fin(2), 3 (Inf(0)&Inf(1)) | Inf(2)
+EOF
+
+while IFS=, read a b
+do
+    (cat header; echo 'Acceptance:' $a; cat body) |
+	../../bin/autfilt -H --complement-acc --stats '%A %G, %a %g'
+done < acceptances > output
+
+diff acceptances output