Producer-Consumer System/Process

<graphviz> digraph G {

   rankdir=LR;
   Design [URL="Producer-Consumer System/Design"];
   WriteTLASpec [URL="Producer-Consumer System/Write TLA Spec"];
   TLCModelChecking [URL="Producer-Consumer System/TLC Model Checking"];
   IntepretErrorTrace [URL="Producer-Consumer System/Intepret Error Trace"];
   Finish [URL="Producer-Consumer System/Finish"];

   Design -> WriteTLASpec -> TLCModelChecking;

TLCModelChecking->Finish[label="succeed"]; TLCModelChecking->IntepretErrorTrace [label="not succeed"]; IntepretErrorTrace->Design; Finish [shape=Msquare]; { rank=same; IntepretErrorTrace;WriteTLASpec; }

} </graphviz>

• Producer-Consumer System/Design
• Producer-Consumer System/Write TLA Spec
• Producer-Consumer System/TLC Model Checking
• Producer-Consumer System/Intepret Error Trace
• Producer-Consumer System/Finish