finite_state

{ "cells": [ { "cell_type": "markdown", "id": "c200034d-b5f7-4af8-89fe-589d508d65d5", "metadata": { "tags": [] }, "source": [ "# PRINTER_SELL" ] }, { "cell_type": "code", "execution_count": 1, "id": "60301507-1d96-4e3c-97cd-390dc512bcb5", "metadata": {}, "outputs": [ { "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(\"Chp4\", overwrite=True)\n", "\n", "statenum=4 #number of states\n", "#states are sequentially labeled 0,1,...,statenum\n", "#initial state is labeled 0\n", "\n", "trans=[(0,'start',1,'c'),\n", " (1,'auto_finish',0,'u'),\n", " (1,'manual_stop',0,'c'),\n", " (1,'breakdown',2,'u'),\n", " (2,'fix',0,'c'),\n", " (2,'sell',3,'c')] #set of transitions\n", "#each triple is (exit state, event label, entering state)\n", "#each event is either 'c' (controllable) or 'u' (uncontrollable)\n", "\n", "marker = [0,1,3] #set of marker states\n", "\n", "pytct.create('PRINTER_SELL', statenum, trans, marker)\n", "#create automaton PRINTER_SELL\n", "\n", "pytct.display_automaton('PRINTER_SELL',color=True)\n", "#plot PRINTER_SELL.DES with color coding" ] }, { "cell_type": "code", "execution_count": 2, "id": "0bcac9b6-4758-460a-bdbb-3cc4ab739c8a", "metadata": {}, "outputs": [], "source": [ "#statenum=4 #number of states\n", "#states are sequentially labeled 0,1,...,statenum\n", "#initial state is labeled 0\n", "\n", "#trans=[(0,11,1),\n", "# (1,10,0),\n", "# (1,13,0),\n", "# (1,12,2),\n", "# (2,15,0),\n", "# (2,17,3)] #set of transitions\n", "#each triple is (exit state, event label, entering state)\n", "#odd numbers for controllable events; even numbers for uncontrollable events\n", "\n", "#marker = [0,1,3] #set of marker states\n", "\n", "#pytct.create('PRINTER_SELL', statenum, trans, marker)\n", "#create automaton PRINTER_SELL\n", "\n", "#pytct.display_automaton('PRINTER_SELL',color=True)\n", "#plot PRINTER_SELL.DES with color coding" ] }, { "cell_type": "code", "execution_count": 3, "id": "8f7c9a7e-a099-4250-83ef-5decc782f2f3", "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.subautomaton('S1','PRINTER_SELL',[],[(1,'manual_stop',0)])\n", "#create subautomaton S1 by removing from PRINTER_SELL \n", "#[state list] and [transition list]\n", "\n", "pytct.display_automaton('S1',color=True)\n", "#plot S1.DES with color coding" ] }, { "cell_type": "code", "execution_count": 4, "id": "dffd7084-e234-4170-bfb8-ce68fbc5f8ff", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_controllable('PRINTER_SELL','S1')\n", "#check if S1 is controllable wrt. PRINTER_SELL" ] }, { "cell_type": "code", "execution_count": 5, "id": "b91e36f5-b192-486b-9b16-65f6479245a2", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[]" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.uncontrollable_states('PRINTER_SELL','S1')\n", "#compute the set of uncontrollable states" ] }, { "cell_type": "code", "execution_count": 6, "id": "0c7d1961-2f38-4414-a740-0a4db2c662a6", "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/opt/conda/lib/python3.11/site-packages/pytct/des_check.py:65: UserWarning: Too many number of state. It is recommend to set 2\n", " warnings.warn(f\"Too many number of state. It is recommend to set {max_state}\")\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.subautomaton('S2','PRINTER_SELL',[2],[])\n", "#create subautomaton S2 by removing from PRINTER_SELL \n", "# [state list] and [transition list]\n", "\n", "pytct.display_automaton('S2',color=True)\n", "#plot S2.DES with color coding" ] }, { "cell_type": "code", "execution_count": 7, "id": "e5114885-d6ba-4d9b-93cd-5ab00387c37f", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_controllable('PRINTER_SELL','S2')\n", "#check if S1 is controllable wrt. PRINTER_SELL" ] }, { "cell_type": "code", "execution_count": 8, "id": "f5946698-0b04-4a10-aaae-9907a8e46acd", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[1]" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.uncontrollable_states('PRINTER_SELL','S2')\n", "#compute the set of uncontrollable states" ] }, { "cell_type": "code", "execution_count": 9, "id": "a0060523-4eb5-40df-b6d0-b09f75940e37", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# creat automaton E1\n", "\n", "statenum=3 #number of states\n", "#states are sequentially labeled 0,1,...,statenum\n", "#initial state is labeled 0\n", "\n", "trans=[(0,'start',0,'c'),\n", " (0,'auto_finish',0,'u'),\n", " (0,'manual_stop',0,'c'),\n", " (0,'breakdown',1,'u'),\n", " (1,'start',1,'c'),\n", " (1,'auto_finish',1,'u'),\n", " (1,'manual_stop',1,'c'),\n", " (1,'fix',1,'c'),\n", " (1,'breakdown',2,'u'),\n", " (2,'start',2,'c'),\n", " (2,'auto_finish',2,'u'),\n", " (2,'manual_stop',2,'c'),\n", " (2,'sell',2,'c')] #set of transitions\n", "#each triple is (exit state, event label, entering state)\n", "#each event is either 'c' (controllable) or 'u' (uncontrollable)\n", "\n", "marker = [0,1,2] #set of marker states\n", "\n", "pytct.create('E1', statenum, trans, marker)\n", "#create automaton E1\n", "\n", "pytct.display_automaton('E1',color=True)\n", "#plot E1.DES with color coding" ] }, { "cell_type": "code", "execution_count": 10, "id": "32a50cc2-4042-4f2b-90e1-66626d3d6f10", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_controllable('PRINTER_SELL','E1')\n", "#check if E1 is controllable wrt. PRINTER_SELL" ] }, { "cell_type": "code", "execution_count": 11, "id": "fb1d4451-3dbf-4183-8c7a-c73a8c7550a1", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[]" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.uncontrollable_states('PRINTER_SELL','E1')\n", "#compute the set of uncontrollable states" ] }, { "cell_type": "code", "execution_count": 12, "id": "e2b54ebf-3551-4ae4-a7dc-ef6b1a8255aa", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.sync('SE1','PRINTER_SELL','E1')\n", "#synchronous product\n", "\n", "pytct.display_automaton('SE1',color=True)\n", "#plot DES with color coding" ] }, { "cell_type": "code", "execution_count": 13, "id": "828e479c-4020-4e76-be55-80e103bb9a49", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_controllable('PRINTER_SELL','SE1')\n", "#check if SE1 is controllable wrt. PRINTER_SELL" ] }, { "cell_type": "code", "execution_count": 14, "id": "bd0e2ad3-31b6-47db-90c5-cd31a8e56bd0", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[]" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.uncontrollable_states('PRINTER_SELL','SE1')\n", "#compute the set of uncontrollable states" ] }, { "cell_type": "code", "execution_count": 15, "id": "762b3f6f-491a-43f4-a20c-56e1ae73ec39", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.subautomaton('SE2','SE1',[],[(4,'breakdown',5)])\n", "#create subautomaton SE2 by removing from SE1 \n", "# [state list] and [transition list]\n", "\n", "pytct.display_automaton('SE2',color=True)\n", "#plot SE2.DES with color coding" ] }, { "cell_type": "code", "execution_count": 16, "id": "fee92691-0964-45c8-8706-b4d41574d44a", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "False" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.is_controllable('PRINTER_SELL','SE2')\n", "#check if SE2 is controllable wrt. PRINTER_SELL" ] }, { "cell_type": "code", "execution_count": 17, "id": "9fab1a1e-2925-4286-9905-d939915373b4", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "[4]" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "pytct.uncontrollable_states('PRINTER_SELL','SE2')\n", "#compute the set of uncontrollable states" ] }, { "cell_type": "code", "execution_count": 18, "id": "771361ea-bcd7-4c9d-bd24-a45c4a6ba7a7", "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "

" ], "text/plain": [ "" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# creat automaton K2\n", "\n", "statenum = 4 # number of states\n", "\n", "trans = [(0,'start',1,'c'), \n", " (1,'auto_finish',2,'u'),\n", " (1,'breakdown',3,'u'),\n", " (3,'fix',2,'c')] # set of transitions\n", "\n", "marker = [2] # set of marker states\n", "\n", "pytct.create('K2', statenum, trans, marker) # create automaton\n", "\n", "pytct.display_automaton('K2', color=True) # display automaton\n", "# red transition: controllable; green transition: uncontrollable" ] }, { "cell_type": "code", "execution_count": 19, "id": "c2919984-2ec7-4fb1-8b8c-f660c27394f5", "metadata": {}, "outputs": [ { "data": { "text/plain": [ "DatInfo(\n", " text=\"Chp4/K2DAT\n", "\n", "\n", "Control data are displayed as a list of supervisor states\n", "where disabling occurs, together with the events that must\n", "be disabled there.\n", "\n", "Chp4/K2DAT is CONTROLLABLE\n", "\n", "control data:\n", "\n", "1: manual_stop\n", "2: start\n", "3: sell\n", "\n", "\",\n", " is_controllable=True,\n", " control_data={1: ['manual_stop'], 2: ['start'], 3: ['sell']}\n", ")" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# check controllability\n", "pytct.condat('K2DAT','PRINTER_SELL','K2')\n", "\n", "# print out control data\n", "pytct.printdat('K2DAT_txt','K2DAT')" ] }, { "cell_type": "code", "execution_count": null, "id": "bc4351ae-7926-4aa0-ba85-3f180a2ff8dd", "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 }