From 02bea0036650c56993be358ecc587dd5e70f85f3 Mon Sep 17 00:00:00 2001 From: Brian Warner Date: Sun, 26 Feb 2017 02:33:14 -0800 Subject: [PATCH] dot: split Mailbox and Nameplate into separate machines add Terminator for shutdown --- docs/machines.dot | 62 +++-- docs/mailbox.dot | 225 ++++++------------ docs/mailbox_close.dot | 77 ------ docs/nameplate.dot | 101 ++++++++ docs/{nameplates.dot => nameplate_lister.dot} | 0 docs/terminator.dot | 50 ++++ 6 files changed, 260 insertions(+), 255 deletions(-) delete mode 100644 docs/mailbox_close.dot create mode 100644 docs/nameplate.dot rename docs/{nameplates.dot => nameplate_lister.dot} (100%) create mode 100644 docs/terminator.dot diff --git a/docs/machines.dot b/docs/machines.dot index 68a6a5e..c3713b6 100644 --- a/docs/machines.dot +++ b/docs/machines.dot @@ -2,6 +2,7 @@ digraph { Wormhole [shape="oval" color="blue" fontcolor="blue"] Boss [shape="box" label="Boss\n(manager)" color="blue" fontcolor="blue"] + Nameplate [shape="box" color="blue" fontcolor="blue"] Mailbox [shape="box" color="blue" fontcolor="blue"] Connection [label="Rendezvous\nConnector" shape="oval" color="blue" fontcolor="blue"] @@ -11,9 +12,9 @@ digraph { Send [shape="box" label="Send" color="blue" fontcolor="blue"] Receive [shape="box" label="Receive" color="blue" fontcolor="blue"] Code [shape="box" label="Code" color="blue" fontcolor="blue"] - Nameplates [shape="box" label="Nameplate\nLister" - color="blue" fontcolor="blue" - ] + NameplateLister [shape="box" label="Nameplate\nLister" + color="blue" fontcolor="blue"] + Terminator [shape="box" color="blue" fontcolor="blue"] Connection -> websocket [color="blue"] #Connection -> Order [color="blue"] @@ -28,37 +29,41 @@ digraph { Boss -> Send [style="dashed" label="send"] - Boss -> Mailbox [style="dashed" - label="set_nameplate\nclose\n(once)" - ] + Boss -> Nameplate [style="dashed" label="set_nameplate"] #Boss -> Mailbox [color="blue"] - Mailbox -> Boss [style="dashed" label="closed\n(once)"] Mailbox -> Order [style="dashed" label="got_message (once)"] Boss -> Key [style="dashed" label="got_code"] Key -> Boss [style="dashed" label="got_verifier\nscared"] Order -> Key [style="dashed" label="got_pake"] Order -> Receive [style="dashed" label="got_message"] #Boss -> Key [color="blue"] - Key -> Mailbox [style="dashed" label="add_message (pake)\nadd_message (version)"] + Key -> Mailbox [style="dashed" + label="add_message (pake)\nadd_message (version)"] Receive -> Send [style="dashed" label="got_verified_key"] Send -> Mailbox [style="dashed" label="add_message (phase)"] Key -> Receive [style="dashed" label="got_key"] Receive -> Boss [style="dashed" - label="happy\nscared\ngot_message"] + label="happy\nscared\ngot_message"] + Nameplate -> Connection [style="dashed" + label="tx_claim\ntx_release"] + Connection -> Nameplate [style="dashed" + label="connected\nlost\nrx_claimed\nrx_released"] + Mailbox -> Nameplate [style="dashed" label="release"] + Nameplate -> Mailbox [style="dashed" label="got_mailbox"] Mailbox -> Connection [style="dashed" - label="tx_claim\ntx_open\ntx_add\ntx_release\ntx_close\nstop" + label="tx_open\ntx_add\ntx_close" ] Connection -> Mailbox [style="dashed" - label="connected\nlost\nrx_claimed\nrx_message\nrx_released\nrx_closed\nstopped"] + label="connected\nlost\nrx_message\nrx_closed\nstopped"] - Connection -> Nameplates [style="dashed" - label="connected\nlost\nrx_nameplates" - ] - Nameplates -> Connection [style="dashed" - label="tx_list" - ] + Connection -> NameplateLister [style="dashed" + label="connected\nlost\nrx_nameplates" + ] + NameplateLister -> Connection [style="dashed" + label="tx_list" + ] #Boss -> Code [color="blue"] Connection -> Code [style="dashed" @@ -66,17 +71,24 @@ digraph { Code -> Connection [style="dashed" label="tx_allocate" ] - Nameplates -> Code [style="dashed" - label="got_nameplates" - ] - #Code -> Nameplates [color="blue"] - Code -> Nameplates [style="dashed" - label="refresh_nameplates" - ] + NameplateLister -> Code [style="dashed" + label="got_nameplates" + ] + #Code -> NameplateLister [color="blue"] + Code -> NameplateLister [style="dashed" + label="refresh_nameplates" + ] Boss -> Code [style="dashed" label="allocate_code\ninput_code\nset_code_code"] Code -> Boss [style="dashed" label="got_code"] - + Nameplate -> Terminator [style="dashed" label="nameplate_done"] + Mailbox -> Terminator [style="dashed" label="mailbox_done"] + Terminator -> Nameplate [style="dashed" label="close"] + Terminator -> Mailbox [style="dashed" label="close"] + Terminator -> Connection [style="dashed" label="stop"] + Connection -> Terminator [style="dashed" label="stopped"] + Terminator -> Boss [style="dashed" label="closed\n(once)"] + Boss -> Terminator [style="dashed" label="close"] } diff --git a/docs/mailbox.dot b/docs/mailbox.dot index 881c617..712fcd7 100644 --- a/docs/mailbox.dot +++ b/docs/mailbox.dot @@ -3,174 +3,93 @@ digraph { title [label="Message\nMachine" style="dotted"] - {rank=same; S0A P0_connected S0B} - S0A [label="S0A:\nknow nothing"] - S0B [label="S0B:\nknow nothing\n(bound)" color="orange"] - S0A -> P0_connected [label="connected"] - P0_connected [label="(nothing)" shape="box" style="dashed"] - P0_connected -> S0B + {rank=same; S0A S0B} + S0A [label="S0A:\nunknown"] + S0A -> S0B [label="connected"] + S0B [label="S0B:\nunknown\n(bound)" color="orange"] + S0B -> S0A [label="lost"] - S0A -> S1A [label="set_nameplate"] - S0B -> P2_connected [label="set_nameplate" color="orange" fontcolor="orange"] - P0A_queue [shape="box" label="queue" style="dotted"] S0A -> P0A_queue [label="add_message" style="dotted"] + P0A_queue [shape="box" label="queue" style="dotted"] P0A_queue -> S0A [style="dotted"] + S0B -> P0B_queue [label="add_message" style="dotted"] + P0B_queue [shape="box" label="queue" style="dotted"] + P0B_queue -> S0B [style="dotted"] - {rank=same; S1A P1A_queue} - S1A [label="S1A:\nnot claimed"] - S1A -> P2_connected [label="connected"] - S1A -> P1A_queue [label="add_message" style="dotted"] - P1A_queue [shape="box" label="queue" style="dotted"] - P1A_queue -> S1A [style="dotted"] + subgraph {rank=same; S1A P_open} + S0A -> S1A [label="got_mailbox"] + S1A [label="S1A:\nknown"] + S1A -> P_open [label="connected"] + S1A -> S2A [style="invis"] + P_open -> P2_connected [style="invis"] - {rank=same; S2A P2_connected S2B} - S2A [label="S2A:\nmaybe claimed"] + S0A -> S2A [style="invis"] + S0B -> P_open [label="got_mailbox" color="orange" fontcolor="orange"] + P_open [shape="box" + label="store mailbox\nRC.tx_open\nRC.tx_add(queued)" color="orange"] + P_open -> S2B [color="orange"] + + subgraph {rank=same; S2A S2B P2_connected} + S2A [label="S2A:\nknown\nmaybe opened"] + S2B [label="S2B:\nopened\n(bound)" color="green"] S2A -> P2_connected [label="connected"] - P2_connected [shape="box" label="RC.tx_claim" color="orange"] - P2_connected -> S2B [color="orange"] - S2B [label="S2B:\nmaybe claimed\n(bound)" color="orange"] - #S2B -> SrB [label="close()" style="dashed"] - #SrB [label="SrB" style="dashed"] - #S2A -> SrA [label="close()" style="dashed"] - #SrA [label="SrA" style="dashed"] + S2B -> S2A [label="lost"] - #S2B -> S2A [label="lost"] # causes bad layout - S2B -> foo [label="lost"] - foo [label="" style="dashed"] - foo -> S2A + P2_connected [shape="box" label="RC.tx_open\nRC.tx_add(queued)"] + P2_connected -> S2B - S2A -> P2C_queue [label="add_message" style="dotted"] - P2C_queue [shape="box" label="queue" style="dotted"] - P2C_queue -> S2A [style="dotted"] - S2B -> P2B_queue [label="add_message" style="dotted"] - P2B_queue [shape="box" label="queue" style="dotted"] - P2B_queue -> S2B [style="dotted"] + S2A -> P2_queue [label="add_message" style="dotted"] + P2_queue [shape="box" label="queue" style="dotted"] + P2_queue -> S2A [style="dotted"] - S1A -> S3A [label="(none)" style="invis"] - S2B -> P_open [label="rx_claimed" color="orange" fontcolor="orange"] - P_open [shape="box" label="store mailbox\nRC.tx_open\nRC.tx_add(queued)" color="orange"] - P_open -> S3B [color="orange"] + S2B -> P2_send [label="add_message"] + P2_send [shape="box" label="queue\nRC.tx_add(msg)"] + P2_send -> S2B - subgraph {rank=same; S3A S3B P3_connected} - S3A [label="S3A:\nclaimed\nopened >=once"] - S3B [label="S3B:\nclaimed\nmaybe open now\n(bound)" color="orange"] + {rank=same; P2_send P2_close P2_process_theirs} + P2_process_theirs -> P2_close [style="invis"] + S2B -> P2_process_ours [label="rx_message\n(ours)"] + P2_process_ours [shape="box" label="dequeue"] + P2_process_ours -> S2B + S2B -> P2_process_theirs [label="rx_message\n(theirs)" + color="orange" fontcolor="orange"] + P2_process_theirs [shape="box" color="orange" + label="N.release\nO.got_message if new\nrecord" + ] + P2_process_theirs -> S2B [color="orange"] + + S2B -> P2_close [label="close" color="red"] + P2_close [shape="box" label="RC.tx_close" color="red"] + P2_close -> S3B [color="red"] + + subgraph {rank=same; S3A P3_connected S3B} + S3A [label="S3A:\nclosing"] S3A -> P3_connected [label="connected"] + P3_connected [shape="box" label="RC.tx_close"] + P3_connected -> S3B + #S3A -> S3A [label="add_message"] # implicit + S3B [label="S3B:\nclosing\n(bound)" color="red"] + S3B -> S3B [label="add_message\nrx_message\nclose"] S3B -> S3A [label="lost"] - P3_connected [shape="box" label="RC.tx_open\nRC.tx_add(queued)"] - P3_connected -> S3B + subgraph {rank=same; P3A_done P3B_done} + P3A_done [shape="box" label="T.mailbox_done" color="red"] + P3A_done -> S4A + S3B -> P3B_done [label="rx_closed" color="red"] + P3B_done [shape="box" label="T.mailbox_done" color="red"] + P3B_done -> S4B - S3A -> P3_queue [label="add_message" style="dotted"] - P3_queue [shape="box" label="queue" style="dotted"] - P3_queue -> S3A [style="dotted"] - - S3B -> S3B [label="rx_claimed"] - - S3B -> P3_send [label="add_message"] - P3_send [shape="box" label="queue\nRC.tx_add(msg)"] - P3_send -> S3B - - S3A -> S4A [label="(none)" style="invis"] - S3B -> P3_process_ours [label="rx_message\n(ours)"] - P3_process_ours [shape="box" label="dequeue"] - P3_process_ours -> S3B - S3B -> P3_process_theirs [label="rx_message\n(theirs)" - color="orange" fontcolor="orange"] - P3_process_theirs [shape="box" color="orange" - label="RC.tx_release\nO.got_message if new\nrecord" - ] - /* pay attention to the race here: this process_message() will - deliver msg_pake to the WormholeMachine, which will compute_key() and - send(version), and we're in between S1A (where send gets - queued) and S3A (where send gets sent and queued), and we're no - longer passing through the P3_connected phase (which drains the queue). - So there's a real possibility of the outbound msg_version getting - dropped on the floor, or put in a queue but never delivered. */ - P3_process_theirs -> S4B [color="orange"] - - subgraph {rank=same; S4A P4_connected S4B} - S4A [label="S4A:\nmaybe released\nopened >=once\n"] - - S4B [label="S4B:\nmaybe released\nmaybe open now\n(bound)" color="orange"] - S4A -> P4_connected [label="connected"] - P4_connected [shape="box" label="RC.tx_open\nRC.tx_add(queued)\nRC.tx_release"] - S4B -> P4_send [label="add_message"] - P4_send [shape="box" label="queue\nRC.tx_add(msg)"] - P4_send -> S4B - S4A -> P4_queue [label="add_message" style="dotted"] - P4_queue [shape="box" label="queue" style="dotted"] - P4_queue -> S4A [style="dotted"] - - P4_connected -> S4B + subgraph {rank=same; S4A S4B} + S4A [label="S4A:\nclosed"] + S4B [label="S4B:\nclosed"] + S4A -> S4B [label="connected"] S4B -> S4A [label="lost"] - S4B -> P4_process_ours [label="rx_message\n(ours)"] - P4_process_ours [shape="box" label="dequeue"] - P4_process_ours -> S4B - S4B -> P4_process_theirs [label="rx_message\n(theirs)"] - P4_process_theirs [shape="box" label="O.got_message if new\nrecord"] - P4_process_theirs -> S4B - - S4A -> S5A [label="(none)" style="invis"] - S4B -> S5B [label="rx released" color="orange" fontcolor="orange"] - - P4_queue -> S5A [style="invis"] - subgraph {S5A P5_connected S5B} - {rank=same; S5A P5_connected S5B} - - S5A [label="S5A:\nreleased\nopened >=once"] - S5A -> P5_connected [label="connected"] - P5_connected [shape="box" label="RC.tx_open\nRC.tx_add(queued)"] - - S5B -> P5_send [label="add_message" color="green" fontcolor="green"] - P5_send [shape="box" label="queue\nRC.tx_add(msg)" color="green"] - P5_send -> S5B [color="green"] - S5A -> P5_queue [label="add_message" style="dotted"] - P5_queue [shape="box" label="queue" style="dotted"] - P5_queue -> S5A [style="dotted"] - - P5_connected -> S5B - S5B [label="S5B:\nreleased\nmaybe open now\n(bound)" color="green"] - S5B -> S5A [label="lost"] - - S5B -> P5_process_ours [label="rx_message\n(ours)"] - P5_process_ours [shape="box" label="dequeue"] - P5_process_ours -> S5B - S5B -> P5_process_theirs [label="rx_message\n(theirs)"] - P5_process_theirs [shape="box" label="O.got_message if new\nrecord"] - P5_process_theirs -> S5B - - foo5 [label="" style="invis"] - S5A -> foo5 [style="invis"] - foo5 -> P5_close [style="invis"] - S5B -> P5_close [label="close" style="dashed" color="orange" fontcolor="orange"] - P5_close [shape="box" label="tx_close" style="dashed" color="orange"] + S4B -> S4B [label="add_message\nrx_message\nclose"] + S0A -> P3A_done [label="close" color="red"] + S0B -> P3B_done [label="close" color="red"] + S1A -> P3A_done [label="close" color="red"] + S2A -> S3A [label="close" color="red"] + } - -/* - -Can this be split into one machine for the Nameplate, and a second for the -Mailbox? - -Nameplate: - -* 0: know nothing (connected, not connected) -* 1: know nameplate, never claimed, need to claim -* 2: maybe claimed, need to claim -* 3: definitely claimed, need to claim -* 4: definitely claimed, need to release -* 5: maybe released -* 6: definitely released - -Mailbox: -* 0: unknown -* 1: know mailbox, need open, not open -* 2: know mailbox, need open, maybe open -* 3: definitely open, need open -* 4: need closed, maybe open -* 5: need closed, maybe closed ? -* 6: definitely closed - - -*/ \ No newline at end of file diff --git a/docs/mailbox_close.dot b/docs/mailbox_close.dot deleted file mode 100644 index b4daeba..0000000 --- a/docs/mailbox_close.dot +++ /dev/null @@ -1,77 +0,0 @@ -digraph { - /* M_close pathways */ - title [label="Mailbox\nClose\nMachine" style="dotted"] - title -> S2B [style="invis"] - - /* All dashed states are from the main Mailbox Machine diagram, and - all dashed lines indicate M_close() pathways in from those states. - Within this graph, all M_close() events leave the state unchanged. */ - - SrA [label="SrA:\nwaiting for:\nrelease"] - SrA -> Pr [label="connected"] - Pr [shape="box" label="C.tx_release" color="orange"] - Pr -> SrB [color="orange"] - SrB [label="SrB:\nwaiting for:\nrelease" color="orange"] - SrB -> SrA [label="lost"] - SrB -> P_stop [label="rx_released" color="orange" fontcolor="orange"] - - ScA [label="ScA:\nwaiting for:\nclosed"] - ScA -> Pc [label="connected"] - Pc [shape="box" label="C.tx_close" color="orange"] - Pc -> ScB [color="orange"] - ScB [label="ScB:\nwaiting for:\nclosed" color="orange"] - ScB -> ScA [label="lost"] - ScB -> P_stop [label="rx_closed" color="orange" fontcolor="orange"] - - SrcA [label="SrcA:\nwaiting for:\nrelease\nclose"] - SrcA -> Prc [label="connected"] - Prc [shape="box" label="C.tx_release\nC.tx_close" color="orange"] - Prc -> SrcB [color="orange"] - Prc2 [shape="box" label="C.tx_close" color="orange"] - Prc2 -> SrcB [color="orange"] - SrcB [label="SrcB:\nwaiting for:\nrelease\nclosed" color="orange"] - SrcB -> SrcA [label="lost"] - SrcB -> ScB [label="rx_released" color="orange" fontcolor="orange"] - SrcB -> SrB [label="rx_closed" color="orange" fontcolor="orange"] - - - P_stop [shape="box" label="C.stop"] - P_stop -> SsB - - SsB [label="SsB: closed\nstopping"] - SsB -> Pss [label="stopped"] - Pss [shape="box" label="B.closed"] - Pss -> Ss - - Ss [label="Ss: closed" color="green"] - - S0A [label="S0A" style="dashed"] - S0A -> P_stop [style="dashed"] - S0B [label="S0B" style="dashed" color="orange"] - S0B -> P_stop [style="dashed" color="orange"] - - {rank=same; S2A S2B S3A S3B S4A S4B S5A S5B} - S1A [label="S1A" style="dashed"] - S1A -> P_stop [style="dashed"] - - S2A [label="S2A" style="dashed"] - S2A -> SrA [label="stop" style="dashed"] - S2B [label="S2B" color="orange" style="dashed"] - S2B -> Pr [color="orange" style="dashed"] - - S3A [label="S3A" style="dashed"] - S3B [label="S3B" color="orange" style="dashed"] - S3A -> SrcA [style="dashed"] - S3B -> Prc [color="orange" style="dashed"] - - S4A [label="S4A" style="dashed"] - S4B [label="S4B" color="orange" style="dashed"] - S4A -> SrcA [style="dashed"] - S4B -> Prc2 [color="orange" style="dashed"] - - S5A [label="S5A" style="dashed"] - S5B [label="S5B" color="green" style="dashed"] - S5A -> ScA [style="dashed"] - S5B -> Pc [style="dashed" color="green"] - -} diff --git a/docs/nameplate.dot b/docs/nameplate.dot new file mode 100644 index 0000000..4e6e682 --- /dev/null +++ b/docs/nameplate.dot @@ -0,0 +1,101 @@ +digraph { + /* new idea */ + + title [label="Nameplate\nMachine" style="dotted"] + title -> S0A [style="invis"] + + {rank=same; S0A S0B} + S0A [label="S0A:\nknow nothing"] + S0B [label="S0B:\nknow nothing\n(bound)" color="orange"] + S0A -> S0B [label="connected"] + S0B -> S0A [label="lost"] + + S0A -> S1A [label="set_nameplate"] + S0B -> P2_connected [label="set_nameplate" color="orange" fontcolor="orange"] + + S1A [label="S1A:\nnever claimed"] + S1A -> P2_connected [label="connected"] + + S1A -> S2A [style="invis"] + S1B [style="invis"] + S0B -> S1B [style="invis"] + S1B -> S2B [style="invis"] + {rank=same; S1A S1B} + S1A -> S1B [style="invis"] + + {rank=same; S2A P2_connected S2B} + S2A [label="S2A:\nmaybe claimed"] + S2A -> P2_connected [label="connected"] + P2_connected [shape="box" + label="RC.tx_claim" color="orange"] + P2_connected -> S2B [color="orange"] + S2B [label="S2B:\nmaybe claimed\n(bound)" color="orange"] + + #S2B -> S2A [label="lost"] # causes bad layout + S2B -> foo2 [label="lost"] + foo2 [label="" style="dashed"] + foo2 -> S2A + + S2A -> S3A [label="(none)" style="invis"] + S2B -> P_open [label="rx_claimed" color="orange" fontcolor="orange"] + P_open [shape="box" label="M.got_mailbox" color="orange"] + P_open -> S3B [color="orange"] + + subgraph {rank=same; S3A S3B} + S3A [label="S3A:\nclaimed"] + S3B [label="S3B:\nclaimed\n(bound)" color="orange"] + S3A -> S3B [label="connected"] + S3B -> foo3 [label="lost"] + foo3 [label="" style="dashed"] + foo3 -> S3A + + #S3B -> S3B [label="rx_claimed"] # shouldn't happen + + S3B -> P3_release [label="release" color="orange" fontcolor="orange"] + P3_release [shape="box" color="orange" label="RC.tx_release"] + P3_release -> S4B [color="orange"] + + subgraph {rank=same; S4A P4_connected S4B} + S4A [label="S4A:\nmaybe released\n"] + + S4B [label="S4B:\nmaybe released\n(bound)" color="orange"] + S4A -> P4_connected [label="connected"] + P4_connected [shape="box" label="RC.tx_release"] + S4B -> S4B [label="release"] + + P4_connected -> S4B + S4B -> foo4 [label="lost"] + foo4 [label="" style="dashed"] + foo4 -> S4A + + S4A -> S5B [style="invis"] + P4_connected -> S5B [style="invis"] + + subgraph {rank=same; P5A_done P5B_done} + S4B -> P5B_done [label="rx released" color="orange" fontcolor="orange"] + P5B_done [shape="box" label="T.nameplate_done" color="orange"] + P5B_done -> S5B [color="orange"] + + subgraph {rank=same; S5A S5B} + S5A [label="S5A:\nreleased"] + S5A -> S5B [label="connected"] + S5B -> S5A [label="lost"] + S5B [label="S5B:\nreleased" color="green"] + + S5B -> S5B [label="release\nclose"] + + P5A_done [shape="box" label="T.nameplate_done"] + P5A_done -> S5A + + S0A -> P5A_done [label="close" color="red"] + S1A -> P5A_done [label="close" color="red"] + S2A -> S4A [label="close" color="red"] + S3A -> S4A [label="close" color="red"] + S4A -> S4A [label="close" color="red"] + S0B -> P5B_done [label="close" color="red"] + S2B -> P3_release [label="close" color="red"] + S3B -> P3_release [label="close" color="red"] + S4B -> S4B [label="close" color="red"] + + +} diff --git a/docs/nameplates.dot b/docs/nameplate_lister.dot similarity index 100% rename from docs/nameplates.dot rename to docs/nameplate_lister.dot diff --git a/docs/terminator.dot b/docs/terminator.dot new file mode 100644 index 0000000..2fe01b9 --- /dev/null +++ b/docs/terminator.dot @@ -0,0 +1,50 @@ +digraph { + /* M_close pathways */ + title [label="Terminator\nMachine" style="dotted"] + + initial [style="invis"] + initial -> Snm [style="dashed"] + + Snm [label="Snm:\nnameplate active\nmailbox active" color="orange"] + Sn [label="Sn:\nnameplate active\nmailbox done"] + Sm [label="Sm:\nnameplate done\nmailbox active" color="green"] + S0 [label="S0:\nnameplate done\nmailbox done"] + + Snm -> Sn [label="mailbox_done"] + Snm -> Sm [label="nameplate_done" color="orange"] + Sn -> S0 [label="nameplate_done"] + Sm -> S0 [label="mailbox_done"] + + Snm -> Snm_closing [label="close"] + Sn -> Sn_closing [label="close"] + Sm -> Sm_closing [label="close" color="red"] + S0 -> P_stop [label="close"] + + Snm_closing [label="Snm_closing:\nnameplate active\nmailbox active" + style="dashed"] + Sn_closing [label="Sn_closing:\nnameplate active\nmailbox done" + style="dashed"] + Sm_closing [label="Sm_closing:\nnameplate done\nmailbox active" + style="dashed" color="red"] + + Snm_closing -> Sn_closing [label="mailbox_done"] + Snm_closing -> Sm_closing [label="nameplate_done"] + Sn_closing -> P_stop [label="nameplate_done"] + Sm_closing -> P_stop [label="mailbox_done" color="red"] + + {rank=same; S_stopping Pss S_stopped} + P_stop [shape="box" label="C.stop" color="red"] + P_stop -> S_stopping [color="red"] + + S_stopping [label="S_stopping" color="red"] + S_stopping -> Pss [label="stopped"] + Pss [shape="box" label="B.closed"] + Pss -> S_stopped + + S_stopped [label="S_stopped"] + + other [shape="box" style="dashed" + label="close -> N.close, M.close"] + + +}