|
|
Kongruence pro stromové automaty
Žufan, Petr ; Janků, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Tento článek pojednává o testování ekvivalence stromových automatů (TA). Přináší nový algoritmus vycházející z algoritmu Bonchiho a Pouse pro slovní automaty. Tento nový algoritmus spojuje bisimulaci s determinizací za běhu. Pomocí optimalizace založené na kongruenčním uzávěru se snaží vyhýbat extrémnímu zvětšování stavového prostoru. Z tohoto hlediska je lepší než jiné metody pro tento problém.
|
|
|
Knihovna pro binární rozhodovací diagramy
Janků, Petr ; Hrubý, Martin (oponent) ; Holík, Lukáš (vedoucí práce)
Efektivní manipulace Booleovských funkcí je důležitou součástí mnoha počítačových návrhů. Jako datová struktura pro reprezentaci a manipulaci s Booleovskými funkcemi se běžně používají binární rozhodovací diagramy. Tyto diagramy se běžně používají v mnoha odvětvích, jako je například ověřování modelů, verifikace systému, návrh obvodů apod. V této práci jsou popsány tyto diagramy a jsou zde uvedeny i jejich modifikace. Dále jsou v této práci uvedeny a popsány techniky pro efektivní manipulaci a reprezentaci binárních rozhodovacích diagramů. Mimoto tato práce popisuje návrh a implementaci knihovny, která bude s těmito diagramy pracovat. Dále je diskutována potenciální aplikace vyvinuté knihovny v knihovně VATA pro manipulaci se stromovými automaty. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná a s knihovnou CacBDD. Výsledky experimentů ukázaly, že navrhovaná knihovna je poměrně blízká CUDD a CacBDD (dosahuje srovnatelného a většinou i lehce lepšího výkonu).
|
|
|
A Converter between the LESS and SASS Stylesheet Formats
Večerek, Attila ; Janků, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
The aim of this thesis is to research the differences between the CSS preprocessor languages, namely Less and Sass, and find applicable transformation methods to implement a converter between their dynamic stylesheet formats. A general introduction to the concept of CSS preprocessors is provided first, which is followed by a thorough description of the Less and Sass language features. In addition to this, all the discovered differences are stated and illustrative examples of the invented conversion methods are provided in this work. This is followed by the description of the design and implementation of the proposed converter. As a part of the contribution of this thesis, a CSS comparison tool based on abstract syntax tree transformation has also been developed. Its design is described along the testing procedure used to verify the invented conversion methods. The last part of the work summarizes the achieved results and the future directions of the converter.
|
|
|
Kongruence pro stromové automaty
Žufan, Petr ; Janků, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Tento článek pojednává o testování ekvivalence stromových automatů (TA). Přináší nový algoritmus vycházející z algoritmu Bonchiho a Pouse pro slovní automaty. Tento nový algoritmus spojuje bisimulaci s determinizací za běhu. Pomocí optimalizace založené na kongruenčním uzávěru se snaží vyhýbat extrémnímu zvětšování stavového prostoru. Z tohoto hlediska je lepší než jiné metody pro tento problém.
|
|
| |
|
|
A Converter between the LESS and SASS Stylesheet Formats
Večerek, Attila ; Janků, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
The aim of this thesis is to research the differences between the CSS preprocessor languages, namely Less and Sass, and find applicable transformation methods to implement a converter between their dynamic stylesheet formats. A general introduction to the concept of CSS preprocessors is provided first, which is followed by a thorough description of the Less and Sass language features. In addition to this, all the discovered differences are stated and illustrative examples of the invented conversion methods are provided in this work. This is followed by the description of the design and implementation of the proposed converter. As a part of the contribution of this thesis, a CSS comparison tool based on abstract syntax tree transformation has also been developed. Its design is described along the testing procedure used to verify the invented conversion methods. The last part of the work summarizes the achieved results and the future directions of the converter.
|
|
|
Plánování optimální trajektorie letadla
Janků, Petr ; Rozman, Jaroslav (oponent) ; Samek, Jan (vedoucí práce)
Tato práce se zabývá hledáním optimální trajektorie letadla, jak ve spojitém, tak v diskretizovaném prostředí. Teoretická část je věnována základním pojmům z problematiky plánování pohybu a popisu vybraných metod plánování pohybu letadla. Praktická část je věnována implementaci vybraných metod a ověření jejich optimálnosti. Z experimentů vyšlo, že menší výpočetní čas potřebuje metoda pracující se spojitým prostředím, ale né vždy najde optimální cestu.
|
|
|
Knihovna pro binární rozhodovací diagramy
Janků, Petr ; Hrubý, Martin (oponent) ; Holík, Lukáš (vedoucí práce)
Efektivní manipulace Booleovských funkcí je důležitou součástí mnoha počítačových návrhů. Jako datová struktura pro reprezentaci a manipulaci s Booleovskými funkcemi se běžně používají binární rozhodovací diagramy. Tyto diagramy se běžně používají v mnoha odvětvích, jako je například ověřování modelů, verifikace systému, návrh obvodů apod. V této práci jsou popsány tyto diagramy a jsou zde uvedeny i jejich modifikace. Dále jsou v této práci uvedeny a popsány techniky pro efektivní manipulaci a reprezentaci binárních rozhodovacích diagramů. Mimoto tato práce popisuje návrh a implementaci knihovny, která bude s těmito diagramy pracovat. Dále je diskutována potenciální aplikace vyvinuté knihovny v knihovně VATA pro manipulaci se stromovými automaty. Na závěr je tato knihovna porovnána s dobře známou a silně optimalizovanou knihovnou CUDD, která je volně dostupná a s knihovnou CacBDD. Výsledky experimentů ukázaly, že navrhovaná knihovna je poměrně blízká CUDD a CacBDD (dosahuje srovnatelného a většinou i lehce lepšího výkonu).
|
|
| |
|
| |
host ::
RSS.