diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index efd0a13fc..6b52ee542 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1401,7 +1401,9 @@ namespace static aig_ptr auts_to_aiger(const std::vector>& strat_vec, - const char* mode) + const char* mode, + const std::vector& unused_ins = {}, + const std::vector& unused_outs = {}) { // The aiger circuit cannot encode the acceptance condition // Test that the acceptance condition is true @@ -1459,6 +1461,17 @@ namespace } } + // Create two new vector holding used and unused inputs/outputs + // Used propositions appear first + std::vector input_names_all = input_names; + input_names_all.insert(input_names_all.end(), + unused_ins.cbegin(), + unused_ins.cend()); + std::vector output_names_all = output_names; + output_names_all.insert(output_names_all.end(), + unused_outs.cbegin(), + unused_outs.cend()); + // Decide on which outcond to use // The edges of the automaton all have the form in&out // due to the unsplit @@ -1530,7 +1543,7 @@ namespace assert(output_names.size() == (unsigned) bdd_nodecount(all_outputs)); aig_ptr circuit_ptr = - std::make_shared(input_names, output_names, + std::make_shared(input_names_all, output_names_all, n_latches, strat_vec[0].first->get_dict()); aig& circuit = *circuit_ptr; @@ -1770,6 +1783,10 @@ namespace // Reset them for (unsigned i = 0; i < n_outs; ++i) circuit.set_output(i, bdd2var_min(out[i], out_dc[i])); + // Add the unused propositions + const unsigned n_outs_all = output_names_all.size(); + for (unsigned i = n_outs; i < n_outs_all; ++i) + circuit.set_output(i, circuit.aig_false()); for (unsigned i = 0; i < n_latches; ++i) circuit.set_next_latch(i, bdd2var_min(latch[i], bddfalse)); return circuit_ptr; @@ -1832,15 +1849,26 @@ namespace spot check_double_names(all_ap, "Atomic propositions appears in input " "and output propositions; "); } - // Register all to make sure they exist in the aut - std::for_each(ins.begin(), ins.end(), - [s = aut](auto&& e){s->register_ap(e); }); - bdd all_outputs = bddtrue; - std::for_each(outs.begin(), outs.end(), - [&ao = all_outputs, s=aut](auto&& e) - {ao &= bdd_ithvar(s->register_ap(e)); }); + // Check if there exist outs or ins that are not used by the + // strategy + // ins -> simply declare them + // outs -> set them to false + std::vector unused_outs; + std::vector unused_ins; + { + std::set used_aps; + for (const auto& f : aut->ap()) + used_aps.insert(f.ap_name()); + for (const auto& ao : outs) + if (!used_aps.count(ao)) + unused_outs.push_back(ao); + for (const auto& ai : ins) + if (!used_aps.count(ai)) + unused_outs.push_back(ai); + } // todo Some additional checks? - return auts_to_aiger({{aut, all_outputs}}, mode); + return auts_to_aiger({{aut, get_synthesis_outputs(aut)}}, mode, + unused_ins, unused_outs); } // Note: This ignores the named property @@ -1875,22 +1903,32 @@ namespace spot std::vector> new_vec; new_vec.reserve(strat_vec.size()); + std::set used_aps; + for (size_t i = 0; i < strat_vec.size(); ++i) { - // Register all to make sure they exist in the aut - std::for_each(ins.begin(), ins.end(), - [s=strat_vec[i]](auto&& e){s->register_ap(e); }); - bdd this_outputs = bddtrue; - std::for_each(outs[i].begin(), outs[i].end(), - [&to = this_outputs, s=strat_vec[i]](auto&& e) - {to &= bdd_ithvar(s->register_ap(e)); }); - if (this_outputs == bddfalse) - throw std::runtime_error("Inconsistency in outputs of strat " - + std::to_string(i) + ".\n"); + for (const auto& f : strat_vec[i]->ap()) + used_aps.insert(f.ap_name()); // todo Some additional checks? - new_vec.emplace_back(strat_vec[i], this_outputs); + new_vec.emplace_back(strat_vec[i], + get_synthesis_outputs(strat_vec[i])); } - return auts_to_aiger(new_vec, mode); + + // Check if there exist outs or ins that are not used by the + // strategy + // ins -> simply declare them + // outs -> set them to false + std::vector unused_outs; + std::vector unused_ins; + for (const auto& cao : outs) + for (const auto& ao : cao) + if (!used_aps.count(ao)) + unused_outs.push_back(ao); + for (const auto& ai : ins) + if (!used_aps.count(ai)) + unused_outs.push_back(ai); + + return auts_to_aiger(new_vec, mode, unused_ins, unused_outs); } aig_ptr diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 4f09f12a0..410e4ea08 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -437,6 +437,10 @@ namespace spot /// \note The states of each strategy are represented by a block of latches /// not affected by the others. For this to work in a general setting, /// the outputs must be disjoint. + /// \note Attention: Only the propositions actually used in the strategy + /// appear in the aiger circuit. So it can happen that, for instance, + /// propositions marked as output during the call to create_game + /// are absent. SPOT_API aig_ptr strategies_to_aig(const std::vector& strat_vec, const char* mode); @@ -444,12 +448,16 @@ namespace spot /// \brief Like above, but explicitly handing over which propositions /// are inputs and outputs and does therefore not rely on the /// named property "synthesis-outputs" + /// \note All properties in ins and out are guaranteed to appear in the + /// aiger circuit. SPOT_API aig_ptr strategy_to_aig(const twa_graph_ptr& aut, const char *mode, const std::vector& ins, const std::vector& outs); /// \brief Like above, but explicitly handing over the propositions + /// \note All properties in ins and out are guaranteed to appear in the + /// aiger circuit. SPOT_API aig_ptr strategies_to_aig(const std::vector& strat_vec, const char* mode, diff --git a/tests/python/games.ipynb b/tests/python/games.ipynb index 6b44b2343..09073f423 100644 --- a/tests/python/games.ipynb +++ b/tests/python/games.ipynb @@ -47,153 +47,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\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", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -285,153 +285,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\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", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "4\n", + "\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -499,153 +499,153 @@ "\n", "\n", - "\n", "\n", "\n", "\n", - "\n", - "t\n", - "[all]\n", + "\n", + "t\n", + "[all]\n", "\n", "\n", "\n", "0\n", "\n", - "0\n", + "0\n", "\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", "\n", - "1\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", "\n", - "3\n", + "3\n", "\n", "\n", "\n", "0->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2\n", "\n", - "2\n", + "2\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", "\n", - "4\n", + "4\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", "\n", - "6\n", + "6\n", "\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", "\n", - "5\n", + "5\n", "\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7\n", "\n", - "7\n", + "7\n", "\n", "\n", "\n", "6->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "7->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", "\n", - "8\n", + "8\n", "\n", "\n", "\n", "7->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -698,649 +698,649 @@ "\n", "\n", - "\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", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\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", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "i0 & i1\n", - "\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", + "i1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "o0\n", - "\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", "12->1\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "!o0\n", - "\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", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", - "\n", + "\n", + "\n", + "i1\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "!i1\n", - "\n", + "\n", + "\n", + "!i1\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "!o0\n", - "\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", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "!i0\n", - "\n", + "\n", + "\n", + "!i0\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "1\n", - "\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", "5->16\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "1\n", - "\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", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "!i0 & i1\n", - "\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", + "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", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\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", + "o0\n", + "\n", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "i0 & i1\n", - "\n", + "\n", + "\n", + "i0 & i1\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "i0 & !i1\n", - "\n", + "\n", + "\n", + "i0 & !i1\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "!i0 & i1\n", - "\n", + "\n", + "\n", + "!i0 & i1\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "!i0 & !i1\n", - "\n", + "\n", + "\n", + "!i0 & !i1\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "o0\n", - "\n", + "\n", + "\n", + "o0\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "!o0\n", - "\n", + "\n", + "\n", + "!o0\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e12721720> >" + " *' at 0x7f7c803ebb10> >" ] }, "metadata": {}, @@ -1377,588 +1377,588 @@ "\n", "\n", - "\n", "\n", "\n", - "\n", - "\n", - "Inf(\n", - "\n", - ") | (Fin(\n", - "\n", - ") & (Inf(\n", - "\n", - ") | Fin(\n", - "\n", - ")))\n", - "[parity max odd 4]\n", + " viewBox=\"0.00 0.00 650.40 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\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", "\n", "\n", "25\n", - "\n", - "25\n", + "\n", + "25\n", "\n", "\n", "\n", "9->25\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "26\n", - "\n", - "26\n", + "\n", + "26\n", "\n", "\n", "\n", "9->26\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "27\n", - "\n", - "27\n", + "\n", + "27\n", "\n", "\n", "\n", "9->27\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "28\n", - "\n", - "28\n", + "\n", + "28\n", "\n", "\n", "\n", "9->28\n", - "\n", - "\n", - "\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", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "10->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "11->0\n", - "\n", - "\n", - "\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", "12->1\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "13->0\n", - "\n", - "\n", - "\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", + "16\n", "\n", "\n", "\n", "2->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "14->15\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "16->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "3->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17->2\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "17->3\n", - "\n", - "\n", - "\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", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "4->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "18->4\n", - "\n", - "\n", - "\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", "5->16\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "5->18\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "5->19\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "19->5\n", - "\n", - "\n", - "\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", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "6->20\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "21\n", - "\n", - "21\n", + "\n", + "21\n", "\n", "\n", "\n", "6->21\n", - "\n", - "\n", - "\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", "\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", "\n", "\n", "\n", "7->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "22\n", - "\n", - "22\n", + "\n", + "22\n", "\n", "\n", "\n", "7->22\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "23\n", - "\n", - "23\n", + "\n", + "23\n", "\n", "\n", "\n", "7->23\n", - "\n", - "\n", - "\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", "\n", "\n", "\n", "23->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "8->13\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8->17\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "8->23\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24\n", - "\n", - "24\n", + "\n", + "24\n", "\n", "\n", "\n", "8->24\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24->5\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "24->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "25->8\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "26->3\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "27->6\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "28->0\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "\n", + "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -1997,217 +1997,217 @@ "\n", "\n", - "\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", "1->1\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->3\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "1->4\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n", "2->4\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "3->3\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n", "3->4\n", - "\n", - "\n", - "i0 & i1 & o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\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", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "4->4\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n", "4->5\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "5->5\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\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", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "6->6\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n" @@ -2232,123 +2232,123 @@ "\n", "\n", - "\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", "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", "0->2\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "1->2\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "i0 & !i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "!i0 & !i1 & o0\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "i0 & i1 & o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n" @@ -2373,89 +2373,89 @@ "\n", "\n", - "\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", "1->1\n", - "\n", - "\n", - "i0 & i1 & o0\n", + "\n", + "\n", + "i0 & i1 & o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i0 & i1 & o0\n", + "\n", + "\n", + "!i0 & i1 & o0\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "i0 & !i1 & o0\n", + "\n", + "\n", + "i0 & !i1 & o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!i0 & !i1 & o0\n", + "\n", + "\n", + "!i0 & !i1 & o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "i0 & i1 & !o0\n", + "\n", + "\n", + "i0 & i1 & !o0\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i0 & i1 & !o0\n", + "\n", + "\n", + "!i0 & i1 & !o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "i0 & !i1 & !o0\n", + "\n", + "\n", + "i0 & !i1 & !o0\n", "\n", "\n", "\n", "0->0\n", - "\n", - "\n", - "!i0 & !i1 & !o0\n", + "\n", + "\n", + "!i0 & !i1 & !o0\n", "\n", "\n", "\n" @@ -2480,61 +2480,61 @@ "\n", "\n", - "\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", "0->0\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n" @@ -2559,61 +2559,61 @@ "\n", "\n", - "\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", + "\n", "0->0\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n" @@ -2638,61 +2638,61 @@ "\n", "\n", - "\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", "0->0\n", - "\n", - "\n", - "i1 & o0\n", + "\n", + "\n", + "i1 & o0\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "0->1\n", - "\n", - "\n", - "!i1 & o0\n", + "\n", + "\n", + "!i1 & o0\n", "\n", "\n", "\n", "1->0\n", - "\n", - "\n", - "i1 & !o0\n", + "\n", + "\n", + "i1 & !o0\n", "\n", "\n", "\n", "1->1\n", - "\n", - "\n", - "!i1 & !o0\n", + "\n", + "\n", + "!i1 & !o0\n", "\n", "\n", "\n" @@ -2732,405 +2732,405 @@ "\n", "\n", - "\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", "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", "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", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "0->8\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "8->7\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "13\n", - "\n", - "13\n", + "\n", + "13\n", "\n", "\n", "\n", "1->13\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "18\n", - "\n", - "18\n", + "\n", + "18\n", "\n", "\n", "\n", "1->18\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "19\n", - "\n", - "19\n", + "\n", + "19\n", "\n", "\n", "\n", "1->19\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "20\n", - "\n", - "20\n", + "\n", + "20\n", "\n", "\n", "\n", "1->20\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "13->7\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "18->5\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "19->3\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "20->1\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "3->13\n", - "\n", - "\n", - "i1\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "3->19\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "5->10\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "5->11\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "15\n", - "\n", - "15\n", + "\n", + "15\n", "\n", "\n", "\n", "5->15\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "16\n", - "\n", - "16\n", + "\n", + "16\n", "\n", "\n", "\n", "5->16\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "10->9\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "11->7\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "14\n", - "\n", - "14\n", + "\n", + "14\n", "\n", "\n", "\n", "15->14\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "16->5\n", - "\n", - "\n", - "o0\n", + "\n", + "\n", + "o0\n", "\n", "\n", "\n", "7->10\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "7->11\n", - "\n", - "\n", - "i1\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "9->13\n", - "\n", - "\n", - "i1\n", + "\n", + "\n", + "i1\n", "\n", "\n", "\n", "12\n", - "\n", - "12\n", + "\n", + "12\n", "\n", "\n", "\n", "9->12\n", - "\n", - "\n", - "!i1\n", + "\n", + "\n", + "!i1\n", "\n", "\n", "\n", "12->9\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n", "14->13\n", - "\n", - "\n", - "i0 & i1\n", + "\n", + "\n", + "i0 & i1\n", "\n", "\n", "\n", "14->18\n", - "\n", - "\n", - "!i0 & i1\n", + "\n", + "\n", + "!i0 & i1\n", "\n", "\n", "\n", "14->12\n", - "\n", - "\n", - "i0 & !i1\n", + "\n", + "\n", + "i0 & !i1\n", "\n", "\n", "\n", "17\n", - "\n", - "17\n", + "\n", + "17\n", "\n", "\n", "\n", "14->17\n", - "\n", - "\n", - "!i0 & !i1\n", + "\n", + "\n", + "!i0 & !i1\n", "\n", "\n", "\n", "17->14\n", - "\n", - "\n", - "!o0\n", + "\n", + "\n", + "!o0\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e127216c0> >" + " *' at 0x7f7c803ebf90> >" ] }, "execution_count": 11, @@ -3163,253 +3163,253 @@ "\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", + " viewBox=\"0.00 0.00 566.58 353.05\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\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", + "4\n", "\n", "\n", "\n", "I->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "4->11\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "5->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "7->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "10->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "10->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "11->1\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "11->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e12721a50> >" + " *' at 0x7f7c803ebd20> >" ] }, "execution_count": 12, @@ -3526,253 +3526,253 @@ "\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", + " viewBox=\"0.00 0.00 566.58 353.05\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\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", + "4\n", "\n", "\n", "\n", "I->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "4->10\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "11\n", - "\n", - "11\n", + "\n", + "11\n", "\n", "\n", "\n", "4->11\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", + "\n", + "0\n", "\n", "\n", "\n", "5\n", - "\n", - "5\n", + "\n", + "5\n", "\n", "\n", "\n", "0->5\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "0->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "5->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "1->6\n", - "\n", - "\n", - "a\n", - "\n", + "\n", + "\n", + "a\n", + "\n", "\n", "\n", "\n", "7\n", - "\n", - "7\n", + "\n", + "7\n", "\n", "\n", "\n", "1->7\n", - "\n", - "\n", - "!a\n", - "\n", + "\n", + "\n", + "!a\n", + "\n", "\n", "\n", "\n", "7->0\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "8->2\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "9\n", - "\n", - "9\n", + "\n", + "9\n", "\n", "\n", "\n", "3->9\n", - "\n", - "\n", - "1\n", - "\n", + "\n", + "\n", + "1\n", + "\n", "\n", "\n", "\n", "9->2\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "9->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "10->0\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "10->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n", "11->1\n", - "\n", - "\n", - "!b\n", - "\n", + "\n", + "\n", + "!b\n", + "\n", "\n", "\n", "\n", "11->3\n", - "\n", - "\n", - "b\n", - "\n", + "\n", + "\n", + "b\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e12721660> >" + " *' at 0x7f7c803ddea0> >" ] }, "execution_count": 15, @@ -3784,13 +3784,6 @@ "spot.highlight_strategy(game)" ] }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [] - }, { "cell_type": "markdown", "metadata": {}, @@ -3828,8 +3821,7 @@ "i0 a\n", "i1 b\n", "o0 c\n", - "o1 d\n", - "\n" + "o1 d\n" ] } ], @@ -3846,8 +3838,7 @@ "i0 a\n", "i1 b\n", "o0 c\n", - "o1 d\n", - "\"\"\"\n", + "o1 d\"\"\"\n", "print(aag_txt)" ] }, @@ -3871,103 +3862,102 @@ "\n", "\n", - "\n", - "\n", + "\n", "\n", - "\n", - "%3\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "i0\n", + "\n", + "i0\n", "\n", "\n", "\n", "6\n", - "\n", - "6\n", + "\n", + "6\n", "\n", "\n", "\n", "2->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8\n", - "\n", - "8\n", + "\n", + "8\n", "\n", "\n", "\n", "2->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "i1\n", + "\n", + "i1\n", "\n", "\n", "\n", "4->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "10\n", - "\n", - "10\n", + "\n", + "10\n", "\n", "\n", "\n", "6->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o1o1\n", - "\n", - "o1\n", + "\n", + "o1\n", "\n", "\n", "\n", "6->o1o1:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "8->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "o0o0\n", - "\n", - "o0\n", + "\n", + "o0\n", "\n", "\n", "\n", "10->o0o0:s\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" @@ -4004,8 +3994,7 @@ "i0 i0\n", "i1 i1\n", "o0 o0\n", - "o1 o1\n", - "\n" + "o1 o1\n" ] } ], @@ -4052,40 +4041,40 @@ "\n", "\n", - "\n", "\n", - "\n", + "\n", "\n", - "\n", - "t\n", - "[all]\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", "0->0\n", - "\n", - "\n", - "(!i0 & !i1 & !o0 & !o1) | (!i0 & i1 & o0 & !o1) | (i0 & !i1 & o0 & !o1) | (i0 & i1 & !o0 & o1)\n", + "\n", + "\n", + "(!i0 & !i1 & !o0 & !o1) | (!i0 & i1 & o0 & !o1) | (i0 & !i1 & o0 & !o1) | (i0 & i1 & !o0 & o1)\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f7e11cdd0f0> >" + " *' at 0x7f7c804061b0> >" ] }, "metadata": {}, @@ -4098,16 +4087,300 @@ ] }, { - "cell_type": "code", - "execution_count": null, + "cell_type": "markdown", "metadata": {}, - "outputs": [], - "source": [] + "source": [ + "

Incomplete circuit

\n", + "\n", + "

\n", + " It can happen that propositions declared as output are ommited in the aig circuit.\n", + " This happens if the output does not appear in the strategy. Since it does not appear in the\n", + " strategy it can take arbritrary values.\n", + "

" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "True\n" + ] + }, + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\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", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "I->1\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "1->3\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7f7c80406540> >" + ] + }, + "execution_count": 22, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "game = spot.create_game(\"o0\", [\"o0\", \"o1\"])\n", + "print(spot.solve_game(game))\n", + "spot.highlight_strategy(game)" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "L0_out\n", + "\n", + "\n", + "\n", + "o0o0\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "2->o0o0:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "L0\n", + "\n", + "L0\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "Const\n", + "\n", + "\n", + "\n", + "0->L0\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "strat = spot.create_strategy(game)\n", + "aig = spot.strategy_to_aig(strat, \"isop\")\n", + "aig" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "By handing over the input and output propositions explicitly, you can force their appearance of the propositions in the circuit" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "L0_out\n", + "\n", + "\n", + "\n", + "o0o0\n", + "\n", + "o0\n", + "\n", + "\n", + "\n", + "2->o0o0:s\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "L0\n", + "\n", + "L0\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "Const\n", + "\n", + "\n", + "\n", + "0->L0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "o1o1\n", + "\n", + "o1\n", + "\n", + "\n", + "\n", + "0->o1o1:s\n", + "\n", + "\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " >" + ] + }, + "execution_count": 24, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aig2 = spot.strategy_to_aig(strat, \"isop\", [], [\"o0\", \"o1\"])\n", + "aig2" + ] } ], "metadata": { "kernelspec": { - "display_name": "Python 3 (ipykernel)", + "display_name": "Python 3", "language": "python", "name": "python3" }, @@ -4121,7 +4394,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.10" + "version": "3.7.3" } }, "nbformat": 4,