Difference between revisions of "Producer-Consumer System/Process"
Jump to navigation
Jump to search
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
<noinclude> | |||
<graphviz> | <graphviz> | ||
digraph G { | digraph G { | ||
| Line 13: | 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; | ||
| Line 21: | Line 22: | ||
} | } | ||
</graphviz> | </graphviz> | ||
</noinclude> | |||
* [[Producer-Consumer System/Design]] | * [[Producer-Consumer System/Design]] | ||
* [[Producer-Consumer System/Write TLA Spec]] | * [[Producer-Consumer System/Write TLA Spec]] | ||
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>