correct to_finite

This fixes issue #596.

* spot/twaalgos/remprop.cc: Rewrite main loop.
* tests/core/ltlf.test: Add test case.
* tests/python/game.py: Remove a test that appears
to make incorrect assumptions about to_finite.
* NEWS: Mention the bug.

NEWS

@@ -117,6 +117,9 @@ New in spot 2.12.1.dev  (not yet released)
     status and the AIG circuit; it now does the job silently as
     requested.
 
+  - to_finite() was dealing incorrectly with edges that were
+    both alive and dead.  (Issue #596.)
+
 New in spot 2.12.1  (2024-09-23)
 
   Bug fixes:

spot/twaalgos/remprop.cc

@@ -19,6 +19,7 @@
 #include "config.h"
 #include <spot/twaalgos/remprop.hh>
 #include <spot/twaalgos/mask.hh>
+#include <spot/twaalgos/sccinfo.hh>
 #include <ctype.h>
 #include <sstream>
 
@@ -180,6 +181,8 @@ namespace spot
       make_twa_graph(aut,
                      { false, false, true, false, false, false });
 
+    scc_info si(aut, scc_info_options::TRACK_SUCCS);
+
     bdd rem = bddtrue;
     bdd neg = bddfalse;
     int v = res->get_dict()->
@@ -194,18 +197,18 @@ namespace spot
     unsigned ns = res->num_states();
     std::vector<bool> isacc(ns, false);
     for (unsigned s = 0; s < ns; ++s)
-      {
+      for (auto& e: res->out(s))
-        for (auto& e: res->out(s))
+        {
-          if (bdd_implies(e.cond, neg))
+          if (!si.is_useful_state(e.dst))
             {
-              isacc[e.src] = true;
               e.cond = bddfalse;
+              continue;
             }
-          else
+          if (bdd_have_common_assignment(e.cond, neg))
-            {
+            isacc[e.src] = true;
-              e.cond = bdd_restrict(e.cond, rem);
+          e.cond = bdd_restrict(e.cond, rem);
-            }
+        }
-      }
+
 
     res->set_buchi();
     res->prop_state_acc(true);

tests/core/ltlf.test

@@ -173,51 +173,62 @@ cmp out3 out4 && exit 1 # make sure we did remove something
 autfilt out3 > out4
 diff out4 expected3
 
-# Issue #526
+# Issue #526 and Issue #596
-ltlfilt -f '(i->XXo)|G(i<->Xo2)' --from-ltlf | ltl2tgba -D |\
+ltlfilt -f '(i->XXo)|G(i<->Xo2)' -f XXXo --from-ltlf | ltl2tgba -D |\
     autfilt -C --to-finite > out
 cat >exp <<EOF
 HOA: v1
-States: 9
+States: 8
 Start: 0
 AP: 3 "o" "o2" "i"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
-properties: trans-labels explicit-labels state-acc complete
+properties: trans-labels explicit-labels state-acc deterministic
-properties: deterministic
 --BODY--
-State: 0 {0}
+State: 0
 [2] 6
 [!2] 7
 State: 1
 [!1&!2] 1
 [!1&2] 5
-[1] 8
 State: 2 {0}
 [0] 7
-[!0] 8
 State: 3 {0}
 [!0&!1&!2] 1
 [!0&!1&2] 5
 [0] 7
-[!0&1] 8
 State: 4 {0}
 [!0&1&!2] 1
 [!0&1&2] 5
 [0] 7
-[!0&!1] 8
 State: 5 {0}
 [1&!2] 1
 [1&2] 5
-[!1] 8
 State: 6 {0}
 [!1] 2
 [1&!2] 3
 [1&2] 4
 State: 7 {0}
 [t] 7
-State: 8
+--END--
-[t] 8
+HOA: v1
+States: 5
+Start: 0
+AP: 1 "o"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[t] 4
+State: 1 {0}
+[0] 3
+State: 2 {0}
+[t] 1
+State: 3 {0}
+[t] 3
+State: 4 {0}
+[t] 2
 --END--
 EOF
 diff out exp

tests/python/game.py

@@ -424,140 +424,3 @@ S1 = list(spot.get_strategy(aut))
 spot.solve_game(aut)
 S2 = list(spot.get_strategy(aut))
 tc.assertEqual(S1, S2)
-
-
-# Finite games
-alive = "__alive__"
-def finite_existential(auts):
-    # 1 Accepting state -> selfloop
-    # 2 Prune
-    acc_state = set()
-    sp = list(spot.get_state_players(auts))
-    for e in auts.edges():
-        if e.acc:
-            acc_state.add(e.src)
-    for s in acc_state:
-        e_kill = auts.out_iteraser(s)
-        while (e_kill):
-            e_kill.erase()
-    for s in acc_state:
-        sprime = auts.new_state()
-        sp.append(not sp[s])
-        auts.new_edge(s, sprime, buddy.bddtrue, [0])
-        auts.new_edge(sprime, s, buddy.bddtrue, [0])
-    spot.set_state_players(auts, sp)
-    auts.purge_dead_states()
-    spot.alternate_players(auts, False, False)
-    return auts
-
-def is_input_complete(auts):
-    sp = spot.get_state_players(auts)
-    for s in range(auts.num_states()):
-        if sp[s]:
-            continue # Player
-        cumul = buddy.bddfalse
-        for e in auts.out(s):
-            cumul |= e.cond
-        if cumul != buddy.bddtrue:
-            return False
-
-    return True
-
-def synt_from_ltlf(f:str, outs):
-    ff = spot.from_ltlf(f, alive)
-    aut = ff.translate("buchi", "sbacc")
-    outbdd = buddy.bddtrue
-    for out in outs:
-        outbdd &= buddy.bdd_ithvar(aut.register_ap(out))
-    alive_bdd = buddy.bdd_ithvar(aut.register_ap(alive))
-    auts = spot.split_2step(aut, outbdd & alive_bdd, False)
-    auts = spot.to_finite(auts, alive)
-    spot.alternate_players(auts, False, False)
-    spot.set_synthesis_outputs(auts, outbdd)
-    if not is_input_complete(auts):
-        print("Not synthesizable")
-        return None
-    auts = finite_existential(auts)
-
-    return auts
-
-def synt_ltlf(f:str, outs, res:str = "aut"):
-    auts = synt_from_ltlf(f, outs)
-
-    succ = spot.solve_parity_game(auts)
-    if not succ:
-        if res == "aut":
-            return False, auts
-        else:
-            return False, None
-
-    mealy_cc = spot.solved_game_to_split_mealy(auts)
-
-    if res == "aut":
-        return True, mealy_cc
-    elif res == "aig":
-        return True, spot.mealy_machine_to_aig(mealy_cc, "isop")
-    else:
-        raise RuntimeError("Unknown option")
-
-
-sink_player = None
-
-def negate_ltlf(f:str, outs, opt = "buchi"):
-
-    global sink_player
-    sink_player = None
-
-    aut = synt_from_ltlf(f, outs)
-    # Implies input completeness
-    # We need output completeness
-    acc = []
-
-    sp = list(spot.get_state_players(aut))
-
-    def get_sink():
-        global sink_player
-        if sink_player is None:
-            sink_player = aut.new_states(2)
-            aut.new_edge(sink_player, sink_player + 1, buddy.bddtrue, acc)
-            aut.new_edge(sink_player + 1, sink_player, buddy.bddtrue, acc)
-            sp.append(False)
-            sp.append(True)
-            spot.set_state_players(aut, sp)
-        return sink_player
-
-    for s in range(aut.num_states()):
-        if not sp[s]:
-            continue
-        rem = buddy.bddtrue
-        for e in aut.out(s):
-            rem -= e.cond
-        if rem != buddy.bddfalse:
-            aut.new_edge(s, get_sink(), rem)
-
-    # Better to invert colors or condition?
-    if opt == "buchi":
-        for e in aut.edges():
-            if e.acc:
-                e.acc = spot.mark_t()
-            else:
-                e.acc = spot.mark_t([0])
-    elif opt == "cobuchi":
-        aut.set_co_buchi()
-    else:
-        raise RuntimeError("Unknown opt")
-    return aut
-
-# Game where the edge_vector is larger
-# than the number of transitions
-f1 = "((((G (F (idle))) && (G (((idle) && (X ((! (grant_0)) \
-      && (! (grant_1))))) -> (X (idle))))) && (G ((X (! (grant_0))) \
-      || (X (((! (request_0)) && (! (idle))) U ((! (request_0)) \
-      && (idle))))))) -> (((G (((((X (((! (grant_0)) && (true)) \
-      || ((true) && (! (grant_1))))) && ((X (grant_0)) -> (request_0))) \
-      && ((X (grant_1)) -> (request_1))) && ((request_0) -> (grant_1))) \
-      && ((! (idle)) -> (X ((! (grant_0)) && (! (grant_1))))))) \
-      && (! (F (G ((request_0) && (X (! (grant_0)))))))) \
-      && (! (F (G ((request_1) && (X (! (grant_1)))))))))"
-outs = ["grant_0", "grant1"]
-tc.assertEqual(synt_ltlf(f1, outs)[0], False)