| digraph network_check_state_machine { |
| label="Network Check State Machine" |
| fontname="Helvetica,Arial,sans-serif" |
| node [fontname="Helvetica,Arial,sans-serif"] |
| edge [fontname="Helvetica,Arial,sans-serif"] |
| rankdir=LR; |
| node [shape = circle, fixedsize = true, height = 1.5, width = 1.5] n0, n1, n2; |
| node [shape = doublecircle, fixedsize = true, height = 1.5, width = 1.5]; n3; |
| ordering = "in" |
| n0 [label="Begin"] |
| n1 [label="Ping Gateway"] |
| n2 [label="Ping Internet"] |
| n3 [label="Idle"] |
| n0 -> n1 [label = "ε"]; |
| n0 -> n2 [label = "ε"]; |
| n0 -> n3 [label = "ε"]; |
| n1 -> n1 [label = "resume()"]; |
| n1 -> n2 [label = "resume()"]; |
| n1 -> n3 [label = "resume()"]; |
| n2 -> n2 [label = "resume()"]; |
| n2 -> n3 [label = "resume()"]; |
| n3 -> n0 [label = "begin()"]; |
| } |
