Fix parity solver if edgevector is not contiguous

Validity of strategies was tested relying on
num_edges() which might be smaller than the edge_number

* spot/twaalgos/game.cc: Fix here
* tests/python/game.py: Test here

spot/twaalgos/game.cc

@@ -272,12 +272,16 @@ namespace spot
         // Only the states owned by the winner need a strategy
         assert([&]()
                {
+                  std::unordered_set<unsigned> valid_strat;
+                  for (const auto& e : arena_->edges())
+                    valid_strat.insert(arena_->edge_number(e));
+
                   for (unsigned v = 0; v < arena_->num_states(); ++v)
                     {
                       if (!solve_globally && (info_->scc_of(v) == -1u))
                         continue;
                       if (((*owner_ptr_)[v] == w_.winner(v))
-                          && ((s_[v] <= 0) || (s_[v] > arena_->num_edges())))
+                          && (valid_strat.count(s_.at(v)) == 0))
                         return false;
                     }
                   return true;

tests/python/game.py

@@ -384,4 +384,141 @@ spot.solve_game(aut)
 S1 = list(spot.get_strategy(aut))
 spot.solve_game(aut)
 S2 = list(spot.get_strategy(aut))
-tc.assertEqual(S1, S2)
+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)