bmc-loop.mp

input rboxes

verbatimtex
  %&latex
  \documentclass{article}
  \usepackage{times}
  \begin{document}
  etex

rbox_radius := 3bp;

diamond_radius := 5bp;

beginfig(1)
  rboxit.unroll (btex $\matrix{\mathrm{Unroll}\cr\mathrm{transition~function}\cr k~\mathrm{times}}$  etex);
  rboxit.check (btex $\matrix{\mathrm{Check~for}\cr\mathrm{counterexample}}$ etex);
  rboxit.checkct (btex $\matrix{\mathrm{Compare~}k\mathrm{~to}\cr\mathrm{completeness}\cr\mathrm{threshold}}$ etex);
  rboxit.increase (btex $\matrix{\mathrm{Increase}\cr k~\mathrm{by~one}}$ etex);

  unroll.c = (0,2cm);
  check.c = (4cm,2cm);
  checkct.c = (4cm,0);
  increase.c = (0,0);
  
  unroll.se - unroll.nw = check.se -  check.nw = checkct.se - checkct.nw = increase.se - increase.nw;

  drawboxed (unroll, check, checkct, increase);
  
  pair diamok;
  diamok = ((xpart check.ne)+12pt,1cm);
  draw diamok+(0,diamond_radius)--diamok+(diamond_radius,0)--diamok+(0,-diamond_radius)--diamok+(-diamond_radius,0)--cycle;
 
  drawarrow (.5[unroll.nw,unroll.ne])..0.5[unroll.c,check.c] shifted (0,1cm)..(.5[check.nw,check.ne]) cutbefore bpath.unroll cutafter bpath.check;

  drawarrow .5[check.ne,check.se]..(.5[check.ne,check.se] shifted (4pt,-4pt))..diamok+(0,diamond_radius) cutbefore bpath.check;
  
  drawarrow diamok+(0,-diamond_radius)..(.5[checkct.ne,checkct.se] shifted (4pt,4pt))..(.5[checkct.ne,checkct.se]) cutafter bpath.checkct;

  drawarrow diamok+(diamond_radius,0)--diamok+(diamond_radius+2cm,0);
  label.top (btex [error found] etex, diamok+(diamond_radius+1cm,0));
  label.rt (btex report etex, diamok+(diamond_radius+2cm,0));

  pair diamnok;
  diamnok = (2cm,(ypart checkct.sw)-12pt);
  draw diamnok+(0,diamond_radius)--diamnok+(diamond_radius,0)--diamnok+(0,-diamond_radius)--diamnok+(-diamond_radius,0)--cycle;

  drawarrow (.5[checkct.se,checkct.sw])..(.5[checkct.se,checkct.sw] shifted (-4pt,-2pt))..diamnok+(diamond_radius,0) cutbefore bpath.checkct;

  drawarrow diamnok+(-diamond_radius,0)..(.5[increase.se,increase.sw] shifted (4pt,-2pt))..(.5[increase.se,increase.sw]) cutafter bpath.increase;

  drawarrow (.5[increase.nw,increase.sw])..(.5[unroll.sw,increase.nw]-(10pt,0))  ..(.5[unroll.nw,unroll.sw]);

  drawarrow diamnok+(0,-diamond_radius)--diamnok+(0,-diamond_radius-1cm);
  label.rt (btex [reached] etex, diamnok+(0,-diamond_radius-0.5cm));
  label.bot (btex OK etex, diamnok+(0,-diamond_radius-1cm));

  drawarrow unroll.nw+(-0.5cm,0.5cm)--unroll.nw cutafter bpath.unroll;
  label.top (btex C program etex, unroll.nw+(-0.5cm,0.5cm));
endfig;

end.