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.

tests/python/game.py

@@ -407,140 +407,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)