{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Additional testing for synthesis" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Testing the different methods to solve" ] }, { "cell_type": "code", "execution_count": 2, "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, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "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", "--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: 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", "--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 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 1 1 1 1\n", "--BODY--\n", "State: 0\n", "[!0&!1] 7\n", "[!0&1] 8\n", "[0&!1] 9\n", "[0&1] 10\n", "State: 1\n", "[0&1] 11\n", "[0&!1] 12\n", "[!0&1] 13\n", "[!0&!1] 14\n", "State: 2\n", "[0] 11\n", "[!0] 13\n", "State: 3\n", "[!0&1] 15\n", "[0&1] 16\n", "[!0&!1] 17\n", "[0&!1] 18\n", "State: 4\n", "[!0] 15\n", "[0] 16\n", "State: 5\n", "[!0] 19\n", "[0] 11\n", "State: 6\n", "[!0&1] 19\n", "[0&1] 11\n", "[!0&!1] 20\n", "[0&!1] 12\n", "State: 7\n", "[t] 1\n", "State: 8\n", "[t] 2\n", "State: 9\n", "[t] 3\n", "State: 10\n", "[t] 4\n", "State: 11\n", "[!2] 4\n", "State: 12\n", "[!2] 3\n", "State: 13\n", "[!2] 2\n", "State: 14\n", "[!2] 1\n", "State: 15\n", "[2] 5\n", "State: 16\n", "[2] 4\n", "State: 17\n", "[2] 6\n", "State: 18\n", "[2] 3\n", "State: 19\n", "[!2] 5\n", "State: 20\n", "[!2] 6\n", "--END--\n", "HOA: v1\n", "States: 2\n", "Start: 1\n", "AP: 3 \"i1\" \"i0\" \"o0\"\n", "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", "--BODY--\n", "State: 0\n", "[0&1&!2] 1\n", "[0&!1&!2] 1\n", "[!0&1&!2] 0\n", "[!0&!1&!2] 0\n", "State: 1\n", "[!0&1&2] 0\n", "[0&1&2] 1\n", "[!0&!1&2] 0\n", "[0&!1&2] 1\n", "--END--\n", "HOA: v1\n", "States: 2\n", "Start: 1\n", "AP: 3 \"i1\" \"i0\" \"o0\"\n", "acc-name: all\n", "Acceptance: 0 t\n", "properties: trans-labels explicit-labels state-acc deterministic\n", "--BODY--\n", "State: 0\n", "[0&1&!2] 1\n", "[0&!1&!2] 1\n", "[!0&1&!2] 0\n", "[!0&!1&!2] 0\n", "State: 1\n", "[!0&1&2] 0\n", "[0&1&2] 1\n", "[!0&!1&2] 0\n", "[0&!1&2] 1\n", "--END--\n", "HOA: v1\n", "States: 6\n", "Start: 1\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 1 1 1\n", "--BODY--\n", "State: 0\n", "[0&1] 2\n", "[0&!1] 2\n", "[!0&1] 3\n", "[!0&!1] 3\n", "State: 1\n", "[!0&1] 4\n", "[0&1] 5\n", "[!0&!1] 4\n", "[0&!1] 5\n", "State: 2\n", "[!2] 1\n", "State: 3\n", "[!2] 0\n", "State: 4\n", "[2] 0\n", "State: 5\n", "[2] 1\n", "--END--\n", "HOA: v1\n", "States: 6\n", "Start: 1\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 1 1 1\n", "--BODY--\n", "State: 0\n", "[0] 2\n", "[!0] 3\n", "State: 1\n", "[0] 4\n", "[!0] 5\n", "State: 2\n", "[!2] 1\n", "State: 3\n", "[!2] 0\n", "State: 4\n", "[2] 1\n", "State: 5\n", "[2] 0\n", "--END--\n", "HOA: v1\n", "States: 2\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", "--BODY--\n", "State: 0\n", "[0&2] 0\n", "[!0&2] 1\n", "State: 1\n", "[0&!2] 0\n", "[!0&!2] 1\n", "--END--\n", "HOA: v1\n", "States: 6\n", "Start: 1\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 1 1 1\n", "--BODY--\n", "State: 0\n", "[0] 2\n", "[!0] 3\n", "State: 1\n", "[0] 4\n", "[!0] 5\n", "State: 2\n", "[!2] 1\n", "State: 3\n", "[!2] 0\n", "State: 4\n", "[2] 1\n", "State: 5\n", "[2] 0\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_separated_mealy(mm0)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\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_separated_mealy(mm2)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\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_split_mealy(mm3)) #Not imposed by the functions pre or post, but results of current impl, change if necessary\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, "metadata": {}, "outputs": [], "source": [ "mus0 = spot.unsplit_mealy(msplit0)\n", "mus2 = spot.unsplit_mealy(msplit2)\n", "mus3 = spot.unsplit_mealy(msplit3)\n", "mmus3 = spot.unsplit_mealy(mm3)" ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [], "source": [ "assert(mm0.equivalent_to(msep0))\n", "assert(mm0.equivalent_to(mus0))\n", "assert(mm2.equivalent_to(msep2))\n", "assert(mm2.equivalent_to(mus2))\n", "assert(mmus3.equivalent_to(msep3))\n", "assert(mmus3.equivalent_to(mus3))" ] } ], "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.10" } }, "nbformat": 4, "nbformat_minor": 5 }