From 5ddac258e1d536c8d61637a2581d51fe35813d19 Mon Sep 17 00:00:00 2001 From: Philipp Schlehuber Date: Sun, 3 Mar 2024 22:15:27 +0100 Subject: [PATCH] Introduce new ways to split an automaton The explicit way of splitting suffers if there are too many input APs, two new ways of splitting are introduced as well as a heuristic to chose between them. * NEWS: update * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: New fonctions * bin/ltlsynt.cc: Add corresponding option * tests/core/gamehoa.test, tests/core/ltlsynt.test, tests/python/_partitioned_relabel.ipynb, tests/python/_synthesis.ipynb, tests/python/game.py, tests/python/split.py, tests/python/synthesis.py: Adjusting and adding test --- NEWS | 9 + bin/ltlsynt.cc | 27 +- spot/twaalgos/synthesis.cc | 1006 ++++++++++++++++++++++- spot/twaalgos/synthesis.hh | 138 ++-- tests/core/gamehoa.test | 6 +- tests/core/ltlsynt.test | 23 +- tests/python/_partitioned_relabel.ipynb | 34 +- tests/python/_synthesis.ipynb | 68 +- tests/python/game.py | 23 +- tests/python/split.py | 166 ++++ tests/python/synthesis.py | 10 +- 11 files changed, 1372 insertions(+), 138 deletions(-) diff --git a/NEWS b/NEWS index c0ab55c77..957b9b254 100644 --- a/NEWS +++ b/NEWS @@ -86,6 +86,15 @@ New in spot 2.12 (2024-05-16) Library: + - split_2step has now multiple ways to split for improved performance. + The option can be controlled via the synthesis_info::splittype + - EXPL: explicit splitting of each state as before + - SEMISYM: The outgoing transition of each state are encoded + as a bdd; Works better for larger number of input APs + - FULLYSYM: The automaton is first translated into a + fully symbolic version, then split. + - AUTO: Let the heuristic decide what to do. + - The following new trivial simplifications have been implemented for SEREs: - f|[+] = [+] if f rejects [*0] - f|[*] = [*] if f accepts [*0] diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 24f4af16a..456d2cb41 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -63,6 +63,7 @@ enum OPT_PRINT_HOA, OPT_REAL, OPT_SIMPLIFY, + OPT_SPLITTYPE, OPT_TLSF, OPT_VERBOSE, OPT_VERIFY @@ -118,6 +119,9 @@ static const argp_option options[] = "reduction with output assignment, (sat) SAT-based minimization, " "(bisim-sat) SAT after bisim, (bwoa-sat) SAT after bwoa. Defaults " "to 'bwoa'.", 0 }, + { "splittype", OPT_SPLITTYPE, "expl|semisym|fullysym|auto", 0, + "Selects the algorithm to use to transform the automaton into " + "a game graph. Defaults to 'auto'.", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, @@ -295,6 +299,23 @@ static unsigned simplify_values[] = }; ARGMATCH_VERIFY(simplify_args, simplify_values); +static const char* const splittype_args[] = + { + "expl", + "semisym", + "fullysym", + "auto", + nullptr + }; +static spot::synthesis_info::splittype splittype_values[] = + { + spot::synthesis_info::splittype::EXPL, + spot::synthesis_info::splittype::SEMISYM, + spot::synthesis_info::splittype::FULLYSYM, + spot::synthesis_info::splittype::AUTO, + }; +ARGMATCH_VERIFY(splittype_args, splittype_values); + namespace { static bool want_game() @@ -909,7 +930,7 @@ namespace return 2; } if (!arena->get_named_prop>("state-player")) - arena = spot::split_2step(arena, true); + arena = spot::split_2step(arena, gi); else { // Check if the game is alternating and fix trivial cases @@ -1127,6 +1148,10 @@ parse_opt(int key, char *arg, struct argp_state *) gi->minimize_lvl = XARGMATCH("--simplify", arg, simplify_args, simplify_values); break; + case OPT_SPLITTYPE: + gi->sp = XARGMATCH("--splittype", arg, + splittype_args, splittype_values); + break; case OPT_TLSF: jobs.emplace_back(arg, job_type::TLSF_FILENAME); break; diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index 2928a642d..3c93137dc 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -32,9 +32,15 @@ #include #include #include +#include +#include #include #include +#include +#ifndef NDEBUG +#include +#endif // Helper function/structures for split_2step namespace{ using namespace spot; @@ -440,9 +446,11 @@ namespace{ namespace spot { + namespace + { twa_graph_ptr - split_2step(const const_twa_graph_ptr& aut, - const bdd& output_bdd, bool complete_env) + split_2step_expl_impl(const const_twa_graph_ptr& aut, + const bdd& output_bdd, bool complete_env) { assert(!aut->get_named_prop("state-player") && "aut is already split!"); @@ -681,14 +689,961 @@ namespace spot // Done return split; + } // End split old impl + + std::vector + do_bin_encode_(unsigned N, int var0, unsigned Nvar) + { + auto bddvec = std::vector>(Nvar); + for (unsigned i = 0; i < Nvar; ++i) + bddvec[i] = {bdd_nithvar(var0+i), bdd_ithvar(var0+i)}; + + auto do_bin_encode_1 = [&bddvec, Nvar](unsigned s) -> bdd { + bdd res = bddtrue; + + for (unsigned i = 0; i < Nvar; ++i) + { + res &= bddvec[i][s&1]; + s >>= 1; + } + return res; + }; + + auto s2bdd = std::vector(N); + for (unsigned s = 0; s < N; ++s) + s2bdd[s] = do_bin_encode_1(s); + + return s2bdd; + } + + struct bitVectDecodeIterator{ + const std::vector& v_; + unsigned u_, idx_ = 0u, vsize_; + bool first_ = true; + + bitVectDecodeIterator(const std::vector& v, unsigned init) + : v_{v} + , u_{init} + , vsize_(v_.size()) + { + } + + // Sets to zero all variable bits before the current idx + void small_reset_() noexcept { + // Skip current idx + for (--idx_; idx_!= -1u; --idx_) + u_ ^= (1u << v_[idx_]); + idx_ = 0; + } + + bitVectDecodeIterator& operator++() noexcept { + first_ = false; + // Search for the next variable bit to increase + while (idx_ < vsize_) + { + auto curr = 1u << v_[idx_]; + if (!(u_ & curr)){ + u_ |= curr; + small_reset_(); + return *this; + } + ++idx_; + } + return *this; + } + + unsigned operator*() const noexcept { + return u_; + } + + explicit operator bool() const noexcept{ + // There is always at least one element + return idx_ < vsize_ || first_; + } + + }; + + class bitVectDecodeRange + { + private: + const std::vector& v_; + const unsigned initval_; + + public: + bitVectDecodeRange(const std::vector& v, unsigned init) + : v_{v} + , initval_{init} + { + } + + auto + begin() const + { + return bitVectDecodeIterator(v_, initval_); + } + + }; + + template + twa_graph_ptr + split_2step_sym_impl(const const_twa_graph_ptr& aut, + const bdd& output_bdd, bool complete_env) + { + + assert(!aut->get_named_prop("state-player") + && "aut is already split!"); + + auto split = make_twa_graph(aut->get_dict()); + + auto [has_unsat, unsat_mark] = aut->acc().unsat_mark(); + bool max_par, odd_par, color_env; + color_env = aut->acc().is_parity(max_par, odd_par, true); + const unsigned Ncolor = aut->acc().all_sets().max_set(); + + split->copy_ap_of(aut); + split->new_states(aut->num_states()); + split->set_init_state(aut->get_init_state_number()); + set_synthesis_outputs(split, output_bdd); + //split->prop_copy(aut, twa::prop_set::all()); // todo why? + + const auto use_color = has_unsat; + color_env &= use_color; + if (has_unsat) + split->copy_acceptance_of(aut); + else + { + if (complete_env) + { + split->set_co_buchi(); // Fin(0) + unsat_mark = acc_cond::mark_t({0}); + has_unsat = true; + } + else + split->acc().set_acceptance(acc_cond::acc_code::t()); + } + + // Reserve all the necessary variables + const unsigned N = split->num_states(); + const unsigned Nstvars = std::ceil(std::log2(N)); + // we use one hot encoding for colors + constexpr unsigned Ncolorvars = SPOT_MAX_ACCSETS; + // Last one is for no color + + auto var_in = std::vector(); + auto var_out = std::vector(); + + { + bdd allbdd = split->ap_vars(); + while (allbdd != bddtrue) + { + int lvar = bdd_var(allbdd); + bdd l = bdd_ithvar(lvar); + if (bdd_implies(output_bdd, l)) + var_out.push_back(lvar); + else + var_in.push_back(lvar); + allbdd = bdd_high(allbdd); + assert(allbdd != bddfalse); + } + } + + const unsigned Nin = var_in.size(); + const unsigned Nout = var_out.size(); + + // Register the vars + // Need to be released + // Two possibilities for the need of variables: + // 1) FULLYSYM == false + // in conditions, (dst) states, color x out + // [(dst) states, color x out] is a player state + // 2) FULLYSYM == true + // (src) states, in conditions, (dst) states, color x out + // [(dst) states, color x out] is a player state + + int zeroIdx = aut->get_dict() + ->register_anonymous_variables(Nstvars*(1+FULLYSYM)+Nout + +Nin+Ncolorvars, &N); + + int srcStIdx = zeroIdx; + int inIdx = srcStIdx + Nstvars*FULLYSYM; + int dstStIdx = inIdx + Nin; + int colorIdx = dstStIdx + Nstvars; + int outIdx = colorIdx + Ncolorvars; + + // Construct the pairs + bddPair* replace_fwd = bdd_newpair(); + bddPair* replace_bkwd = bdd_newpair(); + bddPair* replace_in_fwd = bdd_newpair(); + bddPair* replace_in_bkwd = bdd_newpair(); + bddPair* replace_out_fwd = bdd_newpair(); + bddPair* replace_out_bkwd = bdd_newpair(); + + if (not replace_fwd || not replace_in_fwd || not replace_out_fwd + || not replace_bkwd || not replace_in_bkwd || not replace_out_bkwd) + throw std::runtime_error("split_2step(): bddpair alloc error."); + + { // Map old and contiguous inputs and outputs + auto var_new = std::vector(Nin); + std::iota(var_new.begin(), var_new.end(), inIdx); + bdd_setpairs(replace_fwd, var_in.data(), var_new.data(), Nin); + bdd_setpairs(replace_in_fwd, var_in.data(), var_new.data(), Nin); + bdd_setpairs(replace_bkwd, var_new.data(), var_in.data(), Nin); + bdd_setpairs(replace_in_bkwd, var_new.data(), var_in.data(), Nin); + + var_new.resize(Nout); + std::iota(var_new.begin(), var_new.end(), outIdx); + bdd_setpairs(replace_fwd, var_out.data(), var_new.data(), Nout); + bdd_setpairs(replace_out_fwd, var_out.data(), var_new.data(), Nout); + bdd_setpairs(replace_bkwd, var_new.data(), var_out.data(), Nout); + bdd_setpairs(replace_out_bkwd, var_new.data(), var_out.data(), Nout); + } + + // Encode states -> binary encoding (gray code for faster encode?) + auto dstEnvs2bdd = do_bin_encode_(N, dstStIdx, Nstvars); + //Source states are only needed once + + // Last bdd is no color + auto color2bdd = std::vector>(Ncolorvars); + for (int i = 0; i < (int) Ncolorvars; ++i) + color2bdd[i] = {bdd_nithvar(colorIdx + i), bdd_ithvar(colorIdx + i)}; + + // There are no colors -> All False + const bdd noColorBdd + = std::accumulate(color2bdd.begin(), color2bdd.end(), + (bdd) bddtrue, + [](const bdd& l, const auto& r) -> bdd + {return l & r[0]; }); + + // Each player state corresponds to a set of (dst_state, colors, outs) + // We also store the "least accepting" color + auto playbdd2st + = std::unordered_map, + bdd_hash>(); + playbdd2st.reserve(N); + + // Encode (in, out, state) and split< + auto invar2bdd = std::vector>(Nin); + for (int i = 0; i < (int) Nin; ++i) + invar2bdd[i] = {bdd_nithvar(inIdx+i), bdd_ithvar(inIdx+i)}; + + enum class ctask{ + PUT = 0, + VISIT, + POP + }; + + // Fwd map complete condition + // We could work with int, the bdd will stay in the graph + auto fwd_comp_repl = std::unordered_map(); + + // Encode a single edge in from aut with the new variables + auto encode_edge = [&](const auto& e) -> bdd + { + // Build color cond + // No color -> No bdd + bdd color_cond = noColorBdd; + if (use_color && e.acc != acc_cond::mark_t{}) + { + color_cond = bddtrue; + + for (unsigned acolor = 0; acolor < Ncolor; ++acolor) + color_cond &= color2bdd[acolor][e.acc.has(acolor)]; + } + // The whole edge; Order the and? N-ary and? + + auto [itc, insc] + = fwd_comp_repl.try_emplace(e.cond, bddfalse); + if (insc) + itc->second = bdd_replace(e.cond, replace_fwd); + return itc->second & color_cond & dstEnvs2bdd[e.dst]; + }; + + auto abstract_traverse + = [](auto& stack, auto&& fput, auto&& fpop, auto&& fvisit) -> void + { + while (not stack.empty()) + { + auto [ct, current] = std::move(stack.back()); + + stack.pop_back(); + + switch (ct) + { + case ctask::PUT: + fput(current); + break; + case ctask::POP: + fpop(current); + break; + case ctask::VISIT: + fvisit(current); + break; + } + } + }; + + auto abstract_put = [](auto& stack, const bdd& ccond, auto&& metaf) + { + for (int polprime : {0, 1}) + { + bdd cprime = polprime == 0 ? bdd_low(ccond) : bdd_high(ccond); + + if (cprime != bddfalse) + { + stack.emplace_back(ctask::POP, metaf(polprime)); + stack.emplace_back(ctask::VISIT, cprime); + stack.emplace_back(ctask::PUT, metaf(polprime)); + } + } + }; + + // Bkwd replace map + auto bkwd_out_repl = std::unordered_map(); + + // Final step construct colors and conditions + // cond is a bdd over color variables and new outputs + auto construct_colorcond + = [&](bdd cond) + { + // We need to do a final traversal of the color + // It is similar to the traversal of the states + + // The result + auto all_comb = std::vector>(); + + // int[2] is relative lvl and polarity + using stack_type = std::variant; + auto stack_colors = std::vector>(); + // Variables that do not appear can take both values + auto current_colors = acc_cond::mark_t{}; + + + auto fputCC = [&](const stack_type& ccond) -> void + { + auto lvl = std::get(ccond); + //if (lvl != Ncolorvars - 1) + // current_colors.set(lvl); // One hot + assert(lvl < Ncolorvars || lvl == -1u); + if (lvl != -1u) + current_colors.set(lvl); // One hot + }; + + auto fpopCC = [&](const stack_type& ccond) -> void + { + auto lvl = std::get(ccond); + //if (lvl != Ncolorvars - 1) + // current_colors.clear(lvl); // One cold + assert(lvl < Ncolorvars || lvl == -1u); + if (lvl != -1u) + current_colors.clear(lvl); // One cold + }; + + auto fvisitCC = [&](const stack_type& ccondin) -> void + { + bdd ccond = std::get(ccondin); + //if (ccond == bddfalse) + // return; // Nothing to do + + int clvl = ccond == bddtrue ? outIdx : bdd_var(ccond); + // We either have a out condition or true + if (clvl >= outIdx) + { + // We have found a new color comb + // Leading to ccond -> add + auto [itc, insc] + = bkwd_out_repl.try_emplace(ccond, bddfalse); + if (insc) + itc->second = bdd_replace(ccond, + replace_out_bkwd); + all_comb.emplace_back(current_colors, + itc->second); + + } + else + { + int rel_lvl = clvl - colorIdx; + // If the no color mark appears -> mark must be empty + auto metaf = [&, ulvl = (unsigned) rel_lvl](int pol) + { + // If the polarity is negative ("one cold") + // Then ignore it + assert(!pol || !current_colors.has(ulvl)); + return pol == 0 ? -1u : ulvl; + }; + abstract_put(stack_colors, ccond, metaf); + } + + }; + + stack_colors.emplace_back(ctask::VISIT, cond); + abstract_traverse(stack_colors, fputCC, fpopCC, fvisitCC); + + return all_comb; + }; + + + // The condition contains variables of dst_state, color x cond + // In a much similar manner we need to traverse the states, as we traversed + // the inputs + // Mapping bdd(color x new outs) -> [mark x old outs] + auto bdd2colorCond + = std::unordered_map>, + bdd_hash>(); + + struct unsigedItDescr { + unsigned val; + std::array canChange; + std::vector idx; + + unsigedItDescr() + : val{0u} + , idx{32, -1u} + { + canChange.fill(true); + } + }; + + auto construct_ply_state + = [&](bdd cond) -> std::pair + { + + // Needed to determine "least" accepting color for this state + // That is the color that we can put on all incoming transitions + auto thiscolor = acc_cond::mark_t{}; + bool has_uncolored = false; + unsigned thisstate = split->new_state(); + + // int[2] is relative lvl and polarity + using stack_type = std::variant>; + auto stack_states = std::vector>(); + auto current_dst_states = unsigedItDescr{}; + + auto fputPlySt + = [¤t_dst_states](const stack_type& ccond) -> void + { + assert((std::holds_alternative>(ccond))); + auto [lvl, pol] = std::get>(ccond); + // Fix the corresponding bit + // Not changeable + current_dst_states.canChange[lvl] = false; + if (pol) + // Set the bit true + current_dst_states.val |= (1u << lvl); + else + // Unset it + current_dst_states.val &= ~(1u << lvl); + }; + + auto fpopPlySt + = [¤t_dst_states](const stack_type& ccond) -> void + { + assert((std::holds_alternative>(ccond))); + // We need to unset the bit and mark it as changeable + auto lvl = std::get>(ccond)[0]; + current_dst_states.val &= ~(1u << lvl); + current_dst_states.canChange[lvl] = true; + }; + + auto fvisitPlySt = [&](const stack_type& ccondin) -> void + { + assert(std::holds_alternative(ccondin)); + const bdd& ccond = std::get(ccondin); + int clvl = ccond == bddtrue ? colorIdx : bdd_var(ccond); + if (clvl >= colorIdx) + { + // We have found a new "cube of states" + // Leading to ccond + auto [it_cc, ins_cc] + = bdd2colorCond.try_emplace(ccond, + std::vector< + std::pair>()); + if (ins_cc) + it_cc->second = construct_colorcond(ccond); + + // Loop over all the states in the "cube" + //auto state_range = bitVectDecodeRange(current_dst_states); + //for (auto it_s = state_range.begin(); (bool) it_s; ++it_s) + // Get all the modifiable idx + current_dst_states.idx.clear(); + for (unsigned i = 0; i < Nstvars; ++i) + if (current_dst_states.canChange[i]) + current_dst_states.idx.push_back(i); + // Loop over them + auto state_range = bitVectDecodeRange(current_dst_states.idx, + current_dst_states.val); + for (auto it_s = state_range.begin(); (bool) it_s; ++it_s) + // Loop over all edges + for (const auto& [acolor, acond] : it_cc->second) + { + split->new_edge(thisstate, *it_s, acond, acolor); + // Update color + thiscolor |= acolor; + has_uncolored |= !acolor; + } + + } + else + { + int rel_lvl = clvl - dstStIdx; + auto metaf = [rel_lvl](int pol) + { + return std::array{rel_lvl, pol}; + }; + abstract_put(stack_states, ccond, metaf); + } + + }; + + stack_states.emplace_back(ctask::VISIT, cond); + abstract_traverse(stack_states, fputPlySt, fpopPlySt, fvisitPlySt); + + // Adjust the color depending on options and acceptance conditions + // Todo: check if dead ends are treated correctly + if (!color_env | has_uncolored) + // Do something smart for TELA? + thiscolor = acc_cond::mark_t({}); + else if (max_par) + thiscolor = + acc_cond::mark_t({thiscolor.min_set()-1}); + else // min_par + thiscolor = + acc_cond::mark_t({thiscolor.max_set()-1}); + + return std::make_pair(thiscolor, thisstate); + }; + + // Fwd map for replacing + // Todo is this a good idea? + auto bkwd_in_repl = std::unordered_map(); + + auto stack_inputs = std::vector>(); + + bdd current_in = bddtrue; + + // Define the abstract traverse + auto fputInTrav = [¤t_in](const bdd& ccond) -> void + { + current_in &= ccond; + }; + + auto fpopInTrav = [¤t_in](const bdd& ccond) -> void + { + // At the end, exist is cheap (I hope) + current_in = bdd_exist(current_in, ccond); + }; + + + + unsigned sink_env = -1u; + + if constexpr (FULLYSYM) + { + // First we need to encode the complete automaton + // Create the symbolic aut + // To avoid reencoding, swap + bddPair* replace_dstSt_srcSt = bdd_newpair(); + { + auto varSrc = std::vector(Nstvars); + auto varDst = std::vector(Nstvars); + std::iota(varSrc.begin(), varSrc.end(), srcStIdx); + std::iota(varDst.begin(), varDst.end(), dstStIdx); + bdd_setpairs(replace_dstSt_srcSt, varDst.data(), + varSrc.data(), Nstvars); + } + auto getSrc = [&](unsigned s) + {return bdd_replace(dstEnvs2bdd[s], replace_dstSt_srcSt); }; + + bdd sym_aut = bddfalse; + for (unsigned s = 0; s < N; ++s) + { + bdd enc_out_s = bddfalse; + for (const auto& e : aut->out(s)) + enc_out_s |= encode_edge(e); + sym_aut |= getSrc(s)&enc_out_s; + } + + // Define how to construct an extended player state + // An extended player is constructing the list + // of (player state, input condition) from a bdd + // containing (in const, dst state, color cond) + // This function needs to traverse the incondition + // put and pop can be reused + auto construct_ext_ply_state + = [&](auto& plystatedict, const bdd& ccond) + { + current_in = bddtrue; + + auto& [plyconddict, plycondvect] = plystatedict; + + auto fvisitInTrav + = [&](const bdd& ccond) -> void + { + + int clvl = bdd_var(ccond); + assert(clvl >= inIdx); + if (clvl >= dstStIdx) // States come after input + { + // We have found a new in cube + // Add to the existing ones if necessary + // Translate to old variables + auto [itc, insc] + = bkwd_in_repl.try_emplace(current_in, bddfalse); + if (insc) + itc->second = bdd_replace(current_in, replace_in_bkwd); + const bdd& current_in_old = itc->second; + + // treat it + auto [it_s, ins_s] + = playbdd2st.try_emplace( + ccond, + std::make_pair(acc_cond::mark_t{}, + -1u)); + if (ins_s) + // A new player state and the corresponding least + // accepting color + it_s->second = construct_ply_state(ccond); + + // Add the condition + auto [it_e, ins_e] + = plyconddict.try_emplace(ccond, -1u); + // Add the input + if (ins_e) + { + it_e->second = plycondvect.size(); + plycondvect.emplace_back(ccond, bddfalse); + } + // The second is the in + plycondvect[it_e->second].second |= current_in_old; + assert(plycondvect[it_e->second].second != bddfalse + && "bddfalse is not allowed as condition"); + } + else + { + auto metaf = [&bddopts = invar2bdd[clvl - inIdx]](int pol) + { + return bddopts[pol]; + }; + abstract_put(stack_inputs, ccond, metaf); + } + }; + + // Do the actual visit + assert(stack_inputs.empty()); + stack_inputs.emplace_back(ctask::VISIT, ccond); + abstract_traverse(stack_inputs, fputInTrav, + fpopInTrav, fvisitInTrav); + }; // construct_ext_ply_state + + // What we want is + // dict[bdd (in, dst, cc) -> dict[ ply state bdd -> input bdd]] + // However this is not possible as it would possibly + // reorder the transitions + // So we need an additional vector and idx only into it + // The vector holds the player state cond + // (same as the key of the unordered_map) + // To ensure efficient iteration + auto ext_ply_dict + = std::unordered_map, + std::vector>>, bdd_hash>(); + // bdd over new variables -> bdd over old variables, player state + + // Vist the src states + using stack_type = std::variant>; + auto stack_states = std::vector>(); + // Variables that do not appear can take both values + auto current_src_states = unsigedItDescr{}; + + auto fputSrcSt + = [¤t_src_states](const stack_type& ccond) -> void + { + assert((std::holds_alternative>(ccond))); + auto [lvl, pol] = std::get>(ccond); + // Fix the corresponding bit + // Not changeable + current_src_states.canChange[lvl] = false; + if (pol) + // Set the bit true + current_src_states.val |= (1u << lvl); + else + // Unset it + current_src_states.val &= ~(1u << lvl); + }; + + auto fpopSrcSt + = [¤t_src_states](const stack_type& ccond) -> void + { + assert((std::holds_alternative>(ccond))); + // We need to unset the bit and mark it as changeable + auto lvl = std::get>(ccond)[0]; + current_src_states.val &= ~(1u << lvl); + current_src_states.canChange[lvl] = true; + }; + + auto fvisitSrcSt = [&](const stack_type& ccondin) -> void + { + assert(std::holds_alternative(ccondin)); + const bdd& ccond = std::get(ccondin); + int clvl = ccond == bddtrue ? inIdx : bdd_var(ccond); + if (clvl >= inIdx) + { + // We have found a new "cube of states" + // Leading to ccond + auto [it_cc, ins_cc] + = ext_ply_dict.try_emplace( + ccond, + decltype(ext_ply_dict)::mapped_type{}); + if (ins_cc) + // Construct "in place" + construct_ext_ply_state(it_cc->second, ccond); + + assert(!it_cc->second.second.empty() + && "Dead ends should not be splitted"); + + // Get all the modifiable idx + current_src_states.idx.clear(); + for (unsigned i = 0; i < Nstvars; ++i) + if (current_src_states.canChange[i]) + current_src_states.idx.push_back(i); + // Loop over them + auto state_range = bitVectDecodeRange(current_src_states.idx, + current_src_states.val); + for (auto it_s = state_range.begin(); (bool) it_s; ++it_s) + // Loop over all edges + for (const auto& [plystcond, incond] : it_cc->second.second) + { + const auto& [acolor, plyst] = playbdd2st[plystcond]; + split->new_edge(*it_s, plyst, incond, acolor); + } + } + else + { + int rel_lvl = clvl - srcStIdx; + auto metaf = [rel_lvl](int pol) + { + return std::array{rel_lvl, pol}; + }; + abstract_put(stack_states, ccond, metaf); + } + + }; + + stack_states.emplace_back(ctask::VISIT, sym_aut); + abstract_traverse(stack_states, fputSrcSt, fpopSrcSt, fvisitSrcSt); + + // Free the pairs + bdd_freepair(replace_dstSt_srcSt); + } + else + { + // If a completion is demanded we might have to create sinks + // Sink controlled by player + unsigned sink_con = -1u; + auto get_sink_con_state = [&split, &sink_con, &sink_env, + um = unsat_mark, hu = has_unsat] + (bool create = true) + { + assert(hu); + if (SPOT_UNLIKELY((sink_con == -1u) && create)) + { + sink_con = split->new_state(); + sink_env = split->new_state(); + split->new_edge(sink_con, sink_env, bddtrue, um); + split->new_edge(sink_env, sink_con, bddtrue, um); + } + return sink_con; + }; + + // envstate -> edge number for current state + auto s_edge_dict = std::unordered_map(); + + for (unsigned s = 0; s < N; ++s) + { + s_edge_dict.clear(); // "Local" dict, outgoing for this state + + // Encode the edge as new bdd over (input, state, color, out) vars + bdd enc_out_s = bddfalse; + for (const auto &e: aut->out(s)) + enc_out_s |= encode_edge(e); // Switch to new ins and outs + + // Can only be false if there is no outgoing edge + // In this case: Nothing to do + assert(enc_out_s != bddfalse + || (!(aut->out(s).begin()))); + + if (enc_out_s == bddfalse) + { + std::cerr << "Dead end state: " << s << '\n'; +#ifndef NDEBUG + print_hoa(std::cerr, aut); +#endif + continue; + } + + // traverse the ins to do the actual split + assert(stack_inputs.empty()); + stack_inputs.emplace_back(ctask::VISIT, enc_out_s); + current_in = bddtrue; + + bdd all_in = bddfalse; // Only needed for completion + + auto fvisitInTravS + = [&](const bdd& ccond) -> void + { + int clvl = bdd_var(ccond); + if (clvl >= dstStIdx) // States come after input + { + // We have found a new in cube + // Add to the existing ones if necessary + // Translate to old variables + auto [itc, insc] + = bkwd_in_repl.try_emplace(current_in, bddfalse); + if (insc) + itc->second = bdd_replace(current_in, replace_in_bkwd); + const bdd& current_in_old = itc->second; + + if (complete_env) + all_in |= current_in_old; + // treat it + auto [it_s, ins_s] + = playbdd2st.try_emplace( + ccond, + std::make_pair(acc_cond::mark_t{}, + -1u)); + if (ins_s) + // A new player state and the corresponding least + // accepting color + it_s->second = construct_ply_state(ccond); + + // Add the condition + auto [it_e, ins_e] + = s_edge_dict.try_emplace(it_s->second.second, -1u); + if (ins_e) // Create a new edge + it_e->second + = split->new_edge(s, it_s->second.second, + current_in_old, + it_s->second.first); + else // Disjunction over input + split->edge_storage(it_e->second).cond + |= current_in_old; + } + else + { + auto metaf = [&bddopts = invar2bdd[clvl - inIdx]](int pol) + { + return bddopts[pol]; + }; + abstract_put(stack_inputs, ccond, metaf); + } + }; + + // Traverse all the ins + abstract_traverse(stack_inputs, fputInTrav, + fpopInTrav, fvisitInTravS); + + // Complete if necessary + if (complete_env && (all_in != bddtrue)) + split->new_edge(s, get_sink_con_state(), bddtrue - all_in); + + } // Current state is now split + } // Else + + split->prop_universal(trival::maybe()); + + // The named property + // compute the owners + // env is equal to false + auto owner = std::vector(split->num_states(), false); + // All "new" states belong to the player + std::fill(owner.begin()+aut->num_states(), owner.end(), true); + // Check if sinks have been created + if (sink_env != -1u) + owner.at(sink_env) = false; + + // !use_color -> all words accepted + // complete_env && sink_env == -1u + // complet. for env demanded but already + // satisfied -> split is also all true + if (complete_env && sink_env == -1u && !use_color) + split->acc() = acc_cond::acc_code::t(); + + set_state_players(split, std::move(owner)); + + // release the variables + // Release the pairs + for (auto pair_ptr : {replace_fwd, + replace_bkwd, + replace_in_fwd, + replace_in_bkwd, + replace_out_fwd, + replace_out_bkwd}) + bdd_freepair(pair_ptr); + aut->get_dict()->unregister_all_my_variables(&N); + + // Done + return split; + } // New split impl + + twa_graph_ptr + split_2step_(const const_twa_graph_ptr& aut, + const bdd& output_bdd, bool complete_env, + synthesis_info::splittype sp + = synthesis_info::splittype::AUTO) + { + // Heuristic for AUTO goes here + // For the moment semisym is almost always best except if there are + // really few inputs + unsigned nIns = aut->ap().size() - bdd_nodecount(output_bdd); + sp = sp == synthesis_info::splittype::AUTO ? + (nIns < 4 ? synthesis_info::splittype::EXPL + : synthesis_info::splittype::SEMISYM) + : sp; + + switch (sp) + { + case (synthesis_info::splittype::EXPL): + return split_2step_expl_impl(aut, output_bdd, complete_env); + case (synthesis_info::splittype::SEMISYM): + return split_2step_sym_impl(aut, output_bdd, complete_env); + case (synthesis_info::splittype::FULLYSYM): + return split_2step_sym_impl(aut, output_bdd, complete_env); + default: + throw std::runtime_error("split_2step_(): " + "Expected explicit splittype."); + } + } + + } // End anonymous + + + twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, + const bdd& output_bdd, bool complete_env, + synthesis_info::splittype sp) + { + return split_2step_(aut, output_bdd, complete_env, sp); } twa_graph_ptr - split_2step(const const_twa_graph_ptr& aut, bool complete_env) + split_2step(const const_twa_graph_ptr& aut, bool complete_env, + synthesis_info::splittype sp) { - return split_2step(aut, - get_synthesis_outputs(aut), - complete_env); + return split_2step_(aut, + get_synthesis_outputs(aut), + complete_env, sp); + } + + twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, + synthesis_info& gi) + { + return split_2step_(aut, + get_synthesis_outputs(aut), + true, + gi.sp); } twa_graph_ptr @@ -906,6 +1861,12 @@ namespace spot twa_graph_ptr dpa = nullptr; + auto set_split = [&outs, &gi](auto& g) + { + set_synthesis_outputs(g, outs); + return split_2step(g, gi); + }; + switch (gi.s) { case algo::DET_SPLIT: @@ -927,7 +1888,8 @@ namespace spot << bv->paritize_time << " seconds\n"; if (bv) sw.start(); - dpa = split_2step(tmp, outs, true); + + dpa = set_split(tmp); if (bv) bv->split_time += sw.stop(); if (vs) @@ -949,7 +1911,7 @@ namespace spot << " states\n"; if (bv) sw.start(); - dpa = split_2step(aut, outs, true); + dpa = set_split(aut); if (bv) bv->split_time += sw.stop(); if (vs) @@ -961,7 +1923,7 @@ namespace spot case algo::SPLIT_DET: { sw.start(); - auto split = split_2step(aut, outs, true); + auto split = set_split(aut); if (bv) bv->split_time += sw.stop(); if (vs) @@ -1020,7 +1982,7 @@ namespace spot if (bv) sw.start(); - dpa = split_2step(dpa, outs, true); + dpa = set_split(dpa); if (bv) bv->split_time += sw.stop(); if (vs) @@ -1250,7 +2212,8 @@ namespace spot }; auto ret_sol_exists = - [&vs, &want_strategy, &tmp, &dict](twa_graph_ptr strat) + [&vs, &want_strategy, &tmp, &dict, &output_aps] + (twa_graph_ptr strat) { dict->unregister_all_my_variables(&tmp); if (vs) @@ -1265,7 +2228,17 @@ namespace spot } } if (strat) - strat->merge_edges(); + { + strat->merge_edges(); + bdd outputs = bddtrue; + std::for_each( + output_aps.begin(), + output_aps.end(), + [&strat, &outputs](const std::string& ap) -> void + { outputs &= bdd_ithvar(strat->register_ap(ap)); }); + + set_synthesis_outputs(strat, outputs); + } return mealy_like{ mealy_like::realizability_code::REALIZABLE_REGULAR, strat, @@ -1544,7 +2517,8 @@ namespace // anonymous for subsformula todo.pop(); formula current_form = assumptions[current_index]; done[current_index] = true; - auto [ins_current, outs_current] = form2props.aps_of(current_form); + auto [ins_current, outs_current] + = form2props.aps_of(current_form); result.first.insert(ins_current.begin(), ins_current.end()); result.second.insert(outs_current.begin(), outs_current.end()); for (unsigned i = 0; i < ass_size; ++i) @@ -1552,7 +2526,8 @@ namespace // anonymous for subsformula if (done[i]) continue; auto other_form = assumptions[i]; - auto [ins_other, outs_other] = form2props.aps_of(other_form); + auto [ins_other, outs_other] + = form2props.aps_of(other_form); if (are_intersecting(ins_current, ins_other) || are_intersecting(outs_other, outs_other)) todo.push(i); @@ -1587,7 +2562,8 @@ namespace // anonymous for subsformula // We merge two assumpt or guar. that share a proposition from decRelProps std::vector assumptions_split, guarantees_split; - auto fus = [&](std::vector &forms, std::vector &res) + auto fus = [&](std::vector &forms, + std::vector &res) { std::stack todo; todo.emplace(0); diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index 3d25441e9..2c5bdff1b 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -25,6 +25,71 @@ namespace spot { + + /// \ingroup synthesis + /// \brief Benchmarking data and options for synthesis + struct SPOT_API synthesis_info + { + enum class algo + { + DET_SPLIT=0, + SPLIT_DET, + DPA_SPLIT, + LAR, + LAR_OLD, + ACD, + }; + + enum class splittype + { + AUTO=0, // Uses a heuristic to choose + EXPL, // Explicit enumerations of inputs + SEMISYM, // Works on one bdd per env state + FULLYSYM // Works on a fully symbolic version of the automaton + }; + + struct bench_var + { + double total_time = 0.0; + double trans_time = 0.0; + double split_time = 0.0; + double paritize_time = 0.0; + double solve_time = 0.0; + double strat2aut_time = 0.0; + double simplify_strat_time = 0.0; + double aig_time = 0.0; + unsigned nb_states_arena = 0; + unsigned nb_states_arena_env = 0; + unsigned nb_strat_states = 0; + unsigned nb_strat_edges = 0; + unsigned nb_simpl_strat_states = 0; + unsigned nb_simpl_strat_edges = 0; + unsigned nb_latches = 0; + unsigned nb_gates = 0; + bool realizable = false; + }; + + synthesis_info() + : force_sbacc{false}, + s{algo::LAR}, + minimize_lvl{2}, + sp{splittype::AUTO}, + bv{}, + verbose_stream{nullptr}, + dict(make_bdd_dict()) + { + } + + bool force_sbacc; + algo s; + int minimize_lvl; + splittype sp; + std::optional bv; + std::ostream* verbose_stream; + option_map opt; + bdd_dict_ptr dict; + }; + /// \addtogroup synthesis Reactive Synthesis /// \ingroup twa_algorithms @@ -51,18 +116,33 @@ namespace spot /// are treated as inputs /// \param complete_env Whether the automaton should be complete for the /// environment, i.e. the player of inputs + /// \param sp Defines which splitting algo to use /// \note This function also computes the state players /// \note If the automaton is to be completed, sink states will /// be added for both env and player if necessary SPOT_API twa_graph_ptr split_2step(const const_twa_graph_ptr& aut, - const bdd& output_bdd, bool complete_env = true); + const bdd& output_bdd, bool complete_env = true, + synthesis_info::splittype sp + = synthesis_info::splittype::AUTO); /// \ingroup synthesis /// \brief Like split_2step but relying on the named property /// 'synthesis-outputs' SPOT_API twa_graph_ptr - split_2step(const const_twa_graph_ptr& aut, bool complete_env = true); + split_2step(const const_twa_graph_ptr& aut, bool complete_env = true, + synthesis_info::splittype sp + = synthesis_info::splittype::AUTO); + + /// \ingroup synthesis + /// \brief Like split_2step but allows to fine-tune the splitting + /// via the options set in \a gi, always completes the + /// environment states and relies on the named property to + /// extract the output proposition + SPOT_API twa_graph_ptr + split_2step(const const_twa_graph_ptr& aut, + synthesis_info& gi); + /// \ingroup synthesis /// \brief the inverse of split_2step @@ -75,60 +155,6 @@ namespace spot SPOT_API twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut); - /// \ingroup synthesis - /// \brief Benchmarking data and options for synthesis - struct SPOT_API synthesis_info - { - enum class algo - { - DET_SPLIT=0, - SPLIT_DET, - DPA_SPLIT, - LAR, - LAR_OLD, - ACD, - }; - - struct bench_var - { - double total_time = 0.0; - double trans_time = 0.0; - double split_time = 0.0; - double paritize_time = 0.0; - double solve_time = 0.0; - double strat2aut_time = 0.0; - double simplify_strat_time = 0.0; - double aig_time = 0.0; - unsigned nb_states_arena = 0; - unsigned nb_states_arena_env = 0; - unsigned nb_strat_states = 0; - unsigned nb_strat_edges = 0; - unsigned nb_simpl_strat_states = 0; - unsigned nb_simpl_strat_edges = 0; - unsigned nb_latches = 0; - unsigned nb_gates = 0; - bool realizable = false; - }; - - synthesis_info() - : force_sbacc{false}, - s{algo::LAR}, - minimize_lvl{2}, - bv{}, - verbose_stream{nullptr}, - dict(make_bdd_dict()) - { - } - - bool force_sbacc; - algo s; - int minimize_lvl; - std::optional bv; - std::ostream* verbose_stream; - option_map opt; - bdd_dict_ptr dict; - }; - /// \ingroup synthesis /// \brief Stream algo SPOT_API std::ostream& diff --git a/tests/core/gamehoa.test b/tests/core/gamehoa.test index f50602e34..6135cd438 100755 --- a/tests/core/gamehoa.test +++ b/tests/core/gamehoa.test @@ -21,11 +21,13 @@ set -x -ltlsynt --ins=a,c --outs=b -f 'GF(a <-> XXXc) <-> GFb' --print-game-hoa >out +ltlsynt --ins=a,c --outs=b -f 'GF(a <-> XXXc) <-> GFb' --print-game-hoa \ +--splittype=expl >out grep spot-state-player: out autfilt out >out2 diff out out2 -ltlsynt --ins=a,c --outs=b -f 'GF(a <-> XXXc) <-> GFb' --print-game-hoa=l >out3 +ltlsynt --ins=a,c --outs=b -f 'GF(a <-> XXXc) <-> GFb' --print-game-hoa=l \ +--splittype=expl >out3 test 1 = `wc -l < out3` cmp out out3 && exit 1 autfilt out3 >out2 diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 1e0397a5f..77f661c40 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -484,10 +484,22 @@ i3 i3 o0 o0 o1 o1 EOF -ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop+ud --algo=lar --decompose=no --simpl=no >out +ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1" \ + --aiger=isop+ud --algo=lar --decompose=no --simpl=no \ + --splittype=expl >out diff out exp +for splitt in expl semisym fullysym auto +do + res=$(ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" \ + --outs="o0,o1" --aiger=isop+ud --algo=lar --decompose=no \ + --simpl=no --splittype="$splitt" --realizability) + if [[ "$res" != "REALIZABLE" ]]; then + echo "Expected realizable" + fi +done + + cat >exp <X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop --algo=lar --decompose=no --simpl=no >out + --aiger=isop --algo=lar --decompose=no --simpl=no \ + --splittype=expl >out diff out exp @@ -590,10 +603,10 @@ o0 o0 o1 o1 EOF ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop+ud --algo=lar --decompose=yes --simpl=no >out + --aiger=isop+ud --algo=lar --decompose=yes --simpl=no --splittype=expl >out diff out exp ltlsynt -f "G((i0 && i1)<->X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ - --aiger=isop+ud --algo=lar --simpl=no >out + --aiger=isop+ud --algo=lar --simpl=no --splittype=expl >out diff out exp # Issue #477 diff --git a/tests/python/_partitioned_relabel.ipynb b/tests/python/_partitioned_relabel.ipynb index 446e18a68..a4d6a3f57 100644 --- a/tests/python/_partitioned_relabel.ipynb +++ b/tests/python/_partitioned_relabel.ipynb @@ -203,7 +203,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46fc00> >" + " *' at 0x7f0fd837fe10> >" ] }, "execution_count": 2, @@ -411,7 +411,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46fc00> >" + " *' at 0x7f0fd837fe10> >" ] }, "execution_count": 3, @@ -597,7 +597,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46fc00> >" + " *' at 0x7f0fd837fe10> >" ] }, "execution_count": 4, @@ -782,7 +782,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46dfb0> >" + " *' at 0x7f0fd8394990> >" ] }, "metadata": {}, @@ -1052,7 +1052,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46dfb0> >" + " *' at 0x7f0fd8394990> >" ] }, "execution_count": 5, @@ -1326,7 +1326,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46dfb0> >" + " *' at 0x7f0fd8394990> >" ] }, "execution_count": 6, @@ -1537,7 +1537,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46e9d0> >" + " *' at 0x7f0fd83943c0> >" ] }, "metadata": {}, @@ -1760,7 +1760,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46e9d0> >" + " *' at 0x7f0fd83943c0> >" ] }, "execution_count": 7, @@ -2023,7 +2023,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46e9d0> >" + " *' at 0x7f0fd83943c0> >" ] }, "execution_count": 8, @@ -2055,7 +2055,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 14, "id": "296a93d3", "metadata": {}, "outputs": [ @@ -2304,7 +2304,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46f4b0> >" + " *' at 0x7f0fd8395590> >" ] }, "metadata": {}, @@ -2718,7 +2718,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46eca0> >" + " *' at 0x7f0fd837fcf0> >" ] }, "metadata": {}, @@ -3312,7 +3312,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46eca0> >" + " *' at 0x7f0fd837fcf0> >" ] }, "metadata": {}, @@ -3346,7 +3346,7 @@ "display(aut)\n", "\n", "# Convert to split mealy machine\n", - "auts = spot.split_2step(aut)\n", + "auts = spot.split_2step(aut, True, spot.synthesis_info.splittype_EXPL)\n", "print(auts.to_str(\"hoa\"))\n", "display(auts)\n", "\n", @@ -3951,7 +3951,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f483c46eca0> >" + " *' at 0x7f0fd8396b20> >" ] }, "metadata": {}, @@ -4020,7 +4020,7 @@ " for relabel_player in [True, False]:\n", " for split_env in [True, False]:\n", " for split_player in [True, False]:\n", - " auts = spot.split_2step(aut)\n", + " auts = spot.split_2step(aut, True, spot.synthesis_info.splittype_EXPL)\n", " rel_dicts = spot.partitioned_game_relabel_here(auts, relabel_env, relabel_player, split_env, split_player, 10000, 10000)\n", " spot.relabel_game_here(auts, rel_dicts)\n", " print(spot.are_equivalent(aut, spot.unsplit_2step(auts)))" @@ -4051,7 +4051,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.6" } }, "nbformat": 4, diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb index 1520b0c2f..6623b5820 100644 --- a/tests/python/_synthesis.ipynb +++ b/tests/python/_synthesis.ipynb @@ -48,6 +48,7 @@ "source": [ "si = spot.synthesis_info()\n", "si.s = spot.synthesis_info.algo_LAR # Use LAR algorithm\n", + "si.sp = spot.synthesis_info.splittype_EXPL\n", "game = spot.ltl_to_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], si)\n", "spot.solve_game(game)" ] @@ -787,7 +788,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8777750> >" + " *' at 0x75e94c292280> >" ] }, "execution_count": 8, @@ -930,7 +931,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8777750> >" + " *' at 0x75e94c292280> >" ] }, "execution_count": 9, @@ -1149,7 +1150,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8777660> >" + " *' at 0x75e94c290c30> >" ] }, "execution_count": 10, @@ -1158,7 +1159,7 @@ } ], "source": [ - "a_s = spot.split_2step(a, True)\n", + "a_s = spot.split_2step(a, True, spot.synthesis_info.splittype_EXPL)\n", "print(a.acc())\n", "a_s" ] @@ -1322,7 +1323,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8774840> >" + " *' at 0x75e94c293a20> >" ] }, "execution_count": 11, @@ -1618,7 +1619,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8774930> >" + " *' at 0x75e94fe9f090> >" ] }, "execution_count": 12, @@ -1627,7 +1628,7 @@ } ], "source": [ - "a_snc = spot.split_2step(a, False)\n", + "a_snc = spot.split_2step(a, False, spot.synthesis_info.splittype_EXPL)\n", "print(a_snc.acc())\n", "a_snc" ] @@ -2006,7 +2007,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8776f10> >" + " *' at 0x75e94c292880> >" ] }, "execution_count": 13, @@ -2015,7 +2016,7 @@ } ], "source": [ - "a_s = spot.split_2step(a, True)\n", + "a_s = spot.split_2step(a, True, spot.synthesis_info.splittype_EXPL)\n", "print(a_s.acc())\n", "a_s" ] @@ -2289,7 +2290,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a9ff0db0> >" + " *' at 0x75e94c2910b0> >" ] }, "execution_count": 14, @@ -2531,7 +2532,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a9ff0db0> >" + " *' at 0x75e94c2910b0> >" ] }, "execution_count": 15, @@ -2803,7 +2804,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8775800> >" + " *' at 0x75e94c293720> >" ] }, "execution_count": 16, @@ -3046,7 +3047,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8775800> >" + " *' at 0x75e94c293720> >" ] }, "execution_count": 17, @@ -3757,7 +3758,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876e310> >" + " *' at 0x75e94c290600> >" ] }, "execution_count": 18, @@ -4015,7 +4016,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876e310> >" + " *' at 0x75e94c290600> >" ] }, "execution_count": 19, @@ -4298,7 +4299,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8776850> >" + " *' at 0x75e94c290f90> >" ] }, "metadata": {}, @@ -6066,7 +6067,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a9ff1350> >" + " *' at 0x75e94c2901b0> >" ] }, "execution_count": 20, @@ -6101,7 +6102,7 @@ "\n", "display(aut)\n", "\n", - "aut = spot.split_2step(aut, x, False)\n", + "aut = spot.split_2step(aut, x, False, spot.synthesis_info.splittype_EXPL)\n", "\n", "display(aut.show_storage())\n", "aut" @@ -6975,7 +6976,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a9ff1350> >" + " *' at 0x75e94c2901b0> >" ] }, "execution_count": 21, @@ -7219,7 +7220,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8776970> >" + " *' at 0x75e94c290ea0> >" ] }, "metadata": {}, @@ -8107,7 +8108,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8775620> >" + " *' at 0x75e94c291b60> >" ] }, "execution_count": 22, @@ -8141,7 +8142,7 @@ "\n", "display(aut)\n", "\n", - "aut = spot.split_2step(aut, x, False)\n", + "aut = spot.split_2step(aut, x, False, spot.synthesis_info.splittype_EXPL)\n", "\n", "display(aut.show_storage())\n", "aut" @@ -8529,7 +8530,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a8775620> >" + " *' at 0x75e94c291b60> >" ] }, "execution_count": 23, @@ -8679,7 +8680,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876e100> >" + " *' at 0x75e94c291ad0> >" ] }, "metadata": {}, @@ -8858,7 +8859,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876e100> >" + " *' at 0x75e94c291ad0> >" ] }, "metadata": {}, @@ -9062,7 +9063,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876f570> >" + " *' at 0x75e94c27bde0> >" ] }, "execution_count": 25, @@ -9072,6 +9073,7 @@ ], "source": [ "si = spot.synthesis_info()\n", + "si.sp = spot.synthesis_info.splittype_EXPL\n", "\n", "aut = spot.ltl_to_game(\"(a|b|c|d)->x\", [\"x\"], si)\n", "aut" @@ -9268,7 +9270,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876fae0> >" + " *' at 0x75e94c290210> >" ] }, "execution_count": 27, @@ -9582,7 +9584,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f08a876f2a0> >" + " *' at 0x75e94c292b80> >" ] }, "execution_count": 28, @@ -9594,14 +9596,6 @@ "aig = spot.mealy_machine_to_aig(ctrl, \"ite\")\n", "aig" ] - }, - { - "cell_type": "code", - "execution_count": null, - "id": "eb81b7d3", - "metadata": {}, - "outputs": [], - "source": [] } ], "metadata": { @@ -9620,7 +9614,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.7" + "version": "3.11.6" } }, "nbformat": 4, diff --git a/tests/python/game.py b/tests/python/game.py index e0d880647..3462cc7d2 100644 --- a/tests/python/game.py +++ b/tests/python/game.py @@ -282,8 +282,8 @@ spot.change_parity_here(gdpa, spot.parity_kind_max, spot.parity_style_odd) gsdpa = spot.split_2step(gdpa, b, True) spot.colorize_parity_here(gsdpa, True) tc.assertTrue(spot.solve_parity_game(gsdpa)) -tc.assertEqual(spot.highlight_strategy(gsdpa).to_str("HOA", "1.1"), -"""HOA: v1.1 +gsdpa_solved_ref = spot.automaton( + """HOA: v1.1 States: 18 Start: 0 AP: 2 "a" "b" @@ -292,7 +292,7 @@ Acceptance: 5 Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0)))) properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic spot.highlight.states: 0 4 1 4 2 4 3 4 4 4 5 4 6 4 7 4 8 4 9 4 """ -+"""10 4 11 4 12 4 13 4 14 4 15 4 16 4 17 4 + +"""10 4 11 4 12 4 13 4 14 4 15 4 16 4 17 4 spot.highlight.edges: 15 4 17 4 20 4 22 4 24 4 26 4 28 4 30 4 31 4 32 4 33 4 spot.state-player: 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 controllable-AP: 1 @@ -350,6 +350,23 @@ State: 17 [t] 4 {4} --END--""" ) +tc.assertTrue(spot.solve_parity_game(gsdpa_solved_ref)) + +# Check for the same language +tc.assertTrue(spot.are_equivalent(gsdpa, gsdpa_solved_ref)) +# Check if the winning regions are the same for env states +# Env states should by construction have the same number as before +players_new = spot.get_state_players(gsdpa) +players_ref = spot.get_state_players(gsdpa_solved_ref) +# States maybe renumbered, but remain in the same "class" +tc.assertEqual(players_new, players_ref) +# Check that env states have the same winner +winners_new = spot.get_state_winners(gsdpa) +winners_ref = spot.get_state_winners(gsdpa_solved_ref) + +tc.assertTrue(all([wn == wr for (wn, wr, p) in + zip(winners_new, winners_ref, players_ref) + if not p])) # Test the different parity conditions gdpa = spot.tgba_determinize(spot.degeneralize_tba(g), diff --git a/tests/python/split.py b/tests/python/split.py index a953b82e2..de05e070b 100644 --- a/tests/python/split.py +++ b/tests/python/split.py @@ -135,3 +135,169 @@ aut, s = do_split('((G (((! g_0) || (! g_1)) && ((r_0 && (X r_1)) -> (F (g_0 \ && g_1))))) && (G (r_0 -> F g_0))) && (G (r_1 -> F g_1))', ['g_0', 'g_1']) tc.assertTrue(equiv(aut, spot.unsplit_2step(s))) + + +# check equivalence of split automata +# for the different methods for certain cases +autstr = """HOA: v1 +name: "r2b_ack0 | F((!b2r_req0 & Xr2b_ack0) | (b2r_req0 & XG!r2b_ack0)) \ +| (!b2r_req0 & G(!r2b_ack0 | ((!b2r_req0 | !b2r_req1) & X!b2r_req0 \ +& (!(s2b_req0 | s2b_req1) | XF(b2r_req0 | b2r_req1)) & (!b2r_req0 \ +| X(b2r_req0 | (b2r_req1 M !b2r_req0))) & (!b2r_req0 | r2b_ack0 \ +| Xb2r_req0))))" +States: 12 +Start: 7 +AP: 5 "r2b_ack0" "b2r_req0" "b2r_req1" "s2b_req0" "s2b_req1" +controllable-AP: 2 1 +acc-name: parity max even 4 +Acceptance: 4 Fin(3) & (Inf(2) | (Fin(1) & Inf(0))) +properties: trans-labels explicit-labels trans-acc colored complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {2} +[0] 1 {1} +[!0&1] 3 {2} +State: 1 +[t] 1 {2} +State: 2 +[!0&1] 2 {2} +[0&1] 2 {3} +[!0&!1] 4 {2} +[0&!1] 5 {3} +State: 3 +[!0&!1] 0 {2} +[0&1&2] 2 {1} +[!0&1] 3 {2} +[0&!1&3 | 0&!1&4] 6 {2} +[0&!1&!3&!4] 7 {2} +[0&1&!2] 8 {2} +State: 4 +[0] 1 {1} +[!0&1] 2 {2} +[!0&!1] 4 {2} +State: 5 +[0] 1 {1} +[!0&1] 2 {1} +[!0&!1] 5 {1} +State: 6 +[!0&!1&2] 0 {2} +[0] 1 {1} +[!0&1] 2 {1} +[!0&!1&!2] 9 {1} +State: 7 +[!0&!1] 0 {2} +[0] 1 {1} +[!0&1] 2 {1} +State: 8 +[!0&!1&2] 0 {2} +[1] 2 {1} +[0&!1&2&3 | 0&!1&2&4] 6 {2} +[0&!1&2&!3&!4] 7 {2} +[!0&!1&!2] 10 {1} +[0&!1&!2] 11 {1} +State: 9 +[!0&!1&2] 0 {2} +[0] 1 {1} +[!0&1] 3 {2} +[!0&!1&!2] 9 {1} +State: 10 +[!0&!1&2] 0 {2} +[0] 1 {1} +[!0&1] 2 {1} +[!0&!1&!2] 10 {2} +State: 11 +[!0&!1&2] 0 {2} +[0] 1 {1} +[!0&1] 2 {1} +[!0&!1&!2] 11 {1} +--END-- +HOA: v1 +States: 2 +Start: 0 +AP: 15 "u0room29light0f1dturn2off1b" "u0room29light0f1dturn2on1b" \ + "p0b0room29window29opened" "u0room29light0f1dtoggle1b" \ + "p0b0room29window29closed" "p0p0all2windows2closed0room" \ + "u0system29start2new2timer0f1dmin25231b" \ + "u0system29start2new2timer0f1dhour241b" \ + "u0room29warnlight29control0room29warnlight29control" \ + "u0system29start2new2timer0system29start2new2timer" \ + "u0room29warnlight29control0f1dturn2on1b" \ + "u0room29warnlight29control0f1dturn2off1b" "u0room29light0room29light" \ + "u0system29start2new2timer0f1dhour251b" "p0b0timeout" +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc deterministic +controllable-AP: 0 1 3 6 7 8 9 10 11 12 13 +--BODY-- +State: 0 +[!0&!1&!3&!6&!7&!8&!9&!10&11&12&13 | !0&!1&!3&!6&!7&!8&!9&10&!11&12&13 \ +| !0&!1&!3&!6&!7&!8&9&!10&11&12&!13 | !0&!1&!3&!6&!7&!8&9&10&!11&12&!13 \ +| !0&!1&!3&!6&!7&8&!9&!10&!11&12&13 | !0&!1&!3&!6&!7&8&9&!10&!11&12&!13 \ +| !0&!1&!3&!6&7&!8&!9&!10&11&12&!13 | !0&!1&!3&!6&7&!8&!9&10&!11&12&!13 \ +| !0&!1&!3&!6&7&8&!9&!10&!11&12&!13 | !0&!1&!3&6&!7&!8&!9&!10&11&12&!13 \ +| !0&!1&!3&6&!7&!8&!9&10&!11&12&!13 | !0&!1&!3&6&!7&8&!9&!10&!11&12&!13 \ +| !0&!1&3&!6&!7&!8&!9&!10&11&!12&13 | !0&!1&3&!6&!7&!8&!9&10&!11&!12&13 \ +| !0&!1&3&!6&!7&!8&9&!10&11&!12&!13 | !0&!1&3&!6&!7&!8&9&10&!11&!12&!13 \ +| !0&!1&3&!6&!7&8&!9&!10&!11&!12&13 | !0&!1&3&!6&!7&8&9&!10&!11&!12&!13 \ +| !0&!1&3&!6&7&!8&!9&!10&11&!12&!13 | !0&!1&3&!6&7&!8&!9&10&!11&!12&!13 \ +| !0&!1&3&!6&7&8&!9&!10&!11&!12&!13 | !0&!1&3&6&!7&!8&!9&!10&11&!12&!13 \ +| !0&!1&3&6&!7&!8&!9&10&!11&!12&!13 | !0&!1&3&6&!7&8&!9&!10&!11&!12&!13 \ +| !0&1&!3&!6&!7&!8&!9&!10&11&!12&13 | !0&1&!3&!6&!7&!8&!9&10&!11&!12&13 \ +| !0&1&!3&!6&!7&!8&9&!10&11&!12&!13 | !0&1&!3&!6&!7&!8&9&10&!11&!12&!13 \ +| !0&1&!3&!6&!7&8&!9&!10&!11&!12&13 | !0&1&!3&!6&!7&8&9&!10&!11&!12&!13 \ +| !0&1&!3&!6&7&!8&!9&!10&11&!12&!13 | !0&1&!3&!6&7&!8&!9&10&!11&!12&!13 \ +| !0&1&!3&!6&7&8&!9&!10&!11&!12&!13 | !0&1&!3&6&!7&!8&!9&!10&11&!12&!13 \ +| !0&1&!3&6&!7&!8&!9&10&!11&!12&!13 | !0&1&!3&6&!7&8&!9&!10&!11&!12&!13 \ +| 0&!1&!3&!6&!7&!8&!9&!10&11&!12&13 | 0&!1&!3&!6&!7&!8&!9&10&!11&!12&13 \ +| 0&!1&!3&!6&!7&!8&9&!10&11&!12&!13 | 0&!1&!3&!6&!7&!8&9&10&!11&!12&!13 \ +| 0&!1&!3&!6&!7&8&!9&!10&!11&!12&13 | 0&!1&!3&!6&!7&8&9&!10&!11&!12&!13 \ +| 0&!1&!3&!6&7&!8&!9&!10&11&!12&!13 | 0&!1&!3&!6&7&!8&!9&10&!11&!12&!13 \ +| 0&!1&!3&!6&7&8&!9&!10&!11&!12&!13 | 0&!1&!3&6&!7&!8&!9&!10&11&!12&!13 \ +| 0&!1&!3&6&!7&!8&!9&10&!11&!12&!13 | 0&!1&!3&6&!7&8&!9&!10&!11&!12&!13] 1 +State: 1 +[!0&!1&!3&!6&!7&!8&!9&!10&11&12&13 | !0&!1&!3&!6&!7&!8&!9&10&!11&12&13 \ +| !0&!1&!3&!6&!7&!8&9&!10&11&12&!13 | !0&!1&!3&!6&!7&!8&9&10&!11&12&!13 \ +| !0&!1&!3&!6&!7&8&!9&!10&!11&12&13 | !0&!1&!3&!6&!7&8&9&!10&!11&12&!13 \ +| !0&!1&!3&!6&7&!8&!9&!10&11&12&!13 | !0&!1&!3&!6&7&!8&!9&10&!11&12&!13 \ +| !0&!1&!3&!6&7&8&!9&!10&!11&12&!13 | !0&!1&!3&6&!7&!8&!9&!10&11&12&!13 \ +| !0&!1&!3&6&!7&!8&!9&10&!11&12&!13 | !0&!1&!3&6&!7&8&!9&!10&!11&12&!13 \ +| !0&!1&3&!6&!7&!8&!9&!10&11&!12&13 | !0&!1&3&!6&!7&!8&!9&10&!11&!12&13 \ +| !0&!1&3&!6&!7&!8&9&!10&11&!12&!13 | !0&!1&3&!6&!7&!8&9&10&!11&!12&!13 \ +| !0&!1&3&!6&!7&8&!9&!10&!11&!12&13 | !0&!1&3&!6&!7&8&9&!10&!11&!12&!13 \ +| !0&!1&3&!6&7&!8&!9&!10&11&!12&!13 | !0&!1&3&!6&7&!8&!9&10&!11&!12&!13 \ +| !0&!1&3&!6&7&8&!9&!10&!11&!12&!13 | !0&!1&3&6&!7&!8&!9&!10&11&!12&!13 \ +| !0&!1&3&6&!7&!8&!9&10&!11&!12&!13 | !0&!1&3&6&!7&8&!9&!10&!11&!12&!13 \ +| !0&1&!3&!6&!7&!8&!9&!10&11&!12&13 | !0&1&!3&!6&!7&!8&!9&10&!11&!12&13 \ +| !0&1&!3&!6&!7&!8&9&!10&11&!12&!13 | !0&1&!3&!6&!7&!8&9&10&!11&!12&!13 \ +| !0&1&!3&!6&!7&8&!9&!10&!11&!12&13 | !0&1&!3&!6&!7&8&9&!10&!11&!12&!13 \ +| !0&1&!3&!6&7&!8&!9&!10&11&!12&!13 | !0&1&!3&!6&7&!8&!9&10&!11&!12&!13 \ +| !0&1&!3&!6&7&8&!9&!10&!11&!12&!13 | !0&1&!3&6&!7&!8&!9&!10&11&!12&!13 \ +| !0&1&!3&6&!7&!8&!9&10&!11&!12&!13 | !0&1&!3&6&!7&8&!9&!10&!11&!12&!13 \ +| 0&!1&!3&!6&!7&!8&!9&!10&11&!12&13 | 0&!1&!3&!6&!7&!8&!9&10&!11&!12&13 \ +| 0&!1&!3&!6&!7&!8&9&!10&11&!12&!13 | 0&!1&!3&!6&!7&!8&9&10&!11&!12&!13 \ +| 0&!1&!3&!6&!7&8&!9&!10&!11&!12&13 | 0&!1&!3&!6&!7&8&9&!10&!11&!12&!13 \ +| 0&!1&!3&!6&7&!8&!9&!10&11&!12&!13 | 0&!1&!3&!6&7&!8&!9&10&!11&!12&!13 \ +| 0&!1&!3&!6&7&8&!9&!10&!11&!12&!13 | 0&!1&!3&6&!7&!8&!9&!10&11&!12&!13 \ +| 0&!1&!3&6&!7&!8&!9&10&!11&!12&!13 | 0&!1&!3&6&!7&8&!9&!10&!11&!12&!13] 1 +--END-- +""" + +for autus in spot.automata(autstr): + si = spot.synthesis_info() + all_split = [] + for sp in [spot.synthesis_info.splittype_EXPL, + spot.synthesis_info.splittype_SEMISYM, + spot.synthesis_info.splittype_FULLYSYM, + spot.synthesis_info.splittype_AUTO + ]: + all_split.append(spot.split_2step(autus, si)) + for i in range(len(all_split)): + for j in range(i+1, len(all_split)): + tc.assertTrue(spot.are_equivalent(all_split[i], all_split[j])) + + +del autus +del si +del all_split +gcollect() diff --git a/tests/python/synthesis.py b/tests/python/synthesis.py index 991e1cbf4..0f2aa1ba1 100644 --- a/tests/python/synthesis.py +++ b/tests/python/synthesis.py @@ -29,8 +29,7 @@ for i in range(0, 2): tc.assertFalse(spot.solve_game(game)) # A game can have only inputs -game = spot.ltl_to_game("GFa", []) -tc.assertEqual(game.to_str(), """HOA: v1 +game_ref = spot.automaton("""HOA: v1 States: 3 Start: 0 AP: 1 "a" @@ -49,3 +48,10 @@ State: 1 State: 2 [t] 0 {0} --END--""") + +gi = spot.synthesis_info() +gi.dict = game_ref.get_dict() + +game = spot.ltl_to_game("GFa", [], gi) + +tc.assertTrue(spot.are_equivalent(game, game_ref))