Rozdíly

Zde můžete vidět rozdíly mezi vybranou verzí a aktuální verzí dané stránky.

--- courses:a4m33au:semestralka_vlakove_nadrazi [2012/06/25 10:22]
nardi vytvořeno
+++ courses:a4m33au:semestralka_vlakove_nadrazi [2025/01/03 18:28] (aktuální)
@@ Řádek 1: / Řádek 1: @@
 ====== Automatické Uvažování - Semestrálka - Vlakové nádraží ======
+===== Zadání =====
-~~DISCUSSION~~
+==== 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~~

courses/a4m33au/semestralka_vlakove_nadrazi.1340612570.txt.gz · Poslední úprava: 2025/01/03 18:24 (upraveno mimo DokuWiki)

Nahoru