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

From PKC
Jump to navigation Jump to search
 
(8 intermediate revisions by the same user not shown)
Line 1: Line 1:
[[Producer-Consumer System/Write TLA Spec|Write TLA Spec]]
<noinclude>
[[Producer-Consumer System/TLC Model Checking|TLC Model Checking]]
<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>
</noinclude>
* [[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]]

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>

Retrieved from "https://pkc.pub/index.php?title=Producer-Consumer_System/Process&oldid=10260"