arnost, Nazaretsky: Zápis v promele není vhodný, resp. potřebuju znát jeho přesnou sémantiku. Například si nevím rady s labely, ze kterých nevede žádný přechod (porovnejte BA pro "Xa" a výsledek spinu v promele).
To, co já dělám s tímto BA potom je to, že dělám kartézský součin Buchiho automatu se zásobníkovým systémem (totéž co zásobníkový automat, ale zanedbává se páska, tj. přechodová abeceda). Dokonce mi nevadí ani ty formule na hranách (dokonce to zjednodušuje práci), ale pravidla toho nového zásobníkového systému závisí na pravidlech toho BA.
Abych nemátl -- podívejte se na to Xa. Namalujte si přesně graf výstupu ze spinu (labely jsou stavy). Tady by člověk ještě od oka některé labely poté sloučil v jeden stav, aby mu vyšel BA akceptující požadovaná slova. Ale já to samozřejmě potřebuju obecně. A nechci se spolehnout na heuristiku, kterou vypozoruju z pár indicií.
Tady je PDF, kde se definuje ten kartézský součin (str. 3 dole), kdyby někdo chtěl, je tam de-facto i jádro toho, co jsem programoval. 
