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. 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).

1. Každý uzel s více než jednou výstupní hranou je zároveň výhybka.
2. Časově variabilní prvky v nádraží jsou:
   1. pohybující se vlaky,
   2. na vstupních uzlech řízená návěstidla a
   3. výhybky.
3. V daném časovém okamžiku je každý vlak právě v jednom uzlu.
4. Vlaky se pohybují pouze ve směru orientace hran grafu (tj. nemohou couvat).
5. 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”).
6. 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.
7. 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.
8. 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.
9. 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).

V nádraží rozlišujeme tyto kritické stavy:

1. Vlak stojí v uzlu (který je zároveň výhybkou, viz výše), a dojde k přepnutí výhybky.
2. Dva nebo více vlaků přijede do stejného uzlu.
3. Vstupní návěstidlo zůstane trvale uzavřené.

Navrhněte program, který:

1. pro zadané nádraží navrhne řídící systém a zformalizuje podle uvedeného zadání;
2. 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.

Graf nádraží bude zadáván v následujícím formátu:

digraph moje_nadrazi {
  vjezd1 -> uzel1;
  ...
  uzel1 -> vyjezd1;
  uzel1 -> vyjezd2;
}

digraph nadrazi {
  in -> v;
  v -> out1;
  v -> out2;
}

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í:

1. Formalizace nádraží:
   1. 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).
   2. 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.
2. Zformalizovat návrh řídícího systému stejným způsobem jako v bodě 1.
3. Ukázat, že je výsledná formalizace nádraží + jeho řízení bezesporná.
4. Dokázat, že nikdy nenastane kritický stav.
5. 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 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.

1. Výstup programu budou okomentované soubory ve formátu TPTP, spolu s výsledkem zpracování zvoleným dokazovačem (resp. hledačem modelů).
2. Používejte maximálně TPTP direktivu include, aby byly TPTP výstupy čitelné a neobsahovaly duplicity.
3. Řešení musí být spustitelné v počítačové laboratoři bez instalace dodatečného SW.

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ží:

1. Formalizace nádraží:
   1. 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”.
   2. 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.
2. Zformalizovat návrh řídícího systému stejným způsobem jako v bodě 1.
3. Dokázat (formou vhodných dotazů v UPPALLu), že nikdy nenastane kritický stav.
4. 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.

1. 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í.
2. Ř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.