finite_state

{ "cells": [ { "cell_type": "markdown", "id": "389ac0c8-a903-4e16-8cff-fdf9bf6b6933", "metadata": {}, "source": [ "# Example 1" ] }, { "cell_type": "code", "execution_count": 13, "id": "e4582473-0c39-466a-9312-3f8851d561f2", "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/opt/conda/lib/python3.10/site-packages/pytct/name_converter.py:70: UserWarning: controllable and uncontrollable status of event is not specified. All events are set to be controllable.\n", " warnings.warn(\"controllable and uncontrollable status of event is not specified. All events are set to be controllable.\")\n" ] } ], "source": [ "import pytct\n", "pytct.init(\"Chp2\", overwrite=True)\n", "\n", "statenum=3 #number of states\n", "#states are sequentially labeled 0,1,...,statenum-1\n", "#initial state is labeled 0\n", "\n", "trans=[(0,'start',1),\n", " (1,'auto_finish',0),\n", " (1,'manual_stop',0),\n", " (1,'breakdown',2),\n", " (2,'fix',0)] # set of transitions\n", "#each triple is (exit state, event label, entering state)\n", "\n", "marker = [0,1] #set of marker states\n", "\n", "pytct.create('PRINTER', statenum, trans, marker)\n", "#create automaton A" ] }, { "cell_type": "code", "execution_count": 14, "id": "27b27515-c590-45b8-a880-4f84bd66987e", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.display_automaton('PRINTER')\n", "#pytct.AutomatonDisplay('PRINTER',convert=True, color=True)" ] }, { "cell_type": "code", "execution_count": 15, "id": "04aded7e-299c-492f-9835-11946205879d", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# are all states reachable?\n", "pytct.is_reachable('PRINTER')" ] }, { "cell_type": "code", "execution_count": 16, "id": "1186ba27-6134-4fa1-a726-4337fd16c7a9", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# is state 2 reachable?\n", "pytct.is_reachable('PRINTER',2)" ] }, { "cell_type": "code", "execution_count": 17, "id": "9a3d8a1a-a185-4c6d-a5d0-f84ff0ca60c2", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "['start', 'breakdown']" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# 0(initial state) -> 2\n", "pytct.reachable_string('PRINTER', 2)" ] }, { "cell_type": "code", "execution_count": 18, "id": "f9963477-9cf1-4c68-b523-35635d0b84e4", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# are all states coreachable?\n", "pytct.is_coreachable('PRINTER')" ] }, { "cell_type": "code", "execution_count": 19, "id": "0a32d5a6-d926-47e2-b377-85cd69d893f4", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# is state 2 reachable?\n", "pytct.is_reachable('PRINTER',2)" ] }, { "cell_type": "code", "execution_count": 20, "id": "4bc13057-62d8-4ba9-86fe-26ee4773488f", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "['fix']" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# 2 -> marker state(auto search)\n", "# search all marker states and return the first route found\n", "pytct.coreachable_string('PRINTER', 2)" ] }, { "cell_type": "code", "execution_count": 21, "id": "afa05956-02ef-4839-9e9d-ca5555bc72dc", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "state 0: reachable -> True\n", "state 0: coreachable -> True\n", "state 1: reachable -> True\n", "state 1: coreachable -> True\n", "state 2: reachable -> True\n", "state 2: coreachable -> True\n" ] } ], "source": [ "for i in range(statenum):\n", " print(f\"state {i}: reachable -> {pytct.is_reachable('PRINTER', i)}\")\n", " print(f\"state {i}: coreachable -> {pytct.is_coreachable('PRINTER', i)}\")" ] }, { "cell_type": "code", "execution_count": 10, "id": "8311ea27-947f-4960-8924-fe900e78d8b7", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "['start', 'breakdown']" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.shortest_string('PRINTER', 0, 2)" ] }, { "cell_type": "code", "execution_count": 11, "id": "8f863760-8d05-4165-b229-fd6d8118d816", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_nonblocking('PRINTER')" ] }, { "cell_type": "code", "execution_count": 12, "id": "e9dcba76-de94-4a73-891b-19c834dc34dc", "metadata": { "tags": [] }, "outputs": [ { "data": { "text/plain": [ "[]" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.blocking_states('PRINTER')" ] }, { "cell_type": "code", "execution_count": 13, "id": "c7036d82-437d-4022-b425-806ef15f06dc", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_trim('PRINTER')" ] }, { "cell_type": "code", "execution_count": 22, "id": "05491d33-a8d4-482e-9092-a07f35d433d1", "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/opt/conda/lib/python3.10/site-packages/pytct/name_converter.py:70: UserWarning: controllable and uncontrollable status of event is not specified. All events are set to be controllable.\n", " warnings.warn(\"controllable and uncontrollable status of event is not specified. All events are set to be controllable.\")\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "statenum=4 #number of states\n", "#states are sequentially labeled 0,1,...,statenum-1\n", "#initial state is labeled 0\n", "\n", "trans=[(0,'start',1),\n", " (1,'auto_finish',0),\n", " (1,'manual_stop',0),\n", " (1,'breakdown',2),\n", " (2,'dump',3),\n", " (2,'fix',0)] # set of transitions\n", "#each triple is (exit state, event label, entering state)\n", "\n", "marker = [0,1] #set of marker states\n", "\n", "pytct.create('PRINTER_JUNK', statenum, trans, marker)\n", "#create automaton A\n", "\n", "pytct.display_automaton('PRINTER_JUNK')\n", "#pytct.AutomatonDisplay('PRINTER_JUNK',convert=True, color=True)" ] }, { "cell_type": "code", "execution_count": 23, "id": "23686a19-12e0-4d7f-b51f-1cc624daaf85", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# are all states reachable?\n", "pytct.is_reachable('PRINTER_JUNK')" ] }, { "cell_type": "code", "execution_count": 24, "id": "d206c534-5368-4ecc-832f-e1384a7b8255", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# is state 3 reachable?\n", "pytct.is_reachable('PRINTER_JUNK',3)" ] }, { "cell_type": "code", "execution_count": 25, "id": "c6416017-9b16-494d-8738-88234f108a32", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "['start', 'breakdown', 'dump']" ] }, "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# 0(initial state) -> 3\n", "pytct.reachable_string('PRINTER_JUNK', 3)" ] }, { "cell_type": "code", "execution_count": 26, "id": "668f959f-2168-4009-b791-af39eaff8bd0", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 26, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# are all states coreachable?\n", "pytct.is_coreachable('PRINTER_JUNK')" ] }, { "cell_type": "code", "execution_count": 27, "id": "19765bf6-e75c-40b9-a194-b1eef778750b", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# is state 2 coreachable?\n", "pytct.is_coreachable('PRINTER_JUNK',2)" ] }, { "cell_type": "code", "execution_count": 28, "id": "ea269f09-1e35-44d1-b208-f1fa2fb89eb7", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "['fix']" ] }, "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# 2 -> marker state(auto search)\n", "pytct.coreachable_string('PRINTER_JUNK', 2)" ] }, { "cell_type": "code", "execution_count": 29, "id": "4bd12749-80ff-4127-9f24-8753fa556842", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "state 0: reachable -> True\n", "state 0: coreachable -> True\n", "state 1: reachable -> True\n", "state 1: coreachable -> True\n", "state 2: reachable -> True\n", "state 2: coreachable -> True\n", "state 3: reachable -> True\n", "state 3: coreachable -> False\n" ] } ], "source": [ "for i in range(statenum):\n", " print(f\"state {i}: reachable -> {pytct.is_reachable('PRINTER_JUNK', i)}\")\n", " print(f\"state {i}: coreachable -> {pytct.is_coreachable('PRINTER_JUNK', i)}\")" ] }, { "cell_type": "code", "execution_count": 30, "id": "2c4eb148-ba0b-44af-8068-edd489b4cc70", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "['breakdown', 'dump']" ] }, "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.shortest_string('PRINTER_JUNK', 1, 3)" ] }, { "cell_type": "code", "execution_count": 31, "id": "dbeb2c8f-f9c7-4bad-90f4-5f993cb2322a", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 31, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_nonblocking('PRINTER_JUNK')" ] }, { "cell_type": "code", "execution_count": 32, "id": "a01ad29b-2624-4d4e-a81f-10116603dd07", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[3]" ] }, "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.blocking_states('PRINTER_JUNK')" ] }, { "cell_type": "code", "execution_count": 33, "id": "fca4fae7-6348-4bea-977b-1def602b0a94", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 33, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_trim('PRINTER_JUNK')" ] }, { "cell_type": "code", "execution_count": 34, "id": "3829b697-04c3-4b4d-9f19-a599d2806258", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.trim('PRINTER_TRIM','PRINTER_JUNK')\n", "pytct.display_automaton('PRINTER_TRIM')\n", "#pytct.AutomatonDisplay('PRINTER_TRIM',convert=True, color=True)" ] }, { "cell_type": "code", "execution_count": null, "id": "da933a9e-410e-4a44-a648-93724bc7fc56", "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.11.6" } }, "nbformat": 4, "nbformat_minor": 5 }