hoa: correctly deal with "Acceptance: 1 t"

Report from Tomáš Babiak and František Blahoudek

See also https://github.com/adl/hoaf/issues/36

Also fix a typo in the handling of Fin(1)&Fin(!1) while we are at it.

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Add tests.

src/hoaparse/hoaparse.yy

@@ -998,7 +998,9 @@ incorrectly-labeled-edge: trans-label unlabeled-edge
 never: "never" { res.namer = res.h->aut->create_namer<std::string>();
 	         res.h->aut->set_single_acceptance_set();
 		 res.h->aut->prop_state_based_acc();
-		 res.acc_state = State_Acc; }
+		 res.acc_state = State_Acc;
+		 res.pos_acc_sets = res.h->aut->acc().all_sets();
+	       }
        '{' nc-states '}'
        {
 	 // Add an accept_all state if needed.
@@ -1198,9 +1200,13 @@ nc-transition:
 /**********************************************************************/
 
 lbtt: lbtt-header lbtt-body ENDAUT
+      {
+	res.pos_acc_sets = res.h->aut->acc().all_sets();
+      }
     | lbtt-header-states LBTT_EMPTY
       {
         res.h->aut->set_acceptance_conditions($2);
+	res.pos_acc_sets = res.h->aut->acc().all_sets();
       }
 
 lbtt-header-states: LBTT
@@ -1321,30 +1327,43 @@ hoayy::parser::error(const location_type& location,
 
 static void fix_acceptance(result_& r)
 {
+  auto& acc = r.h->aut->acc();
+  // Compute the unused sets before possibly adding some below.
+  auto unused = acc.comp(r.neg_acc_sets | r.pos_acc_sets);
+
   // If a set x appears only as Inf(!x), we can complement it so that
   // we work with Inf(x) instead.
-  auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
+  if (auto onlyneg = r.neg_acc_sets - r.pos_acc_sets)
-  for (auto& t: r.h->aut->transition_vector())
+    for (auto& t: r.h->aut->transition_vector())
-    t.acc ^= onlyneg;
+      t.acc ^= onlyneg;
 
   // However if set x is used elsewhere, for instance in
   //   Inf(!x) & Inf(x)
   // complementing x would be wrong.  We need to create a
   // new set, y, that is the complement of x, and rewrite
   // this as Inf(y) & Inf(x).
-  auto both = r.neg_acc_sets & r.pos_acc_sets;
+  if (auto both = r.neg_acc_sets & r.pos_acc_sets)
-  if (both)
     {
-      auto& acc = r.h->aut->acc();
       auto v = acc.sets(both);
       auto vs = v.size();
       unsigned base = acc.add_sets(vs);
       for (auto& t: r.h->aut->transition_vector())
 	if ((t.acc & both) != both)
 	  for (unsigned i = 0; i < vs; ++i)
-	    if (!t.acc.has(i))
+	    if (!t.acc.has(v[i]))
 	      t.acc |= acc.mark(base + i);
     }
+
+  // Remove all acceptance sets that are not used in the acceptance
+  // condition.  Because the rest of the code still assume that all
+  // acceptance sets have to be seen.  See
+  //   https://github.com/adl/hoaf/issues/36
+  if (unused)
+    {
+      for (auto& t: r.h->aut->transition_vector())
+	t.acc = acc.strip(t.acc, unused);
+      r.h->aut->set_acceptance_conditions(acc.num_sets() - unused.count());
+    }
 }
 
 static void fix_initial_state(result_& r)
@@ -1455,8 +1474,7 @@ namespace spot
       return nullptr;
     if (r.state_names)
       r.h->aut->set_named_prop("state-names", r.state_names);
-    if (r.neg_acc_sets)
+    fix_acceptance(r);
-      fix_acceptance(r);
     fix_initial_state(r);
     fix_properties(r);
     return r.h;

src/tgbatest/hoaparse.test

@@ -1285,7 +1285,7 @@ State: 2 "G((F(a) && F((b) && (c))) && F((d) || (e)))"
 EOF
 
 
-# name states can be output as comments in never claim
+# named states can be output as comments in never claim
 cat >input <<EOF
 HOA: v1
 name: "a U b"
@@ -1314,3 +1314,95 @@ accept_all: /* s0 */
   skip
 }
 EOF
+
+
+# ltl3ba 1.1.1 has a bug where it outputs
+#   Acceptance: 1 t
+# when it meant
+#   Acceptance: 1 Inf(0)
+# and a development version of our parser would
+# incorrectly interpret the former as the latter.
+#
+# Make sure we ignore all {0} if the acceptance is "1 t".
+# See https://github.com/adl/hoaf/issues/36
+
+cat >input <<EOF
+HOA: v1
+tool: "ltl3ba" "1.1.1"
+name: "TGBA for Fa"
+States: 2
+Start: 0
+acc-name: generalized-Buchi 1
+Acceptance: 1 t
+AP: 1 "a"
+properties: trans-labels explicit-labels trans-acc no-univ-branch
+--BODY--
+State: 0 "F(a)"
+ [(0)] 1 {0}
+ [(!0)] 0
+State: 1 "t"
+ [t] 1 {0}
+--END--
+/* Also try with more acceptance sets */
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "a" "b" "c"
+Acceptance: 5 Inf(0)&Inf(4)&Inf(2)&Inf(!2)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[0&1&2] 0 {0 4 2}
+[!0&1&2] 0 {4 2}
+[0&!1&2] 0 {0 2}
+[!0&!1&2] 0 {2}
+[0&1&!2] 0 {0 4}
+[!0&1&!2] 0 {4}
+[0&!1&!2] 0 {0}
+[!0&!1&!2] 0
+--END--
+EOF
+
+# The mapping of acceptance sets for the second automaton is
+#   input   ->  output
+#     0     ->    0
+#     1     ->   removed
+#     2     ->    1
+#     3     ->   removed
+#     4     ->    2
+#    !2     ->    3
+expectok input <<EOF
+HOA: v1
+name: "TGBA for Fa"
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc complete deterministic
+--BODY--
+State: 0 "F(a)"
+[0] 1
+[!0] 0
+State: 1 "t"
+[t] 1
+--END--
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: generalized-Buchi 4
+Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[0&1&2] 0 {0 1 2}
+[!0&1&2] 0 {1 2}
+[0&!1&2] 0 {0 1}
+[!0&!1&2] 0 {1}
+[0&1&!2] 0 {0 2 3}
+[!0&1&!2] 0 {2 3}
+[0&!1&!2] 0 {0 3}
+[!0&!1&!2] 0 {3}
+--END--
+EOF