99 lines
3.8 KiB
Plaintext
99 lines
3.8 KiB
Plaintext
digraph {
|
|
/* new idea */
|
|
|
|
title [label="Mailbox\nMachine" style="dotted"]
|
|
|
|
{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 -> 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"]
|
|
|
|
subgraph {rank=same; S1A P_open}
|
|
S0A -> S1A [label="got_mailbox"]
|
|
S1A [label="S1A:\nknown"]
|
|
S1A -> P_open [label="connected"]
|
|
S1A -> P1A_queue [label="add_message" style="dotted"]
|
|
P1A_queue [shape="box" label="queue" style="dotted"]
|
|
P1A_queue -> S1A [style="dotted"]
|
|
S1A -> S2A [style="invis"]
|
|
P_open -> P2_connected [style="invis"]
|
|
|
|
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"]
|
|
S2B -> S2A [label="lost"]
|
|
|
|
P2_connected [shape="box" label="RC.tx_open\nRC.tx_add(queued)"]
|
|
P2_connected -> S2B
|
|
|
|
S2A -> P2_queue [label="add_message" style="dotted"]
|
|
P2_queue [shape="box" label="queue" style="dotted"]
|
|
P2_queue -> S2A [style="dotted"]
|
|
|
|
S2B -> P2_send [label="add_message"]
|
|
P2_send [shape="box" label="queue\nRC.tx_add(msg)"]
|
|
P2_send -> S2B
|
|
|
|
{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"]
|
|
|
|
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
|
|
|
|
subgraph {rank=same; S4A S4B}
|
|
S4A [label="S4A:\nclosed"]
|
|
S4B [label="S4B:\nclosed"]
|
|
S4A -> S4B [label="connected"]
|
|
S4B -> S4A [label="lost"]
|
|
S4B -> S4B [label="add_message\nrx_message\nclose"] # is "close" needed?
|
|
|
|
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"]
|
|
|
|
}
|