<graphviz dot right>

digraph G {

  bgcolor = "grey93";
  rankdir="LR";
  subgraph ingredients {
      graph [shape=circle];
      node [shape=circle];
      basil;
      "pine nuts";
      parmesan;
      garlic;
      "olive oil";
      intA;
      intB;
      pesto;
  }
  subgraph transitions {
      node [shape=rect];
      blend;
      grate;
      mix;
  }
  basil -> blend;
  garlic -> blend;
  "pine nuts" -> blend -> intA -> mix;
  parmesan -> grate -> intB -> mix;
  "olive oil" -> mix;
  mix -> pesto [label="until mixed"];

}

</graphviz>

NOTE: pre- and postconditions are not included above.