CourseWare Wiki
Search
Log In
old
courses
a4m33au
semestralni_prace
Warning
This page is located in archive.
Differences
This shows you the differences between two versions of the page.
View differences:
Side by Side
Inline
Go
Link to this comparison view
Both sides previous revision
Previous revision
2014/04/01 21:15 jakubja5 [Technické poznámky]
2014/04/01 21:14 jakubja5 [Technické poznámky]
2014/04/01 21:14 jakubja5 [Varianta pomocí časových automatů]
2014/04/01 21:14 jakubja5 [Varianta automatické dokazování]
2014/03/19 11:08 jakubja5
2014/03/19 11:07 jakubja5
2013/10/04 13:02 external edit
2013/06/25 19:56 pudlapet
2013/05/21 17:08 pudlapet
2012/08/02 08:36 pudlapet
2012/08/01 09:46 pudlapet
2012/05/18 08:23 vyskoji1
2012/05/03 09:13 vyskoji1
2012/05/03 09:11 vyskoji1
2012/05/03 09:10 vyskoji1
2012/05/03 09:10 vyskoji1
2012/05/03 09:09 vyskoji1
2012/05/03 09:09 vyskoji1
2012/03/01 12:03 pudlapet
2012/03/01 11:59 pudlapet
2012/02/26 13:11 pudlapet
2011/06/21 09:26 pudlapet Caste chyby - chybejici zaver
2011/06/21 09:20 pudlapet
2011/06/21 09:18 pudlapet Caste chyby
2011/06/21 09:12 pudlapet Caste chyby
2011/05/23 13:29 pudlapet
2011/05/23 13:28 pudlapet
2011/05/23 13:03 pudlapet jazykova a stylisticka uprava
2011/05/21 20:21 pudlapet
2011/05/21 19:54 pudlapet
2011/05/21 19:48 pudlapet
Go
Next revision
Previous revision
2014/04/01 21:15 jakubja5 [Technické poznámky]
2014/04/01 21:14 jakubja5 [Technické poznámky]
2014/04/01 21:14 jakubja5 [Varianta pomocí časových automatů]
2014/04/01 21:14 jakubja5 [Varianta automatické dokazování]
2014/03/19 11:08 jakubja5
2014/03/19 11:07 jakubja5
2013/10/04 13:02 external edit
2013/06/25 19:56 pudlapet
2013/05/21 17:08 pudlapet
2012/08/02 08:36 pudlapet
2012/08/01 09:46 pudlapet
2012/05/18 08:23 vyskoji1
2012/05/03 09:13 vyskoji1
2012/05/03 09:11 vyskoji1
2012/05/03 09:10 vyskoji1
2012/05/03 09:10 vyskoji1
2012/05/03 09:09 vyskoji1
2012/05/03 09:09 vyskoji1
2012/03/01 12:03 pudlapet
2012/03/01 11:59 pudlapet
2012/02/26 13:11 pudlapet
2011/06/21 09:26 pudlapet Caste chyby - chybejici zaver
2011/06/21 09:20 pudlapet
2011/06/21 09:18 pudlapet Caste chyby
2011/06/21 09:12 pudlapet Caste chyby
2011/05/23 13:29 pudlapet
2011/05/23 13:28 pudlapet
2011/05/23 13:03 pudlapet jazykova a stylisticka uprava
2011/05/21 20:21 pudlapet
2011/05/21 19:54 pudlapet
2011/05/21 19:48 pudlapet
2011/05/21 18:34 pudlapet Doplneni - kolize
2011/05/19 14:43 vyskoji1
2011/05/19 14:35 vyskoji1
2011/05/14 19:51 pudlapet
2011/05/14 19:48 pudlapet Poznamka ke vztahum mezi navestidly.
2011/05/14 19:41 pudlapet Zavislosti mezi navestidly a vyhybkami
2011/05/08 13:23 pudlapet popis TXT souboru
2011/05/04 08:18 pudlapet
2011/05/03 13:09 pudlapet
2011/04/16 10:40 pudlapet doplneni - vst/vys. uzly, delka vlaku
2011/04/03 21:11 pudlapet created
Go
courses:a4m33au:semestralni_prace [2014/03/19 11:07]
jakubja5
courses:a4m33au:semestralni_prace [2014/04/01 21:15]
jakubja5
[Technické poznámky]
Line 3:
Line 3:
Shrnuti: Navrhnete ridici system nadrazi, formalizujte ho a dokazte jeho bezpecnost.
Shrnuti: Navrhnete ridici system nadrazi, formalizujte ho a dokazte jeho bezpecnost.
-
Nádraží je souvislý orientovaný graf, vstupní formát viz [[#Datové_formáty|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á
zadaný
unikátní název (začínající malým písmenem).
+
Nádraží je souvislý orientovaný graf, vstupní formát viz [[#Datové_formáty|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).
===== Vlastnosti nádraží =====
===== Vlastnosti nádraží =====
Line 64:
Line 64:
- Ukázat, že je výsledná formalizace nádraží + jeho řízení bezesporná.
- Ukázat, že je výsledná formalizace nádraží + jeho řízení bezesporná.
- Dokázat, že nikdy nenastane kritický stav.
- 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 {{ :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// směřující do //out2//, že se návěstidlo v //in// v čase //t+1// otevře.
+
- 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 {{ :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// směřující do //out2//, že se návěstidlo v //in// v čase //t+1// otevře.
==== Technické poznámky ====
==== 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ů).
- 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 [[http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#include|include]], aby byly TPTP výstupy čitelné a neobsahovaly duplicity.
- Používejte maximálně TPTP direktivu [[http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#include|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.
+
- Řešení musí být spustitelné v počítačové laboratoři bez instalace dodatečného SW
(až na dokazovač či hledač modelů). V opačném případě budete muset svoje řešení předvést na vlastním počítači
.
===== Varianta pomocí časových automatů =====
===== Varianta pomocí časových automatů =====
Line 80:
Line 80:
- Zformalizovat návrh řídícího systému stejným způsobem jako v bodě 1.
- 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.
- 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.
+
- 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 {{ :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 ====
==== Technické poznámky ====
courses/a4m33au/semestralni_prace.txt
· Last modified: 2014/04/01 21:15 by
jakubja5