lynch done no tested

TP/TP 2/ex_lynch.pml

+#define N 20
+short matches = N;
+
+mtype = {ack, nack, err, accept, next};
+
+proctype transfer(chan inc, chan out, chan chin, chan chout){
+    byte o,i;
+    inc?next(o);
+    end:do
+        ::chin?nack(i) -> out!accept(i); chout!ack(o);
+        ::chin?ack(i)  -> out!accept(i); inc?next(o); chout!ack(o);
+        ::chin?err(i) -> chout!nack(o);
+    od
+}
+
+init {
+    chan AtoB = [1] of {byte, byte};
+    chan BtoA = [1] of {byte, byte};
+    chan Aout = [5] of {byte, byte};
+    chan Bout = [5] of {byte, byte};
+    chan Ain = [5] of {byte, byte};
+    chan Bin = [5] of {byte, byte};
+
+    atomic{
+        run transfer(Ain, Aout, BtoA, AtoB);
+        run transfer(Bin, Bout, AtoB, BtoA);
+
+        Ain!next(1); Ain!next(2); Bin!next(9); Bin!next(8);
+    }
+    AtoB!err(0);
+}

TP/TP1/ex_abin.pml

@@ -26,7 +26,9 @@ proctype node(chan parent){
 
 init {
     chan init_node = [0] of {short, short};
+    short depth;
 
     run node(init_node);
     init_node!create(N);
+    init_node?created(depth);
 }
\ No newline at end of file