Verificarea absentei pierderii sau duplicarii mesajelor.

In general, e posibil ca datorita structurii protocolului, aparitia unei
erori sa fie posibila doar dupa ce un anumit numar de mesaje au fost
schimbate si au fost indeplinite niste conditii necesare pentru activarea
erorii. De aceea, nu e suficient sa verificam ca primul sau al doilea
mesaj nu se poate pierde (nu poate fi duplicat): trebuie verificat acest
lucru pentru al n-lea mesaj, oricare ar fi numarul natural n.
(Bineinteles, daca o eroare e posibila, ea trebuie sa apara dupa un numar
finit de mesaje, dar e dificil de stabilit a propri o limita).

In concluzie, vom adauga la sistemul nostru de transmitator si receptor
un generator de mesaje, care furnizeaza transmitatorului mesajele care
vor fi trimise. Scopul generatorului este de a ne da control asupra
*continutului* mesajelor transmise, astfel incat sa verificam absenta
pierderii sau a duplicarii. Mai precis, sirul de mesaje generat va contine
un singur mesaj cu continut "interesant", plasat intr-o pozitie *arbitrara*
din sir, restul mesajelor fiind "neinteresante". Atunci, este suficient sa
verificam ca receptorul primeste exact un mesaj "interesant" pentru ca
protocolul sa fie corect.

Modelarea in Promela

Programul de selectie a unui lider din seria de exemple livrate cu Spin
exemplifica cele mai multe aspecte relevante din limbajul PROMELA.
Cateva observati la text:
- programul declara canale de comunicatie care accepta mesaje cu doua
campuri: un camp enumerare, de tipul mtype, si unul de tip byte.
- se declara un tablou de N canale de comunicatie, fiecare cu o coada
de asteptare de L mesaje. Pentru protocolul nostru, cea mai potrivita
e probabil comunicarea sincrona (fara tampon) pentru care declaram:

chan send_to_recv = [0] of ...

- pentru a primi de pe canalul c1 un mesaj cu doua campuri, si a le atribui
la variabilele x si y, scriem
   c1?x,y       /* sau, echivalent, c1?x(y) */
La fel, pentru trimitere, c2!x,y
- selectia ramurii urmate pentru structurile repetitive do .. od si de
selectie if .. fi se face *nedeterminist*, dintre toate variantele care
au conditia de executie (din stanga lui ->) adevarata.
- iesirea dintr-o structura repetitiva se face cu break;
- rularea unei instante din tipul de procese declarat cu
	proctype nume(parametri_formali)
se face cu
	run proctype nume(parametri_actuali)