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
This commit is contained in:
Philipp Schlehuber
parent
ddda68403f
commit
406bc8ed17
6 changed files with 27 additions and 63 deletions
|
|
@ -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<std::vector<bool>>("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));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<unsigned> state_map(aut->num_states(), unseen_mark);
|
||||
auto seen = [&](unsigned s){return state_map[s] != unseen_mark; };
|
||||
|
|
@ -456,31 +438,17 @@ 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))
|
||||
{
|
||||
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
|
||||
if (bdd* outptr = aut->get_named_prop<bdd>("synthesis-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();
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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)]:
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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'])
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue