{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "c54c43ba",
   "metadata": {},
   "outputs": [],
   "source": [
    "import spot, buddy\n",
    "spot.setup()"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0576f64a",
   "metadata": {},
   "source": [
    "Additional testing for synthesis"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e25b7989",
   "metadata": {},
   "source": [
    "Testing the different methods to solve"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "007107a6",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "si = spot.synthesis_info()\n",
    "si.s = spot.synthesis_info.algo_LAR # Use LAR algorithm\n",
    "game = spot.ltl_to_game(\"G((F(i0) && F(i1))->(G(i1<->(X(o0)))))\", [\"o0\"], si)\n",
    "spot.solve_game(game)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "a7859f19",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "HOA: v1\n",
      "States: 21\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 2\n",
      "[!0&1] 4\n",
      "[0&!1] 6\n",
      "[0&1] 8\n",
      "State: 1\n",
      "[0&1] 13\n",
      "[0&!1] 18\n",
      "[!0&1] 19\n",
      "[!0&!1] 20\n",
      "State: 2\n",
      "[t] 1\n",
      "State: 3\n",
      "[0] 13\n",
      "[!0] 19\n",
      "State: 4\n",
      "[t] 3\n",
      "State: 5\n",
      "[!0&1] 10\n",
      "[0&1] 11\n",
      "[!0&!1] 15\n",
      "[0&!1] 16\n",
      "State: 6\n",
      "[t] 5\n",
      "State: 7\n",
      "[!0] 10\n",
      "[0] 11\n",
      "State: 8\n",
      "[t] 7\n",
      "State: 9\n",
      "[!0] 12\n",
      "[0] 13\n",
      "State: 10\n",
      "[2] 9\n",
      "State: 11\n",
      "[2] 7\n",
      "State: 12\n",
      "[!2] 9\n",
      "State: 13\n",
      "[!2] 7\n",
      "State: 14\n",
      "[!0&1] 12\n",
      "[0&1] 13\n",
      "[!0&!1] 17\n",
      "[0&!1] 18\n",
      "State: 15\n",
      "[2] 14\n",
      "State: 16\n",
      "[2] 5\n",
      "State: 17\n",
      "[!2] 14\n",
      "State: 18\n",
      "[!2] 5\n",
      "State: 19\n",
      "[!2] 3\n",
      "State: 20\n",
      "[!2] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 7\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 1\n",
      "[!0&1] 2\n",
      "[0&!1] 3\n",
      "[0&1] 4\n",
      "State: 1\n",
      "[0&1&!2] 4\n",
      "[0&!1&!2] 3\n",
      "[!0&1&!2] 2\n",
      "[!0&!1&!2] 1\n",
      "State: 2\n",
      "[0&!2] 4\n",
      "[!0&!2] 2\n",
      "State: 3\n",
      "[!0&1&2] 5\n",
      "[0&1&2] 4\n",
      "[!0&!1&2] 6\n",
      "[0&!1&2] 3\n",
      "State: 4\n",
      "[!0&2] 5\n",
      "[0&2] 4\n",
      "State: 5\n",
      "[!0&!2] 5\n",
      "[0&!2] 4\n",
      "State: 6\n",
      "[!0&1&!2] 5\n",
      "[0&1&!2] 4\n",
      "[!0&!1&!2] 6\n",
      "[0&!1&!2] 3\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 21\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 2\n",
      "[!0&1] 4\n",
      "[0&!1] 6\n",
      "[0&1] 8\n",
      "State: 1\n",
      "[0&1] 13\n",
      "[0&!1] 18\n",
      "[!0&1] 19\n",
      "[!0&!1] 20\n",
      "State: 2\n",
      "[t] 1\n",
      "State: 3\n",
      "[0] 13\n",
      "[!0] 19\n",
      "State: 4\n",
      "[t] 3\n",
      "State: 5\n",
      "[!0&1] 10\n",
      "[0&1] 11\n",
      "[!0&!1] 15\n",
      "[0&!1] 16\n",
      "State: 6\n",
      "[t] 5\n",
      "State: 7\n",
      "[!0] 10\n",
      "[0] 11\n",
      "State: 8\n",
      "[t] 7\n",
      "State: 9\n",
      "[!0] 12\n",
      "[0] 13\n",
      "State: 10\n",
      "[2] 9\n",
      "State: 11\n",
      "[2] 7\n",
      "State: 12\n",
      "[!2] 9\n",
      "State: 13\n",
      "[!2] 7\n",
      "State: 14\n",
      "[!0&1] 12\n",
      "[0&1] 13\n",
      "[!0&!1] 17\n",
      "[0&!1] 18\n",
      "State: 15\n",
      "[2] 14\n",
      "State: 16\n",
      "[2] 5\n",
      "State: 17\n",
      "[!2] 14\n",
      "State: 18\n",
      "[!2] 5\n",
      "State: 19\n",
      "[!2] 3\n",
      "State: 20\n",
      "[!2] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 21\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 2\n",
      "[!0&1] 4\n",
      "[0&!1] 6\n",
      "[0&1] 8\n",
      "State: 1\n",
      "[0&1] 13\n",
      "[0&!1] 18\n",
      "[!0&1] 19\n",
      "[!0&!1] 20\n",
      "State: 2\n",
      "[t] 1\n",
      "State: 3\n",
      "[0] 13\n",
      "[!0] 19\n",
      "State: 4\n",
      "[t] 3\n",
      "State: 5\n",
      "[!0&1] 10\n",
      "[0&1] 11\n",
      "[!0&!1] 15\n",
      "[0&!1] 16\n",
      "State: 6\n",
      "[t] 5\n",
      "State: 7\n",
      "[!0] 10\n",
      "[0] 11\n",
      "State: 8\n",
      "[t] 7\n",
      "State: 9\n",
      "[!0] 12\n",
      "[0] 13\n",
      "State: 10\n",
      "[2] 9\n",
      "State: 11\n",
      "[2] 7\n",
      "State: 12\n",
      "[!2] 9\n",
      "State: 13\n",
      "[!2] 7\n",
      "State: 14\n",
      "[!0&1] 12\n",
      "[0&1] 13\n",
      "[!0&!1] 17\n",
      "[0&!1] 18\n",
      "State: 15\n",
      "[2] 14\n",
      "State: 16\n",
      "[2] 5\n",
      "State: 17\n",
      "[!2] 14\n",
      "State: 18\n",
      "[!2] 5\n",
      "State: 19\n",
      "[!2] 3\n",
      "State: 20\n",
      "[!2] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 7\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 1\n",
      "[!0&1] 2\n",
      "[0&!1] 3\n",
      "[0&1] 4\n",
      "State: 1\n",
      "[0&1&!2] 4\n",
      "[0&!1&!2] 3\n",
      "[!0&1&!2] 2\n",
      "[!0&!1&!2] 1\n",
      "State: 2\n",
      "[0&!2] 4\n",
      "[!0&!2] 2\n",
      "State: 3\n",
      "[!0&1&2] 5\n",
      "[0&1&2] 4\n",
      "[!0&!1&2] 6\n",
      "[0&!1&2] 3\n",
      "State: 4\n",
      "[!0&2] 5\n",
      "[0&2] 4\n",
      "State: 5\n",
      "[!0&!2] 5\n",
      "[0&!2] 4\n",
      "State: 6\n",
      "[!0&1&!2] 5\n",
      "[0&1&!2] 4\n",
      "[!0&!1&!2] 6\n",
      "[0&!1&!2] 3\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 21\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 2\n",
      "[!0&1] 4\n",
      "[0&!1] 6\n",
      "[0&1] 8\n",
      "State: 1\n",
      "[0&1] 13\n",
      "[0&!1] 18\n",
      "[!0&1] 19\n",
      "[!0&!1] 20\n",
      "State: 2\n",
      "[t] 1\n",
      "State: 3\n",
      "[0] 13\n",
      "[!0] 19\n",
      "State: 4\n",
      "[t] 3\n",
      "State: 5\n",
      "[!0&1] 10\n",
      "[0&1] 11\n",
      "[!0&!1] 15\n",
      "[0&!1] 16\n",
      "State: 6\n",
      "[t] 5\n",
      "State: 7\n",
      "[!0] 10\n",
      "[0] 11\n",
      "State: 8\n",
      "[t] 7\n",
      "State: 9\n",
      "[!0] 12\n",
      "[0] 13\n",
      "State: 10\n",
      "[2] 9\n",
      "State: 11\n",
      "[2] 7\n",
      "State: 12\n",
      "[!2] 9\n",
      "State: 13\n",
      "[!2] 7\n",
      "State: 14\n",
      "[!0&1] 12\n",
      "[0&1] 13\n",
      "[!0&!1] 17\n",
      "[0&!1] 18\n",
      "State: 15\n",
      "[2] 14\n",
      "State: 16\n",
      "[2] 5\n",
      "State: 17\n",
      "[!2] 14\n",
      "State: 18\n",
      "[!2] 5\n",
      "State: 19\n",
      "[!2] 3\n",
      "State: 20\n",
      "[!2] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 21\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 2\n",
      "[!0&1] 4\n",
      "[0&!1] 6\n",
      "[0&1] 8\n",
      "State: 1\n",
      "[0&1] 13\n",
      "[0&!1] 18\n",
      "[!0&1] 19\n",
      "[!0&!1] 20\n",
      "State: 2\n",
      "[t] 1\n",
      "State: 3\n",
      "[0] 13\n",
      "[!0] 19\n",
      "State: 4\n",
      "[t] 3\n",
      "State: 5\n",
      "[!0&1] 10\n",
      "[0&1] 11\n",
      "[!0&!1] 15\n",
      "[0&!1] 16\n",
      "State: 6\n",
      "[t] 5\n",
      "State: 7\n",
      "[!0] 10\n",
      "[0] 11\n",
      "State: 8\n",
      "[t] 7\n",
      "State: 9\n",
      "[!0] 12\n",
      "[0] 13\n",
      "State: 10\n",
      "[2] 9\n",
      "State: 11\n",
      "[2] 7\n",
      "State: 12\n",
      "[!2] 9\n",
      "State: 13\n",
      "[!2] 7\n",
      "State: 14\n",
      "[!0&1] 12\n",
      "[0&1] 13\n",
      "[!0&!1] 17\n",
      "[0&!1] 18\n",
      "State: 15\n",
      "[2] 14\n",
      "State: 16\n",
      "[2] 5\n",
      "State: 17\n",
      "[!2] 14\n",
      "State: 18\n",
      "[!2] 5\n",
      "State: 19\n",
      "[!2] 3\n",
      "State: 20\n",
      "[!2] 1\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 7\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 1\n",
      "[!0&1] 2\n",
      "[0&!1] 3\n",
      "[0&1] 4\n",
      "State: 1\n",
      "[0&1&!2] 4\n",
      "[0&!1&!2] 3\n",
      "[!0&1&!2] 2\n",
      "[!0&!1&!2] 1\n",
      "State: 2\n",
      "[0&!2] 4\n",
      "[!0&!2] 2\n",
      "State: 3\n",
      "[!0&1&2] 5\n",
      "[0&1&2] 4\n",
      "[!0&!1&2] 6\n",
      "[0&!1&2] 3\n",
      "State: 4\n",
      "[!0&2] 5\n",
      "[0&2] 4\n",
      "State: 5\n",
      "[!0&!2] 5\n",
      "[0&!2] 4\n",
      "State: 6\n",
      "[!0&1&!2] 5\n",
      "[0&1&!2] 4\n",
      "[!0&!1&!2] 6\n",
      "[0&!1&!2] 3\n",
      "--END--\n",
      "HOA: v1\n",
      "States: 21\n",
      "Start: 0\n",
      "AP: 3 \"i1\" \"i0\" \"o0\"\n",
      "acc-name: all\n",
      "Acceptance: 0 t\n",
      "properties: trans-labels explicit-labels state-acc deterministic\n",
      "spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 1 1 1 0 1 1 1 1 1 1\n",
      "controllable-AP: 2\n",
      "--BODY--\n",
      "State: 0\n",
      "[!0&!1] 2\n",
      "[!0&1] 4\n",
      "[0&!1] 6\n",
      "[0&1] 8\n",
      "State: 1\n",
      "[0&1] 13\n",
      "[0&!1] 18\n",
      "[!0&1] 19\n",
      "[!0&!1] 20\n",
      "State: 2\n",
      "[t] 1\n",
      "State: 3\n",
      "[0] 13\n",
      "[!0] 19\n",
      "State: 4\n",
      "[t] 3\n",
      "State: 5\n",
      "[!0&1] 10\n",
      "[0&1] 11\n",
      "[!0&!1] 15\n",
      "[0&!1] 16\n",
      "State: 6\n",
      "[t] 5\n",
      "State: 7\n",
      "[!0] 10\n",
      "[0] 11\n",
      "State: 8\n",
      "[t] 7\n",
      "State: 9\n",
      "[!0] 12\n",
      "[0] 13\n",
      "State: 10\n",
      "[2] 9\n",
      "State: 11\n",
      "[2] 7\n",
      "State: 12\n",
      "[!2] 9\n",
      "State: 13\n",
      "[!2] 7\n",
      "State: 14\n",
      "[!0&1] 12\n",
      "[0&1] 13\n",
      "[!0&!1] 17\n",
      "[0&!1] 18\n",
      "State: 15\n",
      "[2] 14\n",
      "State: 16\n",
      "[2] 5\n",
      "State: 17\n",
      "[!2] 14\n",
      "State: 18\n",
      "[!2] 5\n",
      "State: 19\n",
      "[!2] 3\n",
      "State: 20\n",
      "[!2] 1\n",
      "--END--\n"
     ]
    }
   ],
   "source": [
    "si.minimize_lvl = 0\n",
    "mm0 = spot.solved_game_to_mealy(game, si)\n",
    "msep0 = spot.solved_game_to_separated_mealy(game, si)\n",
    "msplit0 = spot.solved_game_to_split_mealy(game, si)\n",
    "assert(spot.is_mealy(mm0))\n",
    "assert(spot.is_separated_mealy(msep0))\n",
    "assert(spot.is_split_mealy(msplit0))\n",
    "print(mm0.to_str(\"hoa\"))\n",
    "print(msep0.to_str(\"hoa\"))\n",
    "print(msplit0.to_str(\"hoa\"))\n",
    "si.minimize_lvl = 2\n",
    "mm2 = spot.solved_game_to_mealy(game, si)\n",
    "msep2 = spot.solved_game_to_separated_mealy(game, si)\n",
    "msplit2 = spot.solved_game_to_split_mealy(game, si)\n",
    "assert(spot.is_mealy(mm2))\n",
    "assert(spot.is_separated_mealy(msep2))\n",
    "assert(spot.is_split_mealy(msplit2))\n",
    "print(mm2.to_str(\"hoa\"))\n",
    "print(msep2.to_str(\"hoa\"))\n",
    "print(msplit2.to_str(\"hoa\"))\n",
    "si.minimize_lvl = 3\n",
    "mm3 = spot.solved_game_to_mealy(game, si)\n",
    "msep3 = spot.solved_game_to_separated_mealy(game, si)\n",
    "msplit3 = spot.solved_game_to_split_mealy(game, si)\n",
    "assert(spot.is_mealy(mm3))\n",
    "assert(spot.is_separated_mealy(msep3))\n",
    "assert(spot.is_split_mealy(msplit3))\n",
    "print(mm3.to_str(\"hoa\"))\n",
    "print(msep3.to_str(\"hoa\"))\n",
    "print(msplit3.to_str(\"hoa\"))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "fb57ac53",
   "metadata": {},
   "outputs": [],
   "source": [
    "mus0 = spot.unsplit_mealy(msplit0)\n",
    "mus2 = spot.unsplit_mealy(msplit2)\n",
    "mus3 = spot.unsplit_mealy(msplit3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "40fc65b5",
   "metadata": {},
   "outputs": [],
   "source": [
    "assert(mus0.equivalent_to(msep0))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "f6d8b29c",
   "metadata": {},
   "outputs": [],
   "source": [
    "assert(mus2.equivalent_to(msep2))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "db8d47f2",
   "metadata": {},
   "outputs": [],
   "source": [
    "assert(mus3.equivalent_to(msep3))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c19beeb0",
   "metadata": {},
   "source": [
    "Testing related to #495"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "3736cd1b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(0, t)\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.43.0 (0)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"244pt\" height=\"115pt\"\n",
       " viewBox=\"0.00 0.00 244.00 115.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 111)\">\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-111 240,-111 240,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"115\" y=\"-91.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
       "<text text-anchor=\"start\" x=\"107\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
       "<!-- I -->\n",
       "<!-- 1 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;1 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"218\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"218\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M74.12,-18C102.48,-18 159.32,-18 192.12,-18\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"199.52,-18 192.52,-21.15 196.02,-18 192.52,-18 192.52,-18 192.52,-18 196.02,-18 192.52,-14.85 199.52,-18 199.52,-18\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-21.8\" font-family=\"Lato\" font-size=\"14.00\">(!i &amp; !o) | (i &amp; o)</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M205.29,-31.29C199.86,-42.4 204.09,-54 218,-54 229.08,-54 234.02,-46.63 232.82,-38.02\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"230.71,-31.29 235.81,-37.03 231.76,-34.63 232.81,-37.97 232.81,-37.97 232.81,-37.97 231.76,-34.63 229.8,-38.91 230.71,-31.29 230.71,-31.29\"/>\n",
       "<text text-anchor=\"middle\" x=\"218\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7458055570> >"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a = spot.translate(\"i<->o\", \"parity\")\n",
    "print(a.acc())\n",
    "a"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "da6a7802",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.43.0 (0)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"206pt\" height=\"85pt\"\n",
       " viewBox=\"0.00 0.00 205.50 85.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 81)\">\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-81 201.5,-81 201.5,4 -4,4\"/>\n",
       "<!-- I -->\n",
       "<!-- 1 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;1 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-18C2.79,-18 17.15,-18 30.63,-18\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-18 30.94,-21.15 34.44,-18 30.94,-18 30.94,-18 30.94,-18 34.44,-18 30.94,-14.85 37.94,-18 37.94,-18\"/>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"175\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"175\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M74.01,-18C93.94,-18 127.11,-18 149.73,-18\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"156.97,-18 149.97,-21.15 153.47,-18 149.97,-18 149.97,-18 149.97,-18 153.47,-18 149.97,-14.85 156.97,-18 156.97,-18\"/>\n",
       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94.5,-41 94.5,-60 105.5,-60 105.5,-41 94.5,-41\"/>\n",
       "<text text-anchor=\"start\" x=\"96.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">!i</text>\n",
       "<text text-anchor=\"start\" x=\"109.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"120.5,-41 120.5,-60 137.5,-60 137.5,-41 120.5,-41\"/>\n",
       "<text text-anchor=\"start\" x=\"122.5\" y=\"-46.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94.5,-20 94.5,-39 105.5,-39 105.5,-20 94.5,-20\"/>\n",
       "<text text-anchor=\"start\" x=\"99.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">i</text>\n",
       "<text text-anchor=\"start\" x=\"109.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"120.5,-20 120.5,-39 137.5,-39 137.5,-20 120.5,-20\"/>\n",
       "<text text-anchor=\"start\" x=\"122.5\" y=\"-25.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;0 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M165.19,-33.17C162.21,-43.66 165.48,-54 175,-54 182.29,-54 185.91,-47.94 185.87,-40.39\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"184.81,-33.17 188.95,-39.63 185.32,-36.63 185.83,-40.09 185.83,-40.09 185.83,-40.09 185.32,-36.63 182.71,-40.55 184.81,-33.17 184.81,-33.17\"/>\n",
       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"155,-55.5 155,-74.5 168,-74.5 168,-55.5 155,-55.5\"/>\n",
       "<text text-anchor=\"start\" x=\"157\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "<text text-anchor=\"start\" x=\"172\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"183,-55.5 183,-74.5 196,-74.5 196,-55.5 183,-55.5\"/>\n",
       "<text text-anchor=\"start\" x=\"185\" y=\"-61.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7458055570> >"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "spot.set_synthesis_outputs(a, buddy.bdd_ithvar(a.register_ap(\"o\")))\n",
    "a"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "987219a4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(0, t)\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.43.0 (0)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"363pt\" height=\"136pt\"\n",
       " viewBox=\"0.00 0.00 363.00 136.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 132)\">\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-132 359,-132 359,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"174.5\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
       "<text text-anchor=\"start\" x=\"166.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
       "<!-- I -->\n",
       "<!-- 1 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;1 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-45C2.79,-45 17.15,-45 30.63,-45\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-45 30.94,-48.15 34.44,-45 30.94,-45 30.94,-45 30.94,-45 34.44,-45 30.94,-41.85 37.94,-45 37.94,-45\"/>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>3</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"144,-90 117,-72 144,-54 171,-72 144,-90\"/>\n",
       "<text text-anchor=\"middle\" x=\"144\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;3 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M73.58,-50.21C86.33,-54.21 104.15,-59.8 118.53,-64.32\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"125.29,-66.44 117.66,-67.35 121.95,-65.39 118.61,-64.34 118.61,-64.34 118.61,-64.34 121.95,-65.39 119.55,-61.34 125.29,-66.44 125.29,-66.44\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">!i</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>4</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"144,-36 117,-18 144,0 171,-18 144,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"144\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M73.58,-39.79C86.33,-35.79 104.15,-30.2 118.53,-25.68\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"125.29,-23.56 119.55,-28.66 121.95,-24.61 118.61,-25.66 118.61,-25.66 118.61,-25.66 121.95,-24.61 117.66,-22.65 125.29,-23.56 125.29,-23.56\"/>\n",
       "<text text-anchor=\"start\" x=\"93.5\" y=\"-36.8\" font-family=\"Lato\" font-size=\"14.00\">i</text>\n",
       "</g>\n",
       "<!-- 0 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"238\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"238\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"328,-63 301,-45 328,-27 355,-45 328,-63\"/>\n",
       "<text text-anchor=\"middle\" x=\"328\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;2 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M256.39,-45C267.02,-45 280.98,-45 293.68,-45\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"300.97,-45 293.97,-48.15 297.47,-45 293.97,-45 293.97,-45 293.97,-45 297.47,-45 293.97,-41.85 300.97,-45 300.97,-45\"/>\n",
       "<text text-anchor=\"middle\" x=\"278.5\" y=\"-48.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;0 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>2&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M314.15,-35.81C303.54,-29.35 288.02,-22.44 274,-26 269.14,-27.23 264.22,-29.3 259.67,-31.62\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"253.31,-35.13 257.91,-28.99 256.37,-33.44 259.44,-31.74 259.44,-31.74 259.44,-31.74 256.37,-33.44 260.96,-34.5 253.31,-35.13 253.31,-35.13\"/>\n",
       "<text text-anchor=\"middle\" x=\"278.5\" y=\"-29.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;0 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>3&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M163.18,-66.67C177.62,-62.43 197.92,-56.47 213.58,-51.87\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"220.41,-49.87 214.58,-54.86 217.05,-50.86 213.69,-51.84 213.69,-51.84 213.69,-51.84 217.05,-50.86 212.8,-48.82 220.41,-49.87 220.41,-49.87\"/>\n",
       "<text text-anchor=\"start\" x=\"189\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;0 -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>4&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M163.18,-23.33C177.62,-27.57 197.92,-33.53 213.58,-38.13\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"220.41,-40.13 212.8,-41.18 217.05,-39.14 213.69,-38.16 213.69,-38.16 213.69,-38.16 217.05,-39.14 214.58,-35.14 220.41,-40.13 220.41,-40.13\"/>\n",
       "<text text-anchor=\"start\" x=\"191\" y=\"-37.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f74580553c0> >"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a_s = spot.split_2step(a, True)\n",
    "print(a.acc())\n",
    "a_s"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "958d81f2",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.43.0 (0)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"326pt\" height=\"108pt\"\n",
       " viewBox=\"0.00 0.00 326.00 108.23\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 104.23)\">\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-104.23 322,-104.23 322,4 -4,4\"/>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-42.23C2.79,-42.23 17.15,-42.23 30.63,-42.23\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-42.23 30.94,-45.38 34.44,-42.23 30.94,-42.23 30.94,-42.23 30.94,-42.23 34.44,-42.23 30.94,-39.08 37.94,-42.23 37.94,-42.23\"/>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"176\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"176\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;1 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M72.74,-48.86C78.67,-51.03 85.54,-53.15 92,-54.23 113.04,-57.73 118.96,-57.73 140,-54.23 144.14,-53.54 148.45,-52.42 152.57,-51.13\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"159.26,-48.86 153.64,-54.09 155.94,-49.99 152.63,-51.11 152.63,-51.11 152.63,-51.11 155.94,-49.99 151.62,-48.13 159.26,-48.86 159.26,-48.86\"/>\n",
       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94,-79.23 94,-98.23 110,-98.23 110,-79.23 94,-79.23\"/>\n",
       "<text text-anchor=\"start\" x=\"96\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
       "<text text-anchor=\"start\" x=\"114\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"125,-79.23 125,-98.23 138,-98.23 138,-79.23 125,-79.23\"/>\n",
       "<text text-anchor=\"start\" x=\"127\" y=\"-85.03\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
       "<text text-anchor=\"start\" x=\"108\" y=\"-64.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;0 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M165.21,-27.48C159.03,-19.57 150.28,-10.57 140,-6.23 120.35,2.08 111.65,2.08 92,-6.23 84.13,-9.55 77.16,-15.61 71.55,-21.81\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"66.79,-27.48 68.88,-20.1 69.04,-24.8 71.29,-22.12 71.29,-22.12 71.29,-22.12 69.04,-24.8 73.7,-24.14 66.79,-27.48 66.79,-27.48\"/>\n",
       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"94,-29.23 94,-48.23 110,-48.23 110,-29.23 94,-29.23\"/>\n",
       "<text text-anchor=\"start\" x=\"96\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">i1</text>\n",
       "<text text-anchor=\"start\" x=\"114\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"125,-29.23 125,-48.23 138,-48.23 138,-29.23 125,-29.23\"/>\n",
       "<text text-anchor=\"start\" x=\"127\" y=\"-35.03\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "<text text-anchor=\"start\" x=\"108\" y=\"-14.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"300\" cy=\"-42.23\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"300\" y=\"-38.53\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;2 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M194.22,-42.23C215.2,-42.23 250.79,-42.23 274.59,-42.23\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"281.87,-42.23 274.87,-45.38 278.37,-42.23 274.87,-42.23 274.87,-42.23 274.87,-42.23 278.37,-42.23 274.87,-39.08 281.87,-42.23 281.87,-42.23\"/>\n",
       "<polygon fill=\"#e9f4fb\" stroke=\"transparent\" points=\"214,-65.23 214,-84.23 230,-84.23 230,-65.23 214,-65.23\"/>\n",
       "<text text-anchor=\"start\" x=\"216\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
       "<text text-anchor=\"start\" x=\"234\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">/</text>\n",
       "<polygon fill=\"#ffe5f1\" stroke=\"transparent\" points=\"245,-65.23 245,-84.23 262,-84.23 262,-65.23 245,-65.23\"/>\n",
       "<text text-anchor=\"start\" x=\"247\" y=\"-71.03\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "<text text-anchor=\"start\" x=\"230\" y=\"-50.03\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f743a5ca6c0> >"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a = spot.make_twa_graph()\n",
    "a.acc().set_acceptance(spot.acc_code.t())\n",
    "i0 = buddy.bdd_ithvar(a.register_ap('i0'))\n",
    "i1 = buddy.bdd_ithvar(a.register_ap('i1'))\n",
    "o = buddy.bdd_ithvar(a.register_ap('o'))\n",
    "tt = buddy.bddtrue\n",
    "a0 = spot.mark_t([0])\n",
    "a.new_states(3)\n",
    "a.new_edge(0,1,i0&o,a0)\n",
    "a.new_edge(1,0,i1,a0)\n",
    "a.new_edge(1,2,i0&(buddy.bdd_not(o)),a0)\n",
    "spot.set_synthesis_outputs(a, o)\n",
    "a"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "078bb43e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(0, t)\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.43.0 (0)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"484pt\" height=\"198pt\"\n",
       " viewBox=\"0.00 0.00 484.00 198.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 194)\">\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-194 480,-194 480,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"235\" y=\"-174.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
       "<text text-anchor=\"start\" x=\"227\" y=\"-159.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-80\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-80C2.79,-80 17.15,-80 30.63,-80\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-80 30.94,-83.15 34.44,-80 30.94,-80 30.94,-80 30.94,-80 34.44,-80 30.94,-76.85 37.94,-80 37.94,-80\"/>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>3</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"149,-98 122,-80 149,-62 176,-80 149,-98\"/>\n",
       "<text text-anchor=\"middle\" x=\"149\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;3 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M74.12,-80C85.52,-80 100.87,-80 114.63,-80\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"121.65,-80 114.65,-83.15 118.15,-80 114.65,-80 114.65,-80 114.65,-80 118.15,-80 114.65,-76.85 121.65,-80 121.65,-80\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"239\" cy=\"-80\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"239\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;1 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>3&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M176.4,-80C188.2,-80 202.01,-80 213.57,-80\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"220.79,-80 213.79,-83.15 217.29,-80 213.79,-80 213.79,-80 213.79,-80 217.29,-80 213.79,-76.85 220.79,-80 220.79,-80\"/>\n",
       "<text text-anchor=\"start\" x=\"194\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>4</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-36 337,-18 364,0 391,-18 364,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"364\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;4 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>1&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M255.26,-71.53C261.37,-68.19 268.49,-64.36 275,-61 297.28,-49.51 323.09,-37 340.97,-28.44\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"347.64,-25.26 342.68,-31.12 344.48,-26.77 341.32,-28.27 341.32,-28.27 341.32,-28.27 344.48,-26.77 339.97,-25.43 347.64,-25.26 347.64,-25.26\"/>\n",
       "<text text-anchor=\"start\" x=\"275\" y=\"-64.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 &amp; i1</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>5</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-98 337,-80 364,-62 391,-80 364,-98\"/>\n",
       "<text text-anchor=\"middle\" x=\"364\" y=\"-76.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;5 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M257.1,-80C275.77,-80 306.11,-80 329.55,-80\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"336.58,-80 329.58,-83.15 333.08,-80 329.58,-80 329.58,-80 329.58,-80 333.08,-80 329.58,-76.85 336.58,-80 336.58,-80\"/>\n",
       "<text text-anchor=\"start\" x=\"275\" y=\"-83.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; !i1</text>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>6</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-152 337,-134 364,-116 391,-134 364,-152\"/>\n",
       "<text text-anchor=\"middle\" x=\"364\" y=\"-130.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;6 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M255.65,-87.24C261.68,-90.01 268.65,-93.18 275,-96 297.15,-105.84 322.59,-116.79 340.39,-124.39\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"347.06,-127.24 339.38,-127.39 343.84,-125.86 340.62,-124.49 340.62,-124.49 340.62,-124.49 343.84,-125.86 341.86,-121.59 347.06,-127.24 347.06,-127.24\"/>\n",
       "<text text-anchor=\"start\" x=\"277\" y=\"-118.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; i1</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;0 -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>4&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M338.99,-19.5C295.19,-22.67 199.65,-31.6 122,-53 107.19,-57.08 91.25,-63.67 78.86,-69.31\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"72.37,-72.33 77.39,-66.52 75.55,-70.85 78.72,-69.38 78.72,-69.38 78.72,-69.38 75.55,-70.85 80.05,-72.23 72.37,-72.33 72.37,-72.33\"/>\n",
       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"458\" cy=\"-107\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"458\" y=\"-103.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;2 -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>5&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M385.52,-83.87C396.46,-86.14 410.08,-89.28 422,-93 426.08,-94.27 430.36,-95.81 434.47,-97.39\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"441.16,-100.05 433.49,-100.39 437.91,-98.76 434.66,-97.46 434.66,-97.46 434.66,-97.46 437.91,-98.76 435.82,-94.54 441.16,-100.05 441.16,-100.05\"/>\n",
       "<text text-anchor=\"start\" x=\"409\" y=\"-96.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;0 -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>6&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M338.67,-135.14C320.98,-135.69 296.46,-135.88 275,-134 206.21,-127.98 189.42,-121.91 122,-107 108.53,-104.02 104.82,-104.11 92,-99 87.43,-97.18 82.69,-94.9 78.23,-92.56\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"71.95,-89.13 79.61,-89.72 75.03,-90.81 78.1,-92.49 78.1,-92.49 78.1,-92.49 75.03,-90.81 76.59,-95.25 71.95,-89.13 71.95,-89.13\"/>\n",
       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-128.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;2 -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>6&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M383.18,-128.67C397.62,-124.43 417.92,-118.47 433.58,-113.87\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"440.41,-111.87 434.58,-116.86 437.05,-112.86 433.69,-113.84 433.69,-113.84 433.69,-113.84 437.05,-112.86 432.8,-110.82 440.41,-111.87 440.41,-111.87\"/>\n",
       "<text text-anchor=\"start\" x=\"409\" y=\"-124.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7458059f90> >"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a_snc = spot.split_2step(a, False)\n",
    "print(a_snc.acc())\n",
    "a_snc"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "05b4a138",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(1, Fin(0))\n"
     ]
    },
    {
     "data": {
      "image/svg+xml": [
       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
       "<!-- Generated by graphviz version 2.43.0 (0)\n",
       " -->\n",
       "<!-- Pages: 1 -->\n",
       "<svg width=\"706pt\" height=\"269pt\"\n",
       " viewBox=\"0.00 0.00 706.00 269.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 265)\">\n",
       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-265 702,-265 702,4 -4,4\"/>\n",
       "<text text-anchor=\"start\" x=\"327.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">Fin(</text>\n",
       "<text text-anchor=\"start\" x=\"350.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "<text text-anchor=\"start\" x=\"366.5\" y=\"-246.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
       "<text text-anchor=\"start\" x=\"317.5\" y=\"-232.8\" font-family=\"Lato\" font-size=\"14.00\">[co&#45;Büchi]</text>\n",
       "<!-- I -->\n",
       "<!-- 0 -->\n",
       "<g id=\"node2\" class=\"node\">\n",
       "<title>0</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-59\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"56\" y=\"-55.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
       "</g>\n",
       "<!-- I&#45;&gt;0 -->\n",
       "<g id=\"edge1\" class=\"edge\">\n",
       "<title>I&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-59C2.79,-59 17.15,-59 30.63,-59\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-59 30.94,-62.15 34.44,-59 30.94,-59 30.94,-59 30.94,-59 34.44,-59 30.94,-55.85 37.94,-59 37.94,-59\"/>\n",
       "</g>\n",
       "<!-- 3 -->\n",
       "<g id=\"node3\" class=\"node\">\n",
       "<title>3</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"583,-190 556,-172 583,-154 610,-172 583,-190\"/>\n",
       "<text text-anchor=\"middle\" x=\"583\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;3 -->\n",
       "<g id=\"edge2\" class=\"edge\">\n",
       "<title>0&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M59.28,-76.91C65.47,-116.91 86.48,-210 148,-210 148,-210 148,-210 494,-210 519.79,-210 546.6,-196.08 563.75,-185.08\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"569.61,-181.2 565.52,-187.69 566.69,-183.13 563.78,-185.07 563.78,-185.07 563.78,-185.07 566.69,-183.13 562.04,-182.44 569.61,-181.2 569.61,-181.2\"/>\n",
       "<text text-anchor=\"start\" x=\"289\" y=\"-213.8\" font-family=\"Lato\" font-size=\"14.00\">!i0</text>\n",
       "</g>\n",
       "<!-- 5 -->\n",
       "<g id=\"node4\" class=\"node\">\n",
       "<title>5</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"149,-108 122,-90 149,-72 176,-90 149,-108\"/>\n",
       "<text text-anchor=\"middle\" x=\"149\" y=\"-86.3\" font-family=\"Lato\" font-size=\"14.00\">5</text>\n",
       "</g>\n",
       "<!-- 0&#45;&gt;5 -->\n",
       "<g id=\"edge3\" class=\"edge\">\n",
       "<title>0&#45;&gt;5</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M73.27,-64.54C87.28,-69.31 107.7,-76.27 123.65,-81.71\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"130.63,-84.08 122.99,-84.81 127.32,-82.95 124.01,-81.83 124.01,-81.83 124.01,-81.83 127.32,-82.95 125.02,-78.84 130.63,-84.08 130.63,-84.08\"/>\n",
       "<text text-anchor=\"start\" x=\"92\" y=\"-77.8\" font-family=\"Lato\" font-size=\"14.00\">i0</text>\n",
       "</g>\n",
       "<!-- 4 -->\n",
       "<g id=\"node10\" class=\"node\">\n",
       "<title>4</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"680\" cy=\"-172\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"680\" y=\"-168.3\" font-family=\"Lato\" font-size=\"14.00\">4</text>\n",
       "</g>\n",
       "<!-- 3&#45;&gt;4 -->\n",
       "<g id=\"edge9\" class=\"edge\">\n",
       "<title>3&#45;&gt;4</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M605.09,-175.35C616.59,-176.77 631.07,-177.92 644,-177 647.49,-176.75 651.16,-176.37 654.76,-175.92\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"661.96,-174.93 655.46,-179 658.49,-175.4 655.03,-175.88 655.03,-175.88 655.03,-175.88 658.49,-175.4 654.6,-172.76 661.96,-174.93 661.96,-174.93\"/>\n",
       "<text text-anchor=\"start\" x=\"631.5\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "<text text-anchor=\"start\" x=\"628\" y=\"-180.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "<!-- 1 -->\n",
       "<g id=\"node5\" class=\"node\">\n",
       "<title>1</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"239\" cy=\"-104\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"239\" y=\"-100.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 5&#45;&gt;1 -->\n",
       "<g id=\"edge11\" class=\"edge\">\n",
       "<title>5&#45;&gt;1</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M171.3,-93.39C184.18,-95.44 200.62,-98.05 213.96,-100.18\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"221.01,-101.3 213.61,-103.31 217.56,-100.75 214.1,-100.2 214.1,-100.2 214.1,-100.2 217.56,-100.75 214.6,-97.09 221.01,-101.3 221.01,-101.3\"/>\n",
       "<text text-anchor=\"start\" x=\"194\" y=\"-101.8\" font-family=\"Lato\" font-size=\"14.00\">o</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;3 -->\n",
       "<g id=\"edge4\" class=\"edge\">\n",
       "<title>1&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M249.03,-119.4C255.17,-128.4 264.14,-139.12 275,-145 321.53,-170.19 479.42,-172.57 548.82,-172.35\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"556.04,-172.32 549.06,-175.5 552.54,-172.34 549.04,-172.35 549.04,-172.35 549.04,-172.35 552.54,-172.34 549.03,-169.2 556.04,-172.32 556.04,-172.32\"/>\n",
       "<text text-anchor=\"start\" x=\"409\" y=\"-173.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 &amp; !i1</text>\n",
       "</g>\n",
       "<!-- 6 -->\n",
       "<g id=\"node6\" class=\"node\">\n",
       "<title>6</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-90 337,-72 364,-54 391,-72 364,-90\"/>\n",
       "<text text-anchor=\"middle\" x=\"364\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">6</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;6 -->\n",
       "<g id=\"edge5\" class=\"edge\">\n",
       "<title>1&#45;&gt;6</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M256.59,-99.68C277.36,-94.28 313.15,-84.97 337.44,-78.65\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"344.26,-76.87 338.28,-81.69 340.88,-77.76 337.49,-78.64 337.49,-78.64 337.49,-78.64 340.88,-77.76 336.7,-75.59 344.26,-76.87 344.26,-76.87\"/>\n",
       "<text text-anchor=\"start\" x=\"275\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!i0 &amp; i1</text>\n",
       "</g>\n",
       "<!-- 7 -->\n",
       "<g id=\"node7\" class=\"node\">\n",
       "<title>7</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-144 337,-126 364,-108 391,-126 364,-144\"/>\n",
       "<text text-anchor=\"middle\" x=\"364\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">7</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;7 -->\n",
       "<g id=\"edge6\" class=\"edge\">\n",
       "<title>1&#45;&gt;7</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M255.24,-112.42C261.23,-115.33 268.26,-118.29 275,-120 293.02,-124.57 313.74,-126.16 330.55,-126.56\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"337.97,-126.67 330.92,-129.71 334.47,-126.62 330.97,-126.57 330.97,-126.57 330.97,-126.57 334.47,-126.62 331.02,-123.42 337.97,-126.67 337.97,-126.67\"/>\n",
       "<text text-anchor=\"start\" x=\"275\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; !i1</text>\n",
       "</g>\n",
       "<!-- 8 -->\n",
       "<g id=\"node8\" class=\"node\">\n",
       "<title>8</title>\n",
       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"364,-36 337,-18 364,0 391,-18 364,-36\"/>\n",
       "<text text-anchor=\"middle\" x=\"364\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">8</text>\n",
       "</g>\n",
       "<!-- 1&#45;&gt;8 -->\n",
       "<g id=\"edge7\" class=\"edge\">\n",
       "<title>1&#45;&gt;8</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M250.63,-89.89C257.09,-81.94 265.84,-72.19 275,-65 295.27,-49.1 321.69,-35.81 340.28,-27.47\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"346.74,-24.62 341.6,-30.32 343.54,-26.03 340.33,-27.44 340.33,-27.44 340.33,-27.44 343.54,-26.03 339.06,-24.56 346.74,-24.62 346.74,-24.62\"/>\n",
       "<text text-anchor=\"start\" x=\"277\" y=\"-68.8\" font-family=\"Lato\" font-size=\"14.00\">i0 &amp; i1</text>\n",
       "</g>\n",
       "<!-- 6&#45;&gt;0 -->\n",
       "<g id=\"edge12\" class=\"edge\">\n",
       "<title>6&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M350.67,-62.68C342.25,-56.92 330.55,-50.05 319,-47 233.55,-24.42 127.04,-42.98 80.55,-53.28\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"73.61,-54.85 79.74,-50.23 77.03,-54.08 80.44,-53.3 80.44,-53.3 80.44,-53.3 77.03,-54.08 81.14,-56.37 73.61,-54.85 73.61,-54.85\"/>\n",
       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 2 -->\n",
       "<g id=\"node9\" class=\"node\">\n",
       "<title>2</title>\n",
       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"493\" cy=\"-126\" rx=\"18\" ry=\"18\"/>\n",
       "<text text-anchor=\"middle\" x=\"493\" y=\"-122.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
       "</g>\n",
       "<!-- 7&#45;&gt;2 -->\n",
       "<g id=\"edge13\" class=\"edge\">\n",
       "<title>7&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M391.01,-126C413.57,-126 445.96,-126 467.93,-126\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"474.95,-126 467.95,-129.15 471.45,-126 467.95,-126 467.95,-126 467.95,-126 471.45,-126 467.95,-122.85 474.95,-126 474.95,-126\"/>\n",
       "<text text-anchor=\"start\" x=\"426.5\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;0 -->\n",
       "<g id=\"edge14\" class=\"edge\">\n",
       "<title>8&#45;&gt;0</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M339.67,-16.08C306.97,-13.79 245.73,-10.98 194,-17 161.34,-20.8 153.63,-25.01 122,-34 108.48,-37.84 105.14,-39.01 92,-44 87.96,-45.54 83.71,-47.26 79.6,-48.99\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"72.92,-51.85 78.11,-46.2 76.13,-50.47 79.35,-49.1 79.35,-49.1 79.35,-49.1 76.13,-50.47 80.59,-51.99 72.92,-51.85 72.92,-51.85\"/>\n",
       "<text text-anchor=\"middle\" x=\"198.5\" y=\"-20.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 8&#45;&gt;2 -->\n",
       "<g id=\"edge15\" class=\"edge\">\n",
       "<title>8&#45;&gt;2</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M376.72,-27.97C398.76,-46.71 446.53,-87.34 473.14,-109.96\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"478.8,-114.77 471.42,-112.64 476.13,-112.51 473.47,-110.24 473.47,-110.24 473.47,-110.24 476.13,-112.51 475.51,-107.84 478.8,-114.77 478.8,-114.77\"/>\n",
       "<text text-anchor=\"start\" x=\"426.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">!o</text>\n",
       "</g>\n",
       "<!-- 2&#45;&gt;3 -->\n",
       "<g id=\"edge8\" class=\"edge\">\n",
       "<title>2&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M510.25,-131.34C518.71,-134.35 529.12,-138.42 538,-143 546.64,-147.45 555.69,-153.2 563.32,-158.41\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"569.35,-162.61 561.81,-161.2 566.48,-160.61 563.61,-158.61 563.61,-158.61 563.61,-158.61 566.48,-160.61 565.41,-156.03 569.35,-162.61 569.35,-162.61\"/>\n",
       "<text text-anchor=\"middle\" x=\"533.5\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "</g>\n",
       "<!-- 4&#45;&gt;3 -->\n",
       "<g id=\"edge10\" class=\"edge\">\n",
       "<title>4&#45;&gt;3</title>\n",
       "<path fill=\"none\" stroke=\"black\" d=\"M667.4,-158.86C661.16,-152.78 652.91,-146.21 644,-143 637.31,-140.59 634.81,-140.96 628,-143 618.42,-145.87 608.99,-151.59 601.34,-157.19\"/>\n",
       "<polygon fill=\"black\" stroke=\"black\" points=\"595.36,-161.8 598.98,-155.03 598.13,-159.66 600.9,-157.52 600.9,-157.52 600.9,-157.52 598.13,-159.66 602.82,-160.02 595.36,-161.8 595.36,-161.8\"/>\n",
       "<text text-anchor=\"start\" x=\"631.5\" y=\"-161.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
       "<text text-anchor=\"start\" x=\"628\" y=\"-146.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">⓿</text>\n",
       "</g>\n",
       "</g>\n",
       "</svg>\n"
      ],
      "text/plain": [
       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f7458055870> >"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "a_s = spot.split_2step(a, True)\n",
    "print(a_s.acc())\n",
    "a_s"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "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.10"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}