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 [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 ====