digraph Controller {
  rankdir=LR;
  bgcolor="white";
  node [shape=Mrecord, style="filled,rounded", fontname="Helvetica-Bold", fontsize=12, penwidth=1.5];
  edge [fontname="Helvetica", fontsize=9];

  s00 [label="MODE_SHUTDOWN", fillcolor="#A8D8EA"];
  s01 [label="MODE_OPERATION", fillcolor="#77DD77"];
  s10 [label="MODE_HEATUP", fillcolor="#FFFACD"];
  s11 [label="MODE_SCRAM", fillcolor="#FF6B6B"];

  init [shape=point, width=0.25, color="black"];
  init -> s00 [penwidth=2.0];

  s00 -> s00 [label="!t_avg_above_min", penwidth=1.2, color="#4A90D9", fontcolor="#4A90D9", style="bold"];
  s00 -> s10 [label="t_avg_above_min", penwidth=1.2, color="#228B22", fontcolor="#228B22"];
  s01 -> s01 [label="inv2_holds", penwidth=1.2, color="#4A90D9", fontcolor="#4A90D9", style="bold"];
  s01 -> s11 [label="!inv2_holds", penwidth=1.2, color="#CC0000", fontcolor="#CC0000", style="bold"];
  s10 -> s01 [label="inv1_holds & p_above_crit & t_avg_in_range", penwidth=1.2, color="#228B22", fontcolor="#228B22"];
  s10 -> s10 [label="(inv1_holds & !t_avg_in_range) | (inv1_holds & !p_above_crit)", penwidth=1.2, color="#4A90D9", fontcolor="#4A90D9", style="bold"];
  s10 -> s11 [label="!inv1_holds", penwidth=1.2, color="#CC0000", fontcolor="#CC0000", style="bold"];
  s11 -> s00 [label="manual_reset", penwidth=1.2, color="#228B22", fontcolor="#228B22"];
  s11 -> s11 [label="!manual_reset", penwidth=1.2, color="#4A90D9", fontcolor="#4A90D9", style="bold"];
}