Následující algoritmus transformuje každou síť , která je dobře definovaným systémem GCCS, na systém definic procesů CCS.
Algoritmus je založen na kombinaci prohledávání grafu hierarchie tohoto systému do hloubky i do šířky. Pro procesy se volá předchozí algoritmus TransformujProces.
Idea algoritmu spočívá v postupném přidávání operátorů paralelní kompozice, restrikce a přejmenování aplikované na procesy CCS odpovídající jednotlivým podsystémům transformované sítě. Schéma transformace ukazuje obrázek .
Nejprve se konfrontuje množina akcí každého podsystému s jeho rozhraním v transformované síti, přičemž ty akce podsystému, pro něž neexistuje na jeho rozhraní port, jsou operátorem restrikce skryty (viz a).
Všechny podsystémy sítě jsou propojeny operátorem paralelní kompozice. Napojení portu na sběrnici se transformuje pomocí operátoru přejmenování (viz d), napojení portu na vnitřní sběrnici se transformuje navíc na restrikci výsledných komunikačních akcí (tím je definována -akce, viz c).
V předchozí kapitole jsme za účelem rozlišení vnitřních sběrnic pro potřeby transformace sítí do CCS zavedli množinu jmen vnitřních sběrnic . Kdybychom ponechali pro vnitřní sběrnici jen jedno jméno , jak uvádí [], vznikl by problém demonstrovaný na obrázku .
Figure: Problém jednoho jména pro vnitřní sběrnice v síti
Obě sběrnice v horní síti formálně reprezentují jednu sběrnici, neboť obě musí mít stejné jméno (jediné možné). To implikuje možnost synchronizace nežádoucích akcí.
Problém je vyřešen zavedením množiny jmen vnitřních sběrnic . Obě vnitřní sběrnice z obrázku nyní pojmenujeme rozdílnými jmény. Sběrnici propojující porty 1p nazveme a sběrnici propojující porty little nazveme . Nyní jsou možné jen synchronizace akcí little - 'little a 1p - '1p.
Speciální pozornost vyžadují volné porty stejného jména u různých podsystémů v síti. Paralelní kompozicí procesů CCS představujících jednotlivé podsystémy dochází k nežádoucímu propojení těchto portů ve smyslu komunikace (jakoby byly všechny tyto porty propojeny vnitřní sběrnicí). Problém řešíme přejmenováním jednoho z portů na nové jméno, které se v síti ještě nevyskytuje. Po provedení kompozice provedeme inverzní přejmenování zpět na původní jméno problémového portu (viz b).
Předchozí kroky jsou prováděny v rámci prohledání všech přímých podsystémů sítě do šířky. V dalším kroku je tento algoritmus rekurzivně aplikován na tyto podsystémy. Tato část představuje prohledávání do hloubky. Rekurzivní sestup se zastaví na úrovni procesů, které jsou reprezentovány v procházeném grafu uzly bez výstupních hran. Na procesy je aplikován algoritmus ).
Jak bylo uvedeno v sekci předchozí kapitoly, graf hierarchie systému GCCS může obsahovat více vstupních hran do některých uzlů a případně i cykly. Abychom zajistili, že algoritmus projde každým uzlem právě jednou (a provede příslušný výpočet), budeme značit již navštívené uzly.
4mm
Figure: Transformace sítě GCCS na výraz CCS