tools/verification/models/wwnr.dot

   1 digraph state_automaton {
   2         {node [shape = plaintext, style=invis, label=""] "__init_not_running"};
   3         {node [shape = ellipse] "not_running"};
   4         {node [shape = plaintext] "not_running"};
   5         {node [shape = plaintext] "running"};
   6         "__init_not_running" -> "not_running";
   7         "not_running" [label = "not_running", color = green3];
   8         "not_running" -> "not_running" [ label = "wakeup" ];
   9         "not_running" -> "running" [ label = "switch_in" ];
  10         "running" [label = "running"];
  11         "running" -> "not_running" [ label = "switch_out" ];
  12         { rank = min ;
  13                 "__init_not_running";
  14                 "not_running";
  15         }
  16 }