Differences

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

--- courses:a4m33au:term_en [2014/04/01 21:02]
jakubja5 [Varianta pomocí časových automatů]
+++ courses:a4m33au:term_en [2014/04/01 21:10]
jakubja5 [Technické poznámky]
@@ Line 68: / Line 68: @@
   - Railway station formalization:
     - Formalize in the First Order Logic in the TPTP language the "physical" railway station behavior, that is, how trains go through the railway station based on the state of signaling devices and engine driver decisions. Every time dependent predicate //p// that describe something that we are able to establish has to be described by at most one formula of the shape //p(T+1) <=> φ// where formula //φ// depends only conditions in time //T// or antecedent (this syntactically guaranties correctness of the definition). This covers the state of switches, position of trains, and so on. This does not cover the engine driver will which we do not know (we know only that every train departs at some time).
-    - Show that this formalization is not contradictory with additional conditions which describe that a train departs from a node to another
+    - Prove that this formalization is not contradictory with additional conditions which say that a train moves from one node to another as soon as possible (that is, the engine driver decides to depart immediately).
   - Formalize the railway station control system in the same way as in point 1.
   - Prove that the formalization of the railway station together with the control system is not contradictory.
@@ Line 87: / Line 88: @@
   - Railway station formalization:
+    - Formalize in the UPPALL System the "physical" railway station behavior, that is, how trains go through the railway station based on the state of signaling devices and engine driver decisions.
+    - Show (using suitable UPPALL queries) that this formalization is not contradictory with additional conditions which say that a train moves from one node to another as soon as possible (that is, the engine driver decides to depart immediately).
+  - Formalize the railway station control system in the same way as in point 1.
+  - Prove (using suitable UPPALL queries) that a critical state can not appear.
+  - A railway station must allow a train to enter the railway station as soon as there is free path from its starting entrance node to its departure exit. You need to prove that in the following railway station {{ :courses:a4m33au:semp2012-o1.png?64}} with 2 trains at time //T//, the first at //out1// and the second at //in// both going to exit //out2//, the signaling device at //in// will be opened at time //T+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".
-    - 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 {{ :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.
+==== Technical Notes ====
+  - The output of your program should be in XML format acceptable by the UPPALL system and the output of the UPPALL system which proves required properties.
+  -
-Ú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 {{ :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.