finite_state

{ "cells": [ { "cell_type": "markdown", "id": "c200034d-b5f7-4af8-89fe-589d508d65d5", "metadata": { "tags": [] }, "source": [ "# Example 1" ] }, { "cell_type": "code", "execution_count": 1, "id": "e4582473-0c39-466a-9312-3f8851d561f2", "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/opt/conda/lib/python3.11/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": 1, "metadata": {}, "output_type": "execute_result" } ], "source": [ "import pytct\n", "pytct.init(\"Chp3\", 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\n", "\n", "pytct.display_automaton('PRINTER')\n", "#pytct.AutomatonDisplay('PRINTER',convert=True, color=True)" ] }, { "cell_type": "code", "execution_count": 2, "id": "9c39e080-d563-421e-acaf-8c897c279266", "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/opt/conda/lib/python3.11/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": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "statenum=2 #number of states\n", "#states are sequentially labeled 0,1,...,statenum-1\n", "#initial state is labeled 0\n", "\n", "trans=[(0,'start',0),\n", " (0,'auto_finish',1),\n", " (0,'manual_stop',0),\n", " (1,'take_printouts',0)] # set of transitions\n", "#each triple is (exit state, event label, entering state)\n", "\n", "marker = [0] #set of marker states\n", "\n", "pytct.create('HUMAN', statenum, trans, marker)\n", "#create automaton A\n", "\n", "pytct.display_automaton('HUMAN')\n", "#pytct.AutomatonDisplay('HUMAN',convert=True, color=True)" ] }, { "cell_type": "code", "execution_count": 3, "id": "ee5cb9c5-80da-4ec7-9e8e-63c1cdeb9c69", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.sync('PH_SYNC','PRINTER','HUMAN')\n", "#synchronous product PH of PRINTER and HUMAN\n", "\n", "pytct.display_automaton('PH_SYNC')\n", "#plot PH.DES" ] }, { "cell_type": "code", "execution_count": 4, "id": "1309345b-1c64-4c17-b12e-2f99d885c96a", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "0: 0,0\n", "1: 1,0\n", "2: 0,1\n", "3: 2,0\n", "\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "table = pytct.sync('PH','PRINTER','HUMAN',table=True, convert=True)\n", "#variant of sync that returns table of state correspondence\n", "\n", "print(table)\n", "#print table of state correspondence\n", "\n", "pytct.display_automaton('PH')\n", "#plot PH.DES with state pairs" ] }, { "cell_type": "code", "execution_count": 6, "id": "3f643369-de7c-4acc-bdb1-36b97f3a4f71", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "'0: 0,0\\n1: 1,0\\n2: 0,1\\n3: 2,0\\n'" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "table" ] }, { "cell_type": "code", "execution_count": 9, "id": "d375bac4-f18a-4dce-b76e-822fce1e37b8", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.selfloop('PRINTER_SL','PRINTER',['take_printouts'])\n", "#selfloop PRINTER with event take_printouts\n", "\n", "pytct.display_automaton('PRINTER_SL')\n", "#plot PRINTER_SL.DES" ] }, { "cell_type": "code", "execution_count": 10, "id": "609f1a6b-59a1-4c4e-8e41-419a1dfff949", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.selfloop('HUMAN_SL','HUMAN',['breakdown','fix'])\n", "#selfloop HUMAN with events breakdown, fix\n", "\n", "pytct.display_automaton('HUMAN_SL')\n", "#plot HUMAN_SL.DES" ] }, { "cell_type": "code", "execution_count": 12, "id": "b747a464-253b-4127-a350-b0ee214788af", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.sync('PH_SL','PRINTER_SL','HUMAN_SL')\n", "#synchronous product PH_SL of PRINTER_SL and HUMAN_SL\n", "\n", "pytct.isomorph('PH_SL','PH')\n", "#check if two automata are isomorphic (modulo relabeling of states and events)" ] }, { "cell_type": "code", "execution_count": 13, "id": "69604ce2-8166-4760-9a66-27e6c458244b", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_nonblocking('PH_SYNC')\n", "#check if PH is nonblocking" ] }, { "cell_type": "code", "execution_count": null, "id": "013e1a6e-3f18-4677-b8d2-330daf39606b", "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 }