====== Automatické Uvažování - Semestrálka - Vlakové nádraží ====== ===== Zadání ===== ==== Shrnuti ==== Navrhnete ridici system nadrazi, formalizujte ho a dokazte jeho bezpecnost. Nádraží je souvislý orientovaný graf, vstupní formát viz [[courses/a4m33au/semestralka_vlakove_nadrazi#datove_formaty|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 a každá hrana mají zadaný 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ý 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. ==== 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: digraph nadrazi { in -> v; v -> out1; v -> out2; } (Poznámka: Vstupní jazyk je podmnožinou formátu 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, 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). - 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 je to možné. Je třeba dokázat pro 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 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 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. ==== 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 je to možné. Je třeba dokázat pro 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. ~~DISCUSSION~~