From 760bde093b6b71426c0a8cc3529f36b9f44c2b37 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Sep 2020 15:26:59 +0200 Subject: [PATCH] python: add some parity-game bindings * python/spot/impl.i: Process game.hh. * spot/misc/game.cc, spot/misc/game.hh: Make the output of parity_game_solve() a solved_game object for easier manipulation in Python. * bin/ltlsynt.cc: Adjust usage. * tests/python/paritygame.ipynb: New file. * tests/Makefile.am, doc/org/tut.org: Add it. * NEWS: Mention these bindings. --- NEWS | 5 + bin/ltlsynt.cc | 17 +- doc/org/tut.org | 1 + python/spot/impl.i | 6 +- spot/misc/game.cc | 51 +- spot/misc/game.hh | 28 +- tests/Makefile.am | 1 + tests/python/paritygame.ipynb | 947 ++++++++++++++++++++++++++++++++++ 8 files changed, 1040 insertions(+), 16 deletions(-) create mode 100644 tests/python/paritygame.ipynb diff --git a/NEWS b/NEWS index 1d97f4c83..1e87d29fc 100644 --- a/NEWS +++ b/NEWS @@ -79,6 +79,11 @@ New in spot 2.9.4.dev (not yet released) - print_dot() will display states from player 1 using a diamond shape. + Python: + + - Bindings for functions related to parity games. + See https://spot.lrde.epita.fr/ipynb/paritygame.html for examples. + New in spot 2.9.4 (2020-09-07) Bugs fixed: diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 09bbe02fb..b5fa67bac 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -216,11 +216,10 @@ namespace static spot::twa_graph_ptr strat_to_aut(const spot::const_twa_graph_ptr& pg, const spot::strategy_t& strat, - const spot::twa_graph_ptr& dpa, bdd all_outputs) { - auto aut = spot::make_twa_graph(dpa->get_dict()); - aut->copy_ap_of(dpa); + auto aut = spot::make_twa_graph(pg->get_dict()); + aut->copy_ap_of(pg); unsigned pg_init = pg->get_init_state_number(); std::vector todo{pg_init}; std::vector pg2aut(pg->num_states(), -1); @@ -230,10 +229,10 @@ namespace { unsigned s = todo.back(); todo.pop_back(); - for (auto& e1: dpa->out(s)) + for (auto& e1: pg->out(s)) { unsigned i = 0; - for (auto& e2: dpa->out(e1.dst)) + for (auto& e2: pg->out(e1.dst)) { bool self_loop = false; if (e1.dst == s || e2.dst == e1.dst) @@ -520,18 +519,16 @@ namespace return 0; } - spot::strategy_t strategy[2]; - spot::region_t winning_region[2]; if (want_time) sw.start(); - parity_game_solve(dpa, winning_region, strategy); + auto solution = parity_game_solve(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 (winning_region[1].count(dpa->get_init_state_number())) + if (solution.player_winning_at(1, dpa->get_init_state_number())) { std::cout << "REALIZABLE\n"; if (!opt_real) @@ -539,7 +536,7 @@ namespace if (want_time) sw.start(); auto strat_aut = - strat_to_aut(dpa, strategy[1], dpa, all_outputs); + strat_to_aut(dpa, solution.winning_strategy[1], all_outputs); if (want_time) strat2aut_time = sw.stop(); diff --git a/doc/org/tut.org b/doc/org/tut.org index 187e18144..67f1eae92 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -72,6 +72,7 @@ real notebooks instead. automata - [[https://spot.lrde.epita.fr/ipynb/parity.html][=parity.ipynb=]] documents algorithms for manipulating parity automata in Python +- [[https://spot.lrde.epita.fr/ipynb/paritygame.html][=paritygame.ipynb=]] illustrates support for parity games - [[https://spot.lrde.epita.fr/ipynb/product.html][=product.ipynb=]] shows how to re-implement the product of two automata in Python - [[https://spot.lrde.epita.fr/ipynb/randltl.html][=randltl.ipynb=]] demonstrates a Python-version of [[file:randltl.org][=randltl=]] diff --git a/python/spot/impl.i b/python/spot/impl.i index d5e4bb415..44fe1f480 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -164,6 +164,8 @@ #include +#include + #include #include #include @@ -690,6 +692,8 @@ def state_is_accepting(self, src) -> "bool": %include +%include + %include %include %include diff --git a/spot/misc/game.cc b/spot/misc/game.cc index f4a4cd21a..5751ecd4f 100644 --- a/spot/misc/game.cc +++ b/spot/misc/game.cc @@ -230,9 +230,11 @@ namespace spot } } - void parity_game_solve(const const_twa_graph_ptr& arena, - region_t (&w)[2], strategy_t (&s)[2]) + solved_game parity_game_solve(const const_twa_graph_ptr& arena) { + solved_game result; + result.arena = arena; + const std::vector* owner = ensure_parity_game(arena, "parity_game_solve"); @@ -245,7 +247,10 @@ namespace spot for (const auto& e: arena->edges()) m |= e.acc; - solve_rec(arena, owner, states_, m.max_set(), w, s); + solve_rec(arena, owner, states_, m.max_set(), + result.winning_region, result.winning_strategy); + + return result; } void propagate_players(spot::twa_graph_ptr& arena, @@ -304,4 +309,44 @@ namespace spot arena->set_named_prop("state-player", owner); } + + twa_graph_ptr + highlight_strategy(twa_graph_ptr& aut, const strategy_t& s, + unsigned color) + { + unsigned ns = aut->num_states(); + auto* highlight = aut->get_or_set_named_prop> + ("highlight-edges"); + + for (auto [src, n]: s) + { + if (src >= ns) + throw std::runtime_error + ("highlight_strategy(): strategy refers to unexisting states"); + unsigned int i = 0; + for (auto& t: aut->out(src)) + if (i++ == n) + { + (*highlight)[aut->edge_number(t)] = color; + break; + } + } + + return aut; + } + + twa_graph_ptr + solved_game::highlight_strategy(unsigned player, unsigned color) + { + auto aut = std::const_pointer_cast(arena); + + auto* highlight = aut->get_or_set_named_prop> + ("highlight-states"); + unsigned ns = aut->num_states(); + for (unsigned i = 0; i < ns; ++i) + if (player_winning_at(player, i)) + (*highlight)[i] = color; + + return spot::highlight_strategy(aut, winning_strategy[!!player], color); + } } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index b6cf30d22..5b133a206 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -50,6 +50,24 @@ namespace spot typedef std::unordered_set region_t; typedef std::unordered_map strategy_t; + + struct SPOT_API solved_game + { + const_twa_graph_ptr arena; + + region_t winning_region[2]; + strategy_t winning_strategy[2]; + + /// \brief Highlight the edges of a strategy on the automaton. + twa_graph_ptr highlight_strategy(unsigned player, unsigned color); + + bool player_winning_at(unsigned player, unsigned state) + { + auto& w = winning_region[player]; + return w.find(state) != w.end(); + } + }; + /// \brief solve a parity-game /// /// The arena is a deterministic max odd parity automaton with a @@ -59,10 +77,16 @@ namespace spot /// game for player 1 using Zielonka's recursive algorithm. /// \cite zielonka.98.tcs SPOT_API - void parity_game_solve(const const_twa_graph_ptr& arena, - region_t (&w)[2], strategy_t (&s)[2]); + solved_game parity_game_solve(const const_twa_graph_ptr& arena); /// \brief Print a max odd parity game using PG-solver syntax SPOT_API void pg_print(std::ostream& os, const const_twa_graph_ptr& arena); + + + /// \brief Highlight the edges of a strategy on an automaton. + SPOT_API + twa_graph_ptr highlight_strategy(twa_graph_ptr& arena, + const strategy_t& s, + unsigned color); } diff --git a/tests/Makefile.am b/tests/Makefile.am index cd291c7cf..6f5494e3b 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -362,6 +362,7 @@ TESTS_ipython = \ python/ltsmin-dve.ipynb \ python/ltsmin-pml.ipynb \ python/parity.ipynb \ + python/paritygame.ipynb \ python/product.ipynb \ python/randaut.ipynb \ python/randltl.ipynb \ diff --git a/tests/python/paritygame.ipynb b/tests/python/paritygame.ipynb new file mode 100644 index 000000000..14feb4a17 --- /dev/null +++ b/tests/python/paritygame.ipynb @@ -0,0 +1,947 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "metadata": {}, + "outputs": [], + "source": [ + "import spot\n", + "spot.setup()" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Support for parity games\n", + "\n", + "The support for parity games is currently quite rudimentary, as Spot currently only uses those games in `ltlsynt`.\n", + "\n", + "In essence, a parity game is just a parity automaton with a property named `state-player` that stores the player owning each state. The players are named 0 and 1.\n", + "\n", + "Player 1 is winning if it has a strategy to satisfy the acceptance condition regardless of player 0's moves.\n", + "Player 0 is winning if it has a strategy to not satisfy the acceptance codition regardless of player 1's moves." + ] + }, + { + "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": 2, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + "))\n", + "[parity max odd 3]\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", + "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", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "9->10\n", + "\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "10->9\n", + "\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcb3c55f9f0> >" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "game = spot.automaton(\"ltlsynt --ins=a --outs=b -f '!b & GFa <-> Gb' --print-game-hoa |\");\n", + "game" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "In the graphical output, player 0 is represented by circles (or ellipses or rounded rectangles depending on the situations), while player 1's states are diamond shaped. In the case of `ltlsynt`, player 0 plays the role of the environment, and player 1 plays the role of the controler.\n", + "\n", + "In the HOA output, a header `spot-state-player` (or `spot.state-player` in HOA 1.1) lists the owner of each state." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "HOA: v1\n", + "States: 11\n", + "Start: 0\n", + "AP: 2 \"b\" \"a\"\n", + "acc-name: parity max odd 3\n", + "Acceptance: 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", + "--BODY--\n", + "State: 0\n", + "[!1] 1 {1}\n", + "[1] 2 {1}\n", + "State: 1\n", + "[!0] 3 {1}\n", + "[0] 4 {1}\n", + "State: 2\n", + "[0] 4 {1}\n", + "[!0] 5 {1}\n", + "State: 3\n", + "[!1] 6 {1}\n", + "[1] 7 {2}\n", + "State: 4\n", + "[t] 8 {2}\n", + "State: 5\n", + "[1] 7 {2}\n", + "[!1] 6 {1}\n", + "State: 6\n", + "[t] 3 {1}\n", + "State: 7\n", + "[t] 5 {2}\n", + "State: 8\n", + "[0] 4 {2}\n", + "[!0] 9 {1}\n", + "State: 9\n", + "[t] 10 {1}\n", + "State: 10\n", + "[t] 9 {1}\n", + "--END--\n" + ] + } + ], + "source": [ + "print(game.to_str('hoa'))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Solving games" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The `parity_game_solve()` function returns a `solved_game` object." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": {}, + "outputs": [], + "source": [ + "sol = spot.parity_game_solve(game)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The solved game can be queried to know if a player is winning when the game starts in some given." + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "sol.player_winning_at(1, game.get_init_state_number())" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Calling the `highlight_strategy` method will decorate the original game with colors showing the winning region (states from which a player has a strategy to win), and strategy (which transition should be used for each winning state owned by that player) of a given player. Let's paint the strategy of player 1 in green (color 4) for this example:" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + "))\n", + "[parity max odd 3]\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", + "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", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "9->10\n", + "\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "10->9\n", + "\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcb3c55a1e0> >" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "sol.highlight_strategy(1, 4)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Because `highlight_strategy` simply decorates the original automaton, we can call it a second time to show that player 0 could win if it had a way to reach the red (color 5) region and play the red strategy." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": {}, + "outputs": [ + { + "data": { + "image/svg+xml": [ + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + "))\n", + "[parity max odd 3]\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", + "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", + "\n", + "10\n", + "\n", + "10\n", + "\n", + "\n", + "\n", + "9->10\n", + "\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n", + "10->9\n", + "\n", + "\n", + "1\n", + "❶\n", + "\n", + "\n", + "\n" + ], + "text/plain": [ + " *' at 0x7fcb3c55a900> >" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "sol.highlight_strategy(0, 5)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.8.5" + } + }, + "nbformat": 4, + "nbformat_minor": 4 +}