sbacc: fix a typo and remove some useless code

* spot/twaalgos/sbacc.cc: Do not assign to one_in twice, and
fix the value of init_acc.
* tests/core/sbacc.test: Add a test case.
* NEWS: Mention the bug.

NEWS

@@ -19,6 +19,10 @@ New in spot 2.3.1.dev (not yet released)
   - genltl was never meant to have (randomly attributed) short
     options for --postive and --negative.
 
+  - a typo in the code for transformating transition-based acceptance
+    to state-based acceptance could cause a superfluous initial state
+    to be output in some cases (the result was still correct).
+
   Deprecation notices:
 
   - Using --format=%a to print the number of atomic propositions in

spot/twaalgos/sbacc.cc

@@ -37,21 +37,22 @@ namespace spot
 
     unsigned ns = old->num_states();
     acc_cond::mark_t all = old->acc().all_sets();
+    // Marks that are common to all ingoing or outgoing transitions.
     std::vector<acc_cond::mark_t> common_in(ns, all);
     std::vector<acc_cond::mark_t> common_out(ns, all);
+    // Marks that label one incoming transition from the same SCC.
     std::vector<acc_cond::mark_t> one_in(ns, 0U);
     for (auto& e: old->edges())
       if (si.scc_of(e.src) == si.scc_of(e.dst))
         {
           common_in[e.dst] &= e.acc;
           common_out[e.src] &= e.acc;
-          one_in[e.dst] = e.acc;
         }
     for (unsigned s = 0; s < ns; ++s)
       common_out[s] |= common_in[s];
     for (auto& e: old->edges())
       if (si.scc_of(e.src) == si.scc_of(e.dst))
-        one_in[e.dst] = (e.acc - common_out[e.src]);
+        one_in[e.dst] = e.acc - common_out[e.src];
 
     auto res = make_twa_graph(old->get_dict());
     res->copy_ap_of(old);
@@ -83,7 +84,7 @@ namespace spot
     if (!si.is_rejecting_scc(si.scc_of(old_init)))
       // Use any edge going into the initial state to set the first
       // acceptance mark.
-      init_acc = one_in[old_init] | common_out[init_acc];
+      init_acc = one_in[old_init] | common_out[old_init];
 
     res->set_init_state(new_state(old_init, init_acc));
     while (!todo.empty())

tests/core/sbacc.test

@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
+# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -76,6 +76,22 @@ State: 1 {0}
 State: 2
 [0] 0 {1}
 --END--
+/* The following example used to be converted into a
+   3-state automaton instead of just 2 states, due to
+   a typo in the code. */
+HOA: v1
+States: 2
+Start: 1
+AP: 2 "a" "b"
+Acceptance: 2 Fin(0) & Inf(1)
+--BODY--
+State: 0
+[t] 0 {0}
+State: 1
+[1] 0
+[0&!1] 1 {1}
+--END--
+
 EOF
 
 run 0 $autfilt --state-based-acceptance in.hoa -H > out.hoa
@@ -96,6 +112,20 @@ State: 1 {0}
 State: 2 {0 1}
 [0] 0
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0 {1}
+[0&!1] 0
+[1] 1
+State: 1
+[t] 1
+--END--
 EOF
 
 diff out.hoa expected
@@ -103,7 +133,7 @@ diff out.hoa expected
 $autfilt --sba -H expected > out.hoa
 diff out.hoa expected
 
-$autfilt --strip-acc -H expected > out.hoa
+$autfilt --strip-acc -H expected -n1 > out.hoa
 cat >expected <<EOF
 HOA: v1
 States: 3