Jazyk termů GCCS

  Jelikož GCCS je vizuální formalizmus, jeho syntaxí jsou grafické objekty diskutované v předchozí sekci. Protože se budeme zabývat překladem systémů GCCS do výrazů CCS, potřebujeme jejich formální definici.

Uvedeme definici jazyka termů GCCS (definice ) vycházející z [], v níž provedeme úpravy diskutované v poznámce následující tuto definici. Jedná se především o upřesnění zaměřená na specifikaci konečně stavových systémů s možností transformace do CCS.

Přiřazení grafických objektů z předchozí sekce k následně definovaným termům je zřejmé, neboť je dodržena shodná terminologie.

Nejprve zavedeme notaci pro základní pojmy (uvedené neformálně v předchozí sekci).

• Buď množina vnitřních sběrnic, .
• Označme nekonečnou množinu jmen portů tak, že a .

  Prvky budeme značit ...

• Dále označme množinu jmen sběrnic. Její prvky budeme značit ...
• Nechť množina vstupních akcí a množina výstupních akcí.

  Označme ...prvky množiny .

• Dále označíme množinu všech akcí , kde je vnitřní akce. Prvky Act značme ,...
• Zavedeme funkci , která přiřazuje každé akci l (mimo ) jméno jejího portu (tj. port(a)=a, a , ).

Pro grafický popis procesů GCCS používáme přechodový graf s návěštími. Zde uvádíme jeho formální definici převzatou z []:

 
• Definice .
• Poznámka:
• Definice .
• Poznámka:
• Lemma .
• Důkaz:
• Příklad .
• Definice .
• Poznámka:
• Označení:
• Definice .
• Definice .
• Poznámka: