digraph InspectorFSM {
  node [shape = point];
  init1;
  init2;

  node [shape = circle];
  init1 -> RWE [ label = " pauseOnFirstStmt " ]
  init2 -> RD [ label = " !pauseOnFirstStmt " ]
  RD -> RD [ label = " didPause" ];
  RD -> PWE [ label = " debuggerStmt " ];
  RWE -> PWE [ label = " didPause " ];
  RWP -> P [label = " didPause " ];
  RD -> R [ label = " enable " ];
  PWE -> P [label = " enable " ];
  RWE -> RWP [ label = " enable" ];
  R -> P [ label = " !implicitPause " ];
  R -> R [ label = " implicitPause "];
  P -> R [ label = " receivedCommand " ];
  P -> RD [ label = " disable "];
  R -> RD [ label = " disable "];

  { rank = same; RD RWE }
  { rank = same; R P }

  label = < <table border="0">
    <!-- hack: empty row for spacing -->
    <tr> <td></td><td> </td></tr>

    <tr><td>Abbrev</td><td>State</td></tr>
    <hr/>
    <tr><td>RWE</td><td>RunningWaitEnable</td></tr>
    <tr><td>RWP</td><td>RunningWaitPause</td></tr>
    <tr><td>RD</td><td>RunningDetached</td></tr>
    <tr><td>PWE</td><td>PausedWaitEnable</td></tr>
    <tr><td>P</td><td>Paused</td></tr>
    <tr><td>R</td><td>Running</td></tr>
  </table> >;
  labelloc = "b";
}