diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 340eba00a..01210c824 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1298,6 +1298,36 @@ def sat_minimize(aut, acc=None, colored=False, else: return sm(aut, args, state_based) +# Adding the inline csv-display option +def minimize_mealy(mm, opt = -1, display_log = False, return_log = False): + from spot.impl import minimize_mealy as minmealy + + try: + lvl = int(opt) + opt = synthesis_info() + opt.minimize_lvl = lvl + 4 + except (ValueError, TypeError) as _: + pass + + if display_log or return_log: + import pandas as pd + with tempfile.NamedTemporaryFile(dir='.', suffix='.minlog') as t: + opt.opt.set_str("satlogcsv", t.name) + resmm = minmealy(mm, opt) + + dfrm = pd.read_csv(t.name, dtype=object) + if display_log: + from IPython.display import display + del dfrm['instance'] + display(dfrm) + if return_log: + return resmm, dfrm + else: + return resmm + else: + return minmealy(mm, opt) + + def parse_word(word, dic=_bdd_dict): from spot.impl import parse_word as pw diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index 6bbb9c4f7..3635e6334 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -27,6 +27,7 @@ #include #include #include +#include #include #include @@ -88,6 +89,33 @@ namespace #endif } +namespace +{ + static std::unique_ptr sat_csv_file; + struct fwrapper{ + std::string fname; + std::FILE* f; + fwrapper(const std::string& name) + : fname{name} + , f{std::fopen(name.c_str(), "a")} + { + if (!f) + throw std::runtime_error("File could not be oppened for writing."); + } + ~fwrapper() + { + std::fclose(f); + f = nullptr; + } + fwrapper& operator=(const fwrapper&) = delete; + fwrapper& operator=(fwrapper&&) = delete; + fwrapper(const fwrapper&) = delete; + fwrapper(fwrapper&&) = delete; + }; + static std::unique_ptr sat_dimacs_file; + static std::string sat_instance_name = ""; +} + namespace spot { @@ -817,6 +845,119 @@ namespace #else void trace_clause(const std::vector&){} #endif + struct satprob_info + { + stopwatch sw; + + double premin_time, reorg_time, partsol_time, player_incomp_time, + incomp_time, split_all_let_time, split_min_let_time, + split_cstr_time, prob_init_build_time, sat_time, + build_time, refine_time, total_time; + long long n_classes, n_refinement, n_lit, n_clauses, + n_iteration, n_bisim_let, n_min_states, done; + std::string task; + const std::string instance; + + satprob_info(const std::string& instance) + : premin_time{-1} + , reorg_time{-1} + , partsol_time{-1} + , player_incomp_time{-1} + , incomp_time{-1} + , split_all_let_time{-1} + , split_min_let_time{-1} + , split_cstr_time{-1} + , prob_init_build_time{-1} + , sat_time{-1} + , build_time{-1} + , refine_time{-1} + , total_time{-1} + , n_classes{-1} + , n_refinement{-1} + , n_lit{-1} + , n_clauses{-1} + , n_iteration{-1} + , n_bisim_let{-1} + , n_min_states{-1} + , done{-1} + , task{} + , instance{instance+","} + { + } + + void start() + { + sw.start(); + } + double stop() + { + return sw.stop(); + } + double restart() + { + double res = sw.stop(); + sw.start(); + return res; + } + // Writing also "flushes" + void write() + { + auto f = [](std::ostream& o, auto& v, bool sep = true) + { + if (v >= 0) + o << v; + if (sep) + o.put(','); + v = -1; + }; + if (!sat_csv_file) + return; + + auto& out = *sat_csv_file; + if (out.tellp() == 0) + { + out << "instance,task,premin_time,reorg_time,partsol_time," + << "player_incomp_time,incomp_time,split_all_let_time," + << "split_min_let_time,split_cstr_time,prob_init_build_time," + << "sat_time,build_time,refine_time,total_time,n_classes," + << "n_refinement,n_lit,n_clauses,n_iteration,n_bisim_let," + << "n_min_states,done\n"; + } + + assert(!task.empty()); + out << instance; + out << task; + task = ""; + out.put(','); + + std::stringstream ss; + + f(ss, premin_time); + f(ss, reorg_time); + f(ss, partsol_time); + f(ss, player_incomp_time); + f(ss, incomp_time); + f(ss, split_all_let_time); + f(ss, split_min_let_time); + f(ss, split_cstr_time); + f(ss, prob_init_build_time); + f(ss, sat_time); + f(ss, build_time); + f(ss, refine_time); + f(ss, total_time); + f(ss, n_classes); + f(ss, n_refinement); + f(ss, n_lit); + f(ss, n_clauses); + f(ss, n_iteration); + f(ss, n_bisim_let); + f(ss, n_min_states); + f(ss, done, false); + out << ss.str(); + out.put('\n'); + } + }; + template bool all_of(const CONT& c) @@ -1125,7 +1266,7 @@ namespace square_matrix compute_incomp(const_twa_graph_ptr mm, const unsigned n_env, - stopwatch& sw) + satprob_info& si) { const unsigned n_tot = mm->num_states(); @@ -1201,7 +1342,7 @@ namespace return inc_player.get(ps2c[s1].second, ps2c[s2].second); }; - dotimeprint << "Done computing player incomp " << sw.stop() << '\n'; + si.player_incomp_time = si.restart(); #ifdef TRACE trace << "player cond id incomp\n"; @@ -1284,7 +1425,7 @@ namespace trace << "Env state incomp\n"; inc_env.print(std::cerr); #endif - + si.incomp_time = si.restart(); return inc_env; } @@ -1912,26 +2053,22 @@ namespace std::pair reduce_and_split(const_twa_graph_ptr mmw, const unsigned n_env, const square_matrix& incompmat, - stopwatch& sw) + satprob_info& si) { reduced_alphabet_t red; + si.start(); + std::tie(red.n_groups, red.which_group) = trans_comp_classes(incompmat); - dotimeprint << "Done trans comp " << red.n_groups - << " - " << sw.stop() << '\n'; compute_all_letters(red, mmw, n_env); - dotimeprint << "Done comp all letters " << " - " << sw.stop() << '\n'; + si.split_all_let_time = si.restart(); compute_minimal_letters(red, mmw, n_env); -#ifdef MINTIMINGS - dotimeprint << "Done comp all min sim letters "; - for (const auto& al : red.bisim_letters) - dotimeprint << al.size() << ' '; - dotimeprint << " - " << sw.stop() << '\n'; -#endif + si.split_min_let_time = si.restart(); + si.n_bisim_let = red.n_red_sigma; twa_graph_ptr split_mmw = split_on_minimal(red, mmw, n_env); - dotimeprint << "Done splitting " << sw.stop() << '\n'; + si.split_cstr_time = si.restart(); trace << std::endl; return std::make_pair(split_mmw, red); @@ -2234,9 +2371,10 @@ namespace struct mm_sat_prob_t { mm_sat_prob_t(unsigned n_classes, unsigned n_env, - unsigned n_sigma_red) + unsigned n_sigma_red, satprob_info& si) : lm(n_classes, n_env, n_sigma_red) , n_classes{lm.n_classes_} + , si{si} { state_cover_clauses.reserve(n_classes); trans_cover_clauses.reserve(n_classes*n_sigma_red); @@ -2288,6 +2426,13 @@ namespace // res[i] == -1 : i not used in lit mapper // res[i] == 0 : i is assigned false // res[i] == 1 : i is assigned true + if (sat_dimacs_file) + { + fprintf(sat_dimacs_file->f, + "c ### Next Instance %lld %lld ###\n", + this->si.n_classes, this->si.n_refinement); + picosat_print(lm.psat_, sat_dimacs_file->f); + } switch (picosat_sat(lm.psat_, -1)) { case PICOSAT_UNSATISFIABLE: @@ -2353,6 +2498,8 @@ namespace std::unordered_map> cube_map; // A map that indicates if two cubes are compatible or not via their id std::unordered_map, bool, pair_hash> cube_incomp_map; + // Piggy-back a struct for performance measure + satprob_info& si; }; template<> @@ -2431,14 +2578,15 @@ namespace const square_matrix& incompmat, const reduced_alphabet_t& red, const part_sol_t& psol, - const unsigned n_env) + const unsigned n_env, + satprob_info& si) { const auto& psolv = psol.psol; const unsigned n_classes = psolv.size(); const unsigned n_red = red.n_red_sigma; const unsigned n_groups = red.n_groups; - mm_sat_prob_t mm_pb(n_classes, n_env, n_red); + mm_sat_prob_t mm_pb(n_classes, n_env, n_red, si); auto& lm = mm_pb.lm; @@ -3372,7 +3520,7 @@ namespace const reduced_alphabet_t& red, const part_sol_t& psol, const unsigned n_env, - stopwatch& sw) + satprob_info& si) { const auto& psolv = psol.psol; const unsigned n_psol = psolv.size(); @@ -3393,15 +3541,16 @@ namespace mm_pb.lm.print(std::cerr); #endif mm_pb.set_variable_clauses(); - dotimeprint << "Done constructing SAT " << sw.stop() << '\n'; - dotimeprint << "n literals " << mm_pb.n_lits() - << " n clauses " << mm_pb.n_clauses() << '\n'; + si.n_lit = mm_pb.n_lits(); + si.n_clauses = mm_pb.n_clauses(); + si.start(); auto sol = mm_pb.get_sol(); - dotimeprint << "Done solving SAT " << sw.stop() << '\n'; + si.sat_time = si.restart(); if (sol.empty()) { mm_pb.unset_variable_clauses(); + si.write(); return nullptr; } #ifdef TRACE @@ -3606,20 +3755,25 @@ namespace for (const auto& el : used_ziaj_map) if (el.second == bddfalse) infeasible_classes.emplace_back(el.first.i, el.first.a); + si.build_time = si.restart(); + if (!infeasible_classes.empty()) { // Remove the variable clauses // This is suboptimal but the contexts form a stack so... - dotimeprint << "Refining constraints for " - << infeasible_classes.size() << " classses.\n"; + auto oldrefine = si.n_refinement; + si.write(); + si.task = "refinement"; + si.n_classes = n_classes; + si.n_refinement = oldrefine + infeasible_classes.size(); mm_pb.unset_variable_clauses(); add_bdd_cond_constr(mm_pb, mmw, red, n_env, infeasible_classes, x_in_class); + si.refine_time = si.restart(); continue; //retry } cstr_split_mealy(minmach, red, x_in_class, used_ziaj_map); - // todo: What is the impact of chosing one of the possibilities minmach->set_init_state(init_class_v.front()); return minmach; @@ -3634,8 +3788,10 @@ namespace spot { assert(is_mealy(mm)); - stopwatch sw; - sw.start(); + satprob_info si(sat_instance_name); + si.task = "presat"; + stopwatch sglob; + sglob.start(); if ((premin < -1) || (premin > 1)) throw std::runtime_error("premin has to be -1, 0 or 1"); @@ -3672,7 +3828,9 @@ namespace spot const_twa_graph_ptr mmw = do_premin(); assert(is_split_mealy(mmw)); - dotimeprint << "Done premin " << sw.stop() << '\n'; + si.premin_time = si.restart(); + + // 0 -> "Env" next is input props // 1 -> "Player" next is output prop @@ -3690,24 +3848,24 @@ namespace spot print_hoa(std::cerr, mmw); #endif assert(n_env != -1u); - dotimeprint << "Done reorganise " << n_env << " - " - << sw.stop() << '\n'; + si.reorg_time = si.restart(); // Compute incompatibility based on bdd - auto incompmat = compute_incomp(mmw, n_env, sw); - dotimeprint << "Done incompatibility " << sw.stop() << '\n'; + auto incompmat = compute_incomp(mmw, n_env, si); #ifdef TRACE incompmat.print(std::cerr); #endif // Get a partial solution auto partsol = get_part_sol(incompmat); - dotimeprint << "Done partial solution " << partsol.psol.size() - << " - " << sw.stop() << '\n'; + si.partsol_time = si.restart(); auto early_exit = [&]() { + si.done = 1; + si.total_time = sglob.stop(); + si.write(); // Always keep machines split if (mm->get_named_prop("state-player")) assert(is_split_mealy_specialization(mm, mmw)); @@ -3721,58 +3879,78 @@ namespace spot // states as the original automaton -> we are done if (partsol.psol.size() == n_env) { - dotimeprint << "Done trans comp " << 1 << " - " << sw.stop() << '\n'; - dotimeprint << "Done comp all letters " << " - " - << sw.stop() << '\n'; -#ifdef MINTIMINGS - dotimeprint << "Done comp all min sim letters 0 - " - << sw.stop() << '\n'; -#endif - dotimeprint << "Done splitting " << sw.stop() << '\n'; - dotimeprint << "Done split and reduce " << sw.stop() << '\n'; - dotimeprint << "Done build init prob " << sw.stop() << '\n'; - dotimeprint << "Done minimizing - " << mmw->num_states() - << " - " << sw.stop() << '\n'; return early_exit(); } // Get the reduced alphabet auto [split_mmw, reduced_alphabet] = - reduce_and_split(mmw, n_env, incompmat, sw); - dotimeprint << "Done split and reduce " << sw.stop() << '\n'; + reduce_and_split(mmw, n_env, incompmat, si); auto mm_pb = build_init_prob(split_mmw, incompmat, - reduced_alphabet, partsol, n_env); - dotimeprint << "Done build init prob " << sw.stop() << '\n'; + reduced_alphabet, partsol, n_env, si); + si.prob_init_build_time = si.restart(); + si.write(); twa_graph_ptr minmachine = nullptr; for (size_t n_classes = partsol.psol.size(); n_classes < n_env; ++n_classes) { + if (si.task.empty()) + si.task = "sat"; + si.n_iteration = (n_classes-partsol.psol.size()); + si.n_refinement = 0; + si.n_classes = n_classes; + minmachine = try_build_min_machine(mm_pb, mmw, reduced_alphabet, partsol, n_env, - sw); - dotimeprint << "Done try_build " << n_classes - << " - " << sw.stop() << '\n'; + si); if (minmachine) break; increment_classes(split_mmw, incompmat, reduced_alphabet, partsol, mm_pb); - dotimeprint << "Done incrementing " << sw.stop() << '\n'; + } // Is already minimal -> Return a copy // Set state players! if (!minmachine) return early_exit(); set_synthesis_outputs(minmachine, get_synthesis_outputs(mm)); - dotimeprint << "Done minimizing - " << minmachine->num_states() - << " - " << sw.stop() << '\n'; + + si.done=1; + si.n_min_states = minmachine->num_states(); + si.total_time = sglob.stop(); + si.write(); assert(is_split_mealy_specialization(mm, minmachine)); return minmachine; } + + twa_graph_ptr + minimize_mealy(const const_twa_graph_ptr& mm, + synthesis_info& si) + { + if ((si.minimize_lvl < 3) || (5 < si.minimize_lvl)) + throw std::runtime_error("Invalid option"); + + std::string csvfile = si.opt.get_str("satlogcsv"); + std::string dimacsfile = si.opt.get_str("satlogdimacs"); + + if (!csvfile.empty()) + sat_csv_file + = std::make_unique(csvfile, + std::ios_base::ate + | std::ios_base::app); + if (!dimacsfile.empty()) + sat_dimacs_file + = std::make_unique(dimacsfile); + sat_instance_name = si.opt.get_str("satinstancename"); + auto res = minimize_mealy(mm, si.minimize_lvl-4); + sat_csv_file.reset(); + sat_dimacs_file.reset(); + return res; + } } namespace spot diff --git a/spot/twaalgos/mealy_machine.hh b/spot/twaalgos/mealy_machine.hh index d603d8000..3bdb71b73 100644 --- a/spot/twaalgos/mealy_machine.hh +++ b/spot/twaalgos/mealy_machine.hh @@ -159,6 +159,27 @@ namespace spot SPOT_API twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm, int premin = -1); + /// \ingroup mealy + /// \brief Minimizes an (in)completely specified mealy machine + /// + /// The approach is described in \cite renkin.22.forte. + /// + /// \param si synthesis_info structure used to store data for benchmarking + /// and indicates which premin level to use + /// + /// \return A split mealy machines which is a minimal + /// specialization of the original machine. + /// + /// \note Enabling \a premin will remove finite traces. + /// \note If si.opt contains an option "satlogcsv" detailed results will be + /// stored in this file. If it contains "satlogdimacs" all sat problems will + /// stored. + /// \see is_split_mealy_specialization + + SPOT_API twa_graph_ptr + minimize_mealy(const const_twa_graph_ptr& mm, + synthesis_info& si); + /// \ingroup mealy /// \brief Test if the split mealy machine \a right is a specialization of diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb index c2aeb125c..9d7fe7d96 100644 --- a/tests/python/_mealy.ipynb +++ b/tests/python/_mealy.ipynb @@ -7,7 +7,8 @@ "metadata": {}, "outputs": [], "source": [ - "import spot\n", + "import spot, buddy\n", + "import pandas as pd\n", "spot.setup()" ] }, @@ -128,7 +129,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc1244a3d50> >" + " *' at 0x7fcc35aaa030> >" ] }, "execution_count": 4, @@ -208,7 +209,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc124439570> >" + " *' at 0x7fcc35aaa900> >" ] }, "execution_count": 6, @@ -282,7 +283,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fc124439570> >" + " *' at 0x7fcc35aaa900> >" ] }, "execution_count": 8, @@ -296,9 +297,1284 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 9, "id": "923a59d6", "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "\n", + "!i\n", + "/\n", + "\n", + "!o\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "\n", + "i\n", + "/\n", + "\n", + "o\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "\n", + "1\n", + "/\n", + "\n", + "!o\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "1\n", + "/\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc35ac20c0> >" + ] + }, + "execution_count": 9, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "i = buddy.bdd_ithvar(aut.register_ap(\"i\"))\n", + "o = buddy.bdd_ithvar(aut.register_ap(\"o\"))\n", + "spot.set_synthesis_outputs(aut, o)\n", + "aut.new_states(3)\n", + "aut.new_edge(0,1,buddy.bdd_not(i)&buddy.bdd_not(o))\n", + "aut.new_edge(0,2,i&o)\n", + "aut.new_edge(1,1,buddy.bdd_not(o))\n", + "aut.new_edge(2,2,buddy.bddtrue)\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "f06d6df4", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "('o',)\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", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!i\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "0->4\n", + "\n", + "\n", + "i\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!o\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "o\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc35ac2720> >" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_s = spot.split_2step(aut)\n", + "print(spot.get_synthesis_output_aps(aut_s))\n", + "aut_s" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "3cc4d320", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
taskpremin_timereorg_timepartsol_timeplayer_incomp_timeincomp_timesplit_all_let_timesplit_min_let_timesplit_cstr_timeprob_init_build_time...refine_timetotal_timen_classesn_refinementn_litn_clausesn_iterationn_bisim_letn_min_statesdone
0presat25643.31.112e-064.588e-069.888e-064.549e-061.5929e-059.338e-065.901e-066.7276e-05...NaNNaNNaNNaNNaNNaNNaN2NaNNaN
1satNaNNaNNaNNaNNaNNaNNaNNaNNaN...NaN0.000282709207120NaN41
\n", + "

2 rows × 22 columns

\n", + "
" + ], + "text/plain": [ + " task premin_time reorg_time partsol_time player_incomp_time incomp_time \\\n", + "0 presat 25643.3 1.112e-06 4.588e-06 9.888e-06 4.549e-06 \n", + "1 sat NaN NaN NaN NaN NaN \n", + "\n", + " split_all_let_time split_min_let_time split_cstr_time prob_init_build_time \\\n", + "0 1.5929e-05 9.338e-06 5.901e-06 6.7276e-05 \n", + "1 NaN NaN NaN NaN \n", + "\n", + " ... refine_time total_time n_classes n_refinement n_lit n_clauses \\\n", + "0 ... NaN NaN NaN NaN NaN NaN \n", + "1 ... NaN 0.000282709 2 0 7 12 \n", + "\n", + " n_iteration n_bisim_let n_min_states done \n", + "0 NaN 2 NaN NaN \n", + "1 0 NaN 4 1 \n", + "\n", + "[2 rows x 22 columns]" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "i\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!i\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "o\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "!o\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc88735f00> >" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "min_lvl = 0\n", + "aut_ms, table = spot.minimize_mealy(aut_s, min_lvl, display_log=True, return_log=True)\n", + "aut_ms" + ] + }, + { + "cell_type": "markdown", + "id": "bc844797", + "metadata": {}, + "source": [ + "## A more involved example" + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "id": "893bc90e", + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\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", + "\n", + "1\n", + "/\n", + "\n", + "o1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "\n", + "1\n", + "/\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "2->2\n", + "\n", + "\n", + "\n", + "1\n", + "/\n", + "\n", + "(!o0 & o1) | (o0 & !o1)\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc6157fe40> >" + ] + }, + "execution_count": 12, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut = spot.make_twa_graph()\n", + "i = buddy.bdd_ithvar(aut.register_ap(\"i\"))\n", + "o0 = buddy.bdd_ithvar(aut.register_ap(\"o0\"))\n", + "no0 = buddy.bdd_not(o0)\n", + "o1 = buddy.bdd_ithvar(aut.register_ap(\"o1\"))\n", + "no1 = buddy.bdd_not(o1)\n", + "spot.set_synthesis_outputs(aut, o0&o1)\n", + "\n", + "vo1 = o0&o1\n", + "vo2 = no0&o1\n", + "vo3 = o0&no1\n", + "\n", + "aut.new_states(3)\n", + "\n", + "aut.new_edge(0,1,vo1|vo2)\n", + "aut.new_edge(1,2,vo1|vo3)\n", + "aut.new_edge(2,2,vo2|vo3)\n", + "aut" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "23edb107", + "metadata": {}, + "outputs": [ + { + "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", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "o1\n", + "\n", + "\n", + "\n", + "4\n", + "\n", + "4\n", + "\n", + "\n", + "\n", + "1->4\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "4->2\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "5\n", + "\n", + "5\n", + "\n", + "\n", + "\n", + "2->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "5->2\n", + "\n", + "\n", + "(!o0 & o1) | (o0 & !o1)\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc6157f210> >" + ] + }, + "execution_count": 13, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_s = spot.split_2step(aut)\n", + "aut_s" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "837aab84", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
taskpremin_timereorg_timepartsol_timeplayer_incomp_timeincomp_timesplit_all_let_timesplit_min_let_timesplit_cstr_timeprob_init_build_time...refine_timetotal_timen_classesn_refinementn_litn_clausesn_iterationn_bisim_letn_min_statesdone
0presat25643.41.683e-065.611e-062.66e-051.2e-073.647e-068.365e-063.747e-062.5538e-05...NaNNaNNaNNaNNaNNaNNaN1NaNNaN
1satNaNNaNNaNNaNNaNNaNNaNNaNNaN...NaNNaN10360NaNNaNNaN
2refinementNaNNaNNaNNaNNaNNaNNaNNaNNaN...4.4884e-05NaN111016NaNNaNNaNNaN
3satNaNNaNNaNNaNNaNNaNNaNNaNNaN...NaN0.0002003442017291NaN41
\n", + "

4 rows × 22 columns

\n", + "
" + ], + "text/plain": [ + " task premin_time reorg_time partsol_time player_incomp_time \\\n", + "0 presat 25643.4 1.683e-06 5.611e-06 2.66e-05 \n", + "1 sat NaN NaN NaN NaN \n", + "2 refinement NaN NaN NaN NaN \n", + "3 sat NaN NaN NaN NaN \n", + "\n", + " incomp_time split_all_let_time split_min_let_time split_cstr_time \\\n", + "0 1.2e-07 3.647e-06 8.365e-06 3.747e-06 \n", + "1 NaN NaN NaN NaN \n", + "2 NaN NaN NaN NaN \n", + "3 NaN NaN NaN NaN \n", + "\n", + " prob_init_build_time ... refine_time total_time n_classes n_refinement \\\n", + "0 2.5538e-05 ... NaN NaN NaN NaN \n", + "1 NaN ... NaN NaN 1 0 \n", + "2 NaN ... 4.4884e-05 NaN 1 1 \n", + "3 NaN ... NaN 0.000200344 2 0 \n", + "\n", + " n_lit n_clauses n_iteration n_bisim_let n_min_states done \n", + "0 NaN NaN NaN 1 NaN NaN \n", + "1 3 6 0 NaN NaN NaN \n", + "2 10 16 NaN NaN NaN NaN \n", + "3 17 29 1 NaN 4 1 \n", + "\n", + "[4 rows x 22 columns]" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "0 NaN\n", + "1 3\n", + "2 10\n", + "3 17\n", + "Name: n_lit, dtype: object\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", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "o0 & o1\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "3->1\n", + "\n", + "\n", + "o0 & !o1\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcc35ac22a0> >" + ] + }, + "execution_count": 14, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "si = spot.synthesis_info()\n", + "si.minimize_lvl = 3\n", + "aut_ms, table = spot.minimize_mealy(aut_s, si, display_log=True, return_log=True)\n", + "print(table[\"n_lit\"])\n", + "aut_ms" + ] + }, + { + "cell_type": "markdown", + "id": "0fea0269", + "metadata": {}, + "source": [ + "## Testing dimacs output" + ] + }, + { + "cell_type": "code", + "execution_count": 15, + "id": "d14324e8", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + " \n", + "
taskpremin_timereorg_timepartsol_timeplayer_incomp_timeincomp_timesplit_all_let_timesplit_min_let_timesplit_cstr_timeprob_init_build_time...refine_timetotal_timen_classesn_refinementn_litn_clausesn_iterationn_bisim_letn_min_statesdone
0presat25643.51.563e-065.4e-062.0519e-051.3e-073.968e-069.698e-067.624e-063.211e-05...NaNNaNNaNNaNNaNNaNNaN1NaNNaN
1satNaNNaNNaNNaNNaNNaNNaNNaNNaN...NaNNaN10360NaNNaNNaN
2refinementNaNNaNNaNNaNNaNNaNNaNNaNNaN...4.4633e-05NaN111016NaNNaNNaNNaN
3satNaNNaNNaNNaNNaNNaNNaNNaNNaN...NaN0.0002806752017291NaN41
\n", + "

4 rows × 22 columns

\n", + "
" + ], + "text/plain": [ + " task premin_time reorg_time partsol_time player_incomp_time \\\n", + "0 presat 25643.5 1.563e-06 5.4e-06 2.0519e-05 \n", + "1 sat NaN NaN NaN NaN \n", + "2 refinement NaN NaN NaN NaN \n", + "3 sat NaN NaN NaN NaN \n", + "\n", + " incomp_time split_all_let_time split_min_let_time split_cstr_time \\\n", + "0 1.3e-07 3.968e-06 9.698e-06 7.624e-06 \n", + "1 NaN NaN NaN NaN \n", + "2 NaN NaN NaN NaN \n", + "3 NaN NaN NaN NaN \n", + "\n", + " prob_init_build_time ... refine_time total_time n_classes n_refinement \\\n", + "0 3.211e-05 ... NaN NaN NaN NaN \n", + "1 NaN ... NaN NaN 1 0 \n", + "2 NaN ... 4.4633e-05 NaN 1 1 \n", + "3 NaN ... NaN 0.000280675 2 0 \n", + "\n", + " n_lit n_clauses n_iteration n_bisim_let n_min_states done \n", + "0 NaN NaN NaN 1 NaN NaN \n", + "1 3 6 0 NaN NaN NaN \n", + "2 10 16 NaN NaN NaN NaN \n", + "3 17 29 1 NaN 4 1 \n", + "\n", + "[4 rows x 22 columns]" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "c ### Next Instance 1 0 ###\n", + "p cnf 5 5\n", + "-1 2 -3 0\n", + "1 -3 0\n", + "1 -5 0\n", + "2 -5 0\n", + "3 -5 0\n", + "c ### Next Instance 1 1 ###\n", + "p cnf 12 15\n", + "-1 2 -3 0\n", + "4 0\n", + "6 0\n", + "-9 0\n", + "-1 -2 10 0\n", + "-10 0\n", + "1 -3 0\n", + "1 -5 0\n", + "1 -12 0\n", + "2 -5 0\n", + "2 -12 0\n", + "-2 9 0\n", + "3 -5 0\n", + "3 -12 0\n", + "7 8 0\n", + "c ### Next Instance 2 0 ###\n", + "p cnf 19 29\n", + "-3 -1 2 0\n", + "4 0\n", + "6 0\n", + "-9 0\n", + "-1 -2 10 0\n", + "-10 0\n", + "11 -16 -17 0\n", + "1 -15 -17 0\n", + "-1 13 -14 0\n", + "-11 13 -16 0\n", + "-11 -15 2 0\n", + "-13 -15 2 0\n", + "1 11 -19 0\n", + "13 -19 2 0\n", + "15 16 -19 0\n", + "3 14 -19 0\n", + "-2 0\n", + "-12 0\n", + "-5 0\n", + "1 -3 0\n", + "1 -5 0\n", + "1 -12 0\n", + "2 -5 0\n", + "2 -12 0\n", + "-2 9 0\n", + "3 -5 0\n", + "3 -12 0\n", + "7 8 0\n", + "11 -14 0\n", + "\n" + ] + } + ], + "source": [ + "import tempfile\n", + "\n", + "si = spot.synthesis_info()\n", + "si.minimize_lvl = 3\n", + "\n", + "with tempfile.NamedTemporaryFile(dir='.', suffix='.dimacslog') as t:\n", + " si.opt.set_str(\"satlogdimacs\", t.name)\n", + " aut_ms, table = spot.minimize_mealy(aut_s, si, display_log=True, return_log=True)\n", + " with open(t.name, \"r\") as f:\n", + " print(\"\".join(f.readlines()))\n", + " \n", + " " + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "5c9fe115", + "metadata": {}, "outputs": [], "source": [] } @@ -320,6 +1596,11 @@ "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.8.10" + }, + "vscode": { + "interpreter": { + "hash": "916dbcbb3f70747c44a77c7bcd40155683ae19c65e1c03b4aa3499c5328201f1" + } } }, "nbformat": 4, diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 18da81cf8..c6bfcf134 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -143,6 +143,10 @@ def canonicalize(s, type, ignores): # timing result we cannot compare between runs. s = re.sub(r'', '
', s, flags=re.DOTALL) + # Table that contains premin_time are log from the mealy minimization. + # They contain timing result so we cannot compare between runs. + s = re.sub(r'', '
', + s, flags=re.DOTALL) for n, p in enumerate(ignores): s = re.sub(p, 'IGN{}'.format(n), s) diff --git a/tests/python/synthesis.ipynb b/tests/python/synthesis.ipynb index 654d22873..54da20ef7 100644 --- a/tests/python/synthesis.ipynb +++ b/tests/python/synthesis.ipynb @@ -3,6 +3,7 @@ { "cell_type": "code", "execution_count": 1, + "id": "4f84fa79", "metadata": {}, "outputs": [], "source": [ @@ -13,6 +14,7 @@ }, { "cell_type": "markdown", + "id": "4ad017a0", "metadata": {}, "source": [ "This notebook presents functions that can be used to solve the Reactive Synthesis problem using games.\n", @@ -37,6 +39,7 @@ { "cell_type": "code", "execution_count": 2, + "id": "e333be09", "metadata": {}, "outputs": [ { @@ -655,6 +658,7 @@ }, { "cell_type": "markdown", + "id": "4d030586", "metadata": {}, "source": [ "Solving the game, is done with `solve_game()` as with any game. There is also a version that takes a `synthesis_info` as second argument in case the time it takes has to be recorded. Here passing `si` or not makes no difference." @@ -663,6 +667,7 @@ { "cell_type": "code", "execution_count": 3, + "id": "f13ac820", "metadata": {}, "outputs": [ { @@ -1222,6 +1227,7 @@ }, { "cell_type": "markdown", + "id": "98aa1402", "metadata": {}, "source": [ "Once a strategy has been found, it can be extracted as an automaton and simplified using 6 different levels (the default is 2). The output should be interpreted as a Mealy automaton, where transition have the form `(ins)&(outs)` where `ins` and `outs` are Boolean formulas representing possible inputs and outputs (they could be more than just conjunctions of atomic proposition). Mealy machines with this type of labels are called \"separated\" in Spot." @@ -1230,6 +1236,7 @@ { "cell_type": "code", "execution_count": 4, + "id": "4c93add7", "metadata": {}, "outputs": [ { @@ -2228,6 +2235,7 @@ }, { "cell_type": "markdown", + "id": "9d8d52f6", "metadata": {}, "source": [ "If needed, a separated Mealy machine can be turned into game shape using `split_sepearated_mealy()`, which is more efficient than `split_2step()`." @@ -2236,6 +2244,7 @@ { "cell_type": "code", "execution_count": 5, + "id": "707f4cf6", "metadata": {}, "outputs": [ { @@ -2517,6 +2526,7 @@ }, { "cell_type": "markdown", + "id": "b9e4412e", "metadata": {}, "source": [ "# Converting the separated Mealy machine to AIG\n", @@ -2529,6 +2539,7 @@ { "cell_type": "code", "execution_count": 6, + "id": "9f344931", "metadata": {}, "outputs": [ { @@ -2604,6 +2615,7 @@ }, { "cell_type": "markdown", + "id": "92bbe8d0", "metadata": {}, "source": [ "While we are at it, let us mention that you can render those circuits horizontally as follows:" @@ -2612,6 +2624,7 @@ { "cell_type": "code", "execution_count": 7, + "id": "3ae7ce32", "metadata": {}, "outputs": [ { @@ -2687,6 +2700,7 @@ }, { "cell_type": "markdown", + "id": "44fbc0ac", "metadata": {}, "source": [ "To encode the circuit in the AIGER format (ASCII version) use:" @@ -2695,6 +2709,7 @@ { "cell_type": "code", "execution_count": 8, + "id": "566715d5", "metadata": {}, "outputs": [ { @@ -2718,6 +2733,7 @@ }, { "cell_type": "markdown", + "id": "ef304f36", "metadata": {}, "source": [ "# Adding more inputs and outputs by force" @@ -2725,6 +2741,7 @@ }, { "cell_type": "markdown", + "id": "5c2b0b78", "metadata": {}, "source": [ "It can happen that propositions declared as output are ommited in the aig circuit (either because they are not part of the specification, or because they do not appear in the winning strategy). In that case those \n", @@ -2736,6 +2753,7 @@ { "cell_type": "code", "execution_count": 9, + "id": "874c7df1", "metadata": {}, "outputs": [ { @@ -3260,6 +3278,7 @@ }, { "cell_type": "markdown", + "id": "c564dba3", "metadata": {}, "source": [ "To force the presence of extra variables in the circuit, they can be passed to `mealy_machine_to_aig()`." @@ -3268,6 +3287,7 @@ { "cell_type": "code", "execution_count": 10, + "id": "c31a3b38", "metadata": {}, "outputs": [ { @@ -3378,6 +3398,7 @@ }, { "cell_type": "markdown", + "id": "3323fc84", "metadata": {}, "source": [ "# Combining Mealy machines\n", @@ -3397,6 +3418,7 @@ { "cell_type": "code", "execution_count": 11, + "id": "5d8e4cdb", "metadata": {}, "outputs": [ { @@ -3991,6 +4013,7 @@ }, { "cell_type": "markdown", + "id": "c7a1986f", "metadata": {}, "source": [ "# Reading an AIGER-file\n", @@ -4005,6 +4028,7 @@ { "cell_type": "code", "execution_count": 12, + "id": "a10d7e3b", "metadata": {}, "outputs": [], "source": [ @@ -4025,6 +4049,7 @@ { "cell_type": "code", "execution_count": 13, + "id": "2c40e19b", "metadata": {}, "outputs": [ { @@ -4149,6 +4174,7 @@ { "cell_type": "code", "execution_count": 14, + "id": "0ad6c566", "metadata": {}, "outputs": [ { @@ -4177,6 +4203,7 @@ { "cell_type": "code", "execution_count": 15, + "id": "2e1996c1", "metadata": {}, "outputs": [ { @@ -4193,6 +4220,7 @@ }, { "cell_type": "markdown", + "id": "41a8e042", "metadata": {}, "source": [ "An AIG circuit can be transformed into a monitor/Mealy machine. This can be used for instance to check that it does not intersect the negation of the specification." @@ -4201,6 +4229,7 @@ { "cell_type": "code", "execution_count": 16, + "id": "7399ea38", "metadata": {}, "outputs": [ { @@ -4268,6 +4297,7 @@ }, { "cell_type": "markdown", + "id": "7ac06afc", "metadata": {}, "source": [ "Note that the generation of aiger circuits from Mealy machines is flexible and accepts separated Mealy machines\n", @@ -4277,6 +4307,7 @@ { "cell_type": "code", "execution_count": 17, + "id": "bac68923", "metadata": {}, "outputs": [ { @@ -4424,6 +4455,7 @@ { "cell_type": "code", "execution_count": 18, + "id": "03ceb2a8", "metadata": {}, "outputs": [ { @@ -4626,7 +4658,7 @@ ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -4640,7 +4672,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3" + "version": "3.8.10" } }, "nbformat": 4,