Difference between revisions of "Producer-Consumer System/Process"

From PKC
Jump to navigation Jump to search
 
Line 14: Line 14:
TLCModelChecking->IntepretErrorTrace [label="not succeed"];
TLCModelChecking->IntepretErrorTrace [label="not succeed"];
IntepretErrorTrace->Design;
IntepretErrorTrace->Design;
Finish [shape=Msquare];
Finish [shape=square];
{
{
    rank=same;
    rank=same;

Latest revision as of 16:00, 25 August 2021

<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=square]; { rank=same; IntepretErrorTrace;WriteTLASpec; }

} </graphviz>