dp1.sk.tex

\documentclass[11pt,final,oneside]{fithesis}
\usepackage[plainpages=false, pdfpagelabels]{hyperref}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usetikzlibrary{arrows}
\usepackage[toc,page]{appendix}
\usepackage{graphicx}
\usepackage{wrapfig}
\usepackage{subcaption}
\usepackage[T1]{fontenc}
\usepackage[latin2]{inputenc}
\usepackage[slovak]{babel}

\graphicspath{{images/}}

\thesislang{sk}
\thesistitle{Roz\v s\'irenie a refaktoriz\'acia n\'astroja BioDiVinE}
\thesissubtitle{Diplomov\' a pr\' aca}
\thesisstudent{Martin Demko}
\thesiswoman{false}
\thesisfaculty{fi}
\thesisyear{jar 2014}
\thesisadvisor{RNDr. David \v Safr\' anek, Ph.D.}

\begin{document}
\FrontMatter
\ThesisTitlePage


\begin{ThesisDeclaration}
\DeclarationText
\AdvisorName
\end{ThesisDeclaration}

\begin{ThesisThanks}
R\'ad by som po\v dakoval RNDr. Davidovi \v Safr\'ankovi, Ph.D. za jeho \v cas a trpezlivos\v t pri osvet\v lovan\'i problematiky a za jeho cenn\'e rady a 
podnety.
Z\'arove\v n by som chcel po\v dakova\v t aj rodine a svojej priate\v lke za ich mor\'alnu podporu a pomoc s nejednou jazykovou dilemou.
\end{ThesisThanks}

\begin{ThesisAbstract}
Pr\'aca sa venuje roz\v s\'ireniu n\'astroja BioDiVinE 1.0 o nov\'y obecnej\v s\'i popis vstupn\'eho modelu podporuj\'uceho aj neline\'arne funkcie 
preva\v zne sigmoid\'alneho charakteru. Z\'arove\v n s t\'ym mus\'i nov\'a verzia tohto programu poskytova\v t aj prechod od neline\'arneho vstupn\'eho
modelu k multi"~afinn\'emu, aby sa mohol nov\'y n\'astroj vyu\v z\'iva\v t k p\^ ovodn\'emu \'u\v celu, a s\'ice k overovaniu vlastnost\'i modelov.

Ke\v d\v ze sa v skuto\v cnosti jedn\'a o sadu n\'astrojov a nie o ucelen\'y program, dali sme si za \'ulohu zmeni\v t t\'uto skuto\v cnos\v t a vytvori\v t
pre u\v z\'ivate\v la jednoduch\'u, ale pou\v zite\v ln\'u konzolov\'u aplik\'aciu, ktor\'a bude zah\'r\v na\v t p\^ ovodn\'u funkcionalitu.\\\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\noindent
%This thesis is about extension of the BioDiVinE 1.0 tool by new general description of input model that would facilitate even non-linear functions such as 
%sigmoidal functions. This extension must propose with it a conversion of non-linear input model to multi-affine ones so that the new version of tool will 
%be still able of model checking.

%Because of fact that Biodivine 1.0 is a toolset rather than a simple tool we had the task to change this fact and create simplier and more user-friendly
%command-line interface that will offer the most of origin functionalities.

\end{ThesisAbstract}

\begin{ThesisKeyWords}
ordin\'arne diferenci\'alne rovnice, po \v castiach multi"~afinn\'y ODE model, neline\'arne regula\v cn\'e funkcie, overovanie modelov, LTL, 
Michaelis"~Mentenovej kinetika, Hillova kinetika\\\\

%\noindent
%ordinary differential equations, piecewise multi"~affine ODE model, non"~linear regulatory functions, model checking, LTL, Michaelis"~Menten kinetics,
%Hill equation
\end{ThesisKeyWords}

%====================================OBSAH==================================================
\MainMatter
\tableofcontents
%====================================UVOD===================================================
\chapter*{\' Uvod}
Biologick\'e syst\'emy s\'u obvykle zlo\v zit\'e komplexn\'e siete obrovsk\'ych rozmerov. Pr\'aca bioinformatikov a syst\'emov\'ych biol\'ogov v\v sak 
dokazuje, 
\v ze sa tieto siete skladaj\'u z ve\v lk\'eho po\v ctu drobnej\v s\'ich \v cast\'i, tzv. mot\'ivov. Tie s\'u ove\v la jednoduch\v sie na pozorovanie, aj 
ke\v d sa \v casto ukazuje, \v ze m\^ o\v zu aj pri svojej jednoduchosti vykazova\v t zauj\'imav\'e emergentn\'e vlastnosti.

Pre praktick\'e sk\'umanie dynamiky tak\'ychto mot\'ivov alebo stredne ve\v lk\'ych syst\'emov je vhodnou technikou overovanie modelov (vi\v d kapitolu
\ref{sec:modelChecking}). Existuje mno\v zstvo n\'astrojov a aplik\'aci\'i sl\'u\v ziacich k tomuto \'u\v celu (vi\v d kapitolu \ref{sec:similarTools}). Jedn\'ym z nich
je aj n\'astroj BioDiVinE 1.0 vyvinut\'y v Laborat\'oriu syst\'emovej biol\'ogie na Fakulte informatiky Masarykovej univerzity v~Brne. Bohu\v zia\v l je u\v z
mierne zastaran\'y a z\'arove\v n nie je vhodn\'y pre ve\v lk\'u \v sk\'alu modelov. 

V r\'amci neust\'aleho technick\'eho pokroku vznikol n\'avrh tieto chyby 
odstr\'ani\v t a nov\'y n\'astroj otestova\v t a poskytn\'u\v t \v sir\v sej verejnosti. O teoretick\'ych podkladoch, postupe pr\'ace, samotnej 
implement\'acii a praktick\'ych pr\'ikladoch hovoria nasleduj\'uce kapitoly. Hotov\'y n\'astroj bude vo\v lne k dispoz\'icii na \url{https://github.com/martindemko/BioDiVinE-1.1}.

%================================ZAKLADNE=POJMY=============================================
\chapter{Z\' akladn\' e pojmy}
Ne\v z za\v cneme zach\' adza\v t hlb\v sie do problematiky tejto pr\' ace a opisova\v t postupy a n\' astroje v nej pou\v zit\' e, 
je potrebn\' e vysvetli\v t na po\v ciatku nieko\v lko pojmov. Tieto sa v pr\' aci mnohokr\' at opakuj\' u a ich v\v casn\' ym uveden\' im
pred\' ideme nepochopite\v lnosti textu. Je tie\v z d\^ ole\v zit\'e poznamena\v t, \v ze t\'ato kapitola je z ve\v lkej miery doslovne citovan\'a
zo zdrojov uveden\'ych v\v zdy na konci ka\v zdej podkapitoly.

%-------------------------------------------------------------------------------------------
\section{LTL - Line\' arna Tempor\' alna Logika}
\label{sec:logika}
Tempor\' alna logika obecne je \v speci\' alna vetva logiky zaoberaj\' uca sa logickou \v strukt\' urou v\' yrokov v \v case. 
Je to formalizmus vhodn\' y pre overovanie vlastnost\' i form\' alnych dynamick\' ych syst\' emov resp. matematick\' ych modelov.

Line\' arna tempor\' alna logika (\v dalej len LTL) je najjednoduch\v sia verzia tempor\' alnej logiky, ktor\' a neumo\v z\v nuje vetvenie \v casu 
ani kvantifik\' atory.
M\^ o\v zeme ju pova\v zova\v t tie\v z za konkr\' etny v\' ypo\v ctov\' y kalkulus pracuj\' uci s tzv. formulami, definovan\' ymi nasleduj\' ucou syntaxou:
\begin{description}
\item[Atomick\' e propoz\' icie] (\v dalej len $AP$) \hfill
\begin{center}
$A > 0$ \\
$B \leq 5.834$ \\
$C \neq "nie"$ \\
{\it at\v d$\dots{}$}
\end{center}
\item[Logick\' e oper\' atory] \hfill
\begin{align*}
&\neg, \ \vee &-& \ \textrm{\it z\' akladn\' e logick\' e oper\' atory}\\
&\wedge , \ \rightarrow , \ \leftrightarrow , \ \mathbf{true} , \ \mathbf{false} \hfil &-& \ \textrm{\it odvoden\' e logick\' e oper\' atory}
\end{align*}
\item[Tempor\' alne oper\' atory] \hfill
\begin{itemize}
\item $\mathbf{X} \phi$ \ - \ \textrm{ne}$\mathbf{X}$\textrm{t, {\it vyjadruje platnos\v t $\phi$ v \v dal\v som stave}}
\item $\mathbf{G} \phi$ \ - \ $\mathbf{G}$\textrm{lobal, {\it vyjadruje trval\' u platnos\v t $\phi$ }}
\item {$\mathbf{F} \phi$} \ - \ $\mathbf{F}$\textrm{uture, {\it vyjadruje platnos\v t $\phi$ v niektorom z bud\' ucich stavov }}
\item {$\psi \mathbf{U} \phi$} \ - \ $\mathbf{U}$\textrm{ntil, {\it vyjadruje platnos\v t $\psi$, a\v z k\'ym neza\v cne plati\v t $\phi$}}
\item {$\psi \mathbf{R} \phi$} \ - \ $\mathbf{R}$\textrm{elease, {\it vyjadruje platnos\v t $\phi$, a\v z k\'ym neza\v cne plati\v t $\psi$, 
a to vr\'atane tohto bodu. Ak $\psi$ nikdy neza\v cne plati\v t, mus\'i $\phi$ plati\v t do nekone\v cna}},\\
\\
{\it kde $\phi$ a $\psi$ s\' u atomick\' e propoz\' icie.}
\end{itemize}
\end{description}
Potom plat\'i nasleduj\'uce:
\begin{itemize}
\item Ak $p \in AP$, tak $p$ je formula.
\item Ak $\phi$ a $\psi$ s\'u formuly, tak $\neg \psi$, $\phi \lor \psi$, $\phi \wedge \psi$, $\phi \rightarrow \psi$, $\phi \leftrightarrow \psi$, 
$\mathbf{X} \psi$, $\mathbf{F} \psi$, $\mathbf{G} \psi$, $\phi \mathbf{U} \psi$ a $\psi \mathbf{R} \phi$ s\'u formuly.
\end{itemize}
Takto vytvoren\'a LTL formula m\^ o\v ze by\v t splnite\v ln\'a nekone\v cnou postupnos\v tou pravdiv\'ych vyhodnoten\'i jednotliv\'ych $p \in AP$. 
T\'uto postupnos\v t si mo\v zno predstavi\v t ako nekone\v cn\'e slovo $w$, pre ktor\'e plat\'i $w = a_0,a_1,a_2,\dots{}$ a kde $a_i$ je pravdivostn\'a hodnota
nejakej $p \in AP$. Nech $w(i) = a_i$ a $w^i = a_i,a_{i+1},\dots{}$ je podpostupnos\v t alebo sufix slova $w$. Potom form\'alna defin\'icia rel\'acie splnite\v lnosti
$\vDash$ medzi slovom $w$ a LTL formulou vyzer\'a:
\begin{itemize}
\item $w \vDash p$,\hfil ak $p \in AP$ $\bigwedge$ $p = w(0)$
\item $w \vDash \neg\phi$,\hfil ak $\phi$ a $\psi$ s\'u LTL formuly $\bigwedge$ $w \nvDash \phi$
\item $w \vDash \phi \vee \psi$,\hfil ak $w \vDash \phi$ $\bigvee$ $w \vDash \psi$
\item $w \vDash {\bf X}\phi$,\hfil ak $w^1 \vDash \phi$
\item $w \vDash \phi {\bf U} \psi$,\hfil ak $\exists i,\ i \geq 0 \wedge w^i \vDash \psi$ $\bigwedge$ $\forall k,\ 0 \leq k < i \wedge w^k \vDash \phi$
\end{itemize}
Predch\'adzaj\'uce plat\'i pre z\'akladn\'e logick\'e a tempor\'alne oper\'atory, ktor\'e maj\'u ale dostato\v cne expres\'ivnu silu, aby s ich pomocou
mohli by\v t zadefinovan\'e \v lubovoln\'e LTL formuly. Ov\v sem pre u\v lah\v cenie z\'apisu aj \v c\'itania si m\^ o\v zeme dodefinova\v t roz\v s\'iren\'u
paletu oper\'atorov za predpokladu platnosti predch\'adzaj\'ucich pravidiel:
\begin{itemize}
\item $\phi \wedge \psi \ \equiv \ \neg(\neg \phi \vee \neg \psi)$,\hfil ak $\phi, \psi$ s\'u LTL formuly
\item $\phi \rightarrow \psi \ \equiv \ \neg \psi \vee \psi$,
\item $\phi \leftrightarrow \psi \ \equiv \ (\phi \rightarrow \psi) \vee (\psi \rightarrow \phi)$,
\item $\mathbf{true} \ \equiv \ p \vee \neg p$,\hfil ak $p \in AP$
\item $\mathbf{false} \ \equiv \ \neg\mathbf{true}$,
\item $\phi {\bf R} \psi \ \equiv \ \neg(\neg\phi{\bf U}\neg\psi)$,
\item $\mathbf{F} \phi \ \equiv \ \mathbf{true U} \phi$,
\item $\mathbf{G} \phi \ \equiv \ \neg \mathbf{F} \neg \phi$,
\end{itemize}
Napriek tomu, \v ze je LTL tou najprimit\' ivnej\v sou tempor\'alnou logikou, jej prevod do B\"uchiho automatu je v najhor\v som pr\' ipade 
exponenci\' alne zlo\v zit\' y. D\^ ovod tohto prevodu bude vysvetlen\' y v kapitole \ref{sec:modelChecking}. 
\cite{Clarke:MC:LTL}

%-------------------------------------------------------------------------------------------
\section{B\"uchiho automat}	%kniha Model checking str. 121
\label{sec:buchi}
Automat obecne je matematick\' y model stroja s kone\v cn\' ym mno\v zstvom pam\" ate spracov\' avaj\' uci vstup o nezn\' amej ve\v lkosti. 
Kv\^ oli obmedzeniu pam\" ate ho naz\' yvame kone\v cn\' ym automatom. Vstup sa naz\' yva slovo a m\^ o\v ze by\v t kone\v cn\' y aj nekone\v cn\' y.
B\" uchiho automat je potom najjednoduch\v s\' im kone\v cn\'ym automatom nad nekone\v cn\'ym slovom, a preto patr\'i do skupiny {$\omega$"~au\-to\-matov}.

Form\'alne je kone\v cn\' y automat $\mathcal{A}$ p\" atica $(\Sigma, Q, \Delta, Q_0, F)$, pre ktor\' u plat\'i:
\begin{itemize}
\item $\Sigma$\ je kone\v cn\'a abeceda
\item $Q$\ je kone\v cn\'a mno\v zina stavov
\item $\Delta \subseteq Q \times \Sigma \times Q$\ je rel\' acia, naz\'yvan\'a prechodov\'a funkcia
\item $Q_0 \subseteq Q$ je podmno\v zina mno\v ziny stavov, naz\' yvan\' a inici\' alne stavy
\item $F \subseteq Q$ je podmno\v zina mno\v ziny stavov, naz\'yvan\'a akceptuj\'uce stavy.
\end{itemize}
Pr\'iklad jednoduch\'eho automatu je dan\'y na Obr. \ref{fig:buchi}.

Automat nad kone\v cn\'ym slovom akceptuje toto slovo, ak po prejden\' i posledn\'eho znaku slova zodpovedaj\' uceho prechodu medzi dvoma stavmi, 
je tento posledn\' y stav v mno\v zine $F$. Av\v sak automat nad nekone\v cn\' ym slovom nem\^ o\v ze nikdy prejs\v t cez posledn\' y znak. Preto tak\' yto 
automat akceptuje nekone\v cn\' e slovo len v pr\' ipade, \v ze po\v cas prech\' adzania slova je aspo\v n jeden stav nav\v st\'iven\'y nekone\v cne \v casto 
a z\'arove\v n tento stav patr\'i aj do mno\v ziny $F$.

Automaty m\^ o\v zeme e\v ste rozl\'i\v si\v t na deterministick\'e a nedeterministick\'e. Deterministick\' y automat m\'a jednozna\v cne ur\v cen\'e prechody 
medzi stavmi. T\'ym sa mysl\'i, \v ze zo stavu $q \in Q$ sa pod znakom $s \in \Sigma$ d\'a prejs\v t maxim\'alne do jednoho stavu $q^{'} \in Q$. Naproti tomu
nedeterministick\'e automaty umo\v z\v nuj\'u prechod zo stavu $q$ pod slovom $s$ do stavov $Q^{'} \subseteq Q$. Na\v s\v tastie existuje algoritmus prevodu 
nedeterministick\'eho kone\v cn\'eho automatu  na deterministick\'y, ale iba nad kone\v cn\'ym slovom. Nev\'yhodou je ale ve\v lk\'y n\'arast po\v ctu stavov.
\cite{Clarke:MC:BA}
\begin{figure}[h]
\centering
\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,auto]
	\node[state,initial] (q0) {$q_0$};
	\node[state,accepting] (q1) [right of=q0] {$q_1$};
	\path[->]
	(q0) edge [bend left] node {a} (q1)
		 edge [loop below] node {b} ()
	(q1) edge [bend left] node {b} (q0)
		 edge [loop right] node {a} ();
\end{tikzpicture}
\caption{Jednoduch\'y deterministick\'y automat $\mathcal{A} :$ $\Sigma = \{a,b\},$ $Q = \{q_0,q_1\},$ $\Delta = \{(q_0,a,q_1),(q_0,b,q_0),(q_1,a,q_1),(q_1,b,q_0)\},$ 
	$Q_0 = \{q_0\}$, $F = \{q_1\}$}
\label{fig:buchi}
\end{figure}

%-------------------------------------------------------------------------------------------
\section{Z\'akon o mass action kinetike}
\label{sec:massAction}
Tento z\'akon vyjadruje z\'akladn\'e pravidlo fungovania chemick\'ych reakci\'i. Konkr\'etne r\'ychlos\v t, s akou chemick\'e substancie, \v ci u\v z 
ve\v lk\'e makromolekuly alebo mal\'e i\'ony, do seba nar\'a\v zaj\'u a interaguj\'u za tvorby nov\'ych chemick\'ych l\'atok. Predpokladajme, \v ze
substr\'aty $A$ a $B$ spolu reaguj\'u za vzniku novej l\'atky, produktu $C$:
\begin{equation}
\label{eq:simpleReaction}
A + B \overset{k}{\longrightarrow} C.
\end{equation}

R\'ychlos\v t tejto reakcie predstavuje r\'ychlos\v t tvorby produktu $C$, a s\'ice $\frac{d[C]}{dt}$, ktor\'a steles\v nuje po\v cet kol\'izi\'i za jednotku 
\v casu medzi reaktantami $A$ a $B$ a z\'arove\v n pravdepodobnos\v t, \v ze tieto kol\'izie maj\'u dostato\v cn\'u energiu na prekonanie aktiva\v cnej 
energie reakcie. To samozrejme z\'ale\v z\'i po prv\'e na koncentr\'acii reaktantov, ale aj na ich tvare a ve\v lkosti a tie\v z na teplote a pH roztoku. 
Kombin\'aciou t\'ychto a aj \v dal\v s\'ich faktorov dost\'avame neline\'arnu ordin\'arnu diferenci\'alnu rovnicu (z angl. \textit{ordinary differential 
equation}, skr\'atene ODE) \cite{ODE}:
\begin{equation}
\label{eq:differentialReaction}
\frac{d[C]}{dt} = k[A][B]
\end{equation}

Identifik\'acia vz\v tahu \ref{eq:simpleReaction} s rovnicou \ref{eq:differentialReaction} sa naz\'yva z\'akon mass action kinetiky (z angl. \textit{law of mass action}) a kon\v stanta $k$ 
je potom r\'ychlostn\'a kon\v stanta (z angl. \textit{rate constant}) tejto reakcie.

V skuto\v cnosti nejde o z\'akon ako tak\'y. Nie je to neporu\v site\v ln\'e pravidlo ako Newtonov gravita\v cn\'y z\'akon, ale sk\^ or ve\v lmi 
u\v zito\v cn\'y model, ktor\'y v\v sak nemus\'i by\v t vo v\v setk\'ych pr\'ipadoch validn\'y. \cite{Keener:1998:MP:MassAction}

%-------------------------------------------------------------------------------------------
\section{Michaelis-Mentenovej a Hillova kinetika}
\label{kinetiky}
%[odkaz na wiki a LectureNotes.pdf]
Je nutn\'e za\v ca\v t od enz\'ymovej kinetiky, preto\v ze pr\'ave t\'a bola hlavn\'ym kata\-ly\-z\'atorom pre objavenie nov\'ych sp\^ osobov modelovania 
chemick\'ych reakci\'i. Tie\v z je dobr\'e si uvedomi\v t, pre\v co tomu tak bolo. Enz\'ymov\'a kinetika toti\v z patr\'i medzi nieko\v lko pr\'ipadov, 
v ktor\'ych pou\v zitie mass action kinetiky nie je validn\'e. Pod\v la nej sa so zvy\v suj\'ucou koncentr\'aciou substr\'atu $S$ zvy\v suje r\'ychlos\v t
reakcie zlu\v covania s enz\'ymom $E$ line\'arne. Zatia\v l \v co v \textit{in-vivo} pr\'ipade t\'ato r\'ychlos\v t postupne konverguje k ur\v cit\'emu 
maximu, cez ktor\'e sa ned\'a dosta\v t ani dodato\v cn\'ym zv\'y\v sen\'im koncentr\'acie substr\'atu $S$.

Model, ktor\'y vysvet\v loval t\'uto odch\'ylku od z\'akona o mass action kinetike, bol prv\'ykr\'at prezentovan\'y v roku 1913 nemeck\'ym biochemikom Leonardom 
Michaelisom a kanadskou fyzi\v ckou Maud Mentenovou (odtia\v l \textit{kinetika Michaelis-Mentenovej}). V ich reakcii premie\v nal enz\'ym $E$ subtr\'at $S$ 
na produkt $P$ v dvoch f\'azach. Prv\'a bola reverzibiln\'a reakcia zlu\v covania $S$ s~$E$ za vzniku enz\'ym"~substr\'atov\'eho komplexu $C$ a druh\'a 
predstavovala rozpad komplexu $C$ za vzniku produktu $P$ a uvo\v lnenia nezmenen\'eho enz\'ymu $E$ (vi\v d rovnicu \ref{eq:enzimaticReaction}).
\begin{equation}
\label{eq:enzimaticReaction}
S + E \underset{k_2}{\overset{k_1}{\rightleftarrows}} C \overset{k_3}{\longrightarrow} E + P
\end{equation}
Je d\^ ole\v zit\'e si v\v simn\'u\v t, \v ze druh\'a reakcia nie je reverzibiln\'a.

Existuj\'u dva sp\^ osoby ako analyzova\v t t\'uto rovnicu a obe s\'u si ve\v lmi podobn\'e. Ide o rovnov\'a\v znu aproxim\'aciu a aproxim\'aciu 
kv\'azistacion\'arneho stavu. Za\v cneme aplik\'aciou z\'akona o mass action kinetike na tieto reakcie, \v co n\'am vo v\'ysledku d\'a nasleduj\'uce diferenci\'alne
rovnice, vyjadruj\'uce r\'ychlosti zmien jednotliv\'ych chemick\'ych l\'atok:
\begin{align}
\frac{d[S]}{dt} =& \ k_2[C] - k_1[S][E],\\
\frac{d[E]}{dt} =& \ (k_2 + k_3)[C] - k_1[S][E],\\
\frac{d[C]}{dt} =& \ k_1[S][E] - (k_2 + k_3)[C],\\
\frac{d[P]}{dt} =& \ k_3[C].
\end{align}
V\v simnite si, \v ze plat\'i $\frac{d[C]}{dt} + \frac{d[E]}{dt} = 0$, a preto 
\begin{equation}
\label{eq:E0}
[E] + [C] = [E_0], 
\end{equation}
kde $[E_0]$ je absol\'utna koncentr\'acia enz\'ymu v reakcii. \cite{Keener:1998:MP:Enzymes}\\

\noindent
\it A. \ Rovnov\'a\v zna aproxim\'acia\rm
\\

V p\^ ovodnej anal\'yze Michaelis a Mentenov\'a predpokladali, \v ze substr\'at je v neust\'alej rovnov\'ahe s enz\'ym"~substr\'atov\'ym komplexom, 
a teda, \v ze plat\'i 
\begin{equation}
\label{eq:equilibrity}
k_1[S][E] = k_2[C].
\end{equation}
Potom na z\'aklade platnosti vz\v tahov \ref{eq:E0} a \ref{eq:equilibrity}, m\^ o\v zeme zadefinova\v t nasleduj\'uci vz\v tah:
\begin{equation}
[C] = \frac{[E_0][S]}{K_s + [S]},
\end{equation}
kde $K_s = \frac{k_2}{k_1}$. Z toho zase vypl\'yva, \v ze r\'ychlos\v t reakcie $V$, respekt\'ive r\'ychlos\v t tvorby produktu $P$, m\^ o\v ze by\v t 
zadan\'a takto:
\begin{equation}
\label{eq:ks}
V = \frac{d[P]}{dt} = k_3[C] = \frac{k_3[E_0][S]}{K_s + [S]} = \frac{V_{max}[S]}{K_s + [S]},
\end{equation}
kde $V_{max} = k_3[E_0]$ je maxim\'alna reak\v cn\'a r\'ychlos\v t a predstavuje pr\'ipad, ke\v d v\v setky molekuly enz\'ymu s\'u naviazan\'e na substr\'at.

Pri malej koncentr\'acii substr\'atu je r\'ychlos\v t reakcie line\'arna, ak t\'ato koncentr\'acia nepresiahne celkov\'e mno\v zstvo enz\'ymu. Av\v sak pri
v\"a\v c\v s\'ich koncentr\'aci\'ach substr\'atu je r\'ychlos\v t reakcie limitovan\'a mno\v zstvom enz\'ymu a disocia\v cnou kon\v stantou 
(v na\v som pr\'ipade $k_3$). Ak sa koncentr\'acia substr\'atu pribli\v zuje hodnote $K_s$, znamen\'a to, \v ze reak\v cn\'a r\'ychlos\v t je rovn\'a 
polovici svojho maxima.

Poznamenajme v\v sak, \v ze vz\v tah \ref{eq:equilibrity} v re\'alnych podmienkach takmer nikdy neplat\'i a r\'ychlos\v t reakcie je tak ovplyvnen\'a
aj disocia\v cnou kon\v stantou enz\'ym"~substr\'atov\'eho komplexu v smere sp\"atn\'eho rozpadu (v na\v som pr\'ipade $k_2$). Pr\'ave z tohto d\^ ovodu tu
hovor\'ime o aproxim\'acii. \cite{Keener:1998:MP:Enzymes}
\\

\noindent
\textit{B: \ Aproxim\'acia kv\'azistacion\'arneho stavu}
\\

Inou alternat\'ivou anal\'yzi tejto enzymatickej reakcie je pr\'ave aproxim\'acia kv\'azistacion\'arneho stavu 
(z angl. \textit{Quasi-steady state aproximation}), ktor\'a je v dne\v snej dobe aj
najpou\v z\'ivanej\v sia. Jej tvorcovia, George Briggs a J.B.S. Haldane predpokladali, \v ze r\'ychlos\v t tvorby en\-z\'ym"~substr\'atov\'eho komple\-xu 
aj jeho disoci\'acia s\'u si od po\v ciatku rovn\'e. Tak\v ze plat\'i $\frac{d[C]}{dt} = 0$.

Aby sme dali tejto aproxim\'acii spr\'avny matematick\'y z\'aklad, je vhodn\'e zadefinova\v t nasleduj\'uce bezrozmern\'e
\footnote{Existuje viacero sp\^ osobov, ako syst\'em diferenci\'alnych rovn\'ic previes\v t na bezrozmern\'y. O tom v\v sak t\'ato pr\'aca nepojedn\'ava. 
\v Dal\v sie inform\'acie oh\v ladom tejto problematiky je mo\v zn\'e n\'ajs\v t v \cite{Keener:1998:MP:MathBackground}.}
premenn\'e:
\begin{align}
&\sigma = \frac{[S]}{[S_0]}, &\chi = \frac{[C]}{[E_0]},& &\tau = k_1[E_0]t,\nonumber \\
&\kappa = \frac{k_2 + k_3}{k_1[S_0]}, &\epsilon = \frac{[E_0]}{[S_0]},& &\alpha = \frac{k_2}{k_1[S_0]},
\end{align}
s pomocou ktor\'ych dostaneme syst\'em iba dvoch diferenci\'alnych rovn\'ic:
\begin{align}
\frac{d\sigma}{d\tau} &= -\sigma + \chi(\sigma + \alpha),\\
\label{eq:epsilon}
\epsilon\frac{d\chi}{d\tau} &= \sigma - \chi(\sigma + \kappa).
\end{align}

V porovnan\'i s koncentr\'aciou substr\'atu nejakej reakcie je koncentr\'acia enz\'ymu vo v\" a\v c\v sine pr\'ipadov ove\v la men\v sia. T\'ato 
skuto\v cnos\v t pekne odzrkad\v luje efekt\'ivnos\v t enz\'ymov ako katalyz\'atorov chemick\'ych reakci\'i. Preto je $\epsilon$ ve\v lmi mal\'e, typicky 
v rozmedz\'i od $10^{-2}$ do $10^{-7}$. Napriek tomu je reakcia \ref{eq:epsilon} r\'ychla a tie\v z r\'ychlo spad\'a do rovnov\'ahy, v ktorej zost\'ava,
aj ke\v d sa hodnota premennej $\sigma$ men\'i. Preto uva\v zujeme t\'uto aproxim\'aciu ako $\epsilon\frac{d\chi}{d\tau} = 0$. Toto tvrdenie je ekvivalentn\'e
tomu \'uvodn\'emu, \v ze $\frac{d[C]}{dt} = 0$.

Potom z tejto aproxim\'acie vypl\'yva:
\begin{align}
\chi = \frac{\sigma}{\sigma + \kappa},\\
\label{eq:uptakeSubstrate}
\frac{d\sigma}{d\tau} = -\frac{q\sigma}{\sigma + \kappa},
\end{align}
kde $q = \kappa - \alpha = \frac{k_3}{k_1[S_0]}$. Rovnica \ref{eq:uptakeSubstrate} popisuje r\'ychlos\v t pr\'irastku substr\'atu a je pomenovan\'a 
z\'akon Michaelis"~Mentenovej (z angl. \textit{Michaelis"~Menten law}). V znen\'i p\^ ovodn\'ych premenn\'ych tento z\'akon vyzer\'a takto:
\begin{equation}
\label{eq:km}
V = \frac{d[P]}{dt} = -\frac{d[S]}{dt} = \frac{k_3[E_0][S]}{[S] + K_m} = \frac{V_{max}[S]}{[S] + K_m},
\end{equation}
kde $K_m = \frac{k_2 + k_3}{k_1}$. Vz\v tahy \ref{eq:ks} a \ref{eq:km} s\'u si u\v z na prv\'y poh\v lad ve\v lmi podobn\'e. Jedin\'ym rozdielom s\'u
kon\v stanty $K_s$ a $K_m$. Ide o dva podobn\'e v\'ysledky na z\'aklade r\^ oznych predpokladov.

Tak ako z\'akon o mass action kinetike aj Michaelis"~Mentenovej z\'akon (vi\v d rovnicu \ref{eq:km}) nie je platn\'y univerz\'alne. Je v\v sak ve\v lmi u\v zito\v cn\'y 
a pou\v z\'ivan\'y, preto\v ze koeficient $K_m$ je experiment\'alne dobre pozorovate\v ln\'y a teda aj \v lahko merate\v ln\'y na rozdiel od individu\'alnych
r\'ychlostn\'ych kon\v st\'ant jednotliv\'ych chemick\'ych substanci\'i v reakcii. \cite{Keener:1998:MP:Enzymes}
\\

\noindent
\textit{C: \ Enz\'ymov\'a spolupr\'aca}
\\

Reak\v cn\'a r\'ychlos\v t mnoh\'ych enz\'ymov nem\'a klasick\'u hyperbolick\'u kriv\-ku, tak ako je predpokladan\'e pri pou\v zit\'i Michaelis"~Mentenovej 
kinetiky, ale miesto toho m\'a sigmoid\'alny charakter. To je sp\^ osoben\'e vlastnos\v tou t\'ychto enz\'ymov, ktor\'a im umo\v z\v nuje viaza\v t na seba
viacero substr\'atov naraz a z\'arove\v n t\'ym ovplyvni\v t obtia\v znos\v t tohto viazania. T\'ato vlastnos\v t sa naz\'yva kooper\'acia alebo 
s\'u\v cinnos\v t \v ci spolupr\'aca.

Tieto enz\'ymy maj\'u viac ako len jedno viazacie miesto (z angl. \textit{binding site}) a pri naviazan\'i prvej molekuly doch\'adza k zmene konform\'acie 
vzniknut\'eho komplexu, \v co m\^ o\v ze ovplyvni\v t naviazanie \v dal\v sej molekuly pozit\'ivne, ale aj negat\'ivne. Pre ka\v zd\'u nov\'u molekulu sa 
tento proces stup\v nuje.

Predpokladajme, \v ze enz\'ym $E$ dok\'a\v ze viaza\v t a\v z dve molekuly substr\'atu $S$, tak\v ze sa m\^ o\v ze nach\'adza\v t v troch r\^ oznych stavoch:
\begin{enumerate}
\item vo\v ln\'a molekula enz\'ymu ($E$),
\item komplex s jednou naviazanou molekulou substr\'atu ($C_1$),
\item komplex s dvoma naviazan\'ymi molekulami substr\'atu ($C_2$).
\end{enumerate}
Potom samotn\'e reakcie vyzeraj\'u nasledovne:
\begin{align}
S + E \underset{k_2}{\overset{k_1}{\rightleftarrows}} \ &C_1 \overset{k_3}{\longrightarrow} E + P,\\
S + C_1 \underset{k_5}{\overset{k_4}{\rightleftarrows}} \ &C_2 \overset{k_6}{\longrightarrow} C_1 + P.
\end{align}

Pou\v zit\'im z\'akona o mass action kinetike dostaneme najsk\^ or p\"a\v t diferenci\'alnych rovn\'ic a po \'uprave len tri. N\'asledn\'ym uplatnen\'im
aproxim\'acie kv\'azistacion\'arneho stavu dostaneme:
\begin{align}
[C_1] = \frac{K_2[E_0][S]}{K_1K_2 + K_2[S] + [S]^2},\\
[C_2] = \frac{[E_0][S]^2}{K_1K_2 + K_2[S] + [S]^2},
\end{align}
kde $K_1 = \frac{k_2 + k_3}{k_1}$, $K_2 = \frac{k_5 + k_6}{k_4}$ a $[E_0] = [E] + [C_1] + [C_2]$. Reak\v cn\'a r\'ychlos\v t potom vyzer\'a takto:
\begin{equation}
\label{eq:velocity}
V = k_3[C_1] + k_6[C_2] = \frac{(k_3K_2 + k_6[S])[E_0][S]}{K_1K_2 + K_2[S] + [S]^2}.
\end{equation}

Ak budeme teraz pre uk\'a\v zku uva\v zova\v t pr\'ipad pozit\'ivnej spolupr\'ace, tak naviazanie prvej molekuly $S$ bude relat\'ivne pomal\'e, ale
naviazanie druhej molekuly $S$ u\v z bude r\'ychlej\v sie. Tento jav m\^ o\v zeme vyjadri\v t ako $k_4 \rightarrow \infty$ a z\'arove\v n $k_1 \rightarrow 0$,
zatia\v l \v co $k_1k_4$ je kon\v stantn\'a hodnota. V tomto pr\'ipade ale naopak plat\'i, \v ze $K_1 \rightarrow \infty$ a $K_2 \rightarrow 0$, zatia\v l 
\v co $K_1K_2$ je tie\v z kon\v stantn\'e. Po aplik\'acii t\'ychto nov\'ych obmedzen\'i na vz\v tah \ref{eq:velocity} dost\'avame:
\begin{equation}
V = \frac{k_6[E_0][S]^2}{K_m^2 + [S]^2} = \frac{V_{max}[S]^2}{K_m^2 + [S]^2},
\end{equation}
kde $K_m^2 = K_1K_2$ a $V_{max} = k_6[E_0]$.

Obecne sa d\'a poveda\v t, \v ze ak enz\'ym dok\'a\v ze viaza\v t $n$ molek\'ul substr\'atu, existuje tie\v z $n$ rovnov\'a\v znych kon\v st\'ant
$K_1,\dots{},K_n$, pre ktor\'e bude plati\v t $K_n \rightarrow 0$ a $K_1 \rightarrow \infty$, zatia\v l \v co $K_1K_n$ bude st\'ale kon\v stanta a obecn\'a
rovnica reak\v cnej r\'ychlosti potom vyzer\'a:
\begin{equation}
V = \frac{V_{max}[S]^n}{K_m^n + [S]^n},
\end{equation}
kde $K_m^n = \prod_{i=1}^n{K_i}$. T\'ato rovnica je zn\'ama ako Hillova rovnica alebo Hillova kinetika a kon\v stanta $K_m^n$ vyjadruje koncentr\'aciu, 
pri ktorej je r\'ychlos\v t reakcie v polovici svojho maxima, tj. $\frac{V_{max}}{2}$. Typicky faktor $n$, vyjadruj\'uci strmos\v t reak\v cnej krivky 
(vi\v d Obr. \ref{fig:factor})
b\'yva men\v s\'i ako skuto\v cn\'y po\v cet viazac\'ich miest na enz\'yme, \v casto to dokonca nie je ani cel\'e \v c\'islo. Stoj\'i za zmienku, \v ze 
v pr\'ipade, ke\v d $n = 1$, zodpoved\'a Hillova kinetika Michaelis"~Mentenovej kinetike, preto n\'a\v s n\'astroj pon\'uka iba mo\v znos\v t zadania 
Hillovej rovnice (vi\v d kapitolu \ref{sec:model}.B).

T\'ato met\'oda aproxim\'acie je okrem enz\'ymovej kinetiky ve\v lmi vhodn\'a pre simulovanie regul\'acie g\'enovej expresie pomocou represorov alebo 
aktiv\'atorov.
\cite{Keener:1998:MP:Enzymes}
\begin{figure}[h]
	\centering
	\includegraphics[width=1\textwidth]{hill_factor_2.png}
	\caption{Faktor $n$ Hillovej kinetiky pre ve\v lkosti $1, 2$ a $4.5$ ($K_m = 2$)}
	\label{fig:factor}
\end{figure}

%------------------------------------------------------------------------------------------- 
\section{Model checking}
\label{sec:modelChecking}
Model checking alebo overovanie modelov je automatizovan\'a technika form\'alnej verifik\'acie \v specifikovan\'ych vlastnost\'i kone\v cn\'eho stavov\'eho 
syst\'e\-mu. Hlavnou v\'yzvou tejto problematiky je \'uspe\v sne si poradi\v t s probl\'emom expl\'ozie stavov\'eho priestoru (z angl. \textit{state space
explosion}).

Proces overovania modelov pozost\'ava z nasleduj\'ucich pod\'uloh:
\begin{description}
\item[Modelovanie] 
Prvou \'ulohou je prevedenie sk\'uman\'eho syst\'emu do form\'alneho matematick\'eho modelu, ktor\'y bude akceptovan\'y vybran\'ym o\-verovac\'im n\'astrojom.
V niektor\'ych pr\'ipadoch je to \v lahk\'a \'uloha, av\v sak v in\'ych je potreba pou\v zi\v t vhodn\'e abstrakcie za \'u\v celom odstr\'anenia 
irelevantn\'ych detailov alebo naopak zv\'yraznenia ist\'ych \v crtov sk\'uman\'eho syst\'emu.
\item[\v Specifik\'acia]
E\v ste pred samotn\'ym overovan\'im, je nevyhnutn\'e \v specifikova\v t vlastnosti, ktor\'e m\'a sk\'uman\'y syst\'em sp\'l\v na\v t, preto\v ze pr\'ave tie
budeme \v dalej overova\v t. \v Specifik\'aciou sa mysl\'i pou\v zitie nejak\'eho vhodn\'eho formalismu. Typicky napr\'iklad tempor\'alnej logiky, ktor\'a
umo\v z\v nuje sk\'uma\v t spr\'avanie syst\'emu v \v case. My budeme pou\v z\'iva\v t LTL (vi\v d kapitolu \ref{sec:logika}).
\item[Overovanie]
Model checking dok\'a\v ze overi\v t, \v ci model vyhovuje danej \v specifik\'acii, ale nedok\'a\v ze rozhodn\'u\v t, \v ci dan\'a \v specifik\'acia 
pokr\'yva v\v setky vlastnosti, ktor\'ym sk\'uman\'y syst\'em vyhovuje. Toto je ve\v lmi v\'yznam\-n\'y probl\'em form\'alneho overovania modelov.

V\'ysledkom overovania modelu je bu\v d tvrdenie \'ano (v zmysle model sp\'l\v na vlastnos\v t) alebo nie (model nesp\'l\v na vlastnos\v t) a v tomto pr\'ipade
by mal pou\v zit\'y n\'astroj poskytn\'u\v t mo\v znos\v t trasovania chyby (z~angl. \textit{error trace}). T\'ato chybov\'a trasa grafom sa obvykle 
pou\v z\'iva ako protipr\'iklad k overovanej vlastnosti. S jej pomocou m\^ o\v zeme lep\v sie pochopi\v t d\^ ovod a miesto vzniku chyby a upravi\v t syst\'em 
pod\v la toho. \cite{Clarke:MC:Process}
\end{description}

Prv\'e algoritmy pre overovanie modelov pou\v z\'ivali ako formalizmus matematick\'eho modelu dan\'eho syst\'emu Kripkeho \v strukt\'uru. Je to obdoba 
nedeterministick\'eho kone\v cn\'eho automatu (vi\v d kapitolu \ref{sec:buchi}), ktor\'eho stavy s\'u ozna\v cen\'e v\'yrazmi z mno\v ziny $2^{AP}$, kde 
$AP$ s\'u atomick\'e propoz\'icie formuly $f$ (vi\v d kapitolu \ref{sec:logika}). V\v setky tieto stavy s\'u akceptuj\'uce.

Nesk\^ or sa pou\v z\'ival $\mu$-kalkulus, ale v s\'u\v casnosti s\'u najroz\v s\'irenej\v s\'im formalizmom automaty. Konkr\'etne budeme pojedn\'ava\v t 
o pou\v zit\'i B\"uchiho automatu (vi\v d kapitolu \ref{sec:buchi}). Tento je ve\v lmi vhodn\'y, preto\v ze sa s jeho pomocou d\'a vyjadri\v t rovnako
model syst\'emu ako aj \v specifik\'acia vlastnosti po vynalo\v zen\'i ur\v cit\'eho v\'ypo\v ctov\'eho \'usilia.

Prvou f\'azou tvorby modelu syst\'emu je vytvorenie Kripkeho \v strukt\'ury, ktor\'a sa ale ve\v lmi jednoducho prevedie na automat $\mathcal{A}$. 
\v Specifik\'aciu vlastnosti m\^ o\v zeme vyjadri\v t ako automat $\mathcal{S}$. Potom s\'u oba tieto automaty vytvoren\'e nad rovnakou abecedou 
$\Sigma = 2^{AP}$. Overenie modelu teraz znamen\'a jednoducho zisti\v t, \v ci plat\'i $\mathcal{L(A)} \subseteq \mathcal{L(S)}$, kde $\mathcal{L(A)}$ je 
jazyk zodpovedaj\'uci automatu $\mathcal{A}$ a 
$\mathcal{L(S)}$ je jazyk zodpovedaj\'uci automatu $\mathcal{S}$ (Jazyk je mno\v zina v\v setk\'ych slov, ktor\'e je mo\v zno vygenerova\v t 
pr\'islu\v sn\'ym automatom.). To znamen\'a, \v ze ka\v zd\'e chovanie modelovan\'eho syst\'emu, ur\v cen\'eho jazykom $\mathcal{L(A)}$ sa nach\'adza medzi
povolen\'ymi chovaniami, ur\v cen\'ymi jazykom \v specifik\'acie $\mathcal{L(S)}$.

Toto tvrdenie m\^ o\v zeme preformulova\v t. Nech $\overline{\mathcal{L(S)}}$ je komplement k $\mathcal{L(S)}$, potom pri overovan\'i modelu dokazujeme, \v ci
plat\'i $\mathcal{L(A)} \cap \overline{\mathcal{L(S)}} = \emptyset$. Ak je tento prienik nepr\'azdny, predstavuje to chovanie, ktor\'e je protipr\'ikladom 
k overovanej vlastnosti. Pou\v zi\v t predch\'adzaj\'ucu formul\'aciu n\'am umo\v z\v nuje vedomos\v t, \v ze B\"uchiho automaty s\'u uzavret\'e na prienik
a doplnok (komplement). V\v daka tomu m\^ o\v zeme urobi\v t nasledovn\'e:
\begin{align*}
\emptyset =\ &\mathcal{L(A)} \cap \mathcal{L(S^{'})} = \mathcal{L(A \cap S^{'})} = \mathcal{L(M)},\\
&\textrm{kde } \mathcal{M} = \mathcal{A \cap S^{'}} \textrm{ a }\ \mathcal{S^{'}}= \mathcal{S(\neg\phi)},\\
&\textrm{kde } \mathcal{\phi} \textrm{ je LTL formula a } \mathcal{\neg\phi} \textrm{ jej neg\'acia},
\end{align*}
potom $\mathcal{S^{'}}$ je komplement $\mathcal{S(\phi)}$ a v skuto\v cnosti dokazujeme pr\'azdnos\v t jazyka $\mathcal{L(M)}$ 
(Pre \'uplnos\v t treba doda\v t, \v ze $\mathcal{S(\phi)}$ je automat $\mathcal{S}$ zkon\v struovan\'y zo \v specifik\'acie vlastnosti $\phi$.).

V\'yhodou pou\v zitia automatov pre vyjadrenie modelu sk\'uman\'eho syst\'emu aj  \v specifik\'acie vlastnosti je, \v ze sta\v c\'i skon\v struova\v t automat
pre vlastnos\v t (vi\v d kapitolu \ref{sec:ltltoba}) a automat modelu sa kon\v struuje za behu samotn\'eho overovania pomocou algoritmu pre prienik automatov. 
To znamen\'a, \v ze v mnoh\'ych pr\'ipadoch m\^ o\v zeme vyvr\'ati\v t splnite\v lnos\v t ove\v la sk\^ or, ne\v z sa vytvor\'i cel\'y stavov\'y priestor
automatu modelu n\'ajden\'im prv\'eho protipr\'ikladu. \v Co zna\v cne \v setr\'i \v cas a priestor. T\'ato technika sa naz\'yva overovanie modelu za behu 
(z~angl. \textit{on"~the"~fly model checking}).
\cite{Clarke:MC:BA}

%-------------------------------------------------------------------------------------------
\subsection{Prevod LTL do BA}
\label{sec:ltltoba}
Ako sme u\v z predt\'ym nieko\v lko kr\'at spomenuli, prevod LTL formuly na B\"uchiho automat nie je primit\'ivny algoritmus. V skuto\v cnosti je pr\'ili\v s
rozsiahly pre na\v se potreby zoznamovania sa s problematikou. Z tohto d\^ ovodu ho tu nebudeme rozobera\v t, av\v sak uvedieme nieko\v lko d\^ ole\v zit\'ych 
inform\'acii, ktor\'e sa tohto probl\'emu t\'ykaj\'u.

E\v ste pred za\v ciatkom sa mus\'i samotn\'a LTL formula $\phi$ previes\v t do negat\'ivnej norm\'alnej formy (z~angl. \textit{negation normal form}). 
Najsk\^ or sa preformuluj\'u niektor\'e tempor\'alne oper\'atory:
\begin{itemize}
\item $\mathbf{F}\ \phi \ \Rightarrow \ \mathbf{true\ U}\ \phi$
\item $\mathbf{G}\ \phi \ \Rightarrow \ \mathbf{false\ R}\ \phi$
\end{itemize}
a tie\v z logick\'e oper\'atory tak, aby zostali iba $\wedge$, $\vee$ a $\neg$. V poslednom kroku pr\'ipravy s\'u v\v setky neg\'acie presunut\'e dovn\'utra:
\begin{itemize}
\item $\neg(\psi\ \mathbf{U}\ \phi) \ \Rightarrow \ (\neg\psi)\ \mathbf{R}\ (\neg\phi)$
\item $\neg(\psi\ \mathbf{R}\ \phi) \ \Rightarrow \ (\neg\psi)\ \mathbf{U}\ (\neg\phi)$
\item $\neg(\mathbf{X}\ \phi) \ \Rightarrow \ \mathbf{X}\ (\neg\phi)$.
\end{itemize}

\v Dalej pokra\v cuje dlh\'y algoritmus \cite{Clarke:MC:LTLtoBA}, ktor\'eho v\'ysledkom je B\"uchiho automat $\mathcal{S}$. Jeho kon\v strukcia m\'a exponenci\'alnu \v casov\'u
aj priestorov\'u zlo\v zitos\v t z\'avisl\'u od ve\v lkosti formuly $\phi$. Av\v sak v praxi b\'yva takto skon\v struovan\'y automat ovykle men\v s\'i.

Je d\^ ole\v zit\'e e\v ste raz pripomen\'u\v t, \v ze pri overovan\'i modelu vlastne nezis\v tujeme, \v ci model sp\'l\v na vlastnos\v t, ale naopak 
zis\v tujeme, \v ci model nesp\'l\v na opak vlastnosti. D\^ ovodom k tomu je, \v ze je v\'ypo\v ctovo \v lah\v sie vytvori\v t automat z neg\'acie vlastnosti,
ako vytvori\v t komplement automatu z p\^ ovodnej vlastnosti, ktor\'y by mohol ma\v t a\v z dvojn\'asobne exponenci\'alnu priestorov\'u zlo\v zitos\v t.
\cite{Clarke:MC:LTLtoBA}

%-------------------------------------------------------------------------------------------
\subsection{Farebn\' y model checking}
\label{sec:coloredMC}
Farebn\'y model checking sa sna\v z\'i vysporiada\v t s parametriz\'aciou form\'alneho modelu, ktor\'a ho roz\v siruje o nov\'y
rozmer. Ak sa budeme na jednotliv\'e parametre $p_i \in P$, kde $P$ je mno\v zina v\v setk\'ych nezn\'amych parametrov, d\'iva\v t ako na intervaly alebo 
sk\^ or ako na mno\v ziny hodn\^ ot, v\v daka diskretiz\'acii. Potom kombin\'acia evaluaci\'i v\v setk\'ych nezn\'amych parametrov tvor\'i parametrick\'y
priestor $\mathcal{P} = \prod_{i = 1}^n [min(p_i),max(p_i)]$, kde $n = |P|$. Tento roz\v siruje model syst\'emu o parametrizovan\'e multi"~afinn\'e funkcie 
$f_i(x,\pi_i)$, kde $\pi_i \in \mathcal{P}$ namiesto be\v zn\'ych multi"~afinn\'ych funkci\'i $f_i(x)$, kde $x = (x_1,\dots{},x_n)$ je vektor premenn\'ych
a $f = (f_i,\dots{},f_n) : \mathbb{R}^n \rightarrow \mathbb{R}^n$ je vektor multi"~afinn\'ych funkci\'i (vi\v d kapitolu \ref{sec:model}). Hodnota $\pi_i$
vyjadruje konkr\'etnu evalu\'aciu parametrov v celom modeli a ozna\v cujeme ju ako farba.

Aby sa zabr\'anilo opakovan\'emu vytv\'araniu automatu pre ka\v zd\'u evalu\'aciu $\pi_i$ za \'u\v celom overenia modelu, bola vytvoren\'a nov\'a pomocn\'a
\v strukt\'ura pomenovan\'a parametrizovan\'a Kripkeho \v strukt\'ura (\v dalej len PKS). T\'a v sebe tradi\v cne uchov\'ava cel\'y stavov\'y priestor modelu,
ale navy\v se s novou inform\'aciou, ktor\'a rozhoduje pod ktorou farbou, resp. konkr\'etnou evalu\'aciou parametrov sa d\'a prejs\v t z prechodu $s$ 
do prechodu $s^{'}$. Ka\v zd\'y prechod mus\'i by\v t umo\v znen\'y aspo\v n pod jednou farbou, ale z\'arove\v n m\^ o\v ze by\v t aj pod v\v setk\'ymi. Cel\'y
stavov\'y priestor je tak zjednotenie v\v setk\'ych jednofarebn\'ych stavov\'ych priestorov (vi\v d Obr. \ref{fig:kripke}).

V\v daka tomu prebieha overovanie v\v setk\'ych parametriz\'aci\'i modelu naraz. V\'ysledkom je najv\"a\v c\v sia mno\v zina parametriz\'aci\'i, v ktor\'ych
model sp\'l\v na dan\'u vlastnos\v t. \cite{TCBB-2010}
\begin{figure}
\centering
\includegraphics[width=0.7\textwidth]{paramKripke.pdf}
\caption{Parametrizovan\'a Kripkeho \v strukt\'ura. Ka\v zd\'a farba predstavuje in\'u parametriz\'aciu a tvori odli\v sn\'y stavov\'y priestor. 
\cite{TCBB-2010}}
\label{fig:kripke}
\end{figure}

%====================================MODEL==================================================
\chapter{Biochemick\'y dynamick\'y vstupn\'y model}
\label{sec:model}
T\'ato kapitola je z ve\v lkej miery doslovne citovan\'a z ni\v z\v sie uveden\'ych zdrojov.
\\

\noindent
\it A. \ Multi-afinn\'y ODE model\rm
\\

Vstupn\'ym modelom sa u n\'as mysl\'i model biochemick\'ych reakci\'i, ktor\'y je v na\v som po\v nat\'i bran\'y ako po \v castiach 
multi"~afinn\'y syst\'em diferenci\'alnych rovn\'ic. Ale za\v cnime od po\v ciatku a postupne sa dopracujeme k tomuto v\'ysledku.

Na z\'aklade pravidla o mass~action kinetike (vi\v d kapitolu \ref{sec:massAction}) je mo\v zn\'e modelova\v t \v lubovoln\'u biochemick\'u reakciu alebo dokonca 
s\'ustavu tak\'ych\-to reakci\'i pomocou s\'ustavy neline\'arnych ODE \cite{ODE}.

Uva\v zujme o multi"~afinnom syst\'eme, ktor\'y m\'a formu $\dot{x} = f(x)$, kde $x = (x_1,\dots{},x_n)$ je vektor premenn\'ych a $f = (f_1,\dots{},f_n)$ \ : \ 
$\mathbb{R}^n \rightarrow \mathbb{R}^n$ je vektor multi"~afin\-n\'ych funkci\'i. Tieto funkcie s\'u vlastne polyn\'omy, v ktor\'ych je stupe\v n premenn\'ych 
$x_1,\dots{},x_n$ obmedzen\'y na hodnotu 1. Ka\v zd\'a premenn\'a $x_i$, kde $i \in \{1,\dots{},n\}$ predstavuje koncentr\'aciu \v specifickej chemickej 
l\'atky a je interpretovan\'a ako {$\mathbb{R}_+ = \lbrace{}  x \in \mathbb{R}\ |\ {}x \geq 0  \rbrace$}.

Z d\^ ovodu, \v ze premenn\'e m\^ ozeme vyjadri\v t len ako nez\'aporn\'e re\'alne \v cisla, je mo\v zn\'e tie\v z spojit\'y stavov\'y priestor na\v seho 
matematick\'eho syst\'emu obmedzi\v t iba na prv\'y, resp. kladn\'y kvadrant {$\mathbb{R}_+^n = \lbrace{}  x \in \mathbb{R}^n\ |\ {}x \geq 0  \rbrace$}.

Ak uva\v zujeme o premenn\'ych ako o nestabiln\'ych chemick\'ych l\'atkach, ktor\'e sami od seba degraduj\'u v \v case, m\^ o\v zeme s k\v ludom obmedzi\v t 
n\'a\v s spojit\'y stavov\'y priestor $\mathcal{D}$ e\v ste viac. A s\'ice na $n$"~dimenzion\'alny obd\'l\v znik $\mathcal{D} = \prod_{i=1}^n[0,max_i] 
\subset \mathbb{R}^n$, kde $max_i$ je horn\'a hranica koncentr\'acie pre\-men\-nej $x_i$.
\cite{HIBI-2009}\cite{HIBI-2010}
\\

\noindent
\it B. \ Neline\'arny ODE model\rm%Po \v castiach multi"~afinn\'y ODE model\rm
\\

Multi"~afinn\'y syst\'em diferenci\'alnych rovn\'ic dok\'a\v ze pokry\v t skoro cel\'u mass~action kinetiku s jedinou v\'ynimkou. A tou s\'u 
homodim\'ery a reakcie s~nimi spojen\'e. D\^ ovodom je predch\'adzaj\'uce obmedzenie multi"~afinn\'ych funkci\'i $f_1,\dots{},f_n$ s oh\v ladom 
na stupe\v n premenn\'ych $x_1,\dots{},x_n$.

Teoreticky sme schopn\'i  pop\'isa\v t ak\' yko\v lvek biochemick\'y model pomocou pravidiel tejto kinetiky. V skuto\v cnosti, ak sa pok\'usime formulova\v t 
tieto pravidl\'a pre rozsiahly model, zist\'ime, \v ze s narastaj\'ucou ve\v lkos\v tou rastie komplexita t\'ychto pravidiel a navy\v se k \'uplnosti modelu
je potrebn\'e pozna\v t ve\v lk\'e mno\v zstvo \v co najpresnej\v sie vy\v c\'islen\'ych parametrov. Pr\'ave tento druh\'y probl\'em m\^ o\v ze by\v t 
v niektor\'ych pr\'ipadoch experiment\'alne nerie\v site\v ln\'y. \v Ci u\v z ide o ve\v lk\'e enzymatick\'e komplexy alebo o l\'atky s ve\v lmi 
kr\'atkou existenciou.% / o ve\v lmi r\'ychlo degraduj\'uce l\'atky).

Pr\'ave preto sa pon\'ukaj\'u mo\v znosti aproxim\'acie, ktor\'e nielen zmen\v suj\'u syst\'em, a t\'ym aj dimenzionalitu matematick\'eho modelu, 
ale zjednodu\v suj\'u aj v\'ypo\v ctov\'u zlo\v zitos\v t. Takouto mo\v znos\v tou je aj aproxim\'acia kv\'azistacion\'arneho stavu (vi\v d kapitolu \ref{kinetiky}.B). 
Napr\'iklad Michaelis"~Mentenovej kinetika (vi\v d kapitolu \ref{kinetiky}) 
\v ci obecnej\v sia Hillova kinetika (vi\v d kapitolu \ref{kinetiky}.C) a tie\v z sigmoid\'alne prep\'ina\v ce publikovan\'e v \cite{CAV-2011}. 
\v Dalej sem mo\v zno r\'ata\v t aj Heavisideove alebo schodov\'e funkcie \cite{step}. 

V\v setky vy\v s\v sie zmienen\'e abstrakcie n\'a\v s n\'astroj pon\'uka a budeme ich jednotne ozna\v cova\v t ako regula\v cn\'e funkcie $\rho(x_i)$, kde 
$i \in \{1,\dots{},n\}$, ktor\'e m\^ o\v zu nadob\'uda\v t nasleduj\'uce formy:
\begin{align*}
hill^+(x_i, \theta_i, d, a, b) &\ = \ a + (b - a)\frac{[x_i]^d}{[\theta_i]^d + [x_i]^d};\\
hill^+(x_i, \theta_i, d, a, b) &\ = \ 1 - hill^+(x_i, \theta_i, d, a, b);\\
\\
s^+(x_i, e, \theta_i, a, b) &\ = \ a + (b - a)\frac{1 + tanh(e(x_i - \theta_i))}{2};\\
s^-(x_i, e, \theta_i, a, b) &\  = \ 1 - s^+(x_i, e, \theta_i, a, b);\\
\\
h^+(x_i,\theta_i,a,b) &\ = \ a,\ \textrm{ak}\ x_i < \theta_i;\ b\ \textrm{inak};\\
h^-(x_i,\theta_i,a,b) &\ = \ 1 - h^+(x_i,\theta_i,a,b);
\end{align*}
\begin{align*}
\textrm{kde}\ &hill^+, hill^- \textrm{s\'u funkcie Hillovej kinetiky};\\
&s^+, s^- \textrm{s\'u sigmoid\'alne prep\'ina\v ce};\\
&h^+, h^- \textrm{s\'u Heavisideove (schodov\'e) funkcie};\\
&\theta_i \in \mathbb{R}^+; \ \theta_i \leq max_i; \ i \in \{1,\dots{},n\};\\
&a, b \in \mathbb{R}_0^+; \ e, d \in \mathbb{R}^+.
\end{align*}

\noindent\v Speci\'alnym pr\'ipadom je recipro\v cn\'a hodnota sigmoid\'alnej funkcie:
\begin{align*}
s^+(x_i, e, \theta_i, a, b)^{-1} \ = \ s^-(x_i, e, \theta_i + \frac{ln(\frac{a}{b})}{2e}, b^{-1}, a^{-1}),
\end{align*}
ktor\'u ozna\v cujeme ako $s^+inv(x_i, e, \theta_i, a, b)$. Potom klesaj\'ucu recipro\v cn\'u funkciu ozna\v c\'ime obdobne ako doplnok rast\'ucej:
\begin{align*}
\centerline{$s^-inv(x_i, e, \theta_i, a, b) \ = \ 1 - s^+(x_i, e, \theta_i, a, b)$.}
\end{align*}
D\^ okaz mo\v zno n\'ajs\v t v \v cl\'anku \cite{CAV-2011} na strane 6.

Takto redukovan\' e diferenci\'alne rovnice teraz maj\'u formu racion\'alnych polyn\'omov, z\'iskan\'ych ako line\'arna kombin\'acia t\'ychto regula\v cn\'ych 
funkci\'i. V skuto\v cnosti v\'ysledn\'y 
matematick\'y model nie je multi"~afinn\'y, ale na druh\'u stranu je ho mo\v zn\'e aproximova\v t v zmysle po \v castiach mul\-ti"~afin\-n\'eho syst\'emu. 

Nevyhnutnou s\'u\v cas\v tou modelu je mno\v zina prahov\'ych hodn\^ ot (z~angl. \textit{threshold})
$\theta_m^i \in \mathbb{R}^+$ sp\'l\v naj\'uca $min_i = \theta_1^i < \theta_2^i < \dots{} < \theta_{\eta_i}^i = max_i$, kde $i \in \{1,\dots{},n\}$, 
$m \in \{1,\dots{},\eta_i\}$ a plat\'i, \v ze $\eta_i \geq 2$.

Teraz u\v z m\^ o\v zeme zadefinova\v t \'upln\'y form\'at n\'a\v sho vstupn\'eho neline\'arneho ODE modelu. 
Tento model $\mathcal{M}$ je dan\'y ako $\dot{x} = f(x)$, 
kde $x$ je st\'ale vektor premenn\'ych $(x_1,\dots{},x_n)$, ale $f = (f_1,\dots{},f_n)$ : $\mathbb{R}^n \rightarrow \mathbb{R}^n$ je tentokr\'at vektor 
neline\'arnych polynomi\'alnych funkci\'i, ktor\'e maj\'u tvar:
\begin{align}
\label{eq:equationDescribtion1}
f_i(x) = \sum (s\underset{j \in I}\prod{\rho_i^j(x)}),
\end{align}
kde $i \in \{1,\dots{},n\}$, $s \in \{-1,1\}$, $I$ je nepr\'azdna podmno\v zina kone\v cnej mno\v ziny indexov v\v setk\'ych pou\v zit\'ych regula\v cn\'ych
funkci\'i a $\rho_i^j$ je pr\'islu\v sn\'a regula\v cn\'a funkcia, ktor\'a m\^ o\v ze nadob\'uda\v t tieto hodnoty:
\begin{align}
\label{eq:regulatingFunctions1}
\rho(x_t) = 
\left\{ \begin{array}{cl}
c, &c \in \mathbb{R}\\
%p, &p \in \langle g,h \rangle; \ g,h \in \mathbb{R}\\
x_k, & k \in \{1,\dots{},n\}\\
h^*(x_k,\theta_m^k,a,b), &m \in \{1,\dots{},\eta_k-1\}; \ a,b \in \mathbb{R}_0^+\\
s^*(x_k,e,\theta_m^k,a,b), &e \in \mathbb{R}^+\\
s^*inv(x_k,e,\theta_m^k,a,b),\\
hill^*(x_k,\theta_m^k,d,a,b), &d \in \mathbb{R}^+
\end{array} \right. ,
\end{align}
kde $* \in \{+,-\}$. Ak $\rho_i^{j_1}, \rho_i^{j_2}$ s\'u regula\v cn\'e funkcie, ktor\'e patria do jednoho produktu $s\underset{j \in I}\prod\rho_i^j(x)$
tak, \v ze $j_1, j_2 \in I$, mus\'i plati\v t $dep(\rho_i^{j_1})\ \cap\ dep(\rho_i^{j_2}) = \emptyset$, kde $dep(\rho)$ je mno\v zina premenn\'ych $x$,
na ktor\'ych je $\rho$ z\'avisl\'a.

Do modelu je priamo zaveden\'a aj mo\v znos\v t zadania kon\v stantnej funkcie (v pr\'ipade, \v ze $\rho(x_t) = c$) a line\'arnej funkcie 
(v pr\'ipade $\rho(x_t) = x_k$). \v Dal\v sou nevyhnutnou s\'u\v cas\v tou modelu s\'u inici\'alne podmienky, vyjadruj\'uce 
po\v ciato\v cn\'e koncentr\'acie jednotliv\'ych l\'atok. Tie nie s\'u vyjadren\'e presne, ale namiesto toho s\'u ur\v cen\'e intervalom, ktor\'eho
hranice musia by\v t z mno\v ziny $\{ \theta_1^i,\dots{},\theta_{\eta_i}^i \}$.

V pr\'ipade, \v ze sa pou\v zij\'u v modeli iba kon\v stantn\'e a line\'arne funckie, dost\'avame automatick\'y oby\v cajn\'y multi"~afinn\'y model tak, ako
je uveden\'y v~kapitole \ref{sec:model}.A. V opa\v cnom pr\'ipade mus\'i by\v t na tento model aplikovan\'a optim\'alna line\'arna abstrakcia (vi\v d 
kapitolu \ref{sec:abstraction}.A), aby sme 
dostali potrebn\'y multi"~afinn\'y model. Tentokr\'at v\v sak po \v castiach multi"~afinn\'y. Z t\'ych\-to d\^ ovodov je takto definovann\'y model prakticky 
pou\v zite\v ln\'y pre \v lubovoln\'y biologick\'y syst\'em.
\cite{HIBI-2009}\cite{HIBI-2010}
\\

\noindent
\textit{C. \ Po \v castiach multi"~afinn\'y ODE model}
\\

Nahraden\'im v\v setk\'ych regula\v cn\'ych funkci\'i $\rho(x_i)$ z predch\'adzaj\'ucej \v casti s\'ustavou vhodn\'ych po \v castiach line\'arnych 
rampov\'ych funkci\'i, ktor\'e s\'u definovan\'e 
nasledovne:
\begin{align*}
	r^+ (x_i,\theta{}_i,\theta{}_i^{'},y,y^{'}) \ = \left\{ \begin{array}{cl}
y, & \textrm{pre} \ x_i < \theta_i,\\
y + (y^{'} - y)\frac{x_i - \theta_i}{\theta_i^{'} - \theta_i}, & \textrm{pre} \ \theta_i < x_i < \theta_i^{'},\\
y^{'}, & \textrm{pre} \ x_i > \theta_i^{'}.
	\end{array}
	\right.
\end{align*}
\begin{align*}
	\textrm{kde} \ &i \in \{1,\dots{},n\},\\
	&y = x_j, y^{'} = x_j^{'}; j \in \{1,\dots{},n\} \wedge j \neq i,\\
	&\theta_i, \theta_i^{'} \in \mathbb{R}^+, \ \theta_i < \theta_i^{'} \leq max_i
\end{align*}
a potom klesaj\'uce rampov\'e funkcie s\'u definovan\'e ako kvantitat\'ivny doplnok rast\'ucich:
\begin{align*}
r^- (x_i,\theta{}_i,\theta{}_i^{'},y,y^{'}) &\ = \ 1 - r^+ (x_i,\theta{}_i,\theta{}_i^{'},y,y^{'}),
\end{align*}
dost\'avame po \v castiach multi"~a\-fin\-n\'y ODE model 
(\v dalej len PMA model z~angl. \textit{piecewise multi"~affine ODE model}). PMA model $\mathcal{P}$ je dan\'y ako $\dot{x} = f(x)$, 
kde $x$ je st\'ale vektor premenn\'ych $(x_1,\dots{},x_n)$, ale $f = (f_1,\dots{},f_n)$ : $\mathbb{R}^n \rightarrow \mathbb{R}^n$ je tentokr\'at vektor 
po \v castiach multi"~afinn\'ych funkci\'i. 

St\'ale plat\'i mno\v zina prahov\'ych hodn\^ ot 
$\theta_m^i \in \mathbb{R}^+$ sp\'l\v naj\'uca $min_i = \theta_1^i < \theta_2^i < \dots{} < \theta_{\eta_i}^i = max_i$, kde $i \in \{1,\dots{},n\}$, 
$m \in \{1,\dots{},\eta_i\}$ a plat\'i, \v ze $\eta_i \geq 2$, ktor\'a v\v sak m\^ o\v ze by\v t roz\v s\'iren\'a o nov\'e hodnoty -- v\'ysledky 
predch\'adzaj\'ucej line\'arnej abstrakcie.

Uva\v zujme $\Omega$ ako \v cas\v t modelu $\mathcal{P}$ tak, \v ze $\Omega = \prod_{i = 1}^n\{1,\dots{},\eta_i - 1\}$. Funkcia 
$g : \mathbb{R}^n \rightarrow \mathbb{R}^+$ je vtedy po \v castiach multi"~afinn\'a, ak je multi"~afinn\'a na ka\v zdom $n$-dimenzion\'alnom intervale
$(\theta_{j_1}^1,\theta_{j_1 + 1}^1)\times \dots{} \times (\theta_{j_n}^n,\theta_{j_n + 1}^n)$, kde $(j_1,\dots{},j_n) \in \Omega$ a z\'arove\v n 
$\forall{}i, 1 \leq i \leq n, j_i < max_i$. Potom dost\'avame $n$-dimenzion\'alny PMA model pozost\'avaj\'uci z funkci\'i $f$ v nasleduj\'ucom tvare:
\begin{align}
\label{eq:equationDescribtion2}
f_i(x) = \sum (s\underset{j \in I}\prod{\sigma_i^j(x)}),
\end{align}
kde $i \in \{1,\dots{},n\}$, $s \in \{-1,1\}$, $I$ je nepr\'azdna podmno\v zina kone\v cnej mno\v ziny indexov v\v setk\'ych pou\v zit\'ych line\'arnych 
(v zmysle line\'arnych alebo po \v castiach line\'arnych) 
funkci\'i a $\sigma_i^j$ je pr\'islu\v sn\'a line\'arna funkcia, ktor\'a m\^ o\v ze nadob\'uda\v t tieto hodnoty:
\begin{align}
\label{eq:regulatingFunctions2}
\sigma(x_t) = 
\left\{ \begin{array}{cl}
c, &c \in \mathbb{R}\\
%p, &p \in \langle g,h \rangle; \ g,h \in \mathbb{R}\\
x_k, & k \in \{1,\dots{},n\}\\
r^*(x_k,\theta_m^k,\theta_{m+1}^k,x_t,x_t^{'}), &m \in \{1,\dots{},\eta_k-1\};\\
&t \in \{1,\dots{},n\} \wedge t \neq i
\end{array} \right. ,
\end{align}
kde $* \in \{+,-\}$. Ak $\sigma_i^{j_1}, \sigma_i^{j_2}$ s\'u line\'arne funkcie, ktor\'e patria do jednoho produktu $s\underset{j \in I}\prod\sigma_i^j(x)$,
tak \v ze $j_1, j_2 \in I$, mus\'i plati\v t $dep(\sigma_i^{j_1})\ \cap\ dep(\sigma_i^{j_2}) = \emptyset$, kde $dep(\sigma)$ je mno\v zina premenn\'ych $x$,
na ktor\'ych je $\sigma$ z\'avisl\'a.

Pr\'ipad $\sigma(x_t) = c$ predstavuje kon\v stantn\'u funkciu a $\sigma(x_t) = x_k$ zase line\'arnu funkciu. Rovnako ako v \v casti \ref{sec:model}.B. 
Samozrejmou nevyhnutnos\v tou s\'u inici\'alne podmienky, vyjadruj\'uce 
po\v ciato\v cn\'e koncentr\'acie jednotliv\'ych l\'atok. Tieto s\'u zhodn\'e s hodnotami z predch\'adzaj\'uceho neline\'arneho modelu.

Takto definovan\'y PMA syst\'em je mo\v zn\'e pou\v zi\v t priamo ako vstupn\'y model. Nemus\'i by\v t len v\'ysledkom line\'arnej 
abstrakcie predch\'adzaj\'uceho neline\'arneho ODE syst\'emu.
\cite{HIBI-2009}\cite{HIBI-2010}

%-------------------------------------------------------------------------------------------
\section{Abstrakcia}
\label{sec:abstraction}

\noindent
\textit{A. \ Optim\'alna line\'arna abstrakcia neline\'arnych funkci\'i}
\\

V minulej kapitole sme objasnili, pre\v co je potrebn\'e prev\'adza\v t regula\v cn\'e funkcie $\rho(x_i)$, kde $x_i$ je premenn\'a na po \v castiach line\'arne 
rampov\'e funkcie $r^*_j(x_i,\theta^i_j,\theta^i_{j+1},y,y^{'})$, kde $j \in \{1,\dots{},m\}$ a $m$ je po\v cet po\v zadovan\'ych r\'amp, $\theta^i$ je 
prahov\'a hodnota premennej $x_i$, $y$ a $y^{'}$ s\'u funk\v cn\'e hodnoty v t\'ychto prahoch a $* \in \{+,-\}$. 
V tejto \v casti sa pok\'usime objasni\v t princ\'ip tohto prevodu. Vyn\'ara sa hne\v d nieko\v lko probl\'emov:
\begin{enumerate}
\item Ako vhodne rozdeli\v t \v lubovoln\'u krivku na zadan\'y po\v cet r\'amp.
\item Ako vhodne rozdeli\v t nieko\v lko kriviek rovnakej dimenzie na zadan\'y po\v cet r\'amp.
\item Ako vybra\v t spr\'avny po\v cet r\'amp, tak aby stavov\'y syst\'em nebol pr\'ili\v s ve\v lk\'y a z\'arove\v n tak, aby abstrakcia nebola 
pr\'ili\v s hrub\'a.
\end{enumerate}
Na prv\'u ot\'azku d\'ava odpove\v d algoritmus dynamick\'eho programovania vyvinut\'y pre po\v c\'ita\v cov\'u grafiku, konkr\'etne pre aproxim\'aciu
digitalizovan\'ych polygon\'alnych kriviek s minim\'alnou chybou \cite{CURVES}. Tento bol upraven\'y a roz\v s\'iren\'y pre viacero kriviek naraz v 
\v cl\'anku \cite{CAV-2011} a to tak, \v ze zmienen\'a chyba sa po\v c\'ita pre
v\v setky krivky naraz. Aby to bolo mo\v zn\'e, musia by\v t v\v setky krivky diskretizovan\'e v rovnak\'ych $x$-ov\'ych bodoch. 
V na\v som pr\'ipade sa krivkami myslia Hillove funkcie (vi\v d kapitolu \ref{kinetiky}.C) a sigmoid\'alne funckie pop\'isan\'e tie\v z v \v cl\'anku \cite{CAV-2011}.

\' U\v celom tejto abstrakcie je n\'ajs\v t tak\'e body $x_i$, kde $i \in \{1,\dots{},n-1\}$ a $n$ je po\v cet po\v zadovan\'ych line\'arnych segmentov, 
ktor\'e bud\'u 
seka\v t krivky na tieto segmenty s minim\'alnou odch\'ylkou (chybou). Nesmieme v\v sak zabudn\'u\v t, \v ze po\v ciato\v cn\'y $x_0$ a koncov\'y bod $x_n$ 
krivky je vopred zadan\'y. 

Chyba sa po\v c\'ita ako s\'u\v cet druh\'ych mocn\'in vzdialenost\'i dvoch 
bodov na $y$-ovej ose. T\'ymito bodmi s\'u funk\v cn\'a hodnota krivky a funk\v cn\'a hodnota rampy pre konkr\'etny bod $x_i$ na \'useku ohrani\v cenom bodmi 
$x_a$ a $x_b$, kde $x_i \in \langle x_a,x_b\rangle$. Rampa je v tomto zmysle bran\'a ako line\'arna spojnica medzi funk\v cn\'ymi hodnotami t\'ychto
hrani\v cn\'ych bodov. Ako u\v z bolo zmienen\'e vy\v s\v sie, chyba na \'useku $\langle x_a,x_b\rangle$ sa po\v c\'ita pre v\v setky krivky naraz a v tomto 
pr\'ipade sa h\v lad\'a hodnota najvy\v s\v sia. Prakticky to znamen\'a, \v ze sa po\v cas procesu aproxim\'acie h\v ladaj\'u minim\'alne odch\'ylky ch\'yb z 
maxim\'alnych rozdielov kriviek. 
Ak n\'ajden\'a hodnota chyby je men\v sia ako predch\'adzaj\'uca, tak body $x_a$ a $x_b$ mo\v zno pre \v dal\v siu iter\'aciu bra\v t ako hrani\v cn\'e body 
nov\'eho segmentu. Ak sa men\v sia hodnota chyby u\v z nen\'ajde je hrani\v cn\'y bod $x_b$ definit\'ivne ulo\v zen\'y. Bod $x_a$ je ulo\v zen\'y u\v z 
z~predch\'adzaj\'ucej iter\'acie.
So v\v setk\'ymi takto z\'iskan\'ymi bodmi u\v z nie je probl\'em previes\v t ka\v zd\'u funkciu na jej po \v castiach 
line\'arnu formu. Z\'arove\v n treba tieto body ulo\v zi\v t ako nov\'e prahov\'e hodnoty modelu (vi\v d kapitolu \ref{sec:model}.B). 
Pr\'iklad abstrakcie zn\'azor\v nuje Obr. \ref{fig:noabstract}.

Odpove\v d na tretiu ot\'azku oh\v ladom spr\'avneho po\v ctu r\'amp je nasleduj\'uca.
U\v z\'ivate\v l mus\'i nastavi\v t po\v zadovan\'y po\v cet s\'am, to mu v\v sak umo\v z\v nuje, aby sk\'u\v sal r\^ ozne \'urovne abstrakcie osobne.
\cite{CAV-2011}
\\

\noindent
\textit{B. \ Obd\'l\v znikov\'a abstrakcia PMA modelu}
\\

V\'yhodou multi"~afinn\'eho syst\'emu je, \v ze ho mo\v zno abstrahova\v t do podoby obd\'l\v znikov\'eho prechodov\'eho syst\'emu (z~angl. \textit{
Rectangular Abstraction Transition System}, skr\'atene RATS) \cite{RATS}. K tomu je potreba p\^ ovodn\'y $n$"~di\-men\-zion\'alny syst\'em, kde $n$ je po\v cet 
premenn\'ych, najsk\^ or rozdeli\v t na men\v sie $n$-dimenzion\'alne oddiely. Ka\v zd\'a premenn\'a m\'a priraden\'u mno\v zinu prahov\'ych hodn\^ ot alebo
thresholdov, ktor\'e vyjadruj\'u v\'yznamn\'e, \v ci zauj\'imav\'e koncentra\v cn\'e hladiny. Ka\v zdej premennej s\'u priraden\'e aspo\v n dve tak\'eto 
hodnoty, a to minim\'alna a maxim\'alna. \v Dal\v sie m\^ o\v zu by\v t zadefinovan\'e vo vstupnom modeli alebo m\^ o\v zu poch\'adza\v t z predch\'adzaj\'ucej
line\'arnej abstrakcie regula\v cn\'ych funkci\'i.

Teraz u\v z nie je probl\'em rozdeli\v t multi"~afinn\'y syst\'em pod\v la t\'ychto prahov na men\v sie $n$-rozmern\'e ohrani\v cen\'e \v casti nazvan\'e 
obd\'l\v zniky. Tieto si m\^ o\v zeme predstavi\v t ako uzly grafu. Ak s\'u dva obd\'l\v zniky susedmi, m\^ o\v ze medzi nimi vznikn\'u\v t prechod v zmysle
hrany medzi dvoma uzlami. Takto dost\'avame diskr\'etny prechodov\'y syst\'em (RATS) z p\^ ovodne dynamick\'eho syst\'emu. 

Prechody s\'u samozrejme orientovan\'e. Hodnotu orient\'acie dostaneme zo smerov\'ych vektorov vypo\v c\'itan\'ych vo v\v setk\'ych rohoch $n$-rozmern\'eho 
obd\'l\v znika. A to tak, \v ze ak aspo\v n jeden vektor v spolo\v cn\'ych rohoch so susediacim obd\'l\v znikom m\'a smer k tomuto susedovi, prid\'ame 
odch\'adzaj\'ucu hranu z tohto uzla do susedn\'eho. Ak aspo\v n jeden vektor v spolo\v cn\'ych rohoch so susediacim obd\'l\v znikom m\'a smer od tohto
suseda, prid\'ame prich\'adzaj\'ucu hranu zo susediaceho uzla k tomuto uzlu. To znamen\'a, \v ze hrany m\^ o\v zu by\v t aj obojsmern\'e. Podmienkou je, \v ze
ak nastane situ\'acia, kedy uzol nebude ma\v t \v ziadnu odch\'adzaj\'ucu hranu, mus\'ime mu prida\v t slu\v cku. Tento jav symbolizuje rovnov\'a\v zny stav
v dan\'ych podmienkach (vi\v d Obr. \ref{fig:rats}). 

Je zn\'amy fakt, \v ze obd\'l\v znikov\'a abstrakcia je nadaproxim\'aciou vzh\v ladom k trajekt\'oriam p\^ ovodn\'eho dynamick\'eho modelu.
\cite{BIODIVINE}

\begin{figure}[h]
\centering
\begin{subfigure}{.5\textwidth}
	\centering
	\includegraphics[width=0.9\textwidth]{partition2.pdf}
\end{subfigure}%
\begin{subfigure}{.5\textwidth}
	\centering
	\includegraphics[width=0.9\textwidth]{partition3.pdf}
\end{subfigure}
\caption{Pr\'iklad obd\'l\v znikovej abstrakcie 2-rozmern\'eho modelu a v\'ysledn\'y RATS.}
\label{fig:rats}
\end{figure}

\begin{figure}[h]
    \centering
    \includegraphics[width=0.80\textwidth]{abstractNO}
    \includegraphics[width=0.80\textwidth]{abstractYES}
    \caption{Tri krivky s popisom. V prvom pr\'ipade bez pou\v zitia abstrakcie a v~druhom preveden\'e na s\'ustavu r\'amp po pou\v zit\'i abstrakcie 
    s parametrami: diskretiza\v cn\'ych bodov $500$, po\v zadovan\'y po\v cet segmentov $7$.}
	\label{fig:noabstract}
\end{figure}

\section{Vlastnosti modelu}
Nepriamou s\'u\v cas\v tou modelu je aj vlastnos\v t, ktorej splnite\v lnos\v t budeme testova\v t. T\'ato je pop\'isan\'a v tvare LTL formuly (vi\v d
kapitolu \ref{sec:logika}), ktor\'a obsahuje atomick\'e propoz\'icie (\v dalej iba AP). To s\'u v\'yrazy s pravdivostnou hodnotou ({\it true} alebo 
{\it false}) skladaj\'uce sa z porovn\'avan\'i hodn\^ ot premenn\'ych $x_i$ s ich prahov\'ymi hodnotami $\theta^i_j$, kde $i \in \{1,\dots{},n\}$ a $n$ je 
po\v cet premenn\'ych a $j \in \{1,\dots{},m\}$ a $m$ je po\v cet prahov\'ych hodn\^ ot premennej $x_i$ (vi\v d kapitolu \ref{sec:model}), 
pomocou rela\v cn\'ych oper\'atorov ($<$, $>$, $<=$ alebo $>=$). In\'ymi slovami AP vyzer\'a: 
\begin{equation*}
x_i\ \ op \ \ \theta^i_j, \ \textrm{ kde } \ op \in \{<,>,<=,>=\}.
\end{equation*}
Viacero AP mo\v zno sp\'aja\v t logick\'ymi spojkami.

%====================================NASTROJE===============================================
\chapter{V\'ychodiskov\'y stav a podobn\' e n\'astroje}
\label{sec:similarTools}

%-------------------------------------------------------------------------------------------
\section{BioDiVinE 1.0}
\label{sec:biodivine}
P\^ ovodn\'y n\'astroj BioDiVinE bol vyvinut\'y v Laborat\'oriu syst\'emovej biol\'ogie (SYBILA)\footnote{http://sybila.fi.muni.cz/home} v spolupr\'aci 
s Laborat\'oriom paraleln\'ych a distribuovan\'ych syst\'emov (ParaDiSe)\footnote{http://paradise.fi.muni.cz/index.html}. Obe s\'idlom na Fakulte 
informatiky Masarykovej univerzity. 

BioDiVinE 1.0 je n\'astroj vytvoren\'y pre verifik\'aciu vlastnost\'i biochemick\'ych modelov zadan\'ych ako syst\'em ODE (vi\v d kapitolu \ref{sec:model}).
Je to nadstavba n\'astroja DiVinE \cite{divine}, ur\v cen\'eho na model checking (vi\v d kapitolu \ref{sec:modelChecking}). K tomuto 
\'u\v celu pon\'uka nieko\v lko odli\v sn\'ych algoritmov.

Vstupom je, ako u\v z bolo povedan\'e biochemick\'y model v tzv. .bio form\'ate (podrobnosti v \cite{sybila-biodivine}), ktor\'y 
m\^ o\v ze predstavova\v t genov\'u regula\v cn\'u sie\v t alebo vz\'ajomn\'u interakciu prote\'inov \v ci in\'e. D\^ ole\v zitou s\'u\v cas\v tou je aj
s\'ubor s jednou alebo viacer\'ymi vlastnos\v tami zap\'isan\'ymi ako LTL formuly (vi\v d kapitolu \ref{sec:logika}). Tieto dva s\'ubory sa musia skombinova\v t
do jednoho pou\v zit\'im pr\'islu\v sn\'eho n\'astroja, pri\v com vlastnos\v t sa z\'arove\v n prevedie z LTL formuly na B\" uchiho automat (vi\v d kapitolu 
\ref{sec:buchi}). Takto hotov\'y vstup sa m\^ o\v ze preda\v t jednomu z overovac\'ich algoritmov.

Je vidno, \v ze postup nie je ve\v lmi u\v z\'iva\v te\v lsky pr\'ivetiv\'y. U\v z\'ivate\v l mus\'i najsk\^ or pou\v zi\v t jeden n\'astroj 
pre vytvorenie vstupn\'eho s\'uboru, potom ho ru\v cne premenova\v t, aby ho \v dal\v s\'i n\'astroj, tentokr\'at overovac\'i, spr\'avne rozpoznal. V\'ysledky
v podobe protipr\'ikladu alebo podrobn\'y v\'ypis priebehu procesu s\'u vygenerovan\'e do nov\'ych s\'uborov .trail alebo .report po zadan\'i pr\'islu\v sn\'eho
vstupn\'eho prep\'ina\v ca vybran\'eho algoritmu. Jedinou v\'yhodou je, \v ze v\"a\v c\v sina prep\'ina\v cov je unifikovan\'a, preto\v ze n\'astroje boli vytvoren\'e
jedn\'ym v\'yvoj\'arskym t\'imom.

Cel\'y n\'astroj BioDiVinE pritom obsahuje zbyto\v cne ve\v la \v dal\v s\'ich roz\v s\'iren\'i pre in\'e typy modelov, preto\v ze p\^ ovodn\'y n\'astroj 
DiVinE bol prevzat\'y ako celok aj s t\'ymito predch\'adzaj\'ucimi roz\v s\'ireniami.

Kv\^ oli vy\v s\v sie spomenut\'ym d\^ ovodom sme si dali za cie\v l okrem roz\v s\'irenia vstupn\'eho modelu a abstrakcie aj refaktoriz\'aciu star\'eho n\'astroja.
\cite{BIODIVINE}

%-------------------------------------------------------------------------------------------
\section{PEPMC}
\label{sec:pepmc}
N\'astroj vyvinut\'y v Laborat\'oriu syst\'emovej biol\'ogie (SYBILA)\footnote{http://sybila.fi.muni.cz/home} pre overovanie modelov s oh\v ladom na odhad 
parametrov (z~angl. \textit{
Parameter Estimation by Parallel Model Checking}, skr\'atene PEPMC). Funguje na princ\'ipe paralelizovan\'eho farebn\'eho overovania modelov 
(vi\v d kapitolu \ref{sec:coloredMC}). Modelom je syst\'em ODE podobne ako v n\'astroji BioDiVinE 1.0, ale roz\v s\'iren\'y o mo\v znos\v t
zad\'avania po \v castiach line\'arnych rampov\'ych funkci\'i (vi\v d kapitolu \ref{sec:model}). D\^ ole\v zit\'ym rozdielom oproti BioDiVinE-u a s\'u\v casne 
hlavnou podstatou n\'astroja PEPMC v\v sak je parametriz\'acia modelu a s t\'ym s\'uvisiace preh\v lad\'avanie parametrick\'eho priestoru.

Existuje my\v slienka zl\'u\v ci\v t tieto dva n\'astroje, br\'ani tomu v\v sak mierne odli\v sn\'y vstup, datov\'y model a samozrejme rozdielne jadr\'a 
programov. Nebudeme tu v\v sak tento probl\'em \v dalej rozobera\v t, preto\v ze nie je s\'u\v cas\v tou na\v sej t\'emy.
\cite{HIBI-2010}

%-------------------------------------------------------------------------------------------
\section{RoVerGeNe}
RoVerGeNe je podobne ako PEPMC n\'astroj pre anal\'yzu genetick\'ych regula\v cn\'ych siet\'i s neur\v cit\'ymi parametrami. Model siete je zap\'isan\'y ako
po \v castiach multi"~afinn\'y syst\'em diferenci\'alnych rovn\'ic. Vlastnosti, proti ktor\'ym sa model overuje, maj\'u formu LTL formuly a parametre s\'u 
zadan\'e ako intervaly. N\'astroj sa sna\v z\'i overi\v t, \v ci model sp\'l\v na dan\'u vlastnos\v t pre v\v setky parametre.

Na rozdiel od PEPMC v\v sak RoVerGeNe dok\'a\v ze pracova\v t aj s line\'arnymi kombin\'aciami parametrov. To v praxi znamen\'a, \v ze obd\'l\v znikov\'a
abstrakcia (vi\v d kapitolu \ref{sec:abstraction}.B) u neho nie je
pou\v zite\v ln\'a, preto\v ze vy\v zaduje, aby $n$-dimen\-zion\'alne \v stvoruholn\'iky, s ktor\'ymi pracuje, boli ortogon\'alne \v ci\v ze obd\'l\v zniky.
Namiesto toho pou\v z\'iva tento n\'astroj \v standardn\'e polyhedr\'alne oper\'acie bal\'ika MPT \cite{mpt} a cel\'y je naprogramovan\'y v Matlabe.
\cite{rovergene}
\cite{rovergene-site}

%================================BIODIVINE-1.1=============================================
\chapter{BioDiVinE 1.1}
V kapitole \ref{sec:biodivine} boli predstaven\'e niektor\'e nedostatky p\^ ovodn\'eho n\'astroja BioDiVinE 1.0, ktor\'e sme si dali za cie\v l odstr\'ani\v t.
S\'u\v casne bol z\'aujem o~roz\v s\'irenie jeho funkcionality a odstr\'anenie nadbyto\v cn\'ych \v cast\'i k\'odu. 

Prvotn\'y impulz spo\v c\'ival v zov\v seobecnen\'i vstupn\'eho modelu, aby poskytoval \v sir\v s\'i z\'aber mo\v znost\'i. Aby nebol obmedzen\'y iba na mass 
action kinetiku (vi\v d kapitolu \ref{sec:massAction}) a s t\'ym s\'uvisiace neline\'arne diferenci\'alne rovnice. Do \'uvahy prich\'adzali samozrejme 
najbe\v znej\v sie pou\v z\'ivan\'e Hillova kinetika a Michaelis"~Mente\-novej kinetika (vi\v d kapitolu \ref{kinetiky}), ale aj Heavisidove funkcie 
\cite{step}, sigmoid\'alne funkcie spom\'inan\'e v \cite{CAV-2011} a obecn\'e rampov\'e funkcie (vi\v d kapitolu \ref{sec:model}.B), ktor\'e 
sl\'u\v zia aj ako produkt optim\'alnej line\'arnej abstrakcie (vi\v d kapitolu \ref{sec:abstraction}.A).

T\'ym sa dost\'avame k \v dal\v sej novej funkcionalite. Zl\'u\v cenie nov\'eho roz\v s\'iren\'eho vstupn\'eho modelu (vi\v d kapitolu \ref{sec:model}) a p\^ ovodne 
pou\v z\'ivanej obd\'l\v znikovej abstrakcie (vi\v d kapitolu \ref{sec:abstraction}.B). Prechodom medzi t\'ym je pr\'ave vy\v s\v sie spomenut\'a op\-ti\-m\'al\-na 
line\'arna abstrakcia, ktor\'a prevedie novozaveden\'e nemulti"~afin\-n\'e funk\-cie na po \v castiach multi"~afinn\'e, presne ako je potrebn\'e pre 
obd\'l\v znikov\'u abstrakciu.

Pri z\'apise jednotliv\'ych rovn\'ic modelu sme sa chceli vyhn\'u\v t oper\'acii delenia, preto sme sa rozhodli v\v setky prid\'avan\'e funkcie zapisova\v t
v podstate unifikovan\'ym sp\^ osobom, ktor\'y jasne ur\v cuje, o ak\'y typ funkcie ide, \v ci je rast\'uca alebo klesaj\'uca a \v dalej parametre 
nevyhnutn\'e pre jej vy\v c\'islenie (vi\v d kapitolu \ref{sec:modelFile}). Takisto sme pridali p\'ar noviniek ako definovanie pomenovan\'ych kon\v st\'ant a volite\v ln\'e, u\v z\'ivate\v lom 
zad\'avan\'e parametre pre line\'arnu abstrakciu. Konkr\'etne ide o po\v cet bodov, v ktor\'ych maj\'u by\v t funkcie evaluovan\'e a o po\v cet segmentov, 
na ktor\'e maj\'u by\v t funkcie rozdelen\'e a linearizovan\'e.

Z t\'ychto d\^ ovodov sme sa rozhodli vytvori\v t \'uplne nov\'y parser (vi\v d kapitolu \ref{sec:implParser}) a s\'u\v casne s n\'im aj nov\'y datov\'y model pre uchovanie nov\'ych d\'at. Niektor\'e
prvky boli s\'ice zhodn\'e so star\'ym BioDiVinE-om, ale sp\^ osob, ak\'ym boli naimplementovan\'e v starej verzii, bol ve\v lmi zle roz\v s\'irite\v ln\'y. 
Za\v ca\v t v~t\'ychto bodoch odznova n\'am pri\v slo jednoduch\v sie a preh\v ladnej\v sie. 

Av\v sak k\'od star\'eho n\'astroja bol hodne rozsiahly a skladal
sa z ve\v lk\'eho mno\v zstva r\^ oznych tried, z ktor\'ych mnoh\'e u\v z pre na\v se \'u\v cely neboli potrebn\'e. Preto bolo nutn\'e najsk\^ or cel\'y k\'od
postupne prech\'adza\v t a debugova\v t, aby sme mu lep\v sie porozumeli. Na z\'aklade toho sme boli schopn\'i eliminova\v t neu\v zito\v cn\'e a 
nepou\v z\'ivan\'e \v casti k\'odu. Odstr\'anili sme tak po\v cas f\'azy refactoringu asi polovicu tried.

Samotn\'e pripojenie na\v sich nov\'ych tried pre parser a datov\'y model, ale nebolo trivi\'alne. K tomu v\v setk\'emu sme 
potrebovali zachova\v t \v cas\v t star\'eho parseru, ktor\'a mala za \'ulohu na\v c\'ita\v t B\"uchiho automat (vi\v d kapitolu \ref{sec:buchi}) so sk\'umanou 
vlastnos\v tou.

Overovacie algoritmy boli na\v stastie nap\'isan\'e dostato\v cne obecne, tak\v ze po \'uspe\v snom zaveden\'i nov\'ych tried do star\'ych sa nevyskytlo ve\v la 
probl\'emov. Najd\^ ole\v zitej\v sie pre ucelenie cel\'eho n\'astroja v\v sak bolo vytvorenie konzolov\'eho u\v z\'ivate\v lsk\'eho prostredia (\v dalej len 
CLI), ktor\'e do jednoho pr\'ikazu ukryje to, \v co by inak bolo nutn\'e spravi\v t v troch krokoch (vi\v d kapitolu \ref{sec:biodivine}). Okrem toho automaticky over\'i v\v setky vlastnosti 
zadan\'e vo vstupnom s\'ubore s t\'ymito vlastnos\v tami a n\'asledne zma\v ze do\v casn\'e s\'ubory. 

Vstupom pre CLI je n\'azov vybran\'eho overovacieho algoritmu, volite\v ln\'e prep\'ina\v ce a dva s\'ubory. Jedn\'ym 
je cesta k s\'uboru s modelom s pr\'iponou .bio a druh\'ym je cesta k s\'uboru s jednou alebo viacer\'ymi vlastnos\v tami zap\'isan\'ymi ako LTL formuly 
(vi\v d kapitolu \ref{sec:logika}) s~pr\'iponou .ltl. 

Bohu\v zial sme boli don\'uten\'i odstr\'ani\v t GUI z p\^ ovodn\'eho n\'astroja, ktor\'e sl\'u\v zilo na vytv\'aranie a ukladanie modelov a vizualiz\'aciu v\'ysledkov, 
preto\v ze sa uk\'azalo nezlu\v cite\v ln\'e s nov\'ymi roz\v s\'ireniami a bolo by  nutn\'e vytvori\v t \'uplne nov\'u verziu. T\'ato \v cinnos\v t je 
ponechan\'a pre bud\'uce mo\v znosti roz\v s\'irenia.

P\^ ovodn\'y BioDiVinE disponoval aj mo\v znos\v tou paralelne distribuovan\'eho spracov\'avania prostredn\'ictvom protokolu MPI (z~angl. \textit{Message 
Passing Interface}) \cite{MPI}. T\'ato mo\v znos\v t zostala zachovan\'a v r\'amci v\v setk\'ych p\^ ovodn\'ych \v cast\'i zdrojov\'eho k\'odu.

Kv\^ oli lep\v siemu a celistvej\v siemu preh\v ladu v\v setk\'eho vy\v s\v sie zmienen\'eho pon\'ukame poh\v lad na architekt\'uru n\'astroja BioDiVinE 1.1 
v diagrame (Obr. \ref{fig:diagram}), kde je \v cervenou farbou zv\'yraznen\'a oblas\v t ve\v lkej \v casti na\v sej pr\'ace.

\begin{figure}[h]
\centering
\includegraphics[width=1\textwidth]{BiodivineArchitecture2.pdf}
\caption{Diagram architekt\'ury n\'astroja BioDiVinE 1.1. V \v cervenej oblasti je zhrnut\'y n\'a\v s pr\'inos.}
\label{fig:diagram}
\end{figure}

%-------------------------------------------------------------------------------------------
\section{Vstupn\'y s\'ubor s modelom}
\label{sec:modelFile}
Hlavnou n\'apl\v nou tejto podkapitoly je zozn\'ami\v t bli\v z\v sie u\v z\'ivate\v la so syn\-taxou vstupn\'eho modelu. T\'ym sa mysl\'i s\'ubor s pr\'iponou
.bio a vyzer\'a nasledovne:
\begin{itemize}
\item VARS : \ \textit{premenn\'a1{\bf,} premenn\'a2{\bf,} \dots{}}
\item CONSTS : \ \textit{kon\v stanta1{\bf,} hodnota1{\bf;} kon\v stanta2{\bf,} hodnota2 {\bf;} \dots{}}
\item EQ : \ \textit{premenn\'a1 = rovnica1}
\item EQ : \ \textit{premenn\'a2 = rovnica2}
\item THRES : \ \textit{premenn\'a1{\bf:} prah1{\bf,} prah2{\bf,} prah3{\bf,} \dots{}}
\item THRES : \ \textit{premenn\'a2{\bf:} prah1{\bf,} prah2{\bf,} \dots{}}
\item VAR\_POINTS : \ \textit{premenn\'a1{\bf:} po\v cet\_bodov{\bf,} po\v cet\_segmentov{\bf;} premenn\'a2{\bf:} po\v cet\_bodov{\bf,} po\v cet\_segmentov}
\item INIT : \ \textit{premenn\'a1{\bf:} od{\bf,} do{\bf;} premenn\'a2{\bf:} od{\bf,} do}
\item system async;
\end{itemize}
Nieko\v lko vysvetliviek a obmedzen\'i:
\begin{enumerate}
\item V\v setko, \v co je p\'isan\'e neskosen\'ym p\'ismom, mus\'i zosta\v t zachovan\'e. Naopak to, \v co je nap\'isan\'e skosen\'ym p\'ismom, treba 
nahradi\v t vlastn\'ymi hodnotami.
\item Biele znaky s\'u kompletne ignorovan\'e, d\^ ole\v zit\'e s\'u iba odde\v lova\v ce vyzna\v cen\'e hrub\'ym p\'ismom (: ; , =). Na koncoch riadkov sa 
nikdy odde\v lova\v c nesmie nach\'adza\v t s v\'ynimkou posledn\'eho riadku (system async;).
\item N\'azvy premenn\'ych a kon\v st\'ant musia ako prv\'y znak obsahova\v t p\'ismeno nasledovan\'e \v lubovolnou kombin\'aciou p\'ismen, \v c\'isel a 
znakov \_\ \textasciitilde{}\ \{\ \}.
\item \v C\'isla maj\'u tvar cel\'ych alebo desatinn\'ych \v c\'isel s desatinnou bodkou.
\item Riadok (CONSTS) nie je povinn\'y. Je tie\v z mo\v zn\'e pou\v z\'iva\v t iba nepomenovan\'e kon\v stanty (\v ci\v ze \v c\'isla).
\item Riadky (VARS) a (CONSTS) sa musia nach\'adza\v t pred ostatn\'ymi riadkami -- s\'u \'uvodn\'e.
\item Riadok (VAR\_POINTS) nie je povinn\'y a \textit{po\v cet\_bodov} znamen\'a po\v cet bodov, v ktor\'ych bud\'u evaluovan\'e regula\v cn\'e funkcie 
pre dan\'u premenn\'u, {\it po\v cet\_segmentov} ur\v cuje po\v cet r\'amp, na ktor\'e sa tieto funkcie preved\'u.
\item Hodnoty {\it od} a {\it do} v riadku (INIT) musia by\v t niektor\'e z hodn\^ ot v pr\'islu\v snom riadku (THRES) pre dan\'u premenn\'u, pre ktor\'e
mus\'i plati\v t {\it od} $<$ {\it do}.
\item Ka\v zd\'a premenn\'a m\'a povinn\'y vlastn\'y riadok (EQ) a (THRES) a mus\'i sa nach\'adza\v t aj v riadku (INIT) s pr\'islu\v sn\'ymi hodnotami.
\item Riadok (system async;) je povinn\'y a mus\'i sa nach\'adza\v t na konci s\'uboru z historick\'ych d\^ ovodov.
\item Rovnica v riadku (EQ) je matematicky pop\'isan\'a v kapitole \ref{sec:model} a v be\v znom jazyku 
ni\v z\v sie:
\begin{itemize}
\item Parser podporuje un\'arnu oper\'aciu $-$, bin\'arne oper\'acie $+$, $-$ a $*$ a gu\v lat\'e z\'atvorky, ktor\'e m\^ o\v zu by\v t vnoren\'e \v lubovolne
ve\v lakr\'at.
\item Rovnica m\^ o\v ze okrem oper\'aci\'i a z\'atvoriek obsahova\v t pomenovan\'e aj nepomenovan\'e kon\v stanty, premenn\'e a nasleduj\'uce 
funkcie:
\begin{itemize}
\item rpcoor(premenn\'a, prah1, prah2, hodnota1, hodnota2), \\rmcoor(premenn\'a, prah1, prah2, hodnota1, hodnota2),
\item rp(premenn\'a, prah1, prah2, parameter1, parameter2),\\rm(premenn\'a, prah1, prah2, parameter1, parameter2),
\item hp(premenn\'a, prah, parameter1, parameter2),\\hm(premenn\'a, prah, parameter1, parameter2),
\item sp(premenn\'a, faktor, prah, parameter1, parameter2),\\sm(premenn\'a, faktor, prah, parameter1, parameter2),
\item spinv(premenn\'a, faktor, prah, parameter1, parameter2),\\sminv(premenn\'a, faktor, prah, parameter1, parameter2),
\item hillp(premenn\'a, prah, faktor, parameter1, parameter2),\\hillm(premenn\'a, prah, faktor, parameter1, parameter2),
\end{itemize}
\item \' Uvodn\'e znaky (r, h, s) m\^ o\v zu by\v t zadan\'e aj ako ve\v lk\'e p\'ismen\'a.
\item Znak (p) znamen\'a (+) v zmysle rast\'ucej funkcie a znak (m) znamen\'a (--) v zmysle klesaj\'ucej funkcie.
\item Premenn\'a mus\'i by\v t jedna zo sk\^ or uveden\'ych premenn\'ych v riad\-ku (VARS).
\item Hodnoty (prah, faktor, hodnota, parameter) m\^ o\v zu by\v t zadan\'e ako pomenovan\'e alebo nepomenovan\'e kon\v stanty.
\item Prah mus\'i by\v t jednou z prahov\'ych hodn\^ ot premennej.
\item \textbf{Nie je mo\v zn\'e n\'asobi\v t spolu rovnak\'e premenn\'e ani premenn\'u s regula\v cn\'ymi funkciami z\'avisl\'ymi od tejto premennej, ani
samotn\'e regula\v cn\'e funkcie z\'avisl\'e na rovnakej premennej.} Bolo by to poru\v senie pravidla o stupni premennej z kapitoly \ref{sec:model}.A.
\end{itemize}
\end{enumerate}

%-------------------------------------------------------------------------------------------
\section{Vstupn\'y s\'ubor s vlastnos\v{t}ou}
\label{sec:propertyFile}
S\'ubor s vlastnos\v tou alebo vlastnos\v tami je detailne pop\'isan\'y v diplomovej pr\'aci M. Jaro\v sa \cite{Jaros-thesis}. Tu si iba v kr\'atkosti zhrnieme syntax. S\'ubor 
s pr\'iponou .ltl m\^ o\v ze obsahova\v t nasleduj\'uce riadky:
\begin{itemize}
\item \#define \ {\it n\'azov\_premennej \ hodnota\_premennej}
\item \#property \ {\it vlastnos\v t\_vo\_forme\_ltl\_formuly}
\end{itemize}
a platia pre ne nasleduj\'uce pravidl\'a:
\begin{enumerate}
\item S\'ubor m\^ o\v ze obsahova\v t \v lubovoln\'y po\v cet defin\'ici\'i (riadok \#define), mali by sa v\v sak odli\v sova\v t v n\'azve premennej. Ten m\^ o\v ze obsahova\v t
mal\'e p\'ismen\'a, \v c\'isla a znak \_. Za\v c\'ina\v t ale musia bu\v d p\'ismenom alebo znakom \_.
\item Hodnota premennej je v podstate v\'yraz s logickou hodnotou (\v ci\v ze atomick\'a propoz\'icia, AP (vi\v d kapitolu \ref{sec:logika})). T\'a m\^ o\v ze 
ma\v t bu\v d priamo
hodnotu {\it true} alebo {\it false}, alebo m\^ o\v ze by\v t tvoren\'a re\v tazcom obsahuj\'ucim meno nejakej premennej z modelu, rela\v cn\'y oper\'ator (<, >, <=, >=) a \v c\'iseln\'u 
hodnotu (cel\'u alebo re\'alnu), ktor\'a sa mus\'i nach\'adza\v t medzi prahov\'ymi hodnotami premennej z modelu.
\item Po\v cet riadkov (\#property) tie\v z nie je obmedzen\'y, ale u\v z\'ivate\v l by mal vedie\v t, \v ze ka\v zd\'y tak\'yto riadok znamen\'a nov\'u 
vlastnos\v t, ktor\'a sa bude testova\v t na modeli, a to znamen\'a v\'ypo\v ctov\'u r\'e\v ziu.
\item Samotn\'a formula {\it vlastnos\v t\_vo\_forme\_ltl\_formuly} m\^ o\v ze by\v t tvoren\'a nasleduj\'ucimi hodnotami:
\begin{itemize}
\item Un\'arnymi tempor\'alnymi oper\'atormi ({\bf X}$\phi$, {\bf F}$\phi$, {\bf G}$\phi$) a bin\'arnymi tempor\'alnymi oper\'atormi ($\phi${\bf R}$\psi$, 
$\phi${\bf U}$\psi$)(vi\v d kapitolu \ref{sec:logika}), kde $\phi$ a $\psi$ s\'u v\'yrazy s logickou hodnotou.
\item V\'yrazmi s logickou hodnotou, ktor\'e s\'u \v dalej tvoren\'e logick\'ymi oper\'atormi ({\bf !} (neg\'acia), {\bf \&\&} (konjunkcia), {\bf ||} (
disjunkcia), {\bf ->} (implik\'acia), {\bf <->} (ekvivalencia)) a premenn\'ymi definovan\'ymi na za\v ciatku s\'uboru.
\item Syntax podporuje aj \v lubovolne vnoren\'e gu\v lat\'e  z\'atvorky.
\end{itemize}
\item Pre \'uplnos\v t treba doda\v t, \v ze t\'ato syntax podporuje aj p\'ar \v dals\'ich, roz\v s\'iren\'ych oper\'atorov a takmer ku ka\v zd\'emu e\v ste
druh\'y mo\v zn\'y z\'apis, ale n\'a\v s v\'ypo\v cet je dostato\v cn\'y pre z\'apis \v lubovolnej LTL formuly.
\end{enumerate}

%-------------------------------------------------------------------------------------------
\section{Priebeh procesu}
Po zavolan\'i CLI spolu so zadan\'ymi vstupn\'ymi parametrami sa najsk\^ or skontroluje ich po\v cet. Ak je tento men\v s\'i, program vyp\'i\v se \textit{help}
ponuku (vi\v d tabu\v lku v kapitole \ref{sec:using}). V opa\v cnom pr\'ipade skontroluje existenciu vstupn\'ych s\'uborov a pred\'a ich pomocn\'emu n\'astroju {\it divine.combine}.
Ten zist\'i po\v cet vlastnost\'i a pre ka\v zd\'u z nich vytvor\'i nov\'y s\'ubor a z\'arove\v n prevedie vlastnos\v t z LTL formuly na B\"uchiho automat. 
Tento v\'ystupn\'y s\'ubor m\'a tie\v z koncovku .bio, ale je iba pomocn\'y a pred ukon\v cen\'im CLI bude zmazan\'y. \v Dalej sa zist\'i po\v zadovan\'y 
overovac\'i algoritmus. M\^ o\v ze \'is\v t o algoritmy {\it owcty}, {\it distr\_map} alebo {\it owcty\_reversed}. \v Ziadne in\'e nie s\'u pr\'ipustn\'e.

Vybran\'y algoritmus sa spust\'i pre ka\v zd\'y novovytvoren\'y s\'ubor .bio ako n\'astroj {\it divine.n\'azov\_algoritmu} a predaj\'u sa mu pr\'ipadn\'e 
parametre. Potom sa vstup pred\'a triede s parserom a vytvor\'i sa datov\'y model, ktor\'y prejde line\'arnou aproxim\'aciou (vi\v d kapitolu 
\ref{sec:abstraction}.A), ak je to potrebn\'e. T\'ym sa
mysl\'i pr\'ipad, ke\v d rovnice modelu obsahuj\'u aspo\v n jednu Hillovu funkciu alebo aspo\v n jednu sigmoid\'alnu funkciu. Heavisidove funkcie sa 
upravuj\'u zvl\'a\v s\v t hne\v d po na\v c\'itan\'i, preto\v ze ich mo\v zno previes\v t na jedin\'u rampu, a teda line\'arna aproxim\'acia z kapitoly
\ref{sec:abstraction}.A pre ne nem\'a zmysel. 

Prahov\'e hodnoty vygenerovan\'e aproxim\'aciou aj prevodom Heavisidov\'ych funkci\'i sa ulo\v zia medzi ostatn\'e. To na jednu stranu zvy\v suje 
v\'ypo\v ctov\'u r\'e\v ziu, preto\v ze sa zv\" a\v c\v suje stavov\'y priestor generovan\'y nasleduj\'ucou obd\'l\v znikovou aproxim\'aciou, a to line\'arne 
k po\v ctu nov\'ych prahov\'ych hodn\^ ot. No na strane druhej sa t\'ym zlep\v suje presnos\v t tejto aproxim\'acie a cel\'eho v\'ypo\v ctu, preto\v ze sa 
abstrahovan\'y model pribli\v zuje skuto\v cn\'emu spojit\'emu modelu.

U\v z spomenut\'a obd\'l\v znikov\'a aproxim\'acia vygeneruje RATS (vi\v d kapitolu \ref{sec:abstraction}.B), \v ci\v ze diskr\'etny syst\'em p\^ ovodne spojit\'eho 
modelu, ktor\'y sa overuje proti vlastnosti v podobe automatu. Ak ju RATS sp\'l\v na, potom mo\v zno s~istotou tvrdi\v t, \v ze aj p\^ ovodn\'y model t\'uto
vlastnos\v t sp\'l\v na. Naopak, ak je vygenerovan\'y protipr\'iklad, nemus\'i v\^ obec zodpoveda\v t protipr\'ikladu v~skuto\v cnom spojitom modeli.
Av\v sak st\'ale plat\'i, \v ze model, \v ci u\v z abstrahovan\'y alebo skuto\v cn\'y, dan\'u vlastnos\v t nesp\'l\v na. \cite{BIODIVINE}

%================================IMPLEMENTACIA===============================================
\chapter{Implement\' acia}
Na implement\'aciu boli pou\v zit\'e programy {\it flexc++}, {\it bisonc++} a programovac\'i jazyk c++ vo verzii c++11. Preto je pre spr\'avne 
nain\v stalovanie aplik\'acie d\^ ole\v zit\'e ma\v t preklada\v c {\it gcc} verzie 4.7.3 alebo nov\v s\'i. Z historick\'ych d\^ ovodov je pre spr\'avne 
prelo\v zenie n\'astroja potrebn\'e ma\v t aj nasleduj\'uce n\'astroje \v ci programy:
\begin{itemize}
\item MPI - verzia 1.2 alebo nov\v sia
\item Automake - verzia 1.10.1 alebo nov\v sia
\item Autoconf - verzia 2.61
\end{itemize}
\cite{sybila-biodivine}

\section{Parser}
\label{sec:implParser}
Na \'uvod je treba poveda\v t, \v ze za v\'yrazom parser sa ukr\'yva aj druh\'y pomocn\'y n\'astroj tzv. scanner. Samotn\'y parser je n\'astroj na syntaktick\'u 
anal\'yzu vstupu a v niektor\'ych jednoduch\'ych pr\'ikladoch m\^ o\v ze by\v t dostato\v cn\'y, ale nie v na\v som. Aby bolo parsovanie \'uspe\v sn\'e mus\'i
mu predch\'adza\v t e\v ste lexik\'alna anal\'yza a t\'u m\'a na starosti pr\'ave scanner, ktor\'y zjednodu\v sene povedan\'e na\v c\'itava "slov\'a". Tie potom
posiela parseru, ktor\'y z nich sklad\'a "vety", respekt\'ive vzory. Len \v co je nejak\'y vzor rozpoznan\'y, parser vykon\'a pr\'islu\v sn\'e in\v strukcie 
nad spracov\'avan\'ymi d\'atami.

Pre vytvorenie parseru a scanneru s\'u k dispoz\'icii vo\v lne dostupn\'e sestersk\'e programy. Najstar\v sie z nich s\'u {\it flex} a {\it bison}. Tie sa v\v sak uk\'azali by\v t
a\v z pr\'ili\v s zastaran\'e a neschopn\'e vytvori\v t jednoduch\'u \v strukt\'uru typu trieda, ktor\'a by sa dala \v lahko za\v cleni\v t do u\v z 
existuj\'uceho k\'odu. \v Dal\v sou mo\v znos\v tou, ktor\'u sme zva\v zovali, boli programy {\it flex++} a {\it bison++}. Tie \'udajne podporuj\'u triedy, 
ale n\'ajs\v t k nim pou\v zite\v ln\'y u\v z\'ivate\v lsk\'y manu\'al sa uk\'azalo by\v t nemo\v zn\'e. Naopak programy {\it flexc++} a 
{\it bisonc++} s\'u preh\v ladne zdokumentovan\'e a ve\v lmi dobre za\v clenite\v ln\'e do zdrojov\'eho k\'odu v jazyku c++, preto sa 
uk\'azali by\v t tou najlep\v sou vo\v lbou.

Obidva programy generuj\'u nieko\v lko s\'uborov pre vlastn\'u potrebu, ktor\'e nem\'a cenu meni\v t, preto\v ze po ka\v zdom spusten\'i programu sa 
prep\'i\v su. S\'u to s\'ubory {\it ParserBase.h}, {\it parse.cc} pre program {\it bisonc++} a s\'ubory {\it ScannerBase.h} a {\it lex.cc} pre program 
{\it flexc++}. Hlavn\'e s\'ubory ur\v cen\'e pre program\'atora s\'u bez pr\'ipony a m\^ o\v zu by\v t nazvan\'e \v lubovo\v lne. Tie na\v se sa volaj\'u 
{\it parser2} a {\it scanner2}. \v Dal\v sie u\v zito\v cn\'e a modifikovate\v ln\'e s\'ubory s\'u {\it Parser.h}, {\it Parser.ih}, {\it Scanner.h} a 
{\it Scanner.ih}, ktor\'e dod\'avaj\'u potrebn\'u modularitu. To umo\v z\v nuje nar\'aba\v t s parserom a scannerom ako s klasick\'ymi triedami, \v co 
bolo v na\v som pr\'ipade ve\v lmi \v ziadan\'e. 

U\v z na prv\'y poh\v lad vidno pod\v la n\'azvov, \v ze ide o kompatibiln\'e programy vyv\'ijan\'e rovnak\'ym t\'imom, ktor\'y navy\v se pon\'uka ve\v lmi 
dobr\'y u\v z\'ivate\v lsk\'y n\'avod (vi\v d \cite{flexc++} \cite{bisonc++}).

\section{D\'atov\'y model}
\label{sec:dataModel}
Nov\'y d\'atov\'y model sa sklad\'a z troch tried. S\'u to {\it Entite}, {\it Summember} a {\it Model}. Po\v cas procesu parsovania vstupn\'eho modelu sa 
jednotliv\'e 
d\'ata ukladaj\'u do pr\'islu\v sn\'ych \v strukt\'ur in\v stancie triedy {\it Model}. Nazvime ju {\it dataModel}. D\'atami rozumieme u\v z\'ivate\v lom 
\v specifikovan\'e \'udaje na pr\'islu\v sn\'ych riadkoch pod\v la popisu v~kapitole \ref{sec:modelFile}. Jedinou v\'ynimkou s\'u rovnice \v ci\v ze riadky 
za\v c\'inaj\'uce n\'apisom "{EQ:}". Ke\v d\v ze nechceme u\v z\'ivate\v la obmedzova\v t striktne zadanou defin\'iciou pre p\'isanie rovn\'ic, ale naopak 
chceme mu umo\v zni\v t, aby mohol p\'isa\v t obecn\'e rovnice a \v lubovo\v lne pritom z\'atvorkova\v t, mus\'ime nutne rovnice pred ulo\v zen\'im upravi\v t, 
aby dostali podobu pod\v la defin\'icie v~kapitole \ref{sec:model}.B. K tomu sl\'u\v zi trieda {\it Entite} s pomocou triedy {\it Summember}.

Parsovanie rovn\'ic prebieha slovo za slovom, kde pod pojmom slovo rozumieme skupinu znakov rozpoznan\'ych scannerom. Tak\'ymto slovom v~rovnici m\^ o\v ze 
by\v t \v c\'islo, premenn\'a, kon\v stanta, regula\v cn\'e funkcie (vi\v d kapitolu \ref{sec:model}), ale aj gu\v lat\'e z\'atvorky a znamienka $+$, $-$ a
$*$ (\v c\'itaj kr\'at). Prioritou je odstr\'anenie z\'atvoriek a spr\'avne vyhodnotenie znamienok, aby v\v setky \v cleny rovnice boli na jednej \'urovni. 
Tento \v clen predstavuje v podstate in\v stanciu triedy {\it Summember}. Indukt\'ivne, jeden \v clen m\^ o\v ze by\v t zlo\v zen\'y z n\'asobku viacer\'ych 
\v clenov:
\begin{equation}
clen1 \ = \ clen1.1*clen1.2*clen1.3 \dots{}
\end{equation}
In\'ymi slovami, ka\v zd\'e \v c\'islo, re\v tazec znakov (n\'azov premennej alebo kon\v stanty, nie v\v sak funkcia) alebo regula\v cn\'u funkciu
pova\v zujeme za \v clen. Ka\v z\-d\'y n\'asobok t\'ychto \v clenov pova\v zujeme tie\v z za \v clen. Cie\v lom preto je dosta\v t rovnicu do tvaru 
s\v citovania alebo od\v citovania jednotliv\'ych \v clenov:
\begin{equation}
rovnica \ = \ clen1 + clen2 - clen3 + clen4 \dots{}
\end{equation} 
Dokonca ve\v lmi jednoducho sa mo\v zno zbavi\v t aj od\v citovania jednoduch\'ym prevodom:
\begin{equation}
clen2 - clen3 \ = \ clen2 + (-1)clen3,
\end{equation}
tak\v ze vo v\'ysledku dost\'avame:
\begin{equation}
rovnica \ = \ clen1 + clen2 + (-1)clen3 + clen4 \dots{}
\end{equation}

Pre potrebu \'upravy pri parsovan\'i uklad\'ame ka\v zd\'y jednotliv\'y \v clen ako in\v stanciu triedy {\it Entite} do z\'asobn\'ika. Nazvime ju entita.
Obsahuje vektor \v clenov \v ci\v ze in\v stanci\'i triedy {\it Summember}. Potom pri na\v c\'itan\'i znamienka kr\'at ($*$) sa rekurz\'ivne z dvoch 
posledn\'ych na\v c\'itan\'ych ent\'it v z\'asobn\'iku (ka\v z\-d\'a obsahuj\'uca jeden \v clen) stane entita jedna (obsahuj\'uca jeden \v clen tvoren\'y 
n\'asobkom \v clenov z p\^ ovodn\'ych ent\'it). Dve posledn\'e in\v stancie zahod\'ime a navrch z\'asobn\'iku ulo\v z\'ime t\'uto nov\'u.

Pri na\v c\'itan\'i znamienka plus ($+$) sa rekurz\'ivne z dvoch posledn\'ych ent\'it v z\'asobn\'iku (ka\v zd\'a obsahuj\'uca jeden \v clen) stane jedna nov\'a 
entita, tentokr\'at v\v sak obsahuj\'uca \v cleny dva. Star\'e entity sa zahodia, nov\'a sa op\"a\v t ulo\v z\'i. Obecne mo\v zno poveda\v t, \v ze pri 
s\v citovan\'i m\'a v\'ysledn\'a entita to\v lko \v clenov, ko\v lko mali \v clenov dohromady p\^ ovodn\'e entity. Pri na\v c\'itan\'i znamienka m\'inus ($-$) 
sa najsk\^ or \v cleny druhej entity preved\'u na z\'aporn\'e a potom sa pokra\v cuje rovnako ako pri s\v citovan\'i.

\v Speci\'alne treba spomen\'u\v t pr\'ipad, ke\v d entity pri n\'asoben\'i obsahuj\'u ka\v zd\'a nieko\v lko \v clenov. V\'ysledkom bude entita jedna 
obsahuj\'uca to\v lko \v clenov, ko\v lko tvor\'i n\'asobok po\v ctu \v clenov p\^ ovodn\'ych ent\'it. Toto v\v setko je regul\'erne v~zmys\-le roz\v s\'irenia be\v znej 
oper\'acie rozn\'asobenia aj pre ne\v c\'iseln\'e \v cleny.

V\v daka tomuto post-parsovaciemu procesu kone\v cne dost\'avame rovnicu v po\v zadovanom tvare a m\^ o\v zeme ju ulo\v zi\v t ako vektor \v clenov do 
dataModelu.

\section{Line\'arna abstrakcia neline\'arnych funkci\'i}
Ke\v d s\'u v\v setky d\'ata v nami po\v zadovanom form\'ate, je mo\v zn\'e vykona\v t line\'arnu aproxim\'aciu v\v setk\'ych neline\'arnych funkci\'i 
(vi\v d kapitolu \ref{sec:abstraction}.A) d\'atov\'eho modelu (vi\v d kapitolu \ref{sec:dataModel}).

E\v ste predt\'ym ale spome\v nme Heavisidove alebo schodov\'e funkcie \cite{step}, ktor\'e s\'u samostatnou kateg\'oriou. Ke\v d\v ze sa jedn\'a 
o~nespojit\'e funkcie, je potrebn\'e ich nie\v c\'im nahradi\v t. Rampov\'e funkcie (vi\v d kapitolu \ref{sec:model}.C) sa zdaj\'u by\v t vhodnou n\'ahradou. 
Po\v cas parsovania e\v ste pred ulo\v zen\'im do d\'atov\'eho modelu s\'u schodov\'e funkcie preveden\'e priamo na rampy, a to v pomere jedna ku jednej. 
Pr\'ave z tohto d\^ ovodu, \v ze sta\v c\'i nahradi\v t ka\v zd\'u Heavisidovu funkciu jednou rampovou funkciou, nie je nutn\'e zah\'r\v na\v t ich do 
cel\'eho procesu line\'arnej aproxim\'acie, kde sa ka\v zd\'a krivka nahrad\'i nieko\v lk\'ymi (minim\'alne dvoma) rampami. Napriek tomu sa aj tu jedn\'a 
o line\'arnu abstrakciu, av\v sak odli\v sn\'eho typu. 

Schodov\'e funkcie s\'u definovan\'e tak, \v ze prechod medzi funk\v cn\'ymi hodnotami funkcie je v zadanom bode, prahu. Probl\'em ale nast\'ava s funk\v cnou
hodnotou v tomto konkr\'etnom bode. Aby sme z nespojitej funkcie urobili spojit\'u, vytvor\'ime dva nov\'e prahy. Jeden napravo a druh\'y na\v lavo od 
p\^ ovodn\'eho prahu, oba v nepatrnej vzdialenosti. V z\'avislosti od toho, \v ci je to funkcia rast\'uca alebo klesaj\'uca, sa spoja spr\'avne prahov\'e hodnoty 
so spr\'avnymi funk\v cn\'ymi hodnotami a prechod medzi nimi je spojit\'y a z\'arove\v n line\'arny. Nov\'e prahov\'e hodnoty sa samozrejme ulo\v zia medzi
ostatn\'e, aby nech\'ybali pri obd\'l\v znikovej abstrakcii (vi\v d kapitolu \ref{sec:abstraction}.B).

Line\'arnu abstrakciu vykon\'avame v\v zdy pre v\v setky neline\'arne funkcie (krivky) z\'avisl\'e od rovnakej premennej. To znamen\'a, \v ze sa 
vykon\'a to\v lko\-kr\'at, ko\v lko m\'ame v modeli premenn\'ych. Ak na nejakej premennej nie s\'u z\'avisl\'e \v ziadne neline\'arne funkcie, tak sa 
presko\v c\'i.

N\'asledne je na vybran\'e krivky aplikovan\'a abstrakcia pod\v la postupu v kapitole \ref{sec:abstraction}.A. Takto dost\'avame z p\^ ovodnej mno\v ziny
kriviek mno\v zinu mno\v z\'in r\'amp, kde ka\v zd\'a mno\v zina r\'amp nahr\'adza v rovnici krivku. Tento proces je iterat\'ivny a \v ciasto\v cne 
rekurz\'ivny. Preto\v ze krivka sa mus\'i nahradi\v t sumou nov\'ych rampov\'ych funkci\'i. To ale znamen\'a, \v ze z p\^ ovodn\'eho \v clena rovnice 
(vi\v d kapitolu \ref{sec:dataModel}), obsahuj\'uceho nahr\'adzan\'u krivku, sa stane viacero nov\'ych duplicitn\'ych \v clenov, ka\v zd\'y v\v sak s inou 
nahr\'adzaj\'ucou rampou. Nesmieme zabudn\'u\v t p\^ ovodn\'y \v clen zmaza\v t. A rekurz\'ivny preto, lebo je mo\v zn\'e, \v ze v p\^ ovodnom \v clene rovnice
bol n\'asobok hne\v d nieko\v lk\'ych kriviek. V takom pr\'ipade treba nahradi\v t v\v setky duplicitn\'e v\'yskyty \v dal\v sej nahr\'adzanej krivky 
v nov\'ych, rampu obsahuj\'ucich, duplicitn\'ych \v clenoch. Pr\'iklad pre zjednodu\v senie, ak m\'ame \v clen rovnice, v ktorom je n\'asobok troch 
r\^ oznych kriviek a ka\v zd\'a bude nahraden\'a piatimi rampami, tak po skon\v cen\'i line\'arnej abstrakcie bude rovnica miesto jednoho obsahova\v t 
\v clenov hne\v d stodvadsa\v tp\" a\v t.

Vid\'ime, \v ze tento proces podstatne zv\" a\v c\v suje rovnice, a teda aj sta\v zuje ich evalu\'aciu. V skuto\v cnosti je toto z h\v ladiska 
v\'ypo\v ctov\'eho zanedbate\v ln\'e. Podstatnej\v sie je, \v ze touto aproxim\'aciou vznikn\'u nov\'e prahov\'e hodnoty, ktor\'e zv\" a\v c\v suj\'u 
po\v cet stavov produkovan\'ych n\'aslednou obd\'l\v znikovou abstrakciou. T\'u tu podrobne popisova\v t nebudeme, preto\v ze nie je produktom na\v sej 
implement\'acie.

\section{CLI}
\label{sec:implCLI}
CLI alebo konzolov\'e u\v z\'ivate\v lsk\'e prostredie (z~angl. {\it Command-line interface}) sl\'u\v zi ako obal pre n\'astroj BioDiVinE 1.1. Preto\v ze
tak, ako aj p\^ ovodn\'y BioDiVinE 1.0, je aj nov\'a verzia vlastne sada n\'astrojov a my sme chceli u\v z\'ivate\v lovi poskytn\'u\v t jeden schopn\'y 
n\'astroj. Nikomu nebr\'anime pou\v z\'iva\v t samostatne tieto n\'astroje, ale chceme da\v t aj mo\v znos\v t vyhn\'u\v t sa im.

CLI vol\'a n\'astroje {\it divine.combine}, {\it divine.owcty}, {\it divine.owcty\_reversed} a {\it divine.distr\_map} pomocou syst\'emov\'eho volania 
exec(2) a \v cak\'a na ich dokon\v cenie. Samotn\'y n\'astroj {\it divine.combine} je vlastne shellov\'y skript volaj\'uci \v dal\-\v s\'i n\'astroj pre 
prevod LTL formuly (vi\v d kapitolu \ref{sec:logika}) do B\"uchiho automatu (vi\v d kapitolu \ref{sec:buchi}) {\it divine.ltl2ba}.


%================================POUZITIE-PROGRAMU=============================================
\chapter{Pou\v zitie programu}
\label{sec:using}
CLI sa vol\'a z pr\'ikazov\'eho riadku spolu s minim\'alne tromi vstupn\'ymi parametrami. Ak sa nezad\'a spr\'avny po\v cet parametrov alebo je 
prv\'ym parametrom {\tt -h}, resp. {\tt {-}{-}help}, vyvol\'a sa help ponuka \v ci\v ze n\'avod na pou\v zitie CLI.

Prv\'ym parametrom je n\'azov algoritmu, ktor\'y sa pou\v zije na overenie modelu. Na v\'yber s\'u {\it owcty}, {\it distr\_map} a {\it owcty\_reversed}. 
Tieto zodpovedaj\'u n\'astrojom rovnak\'ych mien s prefixom {\it divine.}, ako bolo povedan\'e v kapitole \ref{sec:implCLI}.

\v Dal\v sie parametre m\^ o\v zu by\v t volite\v ln\'e prep\'ina\v ce ur\v cen\'e vybran\'emu overovaciemu algoritmu. CLI ich jednoducho prevezme a n\'asledne 
pred\'a na vstup volan\'emu overovaciemu n\'astroju. M\^ o\v ze \'is\v t o nasleduj\'uce prep\'ina\v ce:
\begin{itemize}
\item Prep\'ina\v ce spolo\v cn\'e pre v\v setky algoritmy:
	\begin{align*}
	&\textrm{-v,}& &\textrm{{-}{-}version}& &\textrm{zobraz\'i verziu vybran\'eho algoritmu}\\
	&\textrm{-h,}& &\textrm{{-}{-}help}& &\textrm{zobraz\'i help ponuku vybran\'eho algoritmu}\\
	&\textrm{-q,}& &\textrm{{-}{-}quiet}& &\textrm{zap\'ina tich\'y m\'od}\\
	&\textrm{-c,}& &\textrm{{-}{-}statelist}& &\textrm{vytvor\'i .ce\_states s\'ubor s protipr\'ikladom}\\
	&\textrm{-t,}& &\textrm{{-}{-}trail}& &\textrm{vytvor\'i .trail s\'ubor s protipr\'ikladom}\\
	&\textrm{-r,}& &\textrm{{-}{-}report}& &\textrm{vytvor\'i .report s\'ubor s \'udajmi o behu procesu}\\
	&\textrm{-L,}& &\textrm{{-}{-}log}& &\textrm{zapne zaznamen\'avanie protokolu}\\
	&\textrm{-H } x\textrm{,}& &\textrm{{-}{-}htsize } x& &\textrm{nastav\'i ve\v lkos\v t hash tabu\v lky takto}\\
	& & & & &x < 33 \textrm{ ? tak } 2^x \textrm{ inak } x\\
	&\textrm{-X w,}& & & &\textrm{nastav\'i meno vytv\'aran\'ych s\'uborov na w}\\
	& & & & &\textrm{(w.trail, w.report, w.ce\_states, \dots{})}\\
	&\textrm{-V,}& & & &\textrm{zobraz\'i dodato\v cn\'e inform\'acie}
	\end{align*}
\item Prep\'ina\v ce navy\v se pre algoritmus {\it owcty}:
	\begin{align*}
	&\textrm{-C x,}& &\textrm{{-}{-}compress x}& &\textrm{nastav\'i met\'odu kompresie stavov}\\
	& & & & &\textrm{(0 = \v ziadna, 1 = Huffman)}\\
	&\textrm{-s,}& &\textrm{{-}{-}simple}& &\textrm{prepne na testovanie dosiahnute\v lnosti}\\
	& & & & &\textrm{akceptuj\'uceho stavu}
	\end{align*}
\item Prep\'ina\v ce navy\v se pre algoritmus {\it owcty\_reversed}:
	\begin{align*}
	&\textrm{-R,}& &\textrm{{-}{-}remove}& &\textrm{odstra\v nuje prechody }\\
	& & & & &\textrm{(ve\v lmi pomal\'e, \v setr\'i pam\"a\v t)}\\
	&\textrm{-s,}& &\textrm{{-}{-}simple}& &\textrm{prepne na testovanie dosiahnute\v lnosti}\\
	& & & & &\textrm{akceptuj\'uceho stavu}
	\end{align*}
\end{itemize}

Predposledn\'ym parametrom je cesta k s\'uboru obsahuj\'ucemu dynamic\-k\'y biochemick\'y model. Popis k nemu mo\v zno n\'ajs\v t v kapitole 
\ref{sec:modelFile}. Povinnos\v tou s\'uboru je pr\'ipona {\it .bio}.

Posledn\'ym vstupn\'ym parametrom je cesta k s\'uboru obsahuj\'ucemu testovan\'u vlastnos\v t vo forme LTL formuly (vi\v d kapitolu \ref{sec:logika}). 
V skuto\v cnosti m\^ o\v ze t\'ychto vlastnost\'i obsahova\v t nieko\v lko. V\v setky sa postupne overuj\'u vo\v ci modelu. S\'ubor mus\'i ma\v t koncovku 
{\it .ltl} a detailnej\v sie je pop\'isan\'y v kapitole \ref{sec:propertyFile}.

V pr\'ipade, \v ze by u\v z\'ivate\v l chcel alebo potreboval pou\v zi\v t niektor\'y z overovac\'ich n\'astrojov samostatne, doklad\'ame tieto 
dodato\v cn\'e inform\'acie. Potom, \v co si u\v z\'ivate\v l zvol\'i model a vlastnos\v t, \v ci\v ze dva separ\'atne s\'ubory, mus\'i zavola\v t
n\'astroj {\it divine.combine} a tieto s\'ubory mu preda\v t ako prv\'y (model) a druh\'y (vlastnos\v t) parameter. V z\'avislosti od po\v ctu vlastnost\'i
v s\'ubore s pr\'iponou {\it .ltl} sa vytvor\'i  rovnak\'y po\v cet nov\'ych s\'uborov {\it n\'azov\_modelu.propX.bio}, kde {\it X} je poradov\'e \v c\'islo
vlastnosti. N\'asledne u\v z len sta\v c\'i vybran\'emu overovaciemu n\'astroju preda\v t jeden z vygenerovan\'ych s\'uborov ako vstupn\'y parameter. 
Prep\'ina\v ce v tabu\v lke umiestnenej vy\v s\v sie s\'u rovnako pou\v zite\v ln\'e.


%====================================CASE-STUDY=============================================
\chapter{Pr\'ipadov\'a \v st\'udia}
% pRB - E2F1  (v cicavcoch) cast z velkeho regulacneho modelu pre rast a delenie buniek
% regulacny mechanizmus fazoveho prechodu medzi G1 a S fazou
% pRB tumor suppressor (retinoblastoma)
% E2F1 transcription factor
% It is widely believed that small units or modules can be regarded as key players in larger networks
Pre kr\'atku uk\'a\v zku n\'astroja BioDiVinE 1.1 sme si zvolili presk\'uma\v t prechod medzi f\'azami bunkov\'eho cyklu. Konkr\'etne medzi f\'azami $G_1$ 
(zodpoved\'a za rast bunky do p\^ ovodnej ve\v lkosti a produkciu prote\'inov k tomu ur\v cen\'ych) a $S$ (zodpoved\'a za synt\'ezu DNA a je prvou 
f\'azou bud\'uceho delenia) a ozna\v cujeme ho ako f\'azov\'y prechod $G_1/S$. U mnohobunkov\'ych organizmov a u cicavcov \v speci\'alne je prechod medzi t\'ymito f\'azami riaden\'y zlo\v zitou sie\v tou
navz\'ajom sa reguluj\'ucich prote\'inov. Bli\v z\v sie inform\'acie k tejto sieti mo\v zno n\'ajs\v t v \v cl\'anku \cite{Swat:2004}. My sa zameriame na
jeden konkr\'etny mot\'iv tvoriaci jadro tejto siete. Ide o vz\'ajomn\'u regul\'aciu n\'adorov\'eho supresora $pRB$ a transkrip\v cn\'eho faktora $E2F1$ 
(vi\v d Obr. \ref{fig:caseStudy}). Napriek tomu, \v ze je tento model pomerne mal\'y, ukazuje sa, \v ze m\'a k\v l\'u\v cov\'u \'ulohu.
\begin{figure}[h]
\centering
\begin{tikzpicture}[shorten >=1pt,node distance=5cm,on grid,auto]
	\node[state, thick] (p) {$pRB$};
	\node[state, thick] (e) [right of=p] {$E2F1$};
	\path[->, thick]
	(e) edge[swap, bend left] node {$+$} (p)
		edge[loop above] node {$+$} ();
	\path[->, dashed, thick]
	(p) edge[bend left] node {$-$} (e)
		edge[loop above] node {$-$} ();
\end{tikzpicture}
\caption{Jadro regula\v cnej siete f\'azov\'eho prechodu $G_1/S$ bunkov\'eho delenia cicavcov}
\label{fig:caseStudy}
\end{figure}

Prepis tohto modelu pomocou Hillovej kinetiky vyzer\'a:
\begin{align}
\frac{d[pRB]}{dt} &= k_1 \frac{[E2F1]}{K_{m_1} + [E2F1]}\frac{K_{m_2}}{K_{m_2} + [pRB]} - \gamma_{pRB}[pRB],\\
\frac{d[E2F1]}{dt} &= k_p + k_2 \frac{a^2 + [E2F1]^2}{K_{m_3}^2 + [E2F1]^2}\frac{K_{m_4}}{K_{m_4} + [pRB]} - \gamma_{E2F1}[E2F1].
\end{align}
Hodnoty v\v setk\'ych kon\v st\'ant s\'u zvolen\'e tak, aby odr\'a\v zali experiment\'alne chovanie. Poch\'adzaj\'u z \v cl\'anku \cite{Swat:2004} a 
vyzeraj\'u nasledovne:
\begin{align}
&K_{m_1} = 0.5,& &K_{m_2} = 0.5,& &K_{m_3} = 4,& &K_{m_4} = 5,\\
&k_1 = 1,& &k_2 = 1.6,& &k_p = 0.05,& &a = 0.04,\\
& & &\gamma_{pRB} = 0.005,& &\gamma_{E2F1} = 0.1.& & &
\end{align}

Tento model je zauj\'imav\'y t\'ym, \v ze vykazuje zn\'amky bistability, k \v comu mu pom\'aha fakt, \v ze faktor $E2F1$ je pozit\'ivne autoregulovan\'y. 
Pok\'usime sa toto tvrdenie otestova\v t na na\v som n\'astroji. Vlastnosti, ktor\'e by mali zodpoveda\v t tomuto chovaniu, s\'u prebran\'e z \v cl\'anku
\cite{TCBB-2010} a nach\'adzaj\'u sa v pr\'iloh\'ach \ref{sec:caseProp1File}, \ref{sec:caseProp2File} a \ref{sec:caseProp3File}. Samotn\'y model je pop\'isan\'y 
v pr\'ilohe \ref{sec:caseStudyFile}. Vo v\v setk\'ych pr\'ipadoch budeme vola\v t algoritmus {\it distr\_map} s parametrami {\it -Srt}.
\begin{itemize}
\item Vlastnos\v t \v c\'islo jedna $(G(E2F1 < 2))$ (vi\v d pr\'iloha \ref{sec:caseProp1File}), ktor\'a mala dokazova\v t, \v ze ak po\v ciato\v cn\'a 
koncentr\'acia faktora $E2F1$ bude n\'izka, tak n\'izka aj zostane, sa n\'am podarilo vyvr\'ati\v t. Protipr\'iklad (vi\v d pr\'ilohu \ref{sec:prop1trail})
n\'am ukazuje, \v ze po\v ciato\v cn\'a n\'izka koncentr\'acia $pRB$ nesta\v c\'i dostato\v cne potl\'a\v ca\v t produkciu $E2F1$, ktor\'a rastie k maximu. 
M\^ o\v ze to by\v t sp\^ osoben\'e nevhodnou kombin\'aciou
parametrov, preto\v ze ich hodnoty sme prebrali z rozsiahlej\v sieho modelu v \cite{Swat:2004} a vlastnosti zase z modelu v~\cite{TCBB-2010} ur\v cen\'eho 
pre testovanie parametriz\'acie v programe PEPMC (vi\v d kapitolu \ref{sec:pepmc}). V\'ypo\v cet trval vy\v se tridsa\v t min\'ut a podrobn\'u spr\'avu 
z~priebehu procesu vidno v pr\'ilohe \ref{sec:prop1report}. Okrem toho priklad\'ame aj \v cas\v t v\'ystupu programu s u\v zito\v cn\'ymi inform\'aciami 
(vi\v d pr\'iloha \ref{sec:prop1output}.
\item Vlastnos\v t \v c\'islo dva $(G(E2F1 >= 2))$ (vi\v d pr\'iloha \ref{sec:caseProp2File}) je sp\'l\v nan\'a uk\'a\v zkov\'ym modelom. Z toho vypl\'yva, 
\v ze ke\v d m\'a raz transkrip\v cn\'y faktor $E2F1$ vysok\'u koncentr\'aciu, tak u\v z do n\'izkych hodn\^ ot neklesne. Pravdepodobne to vych\'adza 
zo silnej pozit\'ivnej autoregul\'acie, ktor\'u nedok\'a\v ze potla\v ci\v t ani inhib\'icia supresorom $pRB$. Inici\'alna koncentr\'acia $E2F1$ bola 
nastaven\'a na interval $\langle4,6\rangle$. V\'ypo\v cet trval len necel\'ych desa\v t min\'ut, z \v coho \v ses\v t a pol min\'uty trvala optim\'alna 
line\'arna aproxim\'acia (vi\v d kapitolu \ref{sec:abstraction}.A). Podrobnej\v siu spr\'avu mo\v zno n\'ajs\v t v~pr\'ilohe \ref{sec:prop2report} a 
\v cas\v t v\'ypisu programu v~pr\'ilohe \ref{sec:prop2output}.
\item Tretia vlastnos\v t $((E2F1 < 2) \rightarrow F G(E2F1 >= 2))$ (vi\v d pr\'ilohu \ref{sec:caseProp3File}) mala dok\'aza\v t, \v ze aj ke\v d bude ma\v t 
transkrip\v cn\'y faktor $E2F1$ na po\v ciatku n\'izku koncentr\'aciu, dok\'a\v ze prekona\v t hranicu (v tomto pr\'ipade $2$) a natrvalo udr\v zat svoju 
koncentr\'aciu na vy\v s\v sej hladine, ne\v z je t\'ato hranica. Uk\'azalo sa, \v ze model t\'uto vlastnos\v t sp\'l\v na a d\^ ovodom bude op\"a\v t 
pravdepodobne siln\'a pozit\'ivna autoregul\'acia a naopak slab\'a inhib\'icia. V\'ypo\v cet trval vy\v se dvadsa\v tp\"a\v t min\'ut, z \v coho op\"a\v t
\v ses\v t a \v stvr\v t min\'uty trvala line\'arna aproxim\'acia. Spr\'ava z priebehu procesu sa nach\'adza v pr\'ilohe \ref{sec:prop3report} a \v cas\v t
v\'ystupu programu zase v~pr\'ilohe \ref{sec:prop3output}.
\end{itemize}

Na z\'aklade z\'iskan\'ych \'udajov sa domnievame, \v ze koncentr\'acia transkrip\v cn\'eho faktora $E2F1$ 
rastie nad v\v setky medze. Aby sme si to mohli potvrdi\v t, rozhodli sme sa otestova\v t \v dal\v siu vlastnos\v t (vi\v d pr\'ilohu \ref{sec:caseProp4File}).
T\'a mala dok\'aza\v t, \v ze aj ke\v d bude ma\v t faktor $E2F1$ na po\v ciatku n\'izku koncentr\'aciu, rovnak\'u ako pri testovan\'i tretej vlastnosti,
tak nakoniec dosiahne naozaj vysokej hodnoty (v tomto pr\'ipade a\v z $8$).

Po \v styridsiatich min\'utach v\'ypo\v ctu sa uk\'azalo, \v ze model naozaj t\'uto vlastnos\v t sp\'l\v na. A teda na\v sa domnienka o bezmedznom raste 
vyzer\'a by\v t spr\'avna. Detailnej\v sia spr\'ava sa nach\'adza v pr\'ilohe \ref{sec:prop4report} a \v cas\v t v\'ypisu programu v pr\'ilohe 
\ref{sec:prop4output}.



%=========================================ZAVER=============================================
\chapter{Z\'aver}
Cie\v lom pr\'ace bolo najsk\^ or zjednodu\v si\v t p\^ ovodn\'y n\'astroj BioDiVinE 1.0 a n\'asledne ho roz\v s\'iri\v t o nov\'u funkcionalitu. 
Zjednodu\v sen\'im m\'ame na mysli refaktoriz\'aciu, po\v cas ktorej sa podarilo odstr\'ani\v t nepotrebn\'e triedy s prefixom {\it dve} 
(dvadsa\v t\v ses\v t), {\it bymoc} (sedem) spolu s jeho VM a testami (vy\v se \v dal\v s\'ich tridsa\v t zdrojov\'ych s\'uborov), nejak\'e obecn\'e triedy 
(tri) a odstr\'anen\'e bolo tie\v z GUI (dvadsa\v ttri s\'uborov), zbytky nepou\v z\'ivanej Java aplik\'acie a vy\v se dvadsa\v t \v dal\v s\'ich 
nepotrebn\'ych s\'uborov.

Novou funkcionalitou mal by\v t nov\'y obecnej\v s\'i popis vstupn\'eho modelu, aby bolo mo\v zn\'e overova\v t \v sir\v siu \v sk\'alu modelov vo\v ci ich 
vlastnostiam. Cel\'e to malo preh\v ladne spoji\v t konzolov\'e u\v z\'ivate\v lsk\'e prostredie.

V\v setko vy\v s\v sie vymenovan\'e sa n\'am podarilo a zost\'ava iba d\'ufa\v t, \v ze aj \'uspe\v sne. Na t\'uto ot\'azku by mohol nadviaza\v t niekto 
\v dal\v s\'i t\'ym, \v ze by n\'a\v s n\'astroj patri\v cne otestoval na dostato\v cnom po\v cte re\'alnych modelov, ktor\'e by poch\'adzali bu\v d z 
experiment\'alne dolo\v zen\'ych \v st\'udi\'i alebo z podobne zameran\'ych programov.

\bibliographystyle{plain} 
\bibliography{dp1}


%\chapter*{Pr\'iloha}
\appendix
\chapter{Model}
\label{sec:caseStudyFile}
V skuto\v cnom s\'ubore mus\'i by\v t jeden z\'apis na jednom riadku. Tu sme v\v sak pre \'usporu miesta don\'uten\'y toto pravidlo poru\v si\v t.\\

\noindent
Obsah s\'uboru {\tt tcbb1.bio}:\\

{\tt
\noindent
VARS: pRB, E2F1\\

\noindent
CONSTS: k1,1; y\_pRB,0.005; kp,0.05; k2,1.6; y\_E2F1,0.1;\\ a,0.04\\

\noindent
VAR\_POINTS: pRB: 1500, 5; E2F1: 1500, 5\\

\noindent
EQ: pRB = k1*Hillp(E2F1,0.5,1,0,1)*Hillm(pRB,0.5,1,1,0)- \\y\_pRB*pRB\\

\noindent
EQ: E2F1 = kp + k2*Hillm(pRB,5,1,1,0)*(a*a*0.0625*\\Hillm(E2F1,4,2,1,0) + Hillp(E2F1,4,2,0,1)) - y\_E2F1*\\E2F1\\

\noindent
THRES: pRB:  0, 1, 2, 6, 7, 8, 10, 3, 4, 5\\
THRES: E2F1: 0, 1, 2, 4, 6, 8, 10, 12, 15\\

\noindent
INIT: pRB: 0, 1; E2F1: 1, 2\\

\noindent
system async;\\
}

\chapter{Vlastnos\v t \v c. 1}
\label{sec:caseProp1File}
Pre \'uplnos\v t treba doda\v t, \v ze sme vykonali zmenu v s\'ubore s modelom. Treba prep\'isa\v t na riadku za\v c\'inaj\'ucom 
{\tt INIT:} hodnoty pre {E2F1} na hodnoty 0, 1.\\

\noindent
Obsah s\'uboru {\tt prop1.ltl}:\\

{\tt
\noindent
\#define a E2F1 < 2\\

\noindent
\#property G (a)\\
}

\section{Spr\'ava}
\label{sec:prop1report}
Obsah s\'uboru {\tt tcbb1.prop1.bio.report}:\\

{\tt\noindent
File:examples/tcbb2010/tcbb1.bio.prop1.bio\\
Algorithm:distr\_map -S -r -t\\
Problem:LTL MC\\
Nodes:1\\
Time:sum:1858.759542\\
Time:avg:1858.759542\\
Time:min:1858.759542\\
Time:max:1858.759542\\
Time:values:1858.759542\\
VMSize:sum:95.984375\\
VMSize:avg:95.984375\\
VMSize:min:95.984375\\
VMSize:max:95.984375\\
VMSize:values:95.984375\\
MsgSent:sum:53\\
MsgSent:avg:53\\
MsgSent:min:53\\
MsgSent:max:53\\
MsgSent:values:53\\
MsgSentUser:sum:0\\
MsgSentUser:avg:0\\
MsgSentUser:min:0\\
MsgSentUser:max:0\\
MsgSentUser:values:0\\
StatesStored:sum:309\\
StatesStored:avg:309\\
StatesStored:min:309\\
StatesStored:max:309\\
StatesStored:values:309\\
SuccsCalls:sum:489\\
SuccsCalls:avg:489\\
SuccsCalls:min:489\\
SuccsCalls:max:489\\
SuccsCalls:values:489\\
CrossTrans:sum:0\\
CrossTrans:avg:0\\
CrossTrans:min:0\\
CrossTrans:max:0\\
CrossTrans:values:0\\
InitTime:sum:406.196788\\
InitTime:avg:406.196788\\
InitTime:min:406.196788\\
InitTime:max:406.196788\\
InitTime:values:406.196788\\
States:sum:309\\
States:avg:309\\
States:min:309\\
States:max:309\\
States:values:309\\
Trans:sum:821\\
Trans:avg:821\\
Trans:min:821\\
Trans:max:821\\
Trans:values:821\\
CEGenerated:Yes\\
IsValid:No\\
ReporterCreated:Sun May 25 01:59:12 2014\\
Workstations:demon-1215B\\
}

\section{\v Cas\v t v\'ystupu}
\label{sec:prop1output}
Obsah s\'uboru {\tt tcbb1.prop1.bio.output}:\\

{\tt\noindent
0: Computation init:  406.197 s\\
0: iteration nr. 1: shrinkA.size: 0\\
0: iteration nr. 2: shrinkA.size: 11\\
======================\\
Accepting cycle found!\\
======================\\
 0: state size:		24\\
 0: appendix size:	56\\
 0: states generated:	309\\
 0: hashtable size:	65536\\
 0: get\_succs called:	489\\
 0: trans. relaxed:	1146\\
 0: all memory used:	95.9844 MB\\
 0: Computation done:	1858.76 s\\
 0: --------------------\\
 0: Accepting cycle:	YES\\
 0: Number of iterations:	2\\
}

\section{Protipr\'iklad}
\label{sec:prop1trail}
Prv\'y s\'tlpec vyjadruje koncentr\'aciu transkrip\v cn\'eho faktora $E2F1$ a druh\'y koncentr\'aciu n\'adorov\'eho supresora $pRB$. V z\'atvork\'ach s\'u 
udan\'e \v c\'isla stavov. Tie v\v sak u\v z\'ivate\v la zauj\'ima\v t nemusia.\\

\noindent
Obsah s\'uboru {\tt tcbb1.prop1.bio.trail}:\\

{\tt\noindent
pre-initial\\
0.607071(1),0.516344(1)-PP:0\\
1(2),0.516344(1)-PP:0\\
2(3),0.516344(1)-PP:0\\
2.1014(4),0.516344(1)-PP:0\\
3(5),0.516344(1)-PP:0\\
4(6),0.516344(1)-PP:0\\
5(7),0.516344(1)-PP:0\\
6(8),0.516344(1)-PP:0\\
6.86458(9),0.516344(1)-PP:0\\
7(10),0.516344(1)-PP:0\\
8(11),0.516344(1)-PP:0\\
10(12),0.516344(1)-PP:0\\
16.0173(13),0.516344(1)-PP:0\\
16.0173(13),1(2)-PP:0\\
16.0173(13),1.62108(3)-PP:0\\
16.0173(13),2(4)-PP:1\\
16.0173(13),4(5)-PP:1\\
16.0173(13),5.23549(6)-PP:1\\
16.0173(13),6(7)-PP:1\\
16.0173(13),8(8)-PP:1\\
16.0173(13),9.42628(9)-PP:1\\
16.0173(13),10(10)-PP:1\\
16.0173(13),12(11)-PP:1\\
================\\
16.0173(13),15(12)-PP:1\\
}


\chapter{Vlastnos\v t \v c. 2}
\label{sec:caseProp2File}
Pre \'uplnos\v t treba doda\v t, \v ze druh\'a vlastnos\v t si vy\v zaduje zmenu s\'uboru s~modelom. Treba prep\'isa\v t na riadku za\v c\'inaj\'ucom 
{\tt INIT:} hodnoty pre {E2F1} tak, aby men\v sia z nich bola v\"a\v c\v sia ako 2.\\

\noindent
Obsah s\'uboru {\tt prop2.ltl}:\\

{\tt
\noindent
\#define b E2F1 >= 2\\

\noindent
\#property G (b)\\
}

\section{Spr\'ava}
\label{sec:prop2report}
Obsah s\'uboru {\tt tcbb1.prop2.bio.report}:\\

{\tt\noindent
File:examples/tcbb2010/tcbb1.bio.prop2.bio\\
Algorithm:distr\_map -S -r -t\\
Problem:LTL MC\\
Nodes:1\\
Time:sum:585.322444\\
Time:avg:585.322444\\
Time:min:585.322444\\
Time:max:585.322444\\
Time:values:585.322444\\
VMSize:sum:95.542969\\
VMSize:avg:95.542969\\
VMSize:min:95.542969\\
VMSize:max:95.542969\\
VMSize:values:95.542969\\
MsgSent:sum:6\\
MsgSent:avg:6\\
MsgSent:min:6\\
MsgSent:max:6\\
MsgSent:values:6\\
MsgSentUser:sum:0\\
MsgSentUser:avg:0\\
MsgSentUser:min:0\\
MsgSentUser:max:0\\
MsgSentUser:values:0\\
StatesStored:sum:113\\
StatesStored:avg:113\\
StatesStored:min:113\\
StatesStored:max:113\\
StatesStored:values:113\\
SuccsCalls:sum:113\\
SuccsCalls:avg:113\\
SuccsCalls:min:113\\
SuccsCalls:max:113\\
SuccsCalls:values:113\\
CrossTrans:sum:0\\
CrossTrans:avg:0\\
CrossTrans:min:0\\
CrossTrans:max:0\\
CrossTrans:values:0\\
InitTime:sum:378.099570\\
InitTime:avg:378.099570\\
InitTime:min:378.099570\\
InitTime:max:378.099570\\
InitTime:values:378.099570\\
States:sum:113\\
States:avg:113\\
States:min:113\\
States:max:113\\
States:values:113\\
Trans:sum:208\\
Trans:avg:208\\
Trans:min:208\\
Trans:max:208\\
Trans:values:208\\
CEGenerated:No\\
IsValid:Yes\\
ReporterCreated:Sun May 25 02:57:19 2014\\
Workstations:demon-1215B\\
}

\section{\v Cas\v t v\'ystupu}
\label{sec:prop2output}
Obsah s\'uboru {\tt tcbb1.prop2.bio.output}:\\

{\tt\noindent 
0: Computation init:  390.049 s\\
0: iteration nr. 1: shrinkA.size: 0\\
 0: state size:		24\\
 0: appendix size:	56\\
 0: states generated:	113\\
 0: hashtable size:	65536\\
 0: get\_succs called:	113\\
 0: trans. relaxed:	208\\
 0: all memory used:	95.543 MB\\
 0: Computation done:	595.286 s\\
 0: --------------------\\
 0: Accepting cycle:	NO\\
 0: Number of iterations:	1\\
}

\chapter{Vlastnos\v t \v c. 3}
\label{sec:caseProp3File}
Obsah s\'uboru {\tt prop3.ltl}:\\

{\tt
\noindent
\#define a E2F1 < 2\\
\#define b E2F1 >= 2\\

\noindent
\#property ((a) -> F G(b))\\

}

\section{Spr\'ava}
\label{sec:prop3report}
Obsah s\'uboru {\tt tcbb1.prop3.bio.report}:\\

{\tt\noindent
File:examples/tcbb2010/tcbb1.bio.prop1.bio\\
Algorithm:distr\_map -S -r -t\\
Problem:LTL MC\\
Nodes:1\\
Time:sum:1557.317334\\
Time:avg:1557.317334\\
Time:min:1557.317334\\
Time:max:1557.317334\\
Time:values:1557.317334\\
VMSize:sum:95.527344\\
VMSize:avg:95.527344\\
VMSize:min:95.527344\\
VMSize:max:95.527344\\
VMSize:values:95.527344\\
MsgSent:sum:21\\
MsgSent:avg:21\\
MsgSent:min:21\\
MsgSent:max:21\\
MsgSent:values:21\\
MsgSentUser:sum:0\\
MsgSentUser:avg:0\\
MsgSentUser:min:0\\
MsgSentUser:max:0\\
MsgSentUser:values:0\\
StatesStored:sum:185\\
StatesStored:avg:185\\
StatesStored:min:185\\
StatesStored:max:185\\
StatesStored:values:185\\
SuccsCalls:sum:633\\
SuccsCalls:avg:633\\
SuccsCalls:min:633\\
SuccsCalls:max:633\\
SuccsCalls:values:633\\
CrossTrans:sum:0\\
CrossTrans:avg:0\\
CrossTrans:min:0\\
CrossTrans:max:0\\
CrossTrans:values:0\\
InitTime:sum:377.244623\\
InitTime:avg:377.244623\\
InitTime:min:377.244623\\
InitTime:max:377.244623\\
InitTime:values:377.244623\\
States:sum:185\\
States:avg:185\\
States:min:185\\
States:max:185\\
States:values:185\\
Trans:sum:427\\
Trans:avg:427\\
Trans:min:427\\
Trans:max:427\\
Trans:values:427\\
CEGenerated:No\\
IsValid:Yes\\
ReporterCreated:Sun May 25 03:48:27 2014\\
Workstations:demon-1215B\\
}


\section{\v Cas\v t v\'ystupu}
\label{sec:prop3output}
Obsah s\'uboru {\tt tcbb1.prop3.bio.output}:\\

{\tt\noindent 
0: Computation init:  377.245 s\\
0: iteration nr. 1: shrinkA.size: 0\\
0: iteration nr. 2: shrinkA.size: 8\\
0: iteration nr. 3: shrinkA.size: 8\\
0: iteration nr. 4: shrinkA.size: 6\\
0: iteration nr. 5: shrinkA.size: 4\\
0: iteration nr. 6: shrinkA.size: 1\\
 0: state size:		24\\
 0: appendix size:	56\\
 0: states generated:	185\\
 0: hashtable size:	65536\\
 0: get\_succs called:	633\\
 0: trans. relaxed:	1392\\
 0: all memory used:	95.5273 MB\\
 0: Computation done:	1557.32 s\\
 0: --------------------\\
 0: Accepting cycle:	NO\\
 0: Number of iterations:	6\\
}

\chapter{Vlastnos\v t \v c. 4}
\label{sec:caseProp4File}
Obsah s\'uboru {\tt prop4.ltl}:\\

{\tt
\noindent
\#define a E2F1 > 8\\

\noindent
\#property FG (a)\\

}

\section{Spr\'ava}
\label{sec:prop4report}
Obsah s\'uboru {\tt tcbb1.prop4.bio.report}:\\

{\tt\noindent
File:examples/tcbb2010/tcbb1.bio.prop1.bio\\
Algorithm:distr\_map -S -r -t\\
Problem:LTL MC\\
Nodes:1\\
Time:sum:2559.146457\\
Time:avg:2559.146457\\
Time:min:2559.146457\\
Time:max:2559.146457\\
Time:values:2559.146457\\
VMSize:sum:95.527344\\
VMSize:avg:95.527344\\
VMSize:min:95.527344\\
VMSize:max:95.527344\\
VMSize:values:95.527344\\
MsgSent:sum:27\\
MsgSent:avg:27\\
MsgSent:min:27\\
MsgSent:max:27\\
MsgSent:values:27\\
MsgSentUser:sum:0\\
MsgSentUser:avg:0\\
MsgSentUser:min:0\\
MsgSentUser:max:0\\
MsgSentUser:values:0\\
StatesStored:sum:238\\
StatesStored:avg:238\\
StatesStored:min:238\\
StatesStored:max:238\\
StatesStored:values:238\\
SuccsCalls:sum:994\\
SuccsCalls:avg:994\\
SuccsCalls:min:994\\
SuccsCalls:max:994\\
SuccsCalls:values:994\\
CrossTrans:sum:0\\
CrossTrans:avg:0\\
CrossTrans:min:0\\
CrossTrans:max:0\\
CrossTrans:values:0\\
InitTime:sum:473.229497\\
InitTime:avg:473.229497\\
InitTime:min:473.229497\\
InitTime:max:473.229497\\
InitTime:values:473.229497\\
States:sum:238\\
States:avg:238\\
States:min:238\\
States:max:238\\
States:values:238\\
Trans:sum:743\\
Trans:avg:743\\
Trans:min:743\\
Trans:max:743\\
Trans:values:743\\
CEGenerated:No\\
IsValid:Yes\\
ReporterCreated:Fri May 23 14:19:57 2014\\
Workstations:demon-1215B\\
}


\section{\v Cas\v t v\'ystupu}
\label{sec:prop4output}
Obsah s\'uboru {\tt tcbb1.prop4.bio.output}:\\

{\tt\noindent 
0: Computation init:  473.23 s\\
0: iteration nr. 1: shrinkA.size: 0\\
0: iteration nr. 2: shrinkA.size: 12\\
0: iteration nr. 3: shrinkA.size: 25\\
0: iteration nr. 4: shrinkA.size: 20\\
0: iteration nr. 5: shrinkA.size: 17\\
0: iteration nr. 6: shrinkA.size: 7\\
0: iteration nr. 7: shrinkA.size: 1\\
0: iteration nr. 8: shrinkA.size: 1\\
 0: state size:		24\\
 0: appendix size:	56\\
 0: states generated:	238\\
 0: hashtable size:	65536\\
 0: get\_succs called:	994\\
 0: trans. relaxed:	2998\\
 0: all memory used:	95.5273 MB\\
 0: Computation done:	2559.15 s\\
 0: --------------------\\
 0: Accepting cycle:	NO\\
 0: Number of iterations:	8\\
}

\end{document}