Difference between revisions of "Producer-Consumer System/Process"
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= | 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>