VWAA for FGa && GFb

{ "cells": [ { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import spot\n", "from spot.jupyter import display_inline\n", "spot.setup(show_default='.bav')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Support for alternating automata" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The following automata are what we will use as examples." ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [], "source": [ "aut1, aut2, aut3, aut4, aut5 = spot.automata('''\n", "HOA: v1 tool: \"ltl3ba\" \"1.1.3\" name: \"VWAA for FGa && GFb\" States: 6\n", "Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP: 2 \"a\" \"b\" properties:\n", "trans-labels explicit-labels state-acc univ-branch very-weak --BODY--\n", "State: 0 \"(FG(a) && GF(b))\" [t] 3&1 State: 1 \"GF(b)\" [(1)] 1 [(!1)]\n", "2&1 State: 2 \"F(b)\" {0} [(1)] 5 [(!1)] 2 State: 3 \"FG(a)\" {0} [(0)] 4\n", "[t] 3 State: 4 \"G(a)\" [(0)] 4 State: 5 \"t\" [t] 5 --END--\n", "/* Example from ADL's PSL2TGBA talk. */\n", "HOA: v1 States: 3 Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:\n", "3 \"a\" \"b\" \"p\" --BODY-- State: 0 \"(a;a*;b)*\" {0} [0] 1 [!0] 2 State: 1\n", "\"a*;b;(a;a*;b)*\" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:\n", "2 [t] 2 --END--\n", "HOA: v1 States: 5 Start: 3 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:\n", "3 \"a\" \"b\" \"p\" --BODY-- State: 0 \"(a;a*;b)*\" {0} [0] 1 [!0] 2 State: 1\n", "\"a*;b;(a;a*;b)*\" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:\n", "2 [t] 2 State: 3 [0] 4&0 State: 4 [t] 3 --END--\n", "HOA: v1 States: 3 Start: 0 acc-name: co-Buchi Acceptance: 1 Fin(0) AP:\n", "3 \"a\" \"b\" \"p\" --BODY-- State: 0 \"(a;a*;b)*\" {0} [0] 1 [!0] 2 State: 1\n", "\"a*;b;(a;a*;b)*\" {0} [0&1&2] 0&1 [!1&2] 1 [!0&!1] 2 [!0&1&2] 0 State:\n", "2 [t] 2 --END--\n", "HOA: v1 tool: \"ltl3dra\" \"0.2.2\" name: \"VWAA for GFa\" States: 3 Start: 0\n", "acc-name: co-Buchi Acceptance: 1 Fin(0) AP: 1 \"a\" properties: trans-labels\n", "explicit-labels state-acc univ-branch very-weak --BODY-- State: 0 \"GF(a)\"\n", "[t] 1&0 State: 1 \"F(a)\" {0} [(0)] 2 [t] 1 State: 2 \"t\" [t] 2 --END--\n", "''')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Various display options" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Here is the default output, using the `bav` options as set by default in the first cell. " ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

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

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display_inline(aut1, aut2, aut3, aut4, aut5)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "If the state labels take too much space, you can reduce the size of the automaton by forcing states to be numbered with option `1`. The original label is still displayed as a tooltip when the mouse is over the state.\n", "\n", "Note that passing option `show=...` to `display_inline` is similar to calling `aut.show(...)` on each argument." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display_inline(aut1, aut2, aut3, aut4, aut5, show='.bav1')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "When working with alternating automata, it is quite common to hide \"true states\", and display \"exiting transitions instead\". You can do that with option `u`." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display_inline(aut1, aut2, aut3, aut4, aut5, show='.bav1u')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Let's make sure that option `u` and `s` (to display SCCs) work well together:" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "display_inline(aut1, aut2, aut3, aut4, aut5, show='.bav1us')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Alternation removal" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The `remove_alternation()` function works on any alternating automaton that is weak (not necessarily very weak), i.e., in each SCC all transition should belong to the same accepting sets.\n", "\n", "The second argument of `remove_alternation()`, set to `True` below, simply asks for states to be labeled to help debugging. As the function builds Transition-based Generalized Büchi acceptance, it can be worthwhile to apply `scc_filter()` in an attempt to reduce the number of acceptance sets.\n", "\n", "The next cell shows this two-step process on our first example automaton." ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

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

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "nba1t = spot.remove_alternation(aut1, True)\n", "nba1 = spot.scc_filter(nba1t, True)\n", "display_inline(aut1.show('.bav1u'), nba1t, nba1)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Let's apply this process to the other 4 automata (which are not very-weak, unlike `aut1`). The states marked with `~` are part of a break-point construction." ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

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

" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "nba2, nba3, nba4, nba5 = [spot.scc_filter(spot.remove_alternation(a, True), True) for a in (aut2, aut3, aut4, aut5)]\n", "display_inline(nba2, nba3, nba4, nba5)" ] } ], "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.6.5" } }, "nbformat": 4, "nbformat_minor": 2 }