====== Semestralni prace - nadrazi ======
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á zadán unikátní název (začínající malým písmenem).
===== Vlastnosti nádraží =====
- Každý uzel s více než jednou výstupní hranou je zároveň výhybka.
- Časově variabilní prvky v nádraží jsou:
- pohybující se vlaky,
- na vstupních uzlech řízená návěstidla a
- výhybky.
- V daném časovém okamžiku je každý vlak právě v jednom uzlu.
- Vlaky se pohybují pouze ve směru orientace hran grafu (tj. nemohou couvat).
- Je-li v uzlu vlak, platí, že vlak někdy do uzlu přijel (nebyl tam od nepaměti) a jednou odjede (ale není určeno, kdy, je to na "rozhodnutí strojvedoucího").
- Na vjezdových uzlech (a pouze tam) jsou návěstidla. Ta blokují odjezd vlaků ze vstupních uzlů: Je-li návěstidlo zavřené, vlak zůstává na vstupním uzlu; je-li otevřené, může (ale nemusí) vyjet. Vlak (strojvedoucí) vždy tato návěstidla respektuje. Každý vjezdový uzel má právě jednu výstupní hranu, není tedy nikdy výhybkou.
- Každý vlak má dán výstupní uzel, do kterého chce dojet. Tento cíl se nemění celou dobu, co vlak projíždí nádražím.
- Nádraží podle tohoto cíle směruje vlak pomocí přepínání výhybek. Řídící systém nádraží může libovolně nastavovat stav výhybek.
- Pokud je vjezdový uzel prázdný, může se v něm kdykoliv objevit nový přijíždějící vlak (i hned po odjezdu předcházejícího).
===== Kritické stavy v nádraží =====
V nádraží rozlišujeme tyto kritické stavy:
- Vlak stojí v uzlu (který je zároveň výhybkou, viz výše), a dojde k přepnutí výhybky.
- Dva nebo více vlaků přijede do stejného uzlu.
- Vstupní návěstidlo zůstane trvale uzavřené.
===== Úkoly =====
Navrhněte program, který:
- pro zadané nádraží navrhne řídící systém a zformalizuje podle uvedeného zadání;
- dokáže, že navržený řídící systém pracuje správně, tj. že se nádraží nemůže dostat do kritického stavu.
Výsledek práce shrňte v (stačí krátké) technické zprávě, kde bude popsán zvolený postup, a zejména podrobně rozebrané dosažené výsledky.
===== Datové formáty =====
Graf nádraží bude zadáván v následujícím formátu:
digraph moje_nadrazi {
vjezd1 -> uzel1;
...
uzel1 -> vyjezd1;
uzel1 -> vyjezd2;
}
Příklad: {{ :courses:a4m33au:semp2012-o1.png?128}}
digraph nadrazi {
in -> v;
v -> out1;
v -> out2;
}
(Poznámka: Vstupní jazyk je podmnožinou formátu [[wikipedia>DOT_language|jazyce DOT]] používaným programem GraphViz.)
===== Varianta automatické dokazování =====
Nádraží je modelováno v diskrétním čase. Čas je lineární, a každý časový okamžik má právě jeden následující a jeden předcházející. V každý časový okamžik si řídící systém nádraží určuje stavy výhybek a návěstidel.
Úkoly, které postupně zpracuje program pro libovolné nádraží pomocí nástrojů pro automatické dokazování:
- Formalizace nádraží:
- Zformalizovat v logice 1. řádu v jazyce TPTP "fyzikální chování" nádraží, tedy jak vlaky projíždějí nádražím na základě návěstidel a "rozhodování strojvedoucích". Každý predikát //p// závislý na čase popisující něco, co dovedeme určit, musí být popsaný nejvýše jednou formulí tvaru //p(T+1) <=> φ//, kde //φ// je formule závislá pouze na okolnostech v čase //T// a dřívějších (tím je syntakticky zaručena korektnost definice). Do toho spadá zejména stav výhybek, zda je v daném uzlu vlak, atd. Nespadá sem především vůle strojvedoucího, kterou neznáme (jen víme, že vždy nakonec s vlakem odjede).
- Ukázat, že tato formalizace není sporná s přidanými podmínkami, že strojvůdce vlaku jede hned, jakmile může, a že do nádraží vjede vlak vždy, jakmile může.
- Zformalizovat návrh řídícího systému stejným způsobem jako v bodě 1.
- 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 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 (až na dokazovač či hledač modelů). V opačném případě budete muset svoje řešení předvést na vlastním počítači.
===== Varianta pomocí časových automatů =====
Nádraží lze modelovat jak v diskrétním, tak ve spojitém čase. V každý časový okamžik si řídící systém nádraží určuje stavy výhybek a návěstidel.
Úkoly, které postupně zpracuje program pro libovolné nádraží:
- Formalizace nádraží:
- Zformalizovat pro systém UPPALL "fyzikální chování" nádraží, tedy jak vlaky projíždějí nádražím na základě návěstidel a "rozhodování strojvedoucích".
- Ukázat (formou vhodných dotazů v UPPALLu), že tato formalizace není sporná s přidanými podmínkami, že strojvůdce vlaku jede hned, jakmile může, a že do nádraží vjede vlak vždy, jakmile může.
- 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 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 ====
- Výstup programu budou soubory ve formátu XML pro zpracovaní systémem UPPALL a UPPALLem zpracované výsledky dotazů dokazující požadované vlastnosti řešení.
- Řešení by mělo být spustitelné v počítačové laboratoři bez instalace dodatečného SW. V opačném případě budete muset svoje řešení předvést na vlastním počítači.