{ "cells": [ { "cell_type": "code", "execution_count": 1, "id": "8bca10b8", "metadata": {}, "outputs": [], "source": [ "import spot, buddy\n", "import pandas as pd\n", "spot.setup()" ] }, { "cell_type": "markdown", "id": "c73e997a", "metadata": {}, "source": [ "Test the Mealy printer." ] }, { "cell_type": "code", "execution_count": 2, "id": "f8eff7ed", "metadata": {}, "outputs": [], "source": [ "g = spot.ltl_to_game('G((a|c) <-> (b|d))', [\"b\", \"d\"])" ] }, { "cell_type": "code", "execution_count": 3, "id": "ad3c80bc", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.solve_game(g)" ] }, { "cell_type": "code", "execution_count": 4, "id": "50130d85", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "t\n", "[all]\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "!a & !c\n", "\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "a | c\n", "\n", "\n", "\n", "1->0\n", "\n", "\n", "!b & !d\n", "\n", "\n", "\n", "2->0\n", "\n", "\n", "b | d\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7fcc35aaa030> >" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.highlight_strategy(g)" ] }, { "cell_type": "code", "execution_count": 5, "id": "3d56cda6", "metadata": {}, "outputs": [], "source": [ "x = spot.solved_game_to_separated_mealy(g)" ] }, { "cell_type": "code", "execution_count": 6, "id": "c24548a1", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "\n", "!a & !c\n", "/\n", "\n", "!b & !d\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "\n", "a | c\n", "/\n", "\n", "b | d\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7fcc35aaa900> >" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "x" ] }, { "cell_type": "code", "execution_count": 7, "id": "88f2c0e0", "metadata": {}, "outputs": [], "source": [ "x.merge_edges()" ] }, { "cell_type": "code", "execution_count": 8, "id": "e626997e", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "\n", "0->0\n", "\n", "\n", "\n", "!a & !c\n", "/\n", "\n", "!b & !d\n", "\n", "a | c\n", "/\n", "\n", "b | d\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7fcc35aaa900> >" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "x" ] }, { "cell_type": "code", "execution_count": 9, "id": "923a59d6", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "0->1\n", "\n", "\n", "\n", "!i\n", "/\n", "\n", "!o\n", "\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "\n", "0->2\n", "\n", "\n", "\n", "i\n", "/\n", "\n", "o\n", "\n", "\n", "\n", "1->1\n", "\n", "\n", "\n", "1\n", "/\n", "\n", "!o\n", "\n", "\n", "\n", "2->2\n", "\n", "\n", "\n", "1\n", "/\n", "\n", "1\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7fcc35ac20c0> >" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "aut = spot.make_twa_graph()\n", "i = buddy.bdd_ithvar(aut.register_ap(\"i\"))\n", "o = buddy.bdd_ithvar(aut.register_ap(\"o\"))\n", "spot.set_synthesis_outputs(aut, o)\n", "aut.new_states(3)\n", "aut.new_edge(0,1,buddy.bdd_not(i)&buddy.bdd_not(o))\n", "aut.new_edge(0,2,i&o)\n", "aut.new_edge(1,1,buddy.bdd_not(o))\n", "aut.new_edge(2,2,buddy.bddtrue)\n", "aut" ] }, { "cell_type": "code", "execution_count": 10, "id": "f06d6df4", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "('o',)\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "\n", "t\n", "[all]\n", "\n", "\n", "\n", "0\n", "\n", "0\n", "\n", "\n", "\n", "I->0\n", "\n", "\n", "\n", "\n", "\n", "3\n", "\n", "3\n", "\n", "\n", "\n", "0->3\n", "\n", "\n", "!i\n", "\n", "\n", "\n", "4\n", "\n", "4\n", "\n", "\n", "\n", "0->4\n", "\n", "\n", "i\n", "\n", "\n", "\n", "1\n", "\n", "1\n", "\n", "\n", "\n", "3->1\n", "\n", "\n", "!o\n", "\n", "\n", "\n", "2\n", "\n", "2\n", "\n", "\n", "\n", "4->2\n", "\n", "\n", "o\n", "\n", "\n", "\n", "1->3\n", "\n", "\n", "1\n", "\n", "\n", "\n", "5\n", "\n", "5\n", "\n", "\n", "\n", "2->5\n", "\n", "\n", "1\n", "\n", "\n", "\n", "5->2\n", "\n", "\n", "1\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7fcc35ac2720> >" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "aut_s = spot.split_2step(aut)\n", "print(spot.get_synthesis_output_aps(aut_s))\n", "aut_s" ] }, { "cell_type": "code", "execution_count": 11, "id": "3cc4d320", "metadata": {}, "outputs": [ { "data": { "text/html": [ "
\n", "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
taskpremin_timereorg_timepartsol_timeplayer_incomp_timeincomp_timesplit_all_let_timesplit_min_let_timesplit_cstr_timeprob_init_build_time...refine_timetotal_timen_classesn_refinementn_litn_clausesn_iterationn_bisim_letn_min_statesdone
0presat25643.31.112e-064.588e-069.888e-064.549e-061.5929e-059.338e-065.901e-066.7276e-05...NaNNaNNaNNaNNaNNaNNaN2NaNNaN
1satNaNNaNNaNNaNNaNNaNNaNNaNNaN...NaN0.000282709207120NaN41
\n", "

2 rows × 22 columns

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

4 rows × 22 columns

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

4 rows × 22 columns

\n", "
" ], "text/plain": [ " task premin_time reorg_time partsol_time player_incomp_time \\\n", "0 presat 25643.5 1.563e-06 5.4e-06 2.0519e-05 \n", "1 sat NaN NaN NaN NaN \n", "2 refinement NaN NaN NaN NaN \n", "3 sat NaN NaN NaN NaN \n", "\n", " incomp_time split_all_let_time split_min_let_time split_cstr_time \\\n", "0 1.3e-07 3.968e-06 9.698e-06 7.624e-06 \n", "1 NaN NaN NaN NaN \n", "2 NaN NaN NaN NaN \n", "3 NaN NaN NaN NaN \n", "\n", " prob_init_build_time ... refine_time total_time n_classes n_refinement \\\n", "0 3.211e-05 ... NaN NaN NaN NaN \n", "1 NaN ... NaN NaN 1 0 \n", "2 NaN ... 4.4633e-05 NaN 1 1 \n", "3 NaN ... NaN 0.000280675 2 0 \n", "\n", " n_lit n_clauses n_iteration n_bisim_let n_min_states done \n", "0 NaN NaN NaN 1 NaN NaN \n", "1 3 6 0 NaN NaN NaN \n", "2 10 16 NaN NaN NaN NaN \n", "3 17 29 1 NaN 4 1 \n", "\n", "[4 rows x 22 columns]" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "c ### Next Instance 1 0 ###\n", "p cnf 5 5\n", "-1 2 -3 0\n", "1 -3 0\n", "1 -5 0\n", "2 -5 0\n", "3 -5 0\n", "c ### Next Instance 1 1 ###\n", "p cnf 12 15\n", "-1 2 -3 0\n", "4 0\n", "6 0\n", "-9 0\n", "-1 -2 10 0\n", "-10 0\n", "1 -3 0\n", "1 -5 0\n", "1 -12 0\n", "2 -5 0\n", "2 -12 0\n", "-2 9 0\n", "3 -5 0\n", "3 -12 0\n", "7 8 0\n", "c ### Next Instance 2 0 ###\n", "p cnf 19 29\n", "-3 -1 2 0\n", "4 0\n", "6 0\n", "-9 0\n", "-1 -2 10 0\n", "-10 0\n", "11 -16 -17 0\n", "1 -15 -17 0\n", "-1 13 -14 0\n", "-11 13 -16 0\n", "-11 -15 2 0\n", "-13 -15 2 0\n", "1 11 -19 0\n", "13 -19 2 0\n", "15 16 -19 0\n", "3 14 -19 0\n", "-2 0\n", "-12 0\n", "-5 0\n", "1 -3 0\n", "1 -5 0\n", "1 -12 0\n", "2 -5 0\n", "2 -12 0\n", "-2 9 0\n", "3 -5 0\n", "3 -12 0\n", "7 8 0\n", "11 -14 0\n", "\n" ] } ], "source": [ "import tempfile\n", "\n", "si = spot.synthesis_info()\n", "si.minimize_lvl = 3\n", "\n", "with tempfile.NamedTemporaryFile(dir='.', suffix='.dimacslog') as t:\n", " si.opt.set_str(\"satlogdimacs\", t.name)\n", " aut_ms, table = spot.minimize_mealy(aut_s, si, display_log=True, return_log=True)\n", " with open(t.name, \"r\") as f:\n", " print(\"\".join(f.readlines()))\n", " \n", " " ] }, { "cell_type": "code", "execution_count": null, "id": "5c9fe115", "metadata": {}, "outputs": [], "source": [] } ], "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" }, "vscode": { "interpreter": { "hash": "916dbcbb3f70747c44a77c7bcd40155683ae19c65e1c03b4aa3499c5328201f1" } } }, "nbformat": 4, "nbformat_minor": 5 }