remfin: introduce less acceptance sets for interferences

Instead of adding one set per term in the DNF, reuse the
removed Fin(x) sets as Inf(x) sets.

* src/tgbaalgos/remfin.cc: Here.
* src/tgbatest/remfin.test: Additional test.

src/tgbaalgos/remfin.cc

@@ -118,6 +118,8 @@ namespace spot
     std::vector<acc_cond::mark_t> keep;
     std::vector<acc_cond::mark_t> add;
     bool has_true_term = false;
+    acc_cond::mark_t allinf = 0U;
+    acc_cond::mark_t allfin = 0U;
     {
       auto acccode = aut->get_acceptance();
 
@@ -138,6 +140,7 @@ namespace spot
 	  // The empty Fin should always come first
 	  assert(p.first != 0U || rem.empty());
 	  rem.push_back(p.first);
+	  allfin |= p.first;
 	  acc_cond::mark_t inf = 0U;
 	  if (!p.second.empty())
 	    {
@@ -163,12 +166,13 @@ namespace spot
 		    }
 		}
 	    }
-	  else
+	  if (inf == 0U)
 	    {
 	      has_true_term = true;
 	    }
 	  code.push_back(std::move(p.second));
 	  keep.push_back(inf);
+	  allinf |= inf;
 	  add.push_back(0U);
 	}
     }
@@ -196,11 +200,29 @@ namespace spot
       if (interference)
 	{
 	  trace << "We have interferences\n";
-	  unsigned base = acc.add_sets(sz);
+	  // We need extra set, but we will try
-	  extra_sets += sz;
+	  // to reuse the Fin number if they are
+	  // not used as Inf as well.
+	  std::vector<int> exs(acc.num_sets());
+	  for (auto f: allfin.sets())
+	    {
+	      if (allinf.has(f)) // Already used as Inf
+		{
+		  exs[f] = acc.add_set();
+		  ++extra_sets;
+		}
+	      else
+		{
+		  exs[f] = f;
+		}
+	    }
 	  for (unsigned i = 0; i < sz; ++i)
 	    {
-	      auto m = acc.marks({base + i});
+	      acc_cond::mark_t m = 0U;
+	      for (auto f: rem[i].sets())
+		m.set(exs[f]);
+	      trace << "rem[" << i << "] = " << rem[i]
+		    << "  m = " << m << '\n';
 	      add[i] = m;
 	      code[i].append_and(acc.inf(m));
 	      trace << "code[" << i << "] = " << code[i] << '\n';
@@ -248,20 +270,21 @@ namespace spot
     std::vector<unsigned> state_map(nst);
     for (unsigned n = 0; n < nscc; ++n)
       {
-	// What to keep and add to the main copy
-	acc_cond::mark_t main_sets = 0U;
-	acc_cond::mark_t main_add = 0U;
-
 	auto m = si.acc(n);
 	auto states = si.states_of(n);
 	trace << "SCC #" << n << " uses " << m << '\n';
 
+	// What to keep and add into the main copy
+	acc_cond::mark_t main_sets = 0U;
+	acc_cond::mark_t main_add = 0U;
 	for (unsigned i = 0; i < cs; ++i)
 	  if (!(m & rem[i]))
 	    {
 	      main_sets |= keep[i];
 	      main_add |= add[i];
 	    }
+	trace << "main_sets " << main_sets << "\nmain_add " << main_add << '\n';
+
 	// Create the main copy
 	for (auto s: states)
 	  for (auto& t: aut->out(s))
@@ -304,7 +327,9 @@ namespace spot
 
 
       }
+    trace << "before cleanup: " << res->get_acceptance() << '\n';
     cleanup_acceptance(res);
+    trace << "after cleanup: " << res->get_acceptance() << '\n';
     return res;
   }
 }

src/tgbatest/remfin.test

@@ -125,6 +125,39 @@ State: 1 {1}
 1
 1
 --END--
+HOA: v1
+States: 8
+Start: 2
+AP: 1 "p1"
+Acceptance: 4 (Fin(3) & Inf(0)) | (Fin(1) & Fin(3)) |
+              (Fin(1) & Inf(2)) | (Inf(0)&Inf(2))
+properties: trans-labels explicit-labels state-acc complete deterministic
+--BODY--
+State: 0
+[!0] 6
+[0] 0
+State: 1 {2}
+[!0] 3
+[0] 3
+State: 2 {2}
+[!0] 5
+[0] 1
+State: 3 {2}
+[!0] 6
+[0] 0
+State: 4 {2}
+[!0] 6
+[0] 4
+State: 5 {2}
+[!0] 7
+[0] 3
+State: 6 {1 2}
+[!0] 6
+[0] 0
+State: 7 {3}
+[!0] 6
+[0] 4
+--END--
 EOF
 
 cat >expected <<EOF
@@ -185,30 +218,30 @@ HOA: v1
 States: 6
 Start: 0
 AP: 2 "a" "b"
-Acceptance: 5 (Inf(0)&Inf(4)) | ((Inf(0) | (Inf(1)&Inf(2))) & Inf(3))
+Acceptance: 5 (Inf(0)&Inf(1)&Inf(4)) | Inf(0) | (Inf(2)&Inf(3))
 properties: trans-labels explicit-labels trans-acc
 --BODY--
 State: 0
-[t] 0 {2 3}
+[t] 0 {3}
-[0] 1 {2 3}
+[0] 1 {3}
-[!0] 2 {0 2 3}
+[!0] 2 {0 3}
 State: 1
-[1] 0 {2 3}
+[1] 0 {3}
-[0&1] 1 {0 2 3}
+[0&1] 1 {0 3}
-[!0&1] 2 {1 2 3}
+[!0&1] 2 {2 3}
 State: 2
-[!1] 0 {3}
+[!1] 0
-[0&!1] 1 {0 3}
+[0&!1] 1 {0}
-[!0&!1] 2 {0 3}
+[!0&!1] 2 {0}
-[!1] 3 {3}
+[!1] 3
-[0&!1] 4 {0 3}
+[0&!1] 4 {0}
-[!0&!1] 5 {0 3}
+[!0&!1] 5 {0}
 State: 3
 State: 4
 State: 5
-[!1] 3 {4}
+[!1] 3 {1 4}
-[0&!1] 4 {0 4}
+[0&!1] 4 {0 1 4}
-[!0&!1] 5 {0 4}
+[!0&!1] 5 {0 1 4}
 --END--
 HOA: v1
 States: 1
@@ -245,6 +278,48 @@ State: 1 {0}
 [!0] 1
 [0] 1
 --END--
+HOA: v1
+States: 12
+Start: 2
+AP: 1 "p1"
+Acceptance: 2 Inf(1) | Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[!0] 6
+[0] 0
+[0] 9
+[0] 11
+State: 1 {0 1}
+[!0] 3
+[0] 3
+State: 2 {0 1}
+[!0] 5
+[0] 1
+State: 3 {0 1}
+[!0] 6
+[0] 0
+State: 4 {0 1}
+[!0] 6
+[0] 4
+State: 5 {0 1}
+[!0] 7
+[0] 3
+State: 6
+[!0] 6
+[0] 0
+State: 7 {1}
+[!0] 6
+[0] 4
+State: 8
+State: 9
+[!0] 8
+[0] 9
+State: 10
+State: 11 {1}
+[!0] 10
+[0] 11
+--END--
 EOF
 
 run 0 $autfilt -H --remove-fin test1 > output