Differences

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

--- courses:a4m33au:term_en [2014/04/01 21:08]
jakubja5 [Timed Automata Variant]
+++ courses:a4m33au:term_en [2014/04/01 21:11]
jakubja5 [Technical Notes]
@@ 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 94: / Line 95: @@
-==== Technické poznámky ====
+==== Technical Notes ====
-  - 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í.
+  - 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.
-  - Ř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.
+  - Your program must be executable in a computer lab without additional SW. Otherwise you will need to present your solution on your computer.