dot: split Mailbox and Nameplate into separate machines
add Terminator for shutdown
This commit is contained in:
Brian Warner
parent
c8be988801
commit
02bea00366
|
|
@ -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"]
|
||||
}
|
||||
|
|
|
|||
225
docs/mailbox.dot
225
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
|
||||
|
||||
|
||||
*/
|
||||
|
|
@ -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"]
|
||||
|
||||
}
|
||||
101
docs/nameplate.dot
Normal file
101
docs/nameplate.dot
Normal file
|
|
@ -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"]
|
||||
|
||||
|
||||
}
|
||||
50
docs/terminator.dot
Normal file
50
docs/terminator.dot
Normal file
|
|
@ -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"]
|
||||
|
||||
|
||||
}
|
||||
Loading…
Reference in New Issue
Block a user