///|
fn dot_string(value : String) -> String {
  let out = StringBuilder()
  out.write_char('"')
  for char in value {
    match char {
      '"' => out.write_string("\\\"")
      '\\' => out.write_string("\\\\")
      '\n' => out.write_string("\\n")
      '\r' => out.write_string("\\r")
      _ => out.write_char(char)
    }
  }
  out.write_char('"')
  out.to_string()
}

///|
fn trace_uses_edge(
  trace : Array[TraceStep],
  from : String,
  to : String,
  action : String,
) -> Bool {
  for i in 1.. String {
  let out = StringBuilder()
  out.write_string("digraph moonctl {\n  rankdir=LR;\n")
  for i in 0.. s\{edge.to} [label=\{dot_string(edge.action)}\{style}];\n",
      )
    }
  }
  out.write_string("}\n")
  out.to_string()
}

///|
/// Export the explicit transition graph as Graphviz DOT. The initial state is
/// a double circle, and terminal stutter loops are shown explicitly.
pub fn Model::to_dot(self : Model) -> String {
  render_dot(self, [])
}

///|
/// Export the graph with a check result's witness or counterexample edges in
/// red. The report must have been produced from this model.
pub fn Model::to_dot_with_trace(self : Model, report : Report) -> String {
  render_dot(self, report.trace())
}