Differences

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

--- courses:a4m33au:semestralni_prace [2014/03/19 11:07]
jakubja5
+++ courses:a4m33au:semestralni_prace [2014/04/01 21:14]
jakubja5 [Technické poznámky]
@@ Line 3: / Line 3: @@
 Shrnuti: Navrhnete ridici system nadrazi, formalizujte ho a dokazte jeho bezpecnost.
-Nádraží je souvislý orientovaný graf, vstupní formát viz [[#Datové_formáty|datové formáty]]. Uzly, z kterých nevedou šipky, nazveme //výjezdy//, uzly, do kterých nevedou vedou šipky, nazveme //vjezdy//. Omezujeme se na grafy, u kterých z každého vjezdu existuje cesta do každého výjezdu. Každý uzel má zadaný unikátní název (začínající malým písmenem).
+Nádraží je souvislý orientovaný graf, vstupní formát viz [[#Datové_formáty|datové formáty]]. Uzly, z kterých nevedou šipky, nazveme //výjezdy//, uzly, do kterých nevedou vedou šipky, nazveme //vjezdy//. Omezujeme se na grafy, u kterých z každého vjezdu existuje cesta do každého výjezdu. Každý uzel má zadán unikátní název (začínající malým písmenem).
 ===== Vlastnosti nádraží =====
@@ 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 ====
   - 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 ====