Differences

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

--- courses:a4m33au:semestralni_prace [2014/03/19 11:08]
jakubja5
+++ courses:a4m33au:semestralni_prace [2014/04/01 21:14]
jakubja5 [Varianta automatické dokazování]
@@ Line 64: / Line 64: @@
   - Ukázat, že je výsledná formalizace nádraží + jeho řízení bezesporná.
   - Dokázat, ž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// směřující do //out2//, ž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// směřující do //out2//, že se návěstidlo v //in// v čase //t+1// otevře.
 ==== Technické poznámky ====