{"id":162,"date":"2019-10-17T20:11:02","date_gmt":"2019-10-18T01:11:02","guid":{"rendered":"http:\/\/multitude.net\/?page_id=162"},"modified":"2021-04-02T20:14:35","modified_gmt":"2021-04-03T01:14:35","slug":"behavior","status":"publish","type":"page","link":"https:\/\/multitude.net\/behavior\/","title":{"rendered":"BLESS Behavior"},"content":{"rendered":"\n<p>BLESS behavior for threads and devices is expressed as state-transition machines.  A set of states is declared, followed by transitions from a source state to a destination state when a transition condition is true, with possibly an action performed after leaving the source state and prior to entering the destination state.<\/p>\n\n\n\n<p>There are four kinds of states.  There must be exactly one &#8220;initial&#8221; state which cannot be the destination of any transition.  There may be one or more &#8220;final&#8221; states which cannot be the source of any transition.  Entering a &#8220;complete&#8221; state suspends execution until next dispatch.  An &#8220;execution&#8221; state is transitory between dispatch and suspension, therefore must always have at least one, enabled outgoing transition .<\/p>\n\n\n\n<p>The code below shows a simple, but non-trivial thread behavior in BLESS.  (It can be found in iPCA_Operation_Threads.aadl in the Open_PCA project in the Open PCA Pump example.)<\/p>\n\n\n\n<pre class=\"wp-block-preformatted\"><strong>thread<\/strong> Patient_Bolus_Checker\n \u00a0 <strong>features<\/strong>\n \u00a0 \u00a0 minimum_time_between_bolus: <strong>in<\/strong> <strong>data<\/strong> <strong>port<\/strong> Physical_Types::Minute\n \u00a0 \u00a0 \u00a0 {BLESS::Assertion => \"&lt;&lt;:=MINIMUM_TIME_BETWEEN_BOLUS>>\";};\n \u00a0 \u00a0 patient_button_request: <strong>in<\/strong> <strong>event<\/strong> <strong>port<\/strong>\n \u00a0 \u00a0 \u00a0 {BLESS::Assertion => \"&lt;&lt;PATIENT_BUTTON_REQUEST>>\";};\n \u00a0 \u00a0 patient_request_not_too_soon: <strong>out<\/strong> <strong>event<\/strong> <strong>port<\/strong>\n \u00a0 \u00a0 \u00a0 {BLESS::Assertion => \"&lt;&lt;PATIENT_REQUEST_NOT_TOO_SOON(now)>>\";};\n \u00a0 \u00a0 patient_request_too_soon: <strong>out<\/strong> <strong>event<\/strong> <strong>port<\/strong>\n \u00a0 \u00a0 \u00a0 {BLESS::Assertion => \"&lt;&lt;PATIENT_REQUEST_TOO_SOON(now)>>\";};\n \u00a0 \u00a0 stop: <strong>in<\/strong> <strong>event<\/strong> <strong>port<\/strong>;\u00a0 --use lower case 'stop'\n \u00a0 <strong>properties<\/strong>\n \u00a0 \u00a0 Dispatch_Protocol => Sporadic;\n <strong>end<\/strong> Patient_Bolus_Checker;<\/pre>\n\n\n\n<pre class=\"wp-block-preformatted\"><strong>thread<\/strong> <strong>implementation<\/strong> Patient_Bolus_Checker.i\n \u00a0 <strong>annex<\/strong> BLESS\n \u00a0 {**\n \u00a0 <strong>assert<\/strong>\n \u00a0\u00a0 <strong>&lt;&lt;<\/strong> LPB<strong>:<\/strong> <strong>:<\/strong>PATIENT_REQUEST_NOT_TOO_SOON<strong>(<\/strong>LAST_PATIENT_BOLUS<strong>)<\/strong> <strong>and<\/strong>\u00a0\n \u00a0 \u00a0 \u00a0 \u00a0 <strong>not<\/strong> <strong>(exists<\/strong> t<strong>~<\/strong>time <strong>in<\/strong> LAST_PATIENT_BOLUS,,<strong>now<\/strong>\u00a0\n \u00a0 \u00a0 \u00a0 \u00a0  \u00a0 \u00a0 <strong>that<\/strong> PATIENT_REQUEST_NOT_TOO_SOON<strong>(<\/strong>t<strong>))<\/strong> <strong>>><\/strong>\n \u00a0 <strong>invariant<\/strong> <strong>&lt;&lt;<\/strong> LPB<strong>()<\/strong> <strong>>><\/strong>\n \u00a0 <strong>variables<\/strong>\n \u00a0 \u00a0 last_patient_bolus <strong>~<\/strong> time<strong>:=<\/strong>0 s\n \u00a0 \u00a0 --\u00a0 variable last_patient_bolus holds ghost value LAST_PATIENT_BOLUS\n \u00a0\u00a0 \u00a0 <strong>&lt;&lt;<\/strong> AXIOM_LPB<strong>:<\/strong> <strong>:<\/strong> last_patient_bolus <strong>=<\/strong> LAST_PATIENT_BOLUS <strong>>>;<\/strong>\n \u00a0 <strong>states<\/strong>\n \u00a0 \u00a0 start<strong>:<\/strong> <strong>initial<\/strong> <strong>state<\/strong>\n \u00a0 \u00a0 \u00a0 <strong>&lt;&lt;<\/strong> last_patient_bolus <strong>=<\/strong> 0 ms <strong>and<\/strong> <strong>now=<\/strong>0 <strong>and<\/strong> LPB<strong>()<\/strong> <strong>>>;<\/strong> \n \u00a0 \u00a0 run<strong>:<\/strong> <strong>complete<\/strong> <strong>state<\/strong>\n \u00a0 \u00a0 \u00a0 <strong>&lt;&lt;<\/strong> LPB<strong>()>>;<\/strong>\n \u00a0 \u00a0 check_last_bolus_time<strong>:<\/strong> <strong>state<\/strong>\n \u00a0 \u00a0 \u00a0 <strong>&lt;&lt;<\/strong> LPB<strong>()<\/strong> <strong>and<\/strong> PATIENT_BUTTON_REQUEST<strong>@now<\/strong> <strong>and<\/strong> AXIOM_LPB<strong>()<\/strong> <strong>>>;<\/strong>\n \u00a0  done<strong>:<\/strong> <strong>final<\/strong> <strong>state;<\/strong>\n \u00a0<strong>transitions<\/strong>\n \u00a0\u00a0 go<strong>:<\/strong> start<strong>-[<\/strong> <strong>]-><\/strong> run<strong>{};<\/strong>\n \u00a0\u00a0 button<strong>:<\/strong> run <strong>-[on<\/strong> <strong>dispatch<\/strong> patient_button_request<strong>]-><\/strong> check_last_bolus_time<strong>{};<\/strong>\n \u00a0\u00a0 nottoosoon<strong>:<\/strong> check_last_bolus_time <strong>-[<\/strong>\n \u00a0 \u00a0  \u00a0 <strong>(now-<\/strong>minimum_time_between_bolus<strong>?)<\/strong> <strong>><\/strong> last_patient_bolus\n \u00a0\u00a0 \u00a0 \u00a0 <strong>]-><\/strong> run\n \u00a0\u00a0 \u00a0 <strong>{<\/strong>\u00a0 <strong>&lt;&lt;<\/strong> LPB<strong>()<\/strong> <strong>and<\/strong> PATIENT_BUTTON_REQUEST<strong>@now<\/strong> <strong>and<\/strong> AXIOM_LPB<strong>()<\/strong> <strong>and<\/strong>\u00a0\n \u00a0\u00a0 \u00a0  \u00a0 <strong>(now-<\/strong>MINIMUM_TIME_BETWEEN_BOLUS<strong>)<\/strong> <strong>><\/strong> last_patient_bolus <strong>>><\/strong>\n \u00a0\u00a0 \u00a0 patient_request_not_too_soon<strong>!<\/strong>\u00a0\n \u00a0\u00a0 \u00a0 <strong>;<\/strong> <strong>&lt;&lt;<\/strong> PATIENT_REQUEST_NOT_TOO_SOON<strong>(now)<\/strong> <strong>>><\/strong>\n \u00a0\u00a0 \u00a0 last_patient_bolus<strong>:=now<\/strong>\n \u00a0\u00a0 \u00a0 <strong>&lt;&lt;<\/strong> PATIENT_REQUEST_NOT_TOO_SOON<strong>(now)<\/strong> <strong>and<\/strong> last_patient_bolus<strong>=now<\/strong>\u00a0\n \u00a0\u00a0 \u00a0 \u00a0 <strong>and<\/strong> AXIOM_LPB<strong>()<\/strong> <strong>>>};<\/strong>\n \u00a0\u00a0 toosoon<strong>:<\/strong> check_last_bolus_time <strong>-[<\/strong>\n \u00a0 \u00a0  \u00a0 <strong>(now-<\/strong>minimum_time_between_bolus<strong>?)<\/strong> <strong>&lt;=<\/strong> last_patient_bolus\n \u00a0\u00a0 \u00a0 \u00a0 <strong>]-><\/strong> run\n \u00a0\u00a0 \u00a0 <strong>{<\/strong> patient_request_too_soon<strong>!<\/strong> <strong>};<\/strong>\n \u00a0\u00a0 quit<strong>:<\/strong> run<strong>-[on<\/strong> <strong>dispatch<\/strong> <strong>stop]-><\/strong>done<strong>{};<\/strong> \u00a0\n \u00a0 **};\u00a0\n <strong>end<\/strong> Patient_Bolus_Checker.i;\n <\/pre>\n","protected":false},"excerpt":{"rendered":"<p>BLESS behavior for threads and devices is expressed as state-transition machines. A set of states is declared, followed by transitions&hellip;<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_coblocks_attr":"","_coblocks_dimensions":"","_coblocks_responsive_height":"","_coblocks_accordion_ie_support":"","footnotes":""},"_links":{"self":[{"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/pages\/162"}],"collection":[{"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/comments?post=162"}],"version-history":[{"count":4,"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/pages\/162\/revisions"}],"predecessor-version":[{"id":453,"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/pages\/162\/revisions\/453"}],"wp:attachment":[{"href":"https:\/\/multitude.net\/wp-json\/wp\/v2\/media?parent=162"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}