From 406bc8ed1702c2ec2a1e117fd8ca94f07a61422f Mon Sep 17 00:00:00 2001 From: Philipp Schlehuber Date: Wed, 22 Sep 2021 12:52:03 +0200 Subject: [PATCH] Remove do_simplify opt from split_2step Removing this option to guarante that all arenas are alternating * spot/twaalgos/synthesis.hh: Here * spot/twaalgos/synthesis.cc: Here * spot/twaalgos/mealy_machine.cc: API change * tests/python/aiger.py: API change * tests/python/mealy.py: API change * tests/python/split.py: API change --- spot/twaalgos/mealy_machine.cc | 4 +- spot/twaalgos/synthesis.cc | 71 +++++++++------------------------- spot/twaalgos/synthesis.hh | 9 ++--- tests/python/aiger.py | 2 +- tests/python/mealy.py | 2 +- tests/python/split.py | 2 +- 6 files changed, 27 insertions(+), 63 deletions(-) diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index b837a436f..f19a474a2 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -507,7 +507,7 @@ namespace spot // Split if the initial aut was split if (orig_is_split) { - mmc = split_2step(mmc, outs, false, false); + mmc = split_2step(mmc, outs, false); bool orig_init_player = mm->get_named_prop>("state-player") ->at(mm->get_init_state_number()); @@ -582,7 +582,7 @@ namespace spot mm->purge_unreachable_states(); if (orig_is_split) { - mm = split_2step(mm, outs, false, false); + mm = split_2step(mm, outs, false); alternate_players(mm, init_player, false); mm->set_named_prop("synthesis-outputs", new bdd(outs)); } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 0af668c44..e655edab5 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -135,8 +135,7 @@ namespace spot { twa_graph_ptr split_2step(const const_twa_graph_ptr& aut, - const bdd& output_bdd, bool complete_env, - bool do_simplify) + const bdd& output_bdd, bool complete_env) { auto split = make_twa_graph(aut->get_dict()); split->copy_ap_of(aut); @@ -216,25 +215,6 @@ namespace spot e_cache.clear(); auto out_cont = aut->out(src); - // Short-cut if we do not want to - // split the edges of nodes that have - // a single outgoing edge - if (do_simplify - && (++out_cont.begin()) == out_cont.end()) - { - // "copy" the edge - const auto& e = *out_cont.begin(); - split->new_edge(src, e.dst, e.cond, e.acc); - // Check if it needs to be completed - if (complete_env) - { - bdd missing = bddtrue - bdd_exist(e.cond, output_bdd); - if (missing != bddfalse) - split->new_edge(src, get_sink_con_state(), missing); - } - // We are done for this state - continue; - } // Avoid looping over all minterms // we only loop over the minterms that actually exist @@ -433,9 +413,11 @@ namespace spot out->copy_acceptance_of(aut); out->copy_ap_of(aut); - // split_2step is not guaranteed to produce - // states that alternate between env and player do to do_simplify + // split_2step is guaranteed to produce an alternating arena auto owner = get_state_players(aut); +#ifndef NDEGUB + (void) owner; +#endif std::vector state_map(aut->num_states(), unseen_mark); auto seen = [&](unsigned s){return state_map[s] != unseen_mark; }; @@ -456,30 +438,16 @@ namespace spot todo.pop_front(); for (const auto& i : aut->out(cur)) - { - // if the dst is also owned env - if (!owner[i.dst]) - { - // This can only happen if there is only - // one outgoing edges for cur - assert(([&aut, cur]()->bool - { - auto out_cont = aut->out(cur); - return (++(out_cont.begin()) == out_cont.end()); - })()); - if (!seen(i.dst)) - todo.push_back(i.dst); - out->new_edge(cur_m, map_s(i.dst), i.cond, i.acc); - continue; // Done with cur - } - for (const auto& o : aut->out(i.dst)) - { - if (!seen(o.dst)) - todo.push_back(o.dst); - out->new_edge(cur_m, map_s(o.dst), - i.cond & o.cond, i.acc | o.acc); - } - } + for (const auto& o : aut->out(i.dst)) + { + assert((owner.at(cur) != owner.at(o.src)) + && (owner.at(cur) == owner.at(o.dst) + && "Arena is not alternating!")); + if (!seen(o.dst)) + todo.push_back(o.dst); + out->new_edge(cur_m, map_s(o.dst), + i.cond & o.cond, i.acc | o.acc); + } } out->set_init_state(map_s(aut->get_init_state_number())); // Try to set outputs @@ -952,7 +920,7 @@ namespace spot << bv->paritize_time << " seconds\n"; if (bv) sw.start(); - dpa = split_2step(tmp, outs, true, false); + dpa = split_2step(tmp, outs, true); colorize_parity_here(dpa, true); if (bv) bv->split_time += sw.stop(); @@ -975,7 +943,7 @@ namespace spot << " states\n"; if (bv) sw.start(); - dpa = split_2step(aut, outs, true, false); + dpa = split_2step(aut, outs, true); colorize_parity_here(dpa, true); if (bv) bv->split_time += sw.stop(); @@ -988,8 +956,7 @@ namespace spot case solver::SPLIT_DET: { sw.start(); - auto split = split_2step(aut, outs, - true, false); + auto split = split_2step(aut, outs, true); if (bv) bv->split_time += sw.stop(); if (vs) @@ -1045,7 +1012,7 @@ namespace spot if (bv) sw.start(); - dpa = split_2step(dpa, outs, true, false); + dpa = split_2step(dpa, outs, true); colorize_parity_here(dpa, true); if (bv) bv->split_time += sw.stop(); diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index e96f9331d..b641fc851 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -25,8 +25,8 @@ namespace spot { - /// \brief make each transition (conditionally, see do_simplify) - /// a 2-step transition + /// \brief make each transition a 2-step transition, transforming + /// the graph into an alternating arena /// /// Given a set of atomic propositions I, split each transition /// p -- cond --> q cond in 2^2^AP @@ -45,16 +45,13 @@ namespace spot /// are treated as inputs /// \param complete_env Whether the automaton should be complete for the /// environment, i.e. the player of I - /// \param do_simplify If a state has a single outgoing transition - /// we do not necessarily have to split it - /// to solve the game /// \note: This function also computes the state players /// \note: If the automaton is to be completed for both env and player /// then egdes between the sinks will be added /// (assuming that the environnement/player of I) plays first SPOT_API twa_graph_ptr split_2step(const const_twa_graph_ptr& aut, - const bdd& output_bdd, bool complete_env, bool do_simplify); + const bdd& output_bdd, bool complete_env); /// \brief make each transition a 2-step transition. diff --git a/tests/python/aiger.py b/tests/python/aiger.py index 85db76144..6938d0703 100644 --- a/tests/python/aiger.py +++ b/tests/python/aiger.py @@ -3333,7 +3333,7 @@ for strat_string, (ins_str, outs_str) in strats: outs &= buddy.bdd_ithvar(strat.register_ap(aout)) spot.set_synthesis_outputs(strat, outs) - strat_s = spot.split_2step(strat, outs, False, False) + strat_s = spot.split_2step(strat, outs, False) for m in ["isop", "ite", "both"]: for ss in [""] + [f"+sub{ii}" for ii in range(3)]: diff --git a/tests/python/mealy.py b/tests/python/mealy.py index ef4c6933e..6c84ac2bc 100644 --- a/tests/python/mealy.py +++ b/tests/python/mealy.py @@ -378,7 +378,7 @@ for (mealy_str, nenv_min) in test_auts: ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name())) else: assert("""Aps must start with either "i" or "o".""") - mealy_min_us_s = spot.split_2step(mealy_min_us, outs, False, False) + mealy_min_us_s = spot.split_2step(mealy_min_us, outs, False) assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True)) diff --git a/tests/python/split.py b/tests/python/split.py index 0949f3425..752b90aea 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -46,7 +46,7 @@ def do_split(f, out_list): outputs = spot.buddy.bddtrue for a in out_list: outputs &= spot.buddy.bdd_ithvar(aut.get_dict().varnum(spot.formula(a))) - s = spot.split_2step(aut, outputs, False, False) + s = spot.split_2step(aut, outputs, False) return aut, s aut, s = do_split('(FG !a) <-> (GF b)', ['b'])