diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index a98d0176e..efd22b9ba 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -19,12 +19,6 @@ #include -#include -#include -#include -#include -#include - #include "argmatch.h" #include "common_aoutput.hh" @@ -38,16 +32,11 @@ #include #include #include -#include -#include #include #include -#include -#include -#include +#include +#include #include -#include -#include #include enum @@ -60,30 +49,31 @@ enum OPT_PRINT_AIGER, OPT_PRINT_HOA, OPT_REAL, - OPT_VERBOSE + OPT_VERBOSE, + OPT_VERIFY }; static const argp_option options[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Input options:", 1 }, - { "ins", OPT_INPUT, "PROPS", 0, - "comma-separated list of uncontrollable (a.k.a. input) atomic" - " propositions", 0}, { "outs", OPT_OUTPUT, "PROPS", 0, "comma-separated list of controllable (a.k.a. output) atomic" " propositions", 0}, + { "ins", OPT_INPUT, "PROPS", OPTION_ARG_OPTIONAL, + "comma-separated list of controllable (a.k.a. output) atomic" + " propositions. If unspecified its the complement of \"outs\".", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { "algo", OPT_ALGO, "sd|ds|ps|lar|lar.old", 0, - "choose the algorithm for synthesis:\n" - " - sd: translate to tgba, split, then determinize (default)\n" - " - ds: translate to tgba, determinize, then split\n" - " - ps: translate to dpa, then split\n" - " - lar: translate to a deterministic automaton with arbitrary" + "choose the algorithm for synthesis:" + " \"sd\": translate to tgba, split, then determinize (default);" + " \"ds\": translate to tgba, determinize, then split;" + " \"ps\": translate to dpa, then split;" + " \"lar\": translate to a deterministic automaton with arbitrary" " acceptance condition, then use LAR to turn to parity," - " then split\n" - " - lar.old: old version of LAR, for benchmarking.\n", 0 }, + " then split;" + " \"lar.old\": old version of LAR, for benchmarking.\n", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, @@ -95,12 +85,16 @@ static const argp_option options[] = { "aiger", OPT_PRINT_AIGER, "ite|isop|both[+ud][+dc]" "[+sub0|sub1|sub2]", OPTION_ARG_OPTIONAL, "prints a winning strategy as an AIGER circuit. The first, and only " - "mandatory options defines the method to be used. ite for If-then-else " - "normal form, isop for irreducible sum of producs. Both tries both" - "encodings and keeps the smaller one. The other options further " - "refine the encoding, see aiger:::encode_bdd.", 0}, + "mandatory option defines the method to be used. \"ite\" for " + "If-then-else normal form; " + "\"isop\" for irreducible sum of producs; " + "\"both\" tries both encodings and keeps the smaller one. " + "The other options further " + "refine the encoding, see aiger:::encode_bdd.", 0}, { "verbose", OPT_VERBOSE, nullptr, 0, "verbose mode", -1 }, + { "verify", OPT_VERIFY, nullptr, 0, + "verifies the strategy or (if demanded) aiger against the spec.", -1 }, { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL, "output statistics as CSV in FILENAME or on standard output " "(if '>>' is used to request append mode, the header line is " @@ -128,33 +122,18 @@ Exit status:\n\ 1 if the input problem is not realizable\n\ 2 if any error has been reported"; -static std::vector input_aps; -static std::vector output_aps; +static std::vector all_output_aps; +static std::vector all_input_aps; static const char* opt_csv = nullptr; static bool opt_print_pg = false; static bool opt_print_hoa = false; static const char* opt_print_hoa_args = nullptr; static bool opt_real = false; +static bool opt_do_verify = false; static const char* opt_print_aiger = nullptr; -static spot::option_map extra_options; -static double trans_time = 0.0; -static double split_time = 0.0; -static double paritize_time = 0.0; -static double solve_time = 0.0; -static double strat2aut_time = 0.0; -static unsigned nb_states_dpa = 0; -static unsigned nb_states_parity_game = 0; - -enum solver -{ - DET_SPLIT, - SPLIT_DET, - DPA_SPLIT, - LAR, - LAR_OLD, -}; +static spot::game_info gi; static char const *const solver_names[] = { @@ -174,22 +153,18 @@ static char const *const solver_args[] = "lar.old", nullptr }; -static solver const solver_types[] = +static spot::game_info::solver const solver_types[] = { - DET_SPLIT, DET_SPLIT, - SPLIT_DET, SPLIT_DET, - DPA_SPLIT, DPA_SPLIT, - LAR, - LAR_OLD, + spot::game_info::solver::DET_SPLIT, spot::game_info::solver::DET_SPLIT, + spot::game_info::solver::SPLIT_DET, spot::game_info::solver::SPLIT_DET, + spot::game_info::solver::DPA_SPLIT, spot::game_info::solver::DPA_SPLIT, + spot::game_info::solver::LAR, + spot::game_info::solver::LAR_OLD, }; ARGMATCH_VERIFY(solver_args, solver_types); -static solver opt_solver = SPLIT_DET; -static bool verbose = false; - namespace { - auto str_tolower = [] (std::string s) { std::transform(s.begin(), s.end(), s.begin(), @@ -197,35 +172,15 @@ namespace return s; }; - static spot::twa_graph_ptr - to_dpa(const spot::twa_graph_ptr& split) - { - // if the input automaton is deterministic, degeneralize it to be sure to - // end up with a parity automaton - auto dpa = spot::tgba_determinize(spot::degeneralize_tba(split), - false, true, true, false); - dpa->merge_edges(); - if (opt_print_pg) - dpa = spot::sbacc(dpa); - spot::reduce_parity_here(dpa, true); - spot::change_parity_here(dpa, spot::parity_kind_max, - spot::parity_style_odd); - assert(( - [&dpa]() -> bool - { - bool max, odd; - dpa->acc().is_parity(max, odd); - return max && odd; - }())); - assert(spot::is_deterministic(dpa)); - return dpa; - } - static void - print_csv(spot::formula f, bool realizable) + print_csv(const spot::formula& f) { - if (verbose) - std::cerr << "writing CSV to " << opt_csv << '\n'; + auto& vs = gi.verbose_stream; + auto& bv = gi.bv; + if (not bv) + throw std::runtime_error("No information available for csv!"); + if (vs) + *vs << "writing CSV to " << opt_csv << '\n'; output_file outf(opt_csv); std::ostream& out = outf.ostream(); @@ -234,306 +189,350 @@ namespace // (Even if that file was empty initially.) if (!outf.append()) { - out << ("\"formula\",\"algo\",\"trans_time\"," + out << ("\"formula\",\"algo\",\"tot_time\",\"trans_time\"," "\"split_time\",\"todpa_time\""); if (!opt_print_pg && !opt_print_hoa) { out << ",\"solve_time\""; if (!opt_real) out << ",\"strat2aut_time\""; - out << ",\"realizable\""; + if (opt_print_aiger) + out << ",\"aig_time\""; + out << ",\"realizable\""; //-1: Unknown, 0: Unreal, 1: Real } - out << ",\"dpa_num_states\",\"parity_game_num_states\"" - << '\n'; + out << ",\"dpa_num_states\",\"dpa_num_states_env\"" + << ",\"strat_num_states\",\"strat_num_edges\""; + if (opt_print_aiger) + out << ",\"nb latches\",\"nb gates\""; + out << '\n'; } std::ostringstream os; os << f; spot::escape_rfc4180(out << '"', os.str()); - out << "\",\"" << solver_names[opt_solver] - << "\"," << trans_time - << ',' << split_time - << ',' << paritize_time; + out << "\",\"" << solver_names[(int) gi.s] + << "\"," << bv->total_time + << ',' << bv->trans_time + << ',' << bv->split_time + << ',' << bv->paritize_time; if (!opt_print_pg && !opt_print_hoa) { - out << ',' << solve_time; + out << ',' << bv->solve_time; if (!opt_real) - out << ',' << strat2aut_time; - out << ',' << realizable; + out << ',' << bv->strat2aut_time; + if (opt_print_aiger) + out << ',' << bv->aig_time; + out << ',' << bv->realizable; } - out << ',' << nb_states_dpa - << ',' << nb_states_parity_game - << '\n'; + out << ',' << bv->nb_states_arena + << ',' << bv->nb_states_arena_env + << ',' << bv->nb_strat_states + << ',' << bv->nb_strat_edges; + + if (opt_print_aiger) + { + out << ',' << bv->nb_latches + << ',' << bv->nb_gates; + } + out << '\n'; outf.close(opt_csv); } + int + solve_formula(const spot::formula& f, + const std::vector& input_aps, + const std::vector& output_aps) + { + spot::stopwatch sw; + if (gi.bv) + sw.start(); + + auto safe_tot_time = [&]() + { + if (gi.bv) + gi.bv->total_time = sw.stop(); + }; + + bool opt_decompose_ltl = + gi.opt.get("specification-decomposition", 0); + std::vector sub_form; + std::vector> sub_outs; + if (opt_decompose_ltl) + { + auto subs = split_independant_formulas(f, output_aps); + if (subs.first.size() > 1) + { + sub_form = subs.first; + sub_outs = subs.second; + } + } + // When trying to split the formula, we can apply transformations that + // increase its size. This is why we will use the original formula if it + // has not been cut. + if (!opt_decompose_ltl || sub_form.empty()) + { + sub_form = { f }; + sub_outs.resize(1); + std::transform(output_aps.begin(), output_aps.end(), + std::inserter(sub_outs[0], sub_outs[0].begin()), + [](const std::string& name) { + return spot::formula::ap(name); + }); + } + std::vector> sub_outs_str; + std::transform(sub_outs.begin(), sub_outs.end(), + std::back_inserter(sub_outs_str), + [](const auto& forms) + { + std::vector r; + r.reserve(forms.size()); + for (auto f : forms) + r.push_back(f.ap_name()); + return r; + }); + + assert((sub_form.size() == sub_outs.size()) + && (sub_form.size() == sub_outs_str.size())); + + const bool want_game = opt_print_pg || opt_print_hoa; + + std::vector arenas; + + auto sub_f = sub_form.begin(); + auto sub_o = sub_outs_str.begin(); + std::vector strategies; + + auto print_game = want_game ? + [](const spot::twa_graph_ptr& game)->void + { + if (opt_print_pg) + pg_print(std::cout, game); + else + spot::print_hoa(std::cout, game, opt_print_hoa_args) << '\n'; + } + : + [](const spot::twa_graph_ptr&)->void{}; + + for (; sub_f != sub_form.end(); ++sub_f, ++sub_o) + { + // If we want to print a game, + // we never use the direct approach + spot::strategy_like_t strat{0, nullptr, bddfalse}; + if (!want_game) + strat = + spot::try_create_direct_strategy(*sub_f, *sub_o, gi); + + switch (strat.success) + { + case -1: + { + std::cout << "UNREALIZABLE" << std::endl; + safe_tot_time(); + return 1; + } + case 0: + { + auto arena = spot::create_game(*sub_f, *sub_o, gi); + if (gi.bv) + { + gi.bv->nb_states_arena += arena->num_states(); + auto spptr = + arena->get_named_prop>("state-player"); + assert(spptr); + gi.bv->nb_states_arena_env += + std::count(spptr->cbegin(), spptr->cend(), false); + assert((spptr->at(arena->get_init_state_number()) == false) + && "Env needs first turn"); + } + print_game(arena); + if (!spot::solve_game(arena, gi)) + { + std::cout << "UNREALIZABLE" << std::endl; + safe_tot_time(); + return 1; + } + // Create the (partial) strategy + // only if we need it + if (!opt_real) + { + spot::strategy_like_t sl; + sl.success = 1; + sl.strat_like = spot::create_strategy(arena, gi); + sl.glob_cond = bddfalse; + strategies.push_back(sl); + } + break; + } + case 1: + { + // the direct approach yielded a strategy + // which can now be minimized + // We minimize only if we need it + assert(strat.strat_like && "Expected success but found no strat!"); + if (!opt_real) + { + spot::stopwatch sw_min; + sw_min.start(); + bool do_split = 3 <= gi.opt.get("minimization-level", 1); + if (do_split) + split_2step_fast_here(strat.strat_like, + spot::get_synthesis_outputs(strat.strat_like)); + minimize_strategy_here(strat.strat_like, gi.minimize_lvl); + if (do_split) + strat.strat_like = spot::unsplit_2step(strat.strat_like); + auto delta = sw_min.stop(); + if (gi.bv) + gi.bv->strat2aut_time += delta; + if (gi.verbose_stream) + *gi.verbose_stream << "final strategy has " + << strat.strat_like->num_states() + << " states and " + << strat.strat_like->num_edges() + << " edges\n" + << "minimization took " << delta + << " seconds\n"; + } + SPOT_FALLTHROUGH; + } + case 2: + if (!opt_real) + strategies.push_back(strat); + break; + default: + throw std::runtime_error("ltlsynt: Recieved unexpected success " + "code during strategy generation!"); + } + } + + // If we only wanted to print the game we are done + if (want_game) + { + safe_tot_time(); + return 0; + } + + std::cout << "REALIZABLE" << std::endl; + if (opt_real) + { + safe_tot_time(); + return 0; + } + // If we reach this line + // a strategy was found for each subformula + assert(strategies.size() == sub_form.size() + && "Strategies are missing"); + + spot::aig_ptr saig = nullptr; + spot::twa_graph_ptr tot_strat = nullptr; + automaton_printer printer; + spot::process_timer timer_printer_dummy; + + if (opt_print_aiger) + { + spot::stopwatch sw2; + if (gi.bv) + sw2.start(); + saig = spot::strategies_to_aig(strategies, opt_print_aiger, + input_aps, + sub_outs_str); + if (gi.bv) + { + gi.bv->aig_time = sw2.stop(); + gi.bv->nb_latches = saig->num_latches(); + gi.bv->nb_gates = saig->num_gates(); + } + if (gi.verbose_stream) + { + *gi.verbose_stream << "AIG circuit was created in " + << gi.bv->aig_time + << " and has " << saig->num_latches() + << " latches and " + << saig->num_gates() << " gates\n"; + } + spot::print_aiger(std::cout, saig) << '\n'; + } + else + { + assert(std::all_of(strategies.begin(), strategies.end(), + [](const auto& sl){return sl.success == 1; }) + && "ltlsynt: Can not handle GTBA as strategy."); + tot_strat = strategies.front().strat_like; + for (size_t i = 1; i < strategies.size(); ++i) + tot_strat = spot::product(tot_strat, strategies[i].strat_like); + printer.print(tot_strat, timer_printer_dummy); + } + + // Final step: Do verification if demanded + if (!opt_do_verify) + { + safe_tot_time(); + return 0; + } + + + // TODO: different options to speed up verification?! + spot::translator trans(gi.dict, &gi.opt); + auto neg_spec = trans.run(spot::formula::Not(f)); + if (saig) + { + // Test the aiger + auto saigaut = saig->as_automaton(false); + if (neg_spec->intersects(saigaut)) + throw std::runtime_error("Aiger and negated specification " + "do intersect -> strategy not OK."); + std::cout << "c\nCircuit was verified\n"; + } + else if (tot_strat) + { + // Test the strat + if (neg_spec->intersects(tot_strat)) + throw std::runtime_error("Strategy and negated specification " + "do intersect -> strategy not OK."); + std::cout << "/*Strategy was verified*/\n"; + } + // Done + + safe_tot_time(); + return 0; + } + class ltl_processor final : public job_processor { private: - spot::translator& trans_; std::vector input_aps_; std::vector output_aps_; public: - - ltl_processor(spot::translator& trans, - std::vector input_aps_, + ltl_processor(std::vector input_aps_, std::vector output_aps_) - : trans_(trans), input_aps_(input_aps_), output_aps_(output_aps_) + : input_aps_(std::move(input_aps_)), + output_aps_(std::move(output_aps_)) { } - int solve_formula(spot::formula f) - { - spot::process_timer timer; - timer.start(); - spot::stopwatch sw; - bool want_time = verbose || opt_csv; - - switch (opt_solver) - { - case LAR: - case LAR_OLD: - trans_.set_type(spot::postprocessor::Generic); - trans_.set_pref(spot::postprocessor::Deterministic); - break; - case DPA_SPLIT: - trans_.set_type(spot::postprocessor::ParityMaxOdd); - trans_.set_pref(spot::postprocessor::Deterministic - | spot::postprocessor::Colored); - break; - case DET_SPLIT: - case SPLIT_DET: - break; - } - - if (want_time) - sw.start(); - auto aut = trans_.run(&f); - bdd all_inputs = bddtrue; - bdd all_outputs = bddtrue; - for (const auto& ap_i : input_aps_) - { - unsigned v = aut->register_ap(spot::formula::ap(ap_i)); - all_inputs &= bdd_ithvar(v); - } - for (const auto& ap_i : output_aps_) - { - unsigned v = aut->register_ap(spot::formula::ap(ap_i)); - all_outputs &= bdd_ithvar(v); - } - if (want_time) - trans_time = sw.stop(); - if (verbose) - { - std::cerr << "translating formula done in " - << trans_time << " seconds\n"; - std::cerr << "automaton has " << aut->num_states() - << " states and " << aut->num_sets() << " colors\n"; - } - - spot::twa_graph_ptr dpa = nullptr; - switch (opt_solver) - { - case DET_SPLIT: - { - if (want_time) - sw.start(); - auto tmp = to_dpa(aut); - if (verbose) - std::cerr << "determinization done\nDPA has " - << tmp->num_states() << " states, " - << tmp->num_sets() << " colors\n"; - tmp->merge_states(); - if (want_time) - paritize_time = sw.stop(); - if (verbose) - std::cerr << "simplification done\nDPA has " - << tmp->num_states() << " states\n" - << "determinization and simplification took " - << paritize_time << " seconds\n"; - if (want_time) - sw.start(); - dpa = split_2step(tmp, all_outputs, true, false); - spot::colorize_parity_here(dpa, true); - if (want_time) - split_time = sw.stop(); - if (verbose) - std::cerr << "split inputs and outputs done in " << split_time - << " seconds\nautomaton has " - << tmp->num_states() << " states\n"; - break; - } - case DPA_SPLIT: - { - if (want_time) - sw.start(); - aut->merge_states(); - if (want_time) - paritize_time = sw.stop(); - if (verbose) - std::cerr << "simplification done in " << paritize_time - << " seconds\nDPA has " << aut->num_states() - << " states\n"; - if (want_time) - sw.start(); - dpa = split_2step(aut, all_outputs, true, false); - spot::colorize_parity_here(dpa, true); - if (want_time) - split_time = sw.stop(); - if (verbose) - std::cerr << "split inputs and outputs done in " << split_time - << " seconds\nautomaton has " - << dpa->num_states() << " states\n"; - break; - } - case SPLIT_DET: - { - if (want_time) - sw.start(); - auto split = split_2step(aut, all_outputs, - true, false); - if (want_time) - split_time = sw.stop(); - if (verbose) - std::cerr << "split inputs and outputs done in " << split_time - << " seconds\nautomaton has " - << split->num_states() << " states\n"; - if (want_time) - sw.start(); - dpa = to_dpa(split); - if (verbose) - std::cerr << "determinization done\nDPA has " - << dpa->num_states() << " states, " - << dpa->num_sets() << " colors\n"; - dpa->merge_states(); - if (verbose) - std::cerr << "simplification done\nDPA has " - << dpa->num_states() << " states\n" - << "determinization and simplification took " - << paritize_time << " seconds\n"; - if (want_time) - paritize_time = sw.stop(); - // The named property "state-player" is set in split_2step - // but not propagated by to_dpa - alternate_players(dpa); - break; - } - case LAR: - case LAR_OLD: - { - if (want_time) - sw.start(); - if (opt_solver == LAR) - { - dpa = spot::to_parity(aut); - // reduce_parity is called by to_parity(), - // but with colorization turned off. - spot::colorize_parity_here(dpa, true); - } - else - { - dpa = spot::to_parity_old(aut); - dpa = reduce_parity_here(dpa, true); - } - spot::change_parity_here(dpa, spot::parity_kind_max, - spot::parity_style_odd); - if (want_time) - paritize_time = sw.stop(); - if (verbose) - std::cerr << "LAR construction done in " << paritize_time - << " seconds\nDPA has " - << dpa->num_states() << " states, " - << dpa->num_sets() << " colors\n"; - - if (want_time) - sw.start(); - dpa = split_2step(dpa, all_outputs, true, false); - spot::colorize_parity_here(dpa, true); - if (want_time) - split_time = sw.stop(); - if (verbose) - std::cerr << "split inputs and outputs done in " << split_time - << " seconds\nautomaton has " - << dpa->num_states() << " states\n"; - break; - } - } - nb_states_dpa = dpa->num_states(); - - if (opt_print_pg) - { - timer.stop(); - pg_print(std::cout, dpa); - return 0; - } - if (opt_print_hoa) - { - timer.stop(); - spot::print_hoa(std::cout, dpa, opt_print_hoa_args) << '\n'; - return 0; - } - set_synthesis_outputs(dpa, all_outputs); - if (want_time) - sw.start(); - bool player1winning = solve_parity_game(dpa); - if (want_time) - solve_time = sw.stop(); - if (verbose) - std::cerr << "parity game solved in " << solve_time << " seconds\n"; - nb_states_parity_game = dpa->num_states(); - timer.stop(); - if (player1winning) - { - std::cout << "REALIZABLE\n"; - if (!opt_real) - { - if (want_time) - sw.start(); - auto strat_aut = apply_strategy(dpa, true, false); - if (want_time) - strat2aut_time = sw.stop(); - - // output the winning strategy - if (opt_print_aiger) - spot::print_aiger(std::cout, strat_aut, opt_print_aiger); - else - { - automaton_printer printer; - printer.print(strat_aut, timer); - } - } - return 0; - } - else - { - std::cout << "UNREALIZABLE\n"; - return 1; - } - } - int process_formula(spot::formula f, const char*, int) override { - unsigned res = solve_formula(f); + int res = solve_formula(f, input_aps_, output_aps_); if (opt_csv) - print_csv(f, res == 0); + print_csv(f); return res; } - }; } -static int -parse_opt(int key, char* arg, struct argp_state*) + static int + parse_opt(int key, char *arg, struct argp_state *) { // Called from C code, so should not raise any exception. BEGIN_EXCEPTION_PROTECT; switch (key) { case OPT_ALGO: - opt_solver = XARGMATCH("--algo", arg, solver_args, solver_types); + gi.s = XARGMATCH("--algo", arg, solver_args, solver_types); break; case OPT_CSV: opt_csv = arg ? arg : "-"; + if (not gi.bv) + gi.bv = spot::game_info::bench_var(); break; case OPT_INPUT: { @@ -542,7 +541,7 @@ parse_opt(int key, char* arg, struct argp_state*) while (std::getline(aps, ap, ',')) { ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); - input_aps.push_back(str_tolower(ap)); + all_input_aps.push_back(str_tolower(ap)); } break; } @@ -553,31 +552,39 @@ parse_opt(int key, char* arg, struct argp_state*) while (std::getline(aps, ap, ',')) { ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end()); - output_aps.push_back(str_tolower(ap)); + all_output_aps.push_back(str_tolower(ap)); } break; } case OPT_PRINT: opt_print_pg = true; + gi.force_sbacc = true; break; case OPT_PRINT_HOA: opt_print_hoa = true; opt_print_hoa_args = arg; break; case OPT_PRINT_AIGER: - opt_print_aiger = arg ? arg : "isop"; + opt_print_aiger = arg ? arg : "INF"; break; case OPT_REAL: opt_real = true; break; case OPT_VERBOSE: - verbose = true; + gi.verbose_stream = &std::cerr; + if (not gi.bv) + gi.bv = spot::game_info::bench_var(); + break; + case OPT_VERIFY: + opt_do_verify = true; break; case 'x': { - const char* opt = extra_options.parse_options(arg); + const char* opt = gi.opt.parse_options(arg); if (opt) error(2, 0, "failed to parse --options near '%s'", opt); + // Dispatch the options to the gi structure + gi.minimize_lvl = gi.opt.get("minimization-level", 1); } break; } @@ -589,24 +596,31 @@ int main(int argc, char **argv) { return protected_main(argv, [&] { - extra_options.set("simul", 0); // no simulation, except... - extra_options.set("dpa-simul", 1); // ... after determinization - extra_options.set("tls-impl", 1); // no automata-based implication check - extra_options.set("wdba-minimize", 2); // minimize only syntactic oblig + //gi.opt.set("simul", 0); // no simulation, except... + //gi.opt.set("dpa-simul", 1); // ... after determinization + gi.opt.set("tls-impl", 1); // no automata-based implication check + gi.opt.set("wdba-minimize", 2); // minimize only syntactic oblig const argp ap = { options, parse_opt, nullptr, argp_program_doc, children, nullptr, nullptr }; if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr)) exit(err); check_no_formula(); - // Setup the dictionary now, so that BuDDy's initialization is - // not measured in our timings. - spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - spot::translator trans(dict, &extra_options); - ltl_processor processor(trans, input_aps, output_aps); + // Check if inputs and outputs are distinct + // Inputs can be empty, outputs not + if (not all_input_aps.empty()) + { + for (const auto& ai : all_input_aps) + if (std::count(all_output_aps.begin(), all_output_aps.end(), ai)) + throw std::runtime_error("ltlsynt(): " + ai + + " appears in the input AND output APs."); + } + ltl_processor processor(all_input_aps, all_output_aps); + + auto res = processor.run(); // Diagnose unused -x options - extra_options.report_unused_options(); - return processor.run(); + gi.opt.report_unused_options(); + return res; }); } diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 17cfbc5da..efd0a13fc 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -34,7 +34,7 @@ #include #include #include -#include +#include #define STR(x) #x #define STR_(x) STR(x) @@ -1893,7 +1893,47 @@ namespace spot return auts_to_aiger(new_vec, mode); } - std::ostream & + aig_ptr + strategies_to_aig(const std::vector& strat_vec, + const char *mode, + const std::vector& ins, + const std::vector>& outs) + { + // todo extend to TGBA and possibly others + const unsigned ns = strat_vec.size(); + std::vector strategies; + strategies.reserve(ns); + std::vector> outs_used; + outs_used.reserve(ns); + + for (unsigned i = 0; i < ns; ++i) + { + switch (strat_vec[i].success) + { + case -1: + throw std::runtime_error("strategies_to_aig(): Partial strat is " + "not feasible!"); + case 0: + throw std::runtime_error("strategies_to_aig(): Partial strat has " + "unknown status!"); + case 1: + { + strategies.push_back(strat_vec[i].strat_like); + outs_used.push_back(outs[i]); + break; + } + case 2: + throw std::runtime_error("strategies_to_aig(): TGBA not " + "yet supported."); + default: + throw std::runtime_error("strategies_to_aig(): Unknown " + "success identifier."); + } + } + return strategies_to_aig(strategies, mode, ins, outs_used); + } + + std::ostream & print_aiger(std::ostream &os, const_aig_ptr circuit) { if (not circuit) diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 876dd4c50..4f09f12a0 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -35,6 +35,9 @@ namespace spot { + // Forward for synthesis + struct strategy_like_t; + class aig; typedef std::shared_ptr aig_ptr; @@ -453,6 +456,13 @@ namespace spot const std::vector& ins, const std::vector>& outs); + /// \brief Like above, but works on strategy_like elements + SPOT_API aig_ptr + strategies_to_aig(const std::vector& strat_vec, + const char* mode, + const std::vector& ins, + const std::vector>& outs); + /// \brief Print the aig to stream in AIGER format SPOT_API std::ostream& print_aiger(std::ostream& os, const_aig_ptr circuit); diff --git a/spot/twaalgos/game.hh b/spot/twaalgos/game.hh index b6f9c4742..63d46762f 100644 --- a/spot/twaalgos/game.hh +++ b/spot/twaalgos/game.hh @@ -24,6 +24,7 @@ #include #include #include +#include #include #include @@ -92,10 +93,9 @@ namespace spot /// \brief Benchmarking and options structure for games and synthesis /// /// \note This structure is designed to interface with the algorithms - /// found in spot/twaalgos/synthesis.hh + /// found in spot/twaalgos/synthesis.hh and spot/twaalgos/game.hh struct SPOT_API game_info { - enum class solver { DET_SPLIT=0, @@ -116,7 +116,6 @@ namespace spot double aig_time = 0.0; unsigned nb_states_arena = 0; unsigned nb_states_arena_env = 0; - unsigned nb_states_parity_game = 0; unsigned nb_strat_states = 0; unsigned nb_strat_edges = 0; unsigned nb_latches = 0; @@ -128,7 +127,6 @@ namespace spot : force_sbacc{false}, s{solver::LAR}, minimize_lvl{0}, - out_choice{0}, bv{}, verbose_stream{nullptr}, dict(make_bdd_dict()) @@ -138,7 +136,6 @@ namespace spot bool force_sbacc; solver s; int minimize_lvl; - int out_choice; std::optional bv; std::ostream* verbose_stream; option_map opt; diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 9f78d5426..a056dfe6d 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -3456,6 +3456,16 @@ namespace spot if (!mm->acc().is_t()) throw std::runtime_error("Mealy machine needs true acceptance!\n"); + auto orig_spref = get_state_players(mm); + if (orig_spref.size() != mm->num_states()) + throw std::runtime_error("Inconsistent \"state-player\""); + + if (std::any_of(mm->edges().begin(), mm->edges().end(), + [&](const auto& e){return orig_spref[e.src] + == orig_spref[e.dst]; })) + throw std::runtime_error("Arena is not alternating!"); + + // Check if finite traces exist // If so, deactivate fast minimization // todo : this is overly conservative @@ -3479,10 +3489,7 @@ namespace spot if (premin == -1) return mm; else - { - auto mm_res = minimize_mealy_fast(mm, premin == 1); - return mm_res; - } + return minimize_mealy_fast(mm, premin == 1); }; const_twa_graph_ptr mmw = do_premin(); @@ -3490,11 +3497,7 @@ namespace spot // 0 -> "Env" next is input props // 1 -> "Player" next is output prop - auto spptr = - mmw->get_named_prop>("state-player"); - if (!spptr) - throw std::runtime_error("\"state-player\" must be defined!"); - const auto& spref = *spptr; + const auto& spref = get_state_players(mmw); assert((spref.size() == mmw->num_states()) && "Inconsistent state players"); diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index a7558eb9e..6392b537e 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -193,14 +193,18 @@ namespace spot // If a completion is demanded we might have to create sinks // Sink controlled by player - auto get_sink_con_state = [&split, um = unsat_mark](bool create = true) + unsigned sink_con = -1u; + unsigned sink_env = -1u; + auto get_sink_con_state = [&split, &sink_con, &sink_env, + um = unsat_mark] + (bool create = true) { - static unsigned sink_con=-1u; if (SPOT_UNLIKELY((sink_con == -1u) && create)) { - sink_con = split->new_states(2); - split->new_edge(sink_con, sink_con+1, bddtrue, um); - split->new_edge(sink_con+1, sink_con, bddtrue, um); + 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; }; @@ -331,14 +335,95 @@ namespace spot // All "new" states belong to the player std::fill(owner->begin()+aut->num_states(), owner->end(), true); // Check if sinks have been created - if (get_sink_con_state(false) != -1u) - owner->at(get_sink_con_state(false)) = false; + if (sink_env != -1u) + owner->at(sink_env) = false; split->set_named_prop("state-player", owner); // Done return split; } + void + split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd) + { + struct dst_cond_color_t + { + std::pair dst_cond; + acc_cond::mark_t color; + }; + + auto hasher = [](const dst_cond_color_t& dcc) noexcept + { + return dcc.color.hash() ^ pair_hash()(dcc.dst_cond); + }; + auto equal = [](const dst_cond_color_t& dcc1, + const dst_cond_color_t& dcc2) noexcept + { + return (dcc1.dst_cond == dcc2.dst_cond) + && (dcc1.color == dcc2.color); + }; + + std::unordered_map player_map(aut->num_edges(), + hasher, equal); + + auto get_ps = [&](unsigned dst, const bdd& ocond, + acc_cond::mark_t color) + { + dst_cond_color_t key{std::make_pair(dst, ocond.id()), + color}; + auto [it, inserted] = + player_map.try_emplace(key, aut->num_states() + 1); + if (!inserted) + return it->second; + unsigned ns = aut->new_state(); + assert(ns == it->second); + aut->new_edge(ns, dst, ocond, color); + return ns; + }; + + std::vector to_treat(aut->num_edges()); + std::transform(aut->edges().begin(), aut->edges().end(), + to_treat.begin(), [&](const auto& e) + { return aut->edge_number(e); }); + + std::for_each(to_treat.begin(), to_treat.end(), + [&](unsigned eidx) + { + const auto& e = aut->edge_storage(eidx); + bdd incond = bdd_exist(e.cond, output_bdd); + bdd outcond = bdd_existcomp(e.cond, output_bdd); + assert(((incond&outcond) == e.cond) + && "Precondition violated"); + // Modify + // Create new state and trans + unsigned new_dst = get_ps(e.dst, outcond, e.acc); + // redirect + aut->edge_storage(eidx).dst = new_dst; + aut->edge_storage(eidx).cond = incond; + }); + + auto* sp_ptr = + aut->get_or_set_named_prop>("state-player"); + + sp_ptr->resize(aut->num_states()); + std::fill(sp_ptr->begin(), sp_ptr->end(), false); + for (auto& eit : player_map) + (*sp_ptr)[eit.second] = true; + //Done + } + + twa_graph_ptr + split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd) + { + auto aut2 = make_twa_graph(aut, twa::prop_set::all()); + aut2->copy_acceptance_of(aut); + aut2->set_named_prop("synthesis-output", new bdd(output_bdd)); + split_2step_fast_here(aut2, output_bdd); + return aut2; + } + twa_graph_ptr unsplit_2step(const const_twa_graph_ptr& aut) { @@ -423,9 +508,13 @@ namespace spot assert((sp[arena->get_init_state_number()] == false) && "Env needs to have first turn!"); - assert(std::all_of(arena->edges().begin(), arena->edges().end(), + assert(std::none_of(arena->edges().begin(), arena->edges().end(), [&sp](const auto& e) - { return sp.at(e.src) != sp.at(e.dst); })); + { bool same_player = sp.at(e.src) == sp.at(e.dst); + if (same_player) + std::cerr << e.src << " and " << e.dst << " belong to same " + << "player, arena not alternating!\n"; + return same_player; })); auto strat_split = spot::make_twa_graph(arena->get_dict()); strat_split->copy_ap_of(arena); @@ -445,7 +534,7 @@ namespace spot size_t operator()(const dca& d) const noexcept { return pair_hash()(std::make_pair(d.dst, d.condvar)) - ^ d.acc.hash(); + ^ wang32_hash(d.acc.hash()); } }; struct dca_equal @@ -453,7 +542,7 @@ namespace spot bool operator()(const dca& d1, const dca& d2) const noexcept { return std::tie(d1.dst, d1.condvar, d1.acc) - == std::tie(d2.dst, d2.condvar, d2.acc); + == std::tie(d2.dst, d2.condvar, d2.acc); } }; @@ -482,16 +571,16 @@ namespace spot // Check if there exists already a local player state // that has the same dst, cond and (if keep_acc is true) acc auto get_spl = [&](unsigned dst, const bdd& cond, acc_cond::mark_t acc) - { - dca d{dst, (unsigned) cond.id(), acc}; - auto it = p_map.find(d); - if (it != p_map.end()) - return it->second; - unsigned ns = strat_split->new_state(); - p_map[d] = ns; - strat_split->new_edge(ns, dst, cond, acc); - return ns; - }; + { + dca d{dst, (unsigned) cond.id(), acc}; + auto it = p_map.find(d); + if (it != p_map.end()) + return it->second; + unsigned ns = strat_split->new_state(); + p_map[d] = ns; + strat_split->new_edge(ns, dst, cond, acc); + return ns; + }; while (!todo.empty()) { @@ -522,10 +611,10 @@ namespace spot // Sorting edges in place auto comp_edge = [](const auto& e1, const auto& e2) - { - return std::tuple(e1.dst, e1.acc, e1.cond.id()) - < std::tuple(e2.dst, e2.acc, e2.cond.id()); - }; + { + return std::tuple(e1.dst, e1.acc, e1.cond.id()) + < std::tuple(e2.dst, e2.acc, e2.cond.id()); + }; auto sort_edges_of = [&, &split_graph = strat_split->get_graph()](unsigned s) { @@ -597,8 +686,6 @@ namespace spot }); }; -// print_hoa(std::cout, strat_split) << '\n'; - const unsigned n_sstrat = strat_split->num_states(); std::vector remap(n_sstrat, -1u); bool changed_any; @@ -633,10 +720,6 @@ namespace spot } } -// std::for_each(remap.begin(), remap.end(), -// [](auto e){std::cout << e << ' ';}); -// std::cout << std::endl; - if (!changed_any) break; // Redirect changed targets and set possibly mergeable states @@ -671,10 +754,6 @@ namespace spot } } -// std::for_each(remap.begin(), remap.end(), [](auto e) -// {std::cout << e << ' '; }); -// std::cout << std::endl; - if (!changed_any) break; // Redirect changed targets and set possibly mergeable states @@ -688,8 +767,6 @@ namespace spot } } -// print_hoa(std::cout, strat_split) << std::endl; - // Defrag and alternate if (remap[strat_split->get_init_state_number()] != -1u) strat_split->set_init_state(remap[strat_split->get_init_state_number()]); @@ -702,16 +779,7 @@ namespace spot strat_split->defrag_states(remap, st); -// unsigned n_old; -// do -// { -// n_old = strat_split->num_edges(); -// strat_split->merge_edges(); -// strat_split->merge_states(); -// } while (n_old != strat_split->num_edges()); - alternate_players(strat_split, false, false); -// print_hoa(std::cout, strat_split) << std::endl; // What we do now depends on whether we unsplit or not if (unsplit) { @@ -1164,6 +1232,34 @@ namespace spot const std::vector& output_aps, game_info &gi) { + auto vs = gi.verbose_stream; + + if (vs) + *vs << "trying to create strategy directly\n"; + + auto ret_sol_maybe = [&vs]() + { + if (vs) + *vs << "direct strategy might exist but was not found.\n"; + return strategy_like_t{0, nullptr, bddfalse}; + }; + auto ret_sol_none = [&vs]() + { + if (vs) + *vs << "no direct strategy exists.\n"; + return strategy_like_t{-1, nullptr, bddfalse}; + }; + auto ret_sol_exists = [&vs](auto strat) + { + if (vs) + { + *vs << "direct strategy was found.\n" + << "direct strat has " << strat->num_states() + << " states and " << strat->num_sets() << " colors\n"; + } + return strategy_like_t{1, strat, bddfalse}; + }; + // We need a lot of look-ups auto output_aps_set = std::set(output_aps.begin(), output_aps.end()); @@ -1174,7 +1270,7 @@ namespace spot if (is_and) { if (f.size() != 2) - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); if (f[1].is(op::G)) f = formula::And({f[1], f[0]}); f_equiv = f[1]; @@ -1188,7 +1284,7 @@ namespace spot if (!f_equiv.is(op::Equiv) || (!f_g.is_tt() && (!f_g.is(op::G) || !f_g[0].is_boolean()))) - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); // stopwatch sw; twa_graph_ptr res; @@ -1215,7 +1311,7 @@ namespace spot } // We need to have f(inputs) <-> f(outputs) if (has_right_ins || has_left_outs || !has_right_outs) - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); bool is_gf_bool_right = right.is({op::G, op::F}); bool is_fg_bool_right = right.is({op::F, op::G}); @@ -1234,7 +1330,7 @@ namespace spot { bool right_bool = right[0][0].is_boolean(); if (!right_bool) - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); auto trans = create_translator(gi); trans.set_type(postprocessor::Buchi); trans.set_pref(postprocessor::Deterministic | postprocessor::Complete); @@ -1246,12 +1342,17 @@ namespace spot sw.start(); res = trans.run(left); if (bv) - bv->trans_time = sw.stop(); + { + auto delta = sw.stop(); + bv->trans_time += delta; + if (vs) + *vs << "tanslating formula done in " << delta << " seconds\n"; + } for (auto& out : right_outs) res->register_ap(out.ap_name()); if (!is_deterministic(res)) - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); bdd form_bdd = bddtrue; if (is_and) { @@ -1262,7 +1363,7 @@ namespace spot formula_to_bdd(f_g[0], res->get_dict(), res); if (bdd_exist(form_bdd, output_bdd) != bddtrue) - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); } bdd right_bdd = formula_to_bdd(right_sub, res->get_dict(), res); bdd neg_right_bdd = bdd_not(right_bdd); @@ -1283,25 +1384,11 @@ namespace spot } // form_bdd has to be true all the time. So we cannot only do it // between SCCs. - e.cond &= form_bdd; - if (e.cond == bddfalse) - return {-1, nullptr, bddfalse}; + if (!bdd_have_common_assignment(e.cond, form_bdd)) + return ret_sol_none(); e.acc = {}; } - if (bv) - { - auto& vs = gi.verbose_stream; - if (vs) - { - *vs << "translating formula into strategy done in " - << bv->trans_time << " seconds\n"; - *vs << "automaton has " << res->num_states() - << " states and " << res->num_sets() << " colors\n"; - } - } - - bdd output_bdd = bddtrue; for (auto &out : output_aps_set) output_bdd &= bdd_ithvar(res->register_ap(out)); @@ -1310,9 +1397,9 @@ namespace spot res->set_acceptance(acc_cond::acc_code::t()); res->prop_complete(trival::maybe()); - return {1, res, bddfalse}; + return ret_sol_exists(res); } - return {0, nullptr, bddfalse}; + return ret_sol_maybe(); } } // spot diff --git a/spot/twaalgos/synthesis.hh b/spot/twaalgos/synthesis.hh index c6e3316ed..e96f9331d 100644 --- a/spot/twaalgos/synthesis.hh +++ b/spot/twaalgos/synthesis.hh @@ -25,7 +25,7 @@ namespace spot { - /// \brief make each transition (conditionally, see do__simpify) + /// \brief make each transition (conditionally, see do_simplify) /// a 2-step transition /// /// Given a set of atomic propositions I, split each transition @@ -56,6 +56,22 @@ namespace spot split_2step(const const_twa_graph_ptr& aut, const bdd& output_bdd, bool complete_env, bool do_simplify); + + /// \brief make each transition a 2-step transition. + /// This algorithm is only applicable if all transitions of the + /// graph have the form p -- ins & outs --> q. + /// That is they are a conjunction of a condition over the input + /// propositions ins and a condition over the output propositions outs + /// \param aut automaton to be transformed + /// \param output_bdd conjunction of all output AP, all APs not present + /// are treated as inputs + SPOT_API void + split_2step_fast_here(const twa_graph_ptr& aut, const bdd& output_bdd); + + SPOT_API twa_graph_ptr + split_2step_fast(const const_twa_graph_ptr& aut, const bdd& output_bdd); + + /// \brief the reverse of split_2step /// /// \note: This function relies on the named property "state-player" diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 89a6b0579..3db3d1c9a 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -74,11 +74,9 @@ diff out exp cat >exp <exp <exp <exp <exp <exp <exp <exp < (GFb & GFc)' --aiger=isop >out +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=isop >out diff out exp cat >exp < (GFb & GFc)' --aiger=isop+dc >out +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ + --algo=ds --aiger=isop+dc >out diff out exp cat >exp < (GFb & GFc)' --aiger=ite >out +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' --algo=ds --aiger=ite >out diff out exp cat >exp < GFb' --verbose --realizability 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < GFb' --verbose --algo=ps 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp cat >exp < GFe' \ --verbose --realizability --algo=lar 2> out sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx diff outx exp +cat >exp < G(i1 <-> o0)" --outs="o0" --algo=lar \ + --verbose --realizability 2> out +sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx +diff outx exp + + for r in '' '--real'; do opts="$r --ins=a --outs=b -f" ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || : @@ -279,10 +275,10 @@ for a in sd ds lar lar.old; do test 1 = `grep -c ",.$a.," FILE` || exit 1 done -ltlsynt --algo=lar $opts 'FGa <-> GF(c&a)' --print-pg --csv >out -grep parity out -grep 'FGa.*,"lar",' out -grep formula out +# ltlsynt --algo=lar --ins=a --outs=b -f 'FGa <-> GF(c&a)' --print-pg --csv >out +# grep parity out +# grep 'FGa.*,"lar",' out +# grep formula out F0='(G ((((req) -> (X ((grant) && (X ((grant) && (X (grant))))))) && ((grant) @@ -424,9 +420,93 @@ ltlsynt --outs=p0 -f '!XXF(p0 & (p0 M Gp0))' > out diff out exp f='Fp0 U XX((p0 & F!p1) | (!p0 & Gp1))' -ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err +ltlsynt --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" -x"dpa-simul=1" 2>err grep 'DPA has 13 states' err ltlsynt -x dpa-simul=0 --verbose --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 29 states' err ltlsynt --verbose -x wdba-minimize=1 --algo=ps --outs=p1 --ins=p0 -f "$f" 2>err grep 'DPA has 12 states' err + +cat >exp <X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ + --aiger=isop --algo=lar -x"specification-decomposition=0" >out +diff out exp + +cat >exp <X(o0)) && G((i2|i3)<->X(o1))" --outs="o0,o1"\ + --aiger=isop --algo=lar -x"specification-decomposition=1" >out +diff out exp \ No newline at end of file diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index 19adaf0d6..6b44b2343 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -688,7 +688,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "game has 28 states, and 53 edges.\n", + "game has 29 states, and 55 edges.\n", "output propositions are ('o0',)\n" ] }, @@ -701,624 +701,646 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", - "[parity max odd 4]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "24\n", - "\n", - "24\n", - "\n", - "\n", - "\n", - "9->24\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", - "\n", + "\n", "9->25\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", - "\n", + "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", - "\n", + "\n", "9->26\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", - "\n", + "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", - "\n", + "\n", "9->27\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "\n", + "28\n", + "\n", + "28\n", + "\n", + "\n", + "\n", + "9->28\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "!i1\n", - "\n", - "\n", - "\n", - "\n", - "10->0\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "10->1\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", "\n", - "11->1\n", - "\n", - "\n", - "o0\n", - "\n", + "11->0\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", - "\n", + "\n", "\n", - "12->0\n", - "\n", - "\n", - "!o0\n", - "\n", + "12->1\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", - "\n", + "\n", "\n", - "13->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "13->0\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "2->16\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", - "\n", + "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", - "\n", - "\n", - "2->15\n", - "\n", - "\n", - "!i1\n", - "\n", - "\n", - "\n", + "\n", "\n", - "15->2\n", - "\n", - "\n", - "1\n", - "\n", + "14->15\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "16->2\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", + "\n", "\n", - "3->12\n", - "\n", - "\n", - "i1\n", - "\n", + "3->13\n", + "\n", + "\n", + "i1\n", + "\n", "\n", - "\n", + "\n", "\n", - "16\n", - "\n", - "16\n", + "17\n", + "\n", + "17\n", "\n", - "\n", + "\n", "\n", - "3->16\n", - "\n", - "\n", - "!i1\n", - "\n", + "3->17\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", - "\n", - "\n", - "16->2\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "17->2\n", + "\n", + "\n", + "o0\n", + "\n", "\n", - "\n", - "\n", - "16->3\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "17->3\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "i0\n", - "\n", + "\n", + "\n", + "i0\n", + "\n", "\n", - "\n", + "\n", "\n", - "17\n", - "\n", - "17\n", + "18\n", + "\n", + "18\n", "\n", - "\n", + "\n", "\n", - "4->17\n", - "\n", - "\n", - "!i0\n", - "\n", + "4->18\n", + "\n", + "\n", + "!i0\n", + "\n", "\n", - "\n", - "\n", - "17->4\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "18->4\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", - "\n", + "\n", "\n", - "5->15\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "\n", - "5->17\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "\n", - "18\n", - "\n", - "18\n", + "5->16\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", - "\n", + "\n", "5->18\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", - "\n", - "\n", - "18->5\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "19\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "5->19\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "\n", + "19->5\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "\n", - "19\n", - "\n", - "19\n", - "\n", - "\n", - "\n", - "6->19\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", - "\n", + "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", - "\n", + "\n", "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", - "\n", - "\n", - "19->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "21\n", + "\n", + "21\n", "\n", - "\n", - "\n", - "19->6\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "6->21\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "o0\n", - "\n", - "\n", - "\n", - "\n", - "7->12\n", - "\n", - "\n", - "i0 & i1\n", - "\n", - "\n", - "\n", - "\n", - "7->13\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "\n", - "21\n", - "\n", - "21\n", - "\n", - "\n", - "\n", - "7->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "\n", - "22\n", - "\n", - "22\n", - "\n", - "\n", - "\n", - "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "\n", + "7->12\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "\n", + "7->13\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "\n", + "22\n", + "\n", + "22\n", + "\n", + "\n", + "\n", + "7->22\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "\n", + "23\n", + "\n", + "23\n", + "\n", + "\n", + "\n", + "7->23\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "\n", + "23->4\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "\n", + "23->6\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", - "\n", + "\n", "\n", - "8->12\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "8->13\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", - "\n", + "\n", "\n", - "8->16\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", - "\n", - "\n", - "\n", - "8->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", - "\n", - "\n", - "\n", - "23\n", - "\n", - "23\n", + "8->17\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", - "\n", + "\n", "8->23\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", - "\n", - "\n", - "23->5\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "24\n", + "\n", + "24\n", "\n", - "\n", - "\n", - "23->8\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "8->24\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", - "\n", + "\n", "\n", - "24->0\n", - "\n", - "\n", - "1\n", - "\n", + "24->5\n", + "\n", + "\n", + "o0\n", + "\n", "\n", - "\n", + "\n", "\n", - "25->3\n", - "\n", - "\n", - "1\n", - "\n", + "24->8\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", - "\n", + "\n", "\n", - "26->6\n", - "\n", - "\n", - "1\n", - "\n", + "25->8\n", + "\n", + "\n", + "1\n", + "\n", "\n", - "\n", + "\n", "\n", - "27->8\n", - "\n", - "\n", - "1\n", - "\n", + "26->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "27->6\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "28->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "15->14\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7249801c30> >" + " *' at 0x7f7e12721720> >" ] }, "metadata": {}, @@ -1358,565 +1380,585 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", - "[parity max odd 4]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + ")))\n", + "[parity max odd 4]\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "I->9\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "24\n", - "\n", - "24\n", - "\n", - "\n", - "\n", - "9->24\n", - "\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", - "\n", + "\n", "9->25\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", - "\n", + "\n", "9->26\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", - "\n", + "\n", "9->27\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "28\n", + "\n", + "28\n", + "\n", + "\n", + "\n", + "9->28\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "0->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "0->11\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "10->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "10->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", "\n", - "11->1\n", - "\n", - "\n", - "\n", + "11->0\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "1->12\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "12->0\n", - "\n", - "\n", - "\n", + "12->1\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "13->1\n", - "\n", - "\n", - "\n", + "13->0\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "2->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", + "\n", + "2->16\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", - "\n", - "\n", - "2->15\n", - "\n", - "\n", - "\n", - "\n", - "\n", + "\n", "\n", - "15->2\n", - "\n", - "\n", - "\n", + "14->15\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "16->2\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", - "\n", + "\n", "\n", - "3->12\n", - "\n", - "\n", - "\n", + "3->13\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "16\n", - "\n", - "16\n", + "17\n", + "\n", + "17\n", "\n", - "\n", + "\n", "\n", - "3->16\n", - "\n", - "\n", - "\n", + "3->17\n", + "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "16->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "17->2\n", + "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "16->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "17->3\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "4->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "17\n", - "\n", - "17\n", + "18\n", + "\n", + "18\n", "\n", - "\n", + "\n", "\n", - "4->17\n", - "\n", - "\n", - "\n", + "4->18\n", + "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "17->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "18->4\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "5->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "5->15\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "5->17\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "18\n", - "\n", - "18\n", + "5->16\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "5->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "18->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "19\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "5->19\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "19->5\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "6->11\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "19\n", - "\n", - "19\n", - "\n", - "\n", - "\n", - "6->19\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", - "\n", + "\n", "6->20\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "19->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "21\n", + "\n", + "21\n", "\n", - "\n", - "\n", - "19->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "6->21\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "20->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "20->7\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "7->12\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "7->13\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "21\n", - "\n", - "21\n", - "\n", - "\n", - "\n", - "7->21\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "22\n", - "\n", - "22\n", - "\n", - "\n", - "\n", - "7->22\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->12\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7->13\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "22\n", + "\n", + "22\n", + "\n", + "\n", + "\n", + "7->22\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "23\n", + "\n", + "23\n", + "\n", + "\n", + "\n", + "7->23\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22->4\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22->7\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "23->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "23->6\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", - "\n", + "\n", "\n", - "8->12\n", - "\n", - "\n", - "\n", + "8->13\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "8->16\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "8->21\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "23\n", - "\n", - "23\n", + "8->17\n", + "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "8->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "23->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "24\n", + "\n", + "24\n", "\n", - "\n", - "\n", - "23->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "8->24\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "24->0\n", - "\n", - "\n", - "\n", + "24->5\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "25->3\n", - "\n", - "\n", - "\n", + "24->8\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "26->6\n", - "\n", - "\n", - "\n", + "25->8\n", + "\n", + "\n", + "\n", "\n", - "\n", + "\n", "\n", - "27->8\n", - "\n", - "\n", - "\n", + "26->3\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "27->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "28->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "15->14\n", + "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -1958,214 +2000,214 @@ "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "0->4\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n", + "2->4\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!i0 & i1 & o0\n", + "\n", + "\n", + "\n", + "3->4\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "1->5\n", - "\n", - "\n", - "!i1 & o0\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "i1 & !o0\n", - "\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "!i1 & !o0\n", - "\n", - "\n", - "\n", - "3->1\n", - "\n", - "\n", - "i0 & i1 & o0\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "5\n", "\n", "\n", - "\n", + "\n", "3->5\n", - "\n", - "\n", - "i0 & !i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", - "\n", - "3->6\n", - "\n", - "\n", - "!i0 & !i1 & o0\n", - "\n", - "\n", "\n", - "4->1\n", - "\n", - "\n", - "i0 & i1 & !o0\n", - "\n", - "\n", - "\n", - "4->2\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", - "\n", - "\n", - "\n", - "4->3\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "3->6\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", - "\n", - "\n", - "5->1\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "5->4\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", - "\n", + "\n", "5->5\n", - "\n", - "\n", - "!i1 & !o0\n", - "\n", - "\n", - "\n", - "6->1\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", - "\n", + "\n", "6->3\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", + "\n", + "\n", + "\n", + "6->4\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", - "\n", + "\n", "6->5\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", - "\n", + "\n", "6->6\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n" @@ -2193,92 +2235,120 @@ "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "0->2\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", - "\n", + "\n", "2->1\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", - "\n", + "\n", "2->2\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n" @@ -2306,58 +2376,86 @@ "\n", "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "I->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1->1\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", - "\n", + "\n", "1->0\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", - "\n", + "\n", "0->0\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n" @@ -2376,85 +2474,6 @@ "minimization lvl 3\n" ] }, - { - "data": { - "image/svg+xml": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "t\n", - "[all]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "!i1 & !o0\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "i1 & !o0\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!i1 & o0\n", - "\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "i1 & o0\n", - "\n", - "\n", - "\n" - ], - "text/plain": [ - "" - ] - }, - "metadata": {}, - "output_type": "display_data" - }, - { - "name": "stdout", - "output_type": "stream", - "text": [ - "minimization lvl 4\n" - ] - }, { "data": { "image/svg+xml": [ @@ -2504,14 +2523,14 @@ "!i1 & o0\n", "\n", "\n", - "\n", + "\n", "1->0\n", "\n", "\n", "i1 & !o0\n", "\n", "\n", - "\n", + "\n", "1->1\n", "\n", "\n", @@ -2531,7 +2550,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "minimization lvl 5\n" + "minimization lvl 4\n" ] }, { @@ -2583,14 +2602,14 @@ "i1 & !o0\n", "\n", "\n", - "\n", + "\n", "1->0\n", "\n", "\n", "!i1 & o0\n", "\n", "\n", - "\n", + "\n", "1->1\n", "\n", "\n", @@ -2605,6 +2624,85 @@ }, "metadata": {}, "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "minimization lvl 5\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "i1 & o0\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "!i1 & o0\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "i1 & !o0\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "!i1 & !o0\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ @@ -2623,15 +2721,6 @@ " display(strat.show())" ] }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Input/Output\n", - "\n", - "An extension of the HOA format makes it possible to store the `state-player` property. This allows us to read the parity game constructed by `ltlsynt` using `spot.automaton()` like any other automaton." - ] - }, { "cell_type": "code", "execution_count": 11, @@ -2646,232 +2735,402 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", - "\n", + "\n", "0->2\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", - "\n", + "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "3->7\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", - "\n", + "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", - "\n", + "\n", + "\n", + "0->8\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", "\n", - "4->8\n", - "\n", - "\n", - "1\n", - "\n", + "2->1\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "5->7\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", + "\n", "\n", - "6->3\n", - "\n", - "\n", - "1\n", - "\n", + "4->3\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "\n", - "7->5\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", "\n", - "\n", - "\n", - "8->4\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "6->5\n", + "\n", + "\n", + "1\n", "\n", - "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "13\n", + "\n", + "13\n", + "\n", + "\n", + "\n", + "1->13\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "18\n", + "\n", + "18\n", + "\n", + "\n", + "\n", + "1->18\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "19\n", + "\n", + "19\n", + "\n", + "\n", + "\n", + "1->19\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", "\n", - "9\n", - "\n", - "9\n", + "20\n", + "\n", + "20\n", "\n", - "\n", - "\n", - "8->9\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "1->20\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "13->7\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "18->5\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "19->3\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "20->1\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "3->13\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "3->19\n", + "\n", + "\n", + "!i1\n", "\n", "\n", - "\n", + "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", - "\n", + "\n", + "\n", + "5->10\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "5->11\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "15\n", + "\n", + "15\n", + "\n", + "\n", + "\n", + "5->15\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "16\n", + "\n", + "16\n", + "\n", + "\n", "\n", - "9->10\n", - "\n", - "\n", - "1\n", - "\n", + "5->16\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", "\n", "\n", - "\n", + "\n", "10->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "11->7\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "14\n", + "\n", + "14\n", + "\n", + "\n", + "\n", + "15->14\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "16->5\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "7->10\n", + "\n", + "\n", + "!i1\n", + "\n", + "\n", + "\n", + "7->11\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "9->13\n", + "\n", + "\n", + "i1\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "12\n", + "\n", + "\n", + "\n", + "9->12\n", + "\n", + "\n", + "!i1\n", + "\n", + "\n", + "\n", + "12->9\n", + "\n", + "\n", + "!o0\n", + "\n", + "\n", + "\n", + "14->13\n", + "\n", + "\n", + "i0 & i1\n", + "\n", + "\n", + "\n", + "14->18\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", + "\n", + "\n", + "14->12\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", + "\n", + "\n", + "17\n", + "\n", + "17\n", + "\n", + "\n", + "\n", + "14->17\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", + "\n", + "\n", + "17->14\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f724981b2d0> >" + " *' at 0x7f7e127216c0> >" ] }, "execution_count": 11, @@ -2879,6 +3138,285 @@ "output_type": "execute_result" } ], + "source": [ + "gi.minimize_lvl = 0\n", + "spot.apply_strategy(game, False, False)\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Input/Output\n", + "\n", + "An extension of the HOA format makes it possible to store the `state-player` property. This allows us to read the parity game constructed by `ltlsynt` using `spot.automaton()` like any other automaton." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))))\n", + "[parity max odd 5]\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "I->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "4->10\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "4->11\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "7->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "3->9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "9->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "\n", + "9->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n", + "10->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "\n", + "10->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n", + "11->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "\n", + "11->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f7e12721a50> >" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], "source": [ "game = spot.automaton(\"ltlsynt --ins=a --outs=b -f '!b & GFa <-> Gb' --print-game-hoa |\");\n", "game" @@ -2895,7 +3433,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 13, "metadata": {}, "outputs": [ { @@ -2903,43 +3441,45 @@ "output_type": "stream", "text": [ "HOA: v1\n", - "States: 11\n", - "Start: 0\n", + "States: 12\n", + "Start: 4\n", "AP: 2 \"b\" \"a\"\n", - "acc-name: parity max odd 3\n", - "Acceptance: 3 Fin(2) & (Inf(1) | Fin(0))\n", + "acc-name: parity max odd 5\n", + "Acceptance: 5 Fin(4) & (Inf(3) | (Fin(2) & (Inf(1) | Fin(0))))\n", "properties: trans-labels explicit-labels trans-acc colored complete\n", "properties: deterministic\n", - "spot-state-player: 0 1 1 0 0 0 1 1 1 0 1\n", + "spot-state-player: 0 0 0 0 0 1 1 1 1 1 1 1\n", "--BODY--\n", "State: 0\n", - "[!1] 1 {1}\n", - "[1] 2 {1}\n", + "[!1] 5 {1}\n", + "[1] 6 {1}\n", "State: 1\n", - "[!0] 3 {1}\n", - "[0] 4 {1}\n", + "[1] 6 {1}\n", + "[!1] 7 {1}\n", "State: 2\n", - "[!0] 5 {1}\n", - "[0] 4 {1}\n", + "[t] 8 {1}\n", "State: 3\n", - "[!1] 6 {1}\n", - "[1] 7 {2}\n", - "State: 4\n", - "[t] 8 {2}\n", - "State: 5\n", - "[!1] 6 {1}\n", - "[1] 7 {2}\n", - "State: 6\n", - "[t] 3 {1}\n", - "State: 7\n", - "[t] 5 {2}\n", - "State: 8\n", - "[!0] 9 {1}\n", - "[0] 4 {2}\n", - "State: 9\n", - "[t] 10 {1}\n", - "State: 10\n", "[t] 9 {1}\n", + "State: 4\n", + "[!1] 10 {1}\n", + "[1] 11 {1}\n", + "State: 5\n", + "[t] 0 {3}\n", + "State: 6\n", + "[t] 1 {4}\n", + "State: 7\n", + "[t] 0 {4}\n", + "State: 8\n", + "[t] 2 {3}\n", + "State: 9\n", + "[!0] 2 {3}\n", + "[0] 3 {4}\n", + "State: 10\n", + "[!0] 0 {3}\n", + "[0] 3 {3}\n", + "State: 11\n", + "[!0] 1 {3}\n", + "[0] 3 {3}\n", "--END--\n" ] } @@ -2957,7 +3497,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 14, "metadata": {}, "outputs": [ { @@ -2966,7 +3506,7 @@ "True" ] }, - "execution_count": 13, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -2977,7 +3517,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 15, "metadata": {}, "outputs": [ { @@ -2989,235 +3529,253 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - "))\n", - "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | (Fin(\n", + "\n", + ") & (Inf(\n", + "\n", + ") | Fin(\n", + "\n", + "))))\n", + "[parity max odd 5]\n", "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "6\n", - "\n", - "\n", - "\n", - "3->6\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "7\n", - "\n", - "7\n", - "\n", - "\n", - "\n", - "3->7\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "8\n", - "\n", - "8\n", - "\n", - "\n", - "\n", - "4->8\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "\n", - "\n", - "5->7\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "\n", - "\n", - "6->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n", - "7->5\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "\n", - "8->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "\n", - "\n", - "9\n", - "\n", - "9\n", - "\n", - "\n", - "\n", - "8->9\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "I->4\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", - "\n", + "\n", + "\n", + "4->10\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "11\n", + "\n", + "\n", + "\n", + "4->11\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "0->5\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "6\n", + "\n", + "6\n", + "\n", + "\n", + "\n", + "0->6\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "6->1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "1->6\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "7\n", + "\n", + "\n", + "\n", + "1->7\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "\n", + "7->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "8\n", + "\n", + "\n", + "\n", + "2->8\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "8->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "9\n", + "\n", + "9\n", + "\n", + "\n", + "\n", + "3->9\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "9->2\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "\n", + "9->3\n", + "\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "\n", + "10->0\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", "\n", - "9->10\n", - "\n", - "\n", - "1\n", - "\n", + "10->3\n", + "\n", + "\n", + "b\n", + "\n", "\n", - "\n", + "\n", "\n", - "10->9\n", - "\n", - "\n", - "1\n", - "\n", + "11->1\n", + "\n", + "\n", + "!b\n", + "\n", + "\n", + "\n", + "\n", + "11->3\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f724981bdb0> >" + " *' at 0x7f7e12721660> >" ] }, - "execution_count": 14, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -3252,7 +3810,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 16, "metadata": {}, "outputs": [ { @@ -3295,7 +3853,7 @@ }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 17, "metadata": {}, "outputs": [], "source": [ @@ -3304,7 +3862,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -3428,7 +3986,7 @@ }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 19, "metadata": {}, "outputs": [ { @@ -3457,7 +4015,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 20, "metadata": {}, "outputs": [ { @@ -3485,7 +4043,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 21, "metadata": {}, "outputs": [ { @@ -3527,7 +4085,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f72497abfc0> >" + " *' at 0x7f7e11cdd0f0> >" ] }, "metadata": {}, @@ -3549,7 +4107,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" },