Differences

This shows you the differences between two versions of the page.

--- courses:a4m33au:semestralni_prace [2014/04/01 21:14]
jakubja5 [Varianta automatické dokazování]
+++ courses:a4m33au:semestralni_prace [2014/04/01 21:14]
jakubja5 [Technické poznámky]
@@ Line 69: / Line 69: @@
   - Výstup programu budou //okomentované// soubory ve formátu TPTP, spolu s výsledkem zpracování zvoleným dokazovačem (resp. hledačem modelů).
   - Používejte maximálně TPTP direktivu [[http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#include|include]], aby byly TPTP výstupy čitelné a neobsahovaly duplicity.
-  - Řešení musí být spustitelné v počítačové laboratoři bez instalace dodatečného SW.
+  - Řešení musí být spustitelné v počítačové laboratoři bez instalace dodatečného SW (až na dokazovač či hledač modelů).
 ===== Varianta pomocí časových automatů =====
@@ Line 80: / Line 80: @@
   - Zformalizovat návrh řídícího systému stejným způsobem jako v bodě 1.
   - Dokázat (formou vhodných dotazů v UPPALLu), že nikdy nenastane kritický stav.
-  - Nádraží musí pouštět vlaky hned, jakmile je to možné. Je třeba dokázat pro {{ :courses:a4m33au:semp2012-o1.png?64}} toto nádraží, že budou-li v čase //t// v tomto nádraží 2 vlaky, jeden vlak na //out1// a jeden na //in//, že se návěstidlo v //in// v čase //t+1// otevře.
+  - Nádraží musí pouštět vlaky hned jakmile existuje volná cesta ze vstupního do výstupního uzlu. Je třeba dokázat pro {{ :courses:a4m33au:semp2012-o1.png?64}} toto nádraží, že budou-li v čase //t// v tomto nádraží 2 vlaky, jeden vlak na //out1// a jeden na //in//, že se návěstidlo v //in// v čase //t+1// otevře.
 ==== Technické poznámky ====