%% History:
% Pavel Tvrdik (26.12.2004)
%  + initial version for PhD Report
%
% Daniel Sykora (27.01.2005)
%
%  Michal Valenta (23.5. 2005)
% Upraveno a vyuzito pro formatovani diplomovych praci
% prozatim pouze v cestine.



%\documentclass[11pt,oneside,a4paper]{mr}%one-page printing
\documentclass[12pt,twoside,a4paper,czech,fleqn]{mr}%two-page printing
\usepackage[latin2]{inputenc}
\usepackage{color}

\usepackage[czech]{babel}
%\usepackage[cp1250]{inputenc}
%\usepackage{czech}
\usepackage{graphicx}


\input diplbakmacro.tex   % specialni makra pro formatovani diplomek
\renewcommand{\baselinestretch}{1.5}

                    
 % muzete si vytvorit i sva vlastni 
 % inspirujte se souborem bakmacro.tex
 % najdete tam radu jednoduchych definic, ktere zde ani nejsou pouzity
 % napriklad: 
 % \newcommand{\bfig}{\begin{figure}\begin{center}}
 % \newcommand{\efig}{\end{center}\end{figure}}
 % umoznuje pouzit prikaz \bfig namisto \begin{figure}\begin{center} atd.

  
\newcommand\TypeOfWork{Diplomová práce}
\newcommand\WorkTitle{Detekce tautologie}
\newcommand\FirstandFamilyName{Bc. Jan Schindler}
\newcommand\Month{květen}
\newcommand\Year{2009}
\newcommand\Supervisor{Ing. Petr Fišer, Ph.D.}

\newcommand\StudProgram{Elektrotechnika a informatika, strukturovaný, navazující magisterský}
\newcommand\StudBranch{Výpočetní technika}
\newcommand\Faculty{Fakulta elektrotechnická}
\newcommand\University{České vysoké učení technické v Praze}
%\hyphenation{hmot-né-ho}

\begin{document}

\coverpagestarts
\newpage ~
\newpage ~
\cleardoublepage %\thispagestyle{empty}
\vspace*{\fill}
\chapter*{Poděkování}
Rád bych na tomto místě poděkovat všem, kteří mi jakýmkoli způsobem pomáhali při tvorbě této diplomové práce. Zvláště pak děkuji svému vedoucímu, Ing. Petru Fišerovi, Ph.D., za odbornou pomoc, podnětné nápady a čas, který mi věnoval při návrhu a implementaci zde popisovaného projektu.

\cleardoublepage %\thispagestyle{empty}
\vspace*{\fill}
\chapter*{Prohlášení}
Prohlašuji, že jsem svou diplomovou práci vypracoval samostatně a použil jsem pouze podklady uvedené v přiloženém seznamu.

Nemám závažný důvod proti užití tohoto školního díla ve smyslu \S 60 Zákona č. 121/2000 Sb., o právu autorském, o právech souvisejících s právem autorským a  o změně některých zákonů (autorský zákon).
\\[15mm]
V  Hradci Králové, dne 15.5. 2009   \hfill \hbox to 70mm{\tiny\dotfill}
 
\cleardoublepage%\thispagestyle{empty}
\chapter*{Abstract}
This thesis deals with the design and the implementation of the tautology detection tool, which is based on algorithms from the Espresso, accepts input data in the Espresso PLA format and is integrable to the kernel of the programm BOOM~II. Emphasis is placed on the time efficiency of solution found in the diversity of the input logic functions.

\vglue60mm
\chapter*{Abstrakt}
Tato práce se zabývá návrhem a realizací nástroje na detekci tautologie, který je založen na algoritmech z nástroje Espresso, vstupní data přijímá ve formátu Espresso PLA a je integrovatelný to jádra programu BOOM~II. Důraz je kladen na časovou efektivitu nalezeného řešení při různorodosti charakteru logických funkcí na vstupu.

\cleardoublepage%\thispagestyle{empty}
\tableofcontents

\cleardoublepage%\thispagestyle{empty}
\listoffigures
%\addcontentsline{toc}{chapter}{\protect\numberline{}{Seznam obrázků}}

\cleardoublepage%\thispagestyle{empty}
\listoftables
%\addcontentsline{toc}{chapter}{\protect\numberline{}{Seznam tabulek}}

%\parskip=\baselineskip  %Mezi odstavci bude prazdny radek
\parskip=0.2cm
%**************************************************************
\cleardoublepage%\thispagestyle{empty}
\newcommand\uv[1]{\quotedblbase #1\textquotedblleft}
\mainbodystarts


\chapter{Úvod}

\input{1uvod} 
%\clearpage 

\cleardoublepage
\chapter{Popis problému, specifikace cíle}
\input{2popis}
\clearpage

\cleardoublepage
\chapter{Analýza a návrh řešení}
\label{analyza}
\input{3analyza}
\clearpage 

\cleardoublepage
\chapter{Realizace}
\label{realizace}
\input{4realizace}
\clearpage 

\cleardoublepage
\chapter{Testování}
\label{testovani}
\input{5testovani}
\clearpage

\cleardoublepage
\chapter{Závěr}
\input{6zaver}
\clearpage

\cleardoublepage
\bibliography{dp}
\bibliographystyle{abbrv}
%\addcontentsline{toc}{chapter}{\protect\numberline{}{Literatura}}

\newpage

\appendix
\chapter{Obsah přiloženého CD}
Na CD, které je přiloženo k této diplomové práci, jsou uložena tato data:

\begin{itemize}
 \item Zdrojový kód programu na detekci tautologie (dvě verze).
 \item Spustitelná verze programu (dvě varianty).
 \item Spustitelné verze všech porovnávaných programů. 
 \item Testované instance logických funkcí ve formátu PLA.
 \item Text diplomové práce ve formátu pdf.
 \item Zdrojový kód textu diplomové práce ve formátu \LaTeX.
 \item Obrázky použité v textu DP.
\end{itemize}


\clearpage
\cleardoublepage
\chapter{Malý slovník použitých pojmů a zkratek}

\begin{itemize}
 \item "0" - daná proměnná v přímém tvaru (např. $a$)
 \item "1" - daná proměnná v negovaném tvaru (např. $\overline{a}$)
 \item "2" - na hodnotě dané proměnné v daném termu nezáleží (totéž co DC)
 \item BDD - binární rozhodovací diagram, viz podkapitola~\ref{bdd-popis}.
 \item binátní - lze použít ve spojení pro sloupec nebo proměnnou, říkáme, že binátní je takový sloupec (proměnná), který obsahuje alespoň jeden symbol "0" a současně i alespoň jeden symbol "1" 
 \item DC - na hodnotě dané proměnné v daném termu nezáleží, z angl. \uv{Don't care} (totéž co "2")
 \item kofaktor - podmnožina z původní logické funkce, ze které je odvozen na základě daného termu, viz podkapitola~\ref{kofaktorDef}.
 \item komponenta - souvislý blok pokrytí logické funkce, kde se souvislost chápe na základě ortogonální incidence symbolů "0" nebo "1", viz podkapitola~\ref{realKomponenty}.
 \item PLA - Programmable logic array, nebo vnitřní třída programu BOOM~II reprezentující logickou funkci, zadanou ve formátu Espresso PLA
 \item pokrytí - dvourozměrné pole, kde sloupce tvoří proměnné dané logické funkce a řádky její termy
 \item unátní - lze použít ve spojení pro sloupec nebo proměnnou, říkáme, že unátní je takový sloupec (proměnná), který obsahuje buď pouze symboly "0" a "2" a nebo pouze "1" a "2".
\end{itemize}

\clearpage
\cleardoublepage
\chapter{Formát Espresso PLA}
\input{8priloha}

\clearpage
\cleardoublepage
\chapter{Integrace do jádra BOOM II}

Náš nástroj na detekci tautologie tvoří zapouzdřenou třídu, které je integrovatelná do jádra nástroje na minimalizaci logických funkcí, BOOM II. Vzájemná komunikace probíhá pomocí {\it interface}, který definuje dvě metody:

\begin{itemize}
\item
  bool isPlaTautology(PLA* pla); 
\item
  bool isSoPlaTautology(SoPLA* pla);
\end{itemize}

První z nich se používá pro příjem vstupních dat ve formě PLA struktury, která je vnitřní třídou nástroje BOOM~II. Druhá metoda je určena pro práci se speciálním případem jedno-vstupového PLA tzv. SoPLA\footnote{SoPLA = Single Output PLA}.

Příklad integrace a inicializace detekce tautologie je demonstrována následující úkázkou kódu:

\begin{verbatim}
  PLA* pla = new PLA();
  pla->LoadPLA("zadani.pla");
  TautologyDetector *tauDetector = new TautologyDetector();
  bool isTautology;
  isTautology = tauDetector->isPLAtautology(pla);
\end{verbatim}

%*****************************************************************************
% seznam literatury
% je v samostatnem souboru dipl.bib
% ten upravte dle vlastnich potreb
% potom zpracujte (a do textu zapracujte)
% pomoci prikazu "bibtex dipl" a nasledne "latex dipl"
% provedte alespon 2x, aby se poresily reference 
%\cleardoublepage
%\bibliography{reference}
%bibliographystyle{plain}
%\bibliographystyle{abbrv}

%*************************************************************************

\end{document}
