== Otázky ==
[http://dsrg.mff.cuni.cz/~ceres/adm/objektove-orientovane-a-komponentove-systemy.php Podrobnější znění otázek] lze nalézt na [http://dsrg.mff.cuni.cz/~ceres/ webu Petra Tůmy]. Píše se tam, že uvedené znění "by mělo vejít v platnost ve školním roce 2005/2006". To se opravdu stalo, tj. otázky přesně odpovídají.
Níže je seznam užitečných materiálů k jednotlivým otázkám. Některé odkazy vedou na materiály na [http://dsrg.mff.cuni.cz/teaching/ocs/ webu předětu Objektově orientované systémy], které jsou zaheslované. O heslo si lze napsat vyučujícím.
Pro přehlednost jsou názvy otázek v nadpisech uvedeny stručně, tj. bez podrobností v závorkách.
=== Třídy a objekty ===
* Wikipedia: [[wen:Class_(computer_science)|Class]], [[wen:Interface_(computer_science)|Interface]], [[wen:Object_(computer_science)|Object]], [[wen:Method_(computer_science)|Method]], [[wen:Abstract type|Abstract type]], [[wen:Information hiding|Information hiding]], [[wen:Inheritance_(computer_science)|Inheritance]], [[wen:Type polymorphism|Type polymorphism]]
* Martín Abadi, Luca Cardelli: [http://lucacardelli.name/TheoryOfObjects.html A Theory of Objects] – [http://dsrg.mff.cuni.cz/teaching/ocs/documents/cardelli-chapter-1n2.pdf 1. a 2. kapitola] (PDF)
* Slajdy z OCS:
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/01/ocs01.pdf Course information and intro to CORBA] (PDF)
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/04/lecture4-1.pdf Object-orientation, Role of Inheritance, Class-based Languages] (PDF)
* [http://www.phpcompiler.org/articles/virtualinheritance.html Virtual Inheritance] s obrazkama
=== Prototypy a klony ===
* Wikipedia: [[wen:Prototype-based programming|Prototype-based programming]], [[wen:Mixin|Mixin]], [[wen:Trait (abstract type)|Trait]], [[wen:Trait class|Trait class]], [[wen:Self (programming language)|Self]]
* [http://research.sun.com/self/papers/selfPower.ps.gz Popis jayzka Self] (.ps.gz) – popisuje i rozdíly mezi class-based a prototype-based jazyky obecně
* [http://www.iam.unibe.ch/~scg/Archive/Papers/Scha03aTraits.pdf Traits: Composable Units of Behavior] (PDF) – vysvětlení pojmu ''trait'' a porovnání s mixins a jednoduchou/mnohonásobou dědičností
* [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.56.4713&rep=rep1&type=pdf Classes vs. Prototypes: Some Philosophical and Historical Observations] (PDF) – obsahuje především popis problémů s class-based jazyky spíše z filozofického pohledu (při nedostatku času klidně přeskočte)
* Martín Abadi, Luca Cardelli: [http://lucacardelli.name/TheoryOfObjects.html A Theory of Objects] – [http://dsrg.mff.cuni.cz/teaching/ocs/documents/cardelli-chapter4.pdf 4. kapitola] (PDF)
* Slajdy z OCS: [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/09/ocs09.pdf Object-based languages] (PDF)
* [http://www.javascriptkit.com/javatutors/oopjs.shtml Objekty v JavaScriptu]
==== Výpisky ====
Programování založené na prototypech je styl OOP, kde nejsou třídy a chování objektů je definováno pomocí klonování a upravování existujících objektů. Nový objekt je označován jako '''klon''', předloha jako '''prototyp'''. Motivací je mimo jiné to, že je problém navrhnout optimální (i do budoucna) hierarchii tříd v klasickém class-based přístupu.
===== Pojmy =====
* '''Method slot''' – v Selfu jsou objekty kolekcemi slotů. Slot může obsahovat buď proměnnou (''field'') nebo metodu. Pokud je to proměnná, tak "se tváří" jako přístupová metoda, která může proměnnou číst (<code>myPerson name</code>) nebo zapisovat (<code>myPerson name: 'Janek'</code>).
* '''Parent slot''' – je slot který ukazuje na rodičovský objekt, což umožňuje ''delegovat'' neznámé zprávy (neodpovídající žádnému z lokálních slotů) na takto označený rodičovský objekt (např. to může simulovat dědičnost či interfacing).
* '''Trait''' – parametrizovaná sada metod, která slouží jako základní stavební blok pro definování chování tříd ([http://www.iam.unibe.ch/~scg/Research/Traits/]). V Selfu jsou to objekty, které se hodí strkat do parent slotů.
* '''Mixin''' – souvisí s postupem, kdy je objekt "smíchán" z více jiných objektů (či tříd) tak, že je podtypem každého z nich (např. pomocí vícenásobné dědičnosti v klasickém class-based OOP, nebo pomocí parent slots v Selfu). Zdroje se různí v tom, zda mixin je výsledek, nebo "ingredience".
=== Dědičnost a subtyping ===
* Martín Abadi, Luca Cardelli: [http://lucacardelli.name/TheoryOfObjects.html A Theory of Objects] – [http://d3s.mff.cuni.cz/teaching/object_component_systems/files/documents/cardelli-chapter-1n2.pdf 1. a 2. kapitola] (PDF), [http://d3s.mff.cuni.cz/teaching/object_component_systems/files/documents/cardelli-chapter3.pdf 3. kapitola] (PDF)
* Slajdy z OCS:
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/04/lecture4-1.pdf Object-orientation, Role of Inheritance, Class-based Languages] (PDF)
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/05/lecture5.pdf Object-orientation Benefits, the Role of Inheritance] (PDF)
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/10/ocs10.pdf Inheritance related problems and Meta-classes Inheritance related problems and Meta-classes] (PDF)
=== Objekty v distribuovaném prostředí ===
* Wikipedia: [[wen:CORBA|CORBA]], [[wen:Java_remote_method_invocation|RMI]]
* [http://dsrg.mff.cuni.cz/~ceres/sch/mwy/notes.php Poznámky k Middleware]: [http://dsrg.mff.cuni.cz/~ceres/sch/mwy/text/ch06s14.php 6.14 CORBA], [http://dsrg.mff.cuni.cz/~ceres/sch/mwy/text/ch06s09.php 6.9 RMI]
* [http://www.ciaranmchale.com/corba-explained-simply/index.html CORBA explained simply]
* [http://d3s.mff.cuni.cz/teaching/object_component_systems/ Slajdy z OCS]:
** [http://d3s.mff.cuni.cz/teaching/object_component_systems/files/lectures/ocs01-02.pdf Course information and intro to CORBA] (PDF)
** [http://d3s.mff.cuni.cz/teaching/object_component_systems/files/examples/hello-world.zip CORBA hello example] (ZIP)
* [http://blog.firetree.net/2005/05/24/corba-object-lifecycle/ Corba Object Lifecycle]
==== Výpisky ====
'''CORBA''' (Common Object Request Broker Architecture)
* IDL připomíná C++, typy:
** interger, FP, character (char + wchar), boolean, special types (octet, any)
** structures, unions, enums, arrays, sequences, strings, fixed point types, exceptions, interfaces, value types (předán hodnotou a přistupován lokálně)
* mapování do jazyků
** v C++ se řeší problém s velikostí pomocí typedefů, správu paměti řetězců pomocí tříd s alokátory,...
** v Javě se řeší problém s "direction" (typeinfo, serializace, ?) pomocí Holder classes, velikost pomocí data conversion exception
** interfaces: type casting zavedením narrow v obou jazycích, v C++ memory management pomocí var classes a reference countingu
* [portable] object adapter – configuration, policies,...
* síťový protokol – GIOP definuje Common Data Representation (CDR), Message Formats a Transport Assumptions; IIOP je GIOP over TCP/IP
'''RMI''' (Remote Method Invocation)
* specifikace rozhraní v Javě, použití standardní serializace
* vzdálený objekt musí implementovat interface Remote, metody hážou RemoteException
* implementační objekt dědí nepřímo od RemoteObject (UnicastRemoteObject – export/unexport, nebo Activatable – perzistentní objekty)
* life cycle – lokálně garbage collection, vzdáleně reference counting + keepalive (leasing)
* existuje RMI-IIOP pro interoperabilitu s CORBA
=== Replikace a mobilita v distribuovaném prostředí ===
* Wikipedia: [[wen:Replication (computer science)|Replication]]
* [http://www.springerlink.com/content/hh255emk67jln8qe/ A Fault-Tolerant Mobile Agent Model in Replicated Secure Services] – část Introduction
* [http://ulita.ms.mff.cuni.cz/pub/predn/PDS/PDS.ppt Slajdy z Principů distribuovaných systémů z PDS] – Code Migration
* Tanenbaum, Steen: Distributed Systems, Principles and Paradigms – kapitola 3.4 (Code Migration), kapitola 6.5 (Consistency Protocols)
==== Výpisky ====
Replikace je klíčová technika distribuovaných systémů. Mohou být replikována data, nebo celé výpočty (data i program). Při replikaci pouhých dat jsou výsledné procesy pasivní (vyřizují jen read requesty) a dodatečně aplikují updaty. Při replikaci výpočtů je obvykle motivací dosažení fault-tolerance.
Problémem je např. nutnost vynutit pořadí přicházejících zpráv, pokud chceme, aby si všechny replicas udržovaly identický stav (viz např. [[wen:Atomic broadcast|Atomic broadcast]]).
Mobilita se týká mobilních agentů. Mobilní agent je autonomní program, který může migrovat mezi hostiteli v heterogení síti (včetně zachování aktuálního stavu [výpočtů]), kdykoli a kamkoli "se mu zachce". To se hodí pro distribuované "výpočty", výhodou je robustnost, kterou přináší autonomie (~absence centrálního řízení výpočtu). Může to také redukovat latenci a bandwith například tím, že celý program dočasně "přeskočí" ze serveru na klienta, čímž eliminuje častou komunikaci mezi klientem a serverem. Problémy konceptu jsou mimo jiné: ''agent fault tolerance'', ''agent security'', a ''inter-agent communication and synchronization''.
===== Pojmy: =====
* '''Replica''' – jedna z instancí [replikovaného] výpočtu (agenta)
* '''Active replication''' – stejný požadavek zpracovávají všechny replicas
* '''Passive replication''' – požadavek zpracovává jen jedna replica a výsledek je přenesen do ostatních
=== Vyhledávání prostředků ===
* [http://www.ciaranmchale.com/corba-explained-simply/the-naming-service.html CORBA explained simply – Chapter 4 (The Naming Service)]
* [http://www.ciaranmchale.com/corba-explained-simply/trading-service.html CORBA explained simply – Chapter 20 (Trading Service)]
* Slajdy z OCS:
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/03/lecture3.pdf Distributed objects – POA details, naming and event services] (PDF)
*** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/03/H5morePOA.pdf H5morePOA.pdf] (PDF)
*** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/03/H6Events.pdf H6Events.pdf] (PDF)
* [http://en.wikipedia.org/wiki/Java_Naming_and_Directory_Interface wen: JNDI]
* [http://en.wikipedia.org/wiki/UDDI wen:UDDI]
==== Výpisky ====
CORBA umí uložit referenci do stringu (a uložit do souboru) a z něj vytvořit proxy (<code>object_to_string()</code> a <code>string_to_object()</code>), vhodné pokud klient a server sdílí file systém.
'''CORBA Naming Service'''
* mapování (human-readable) názvů na IORy
* uloženo hierarchicky, adresáře (= ''naming context''s) jsou taky CORBA objekty (může být uloženo distribuovaně)
* aplikace můžou importovat a exportovat objekty pomocí naming service (musí znát příslušnou cestu, ta obvykle sídlí někde v konfiguráku), např.:
<blockquote><pre>
obj = importObjRef(orb, "name_service#path/in/Naming/Service")
exportObjRef(orb, obj2, "file#/path/to/file.ior")
</pre></blockquote>
* starej interface (importObjRef vyzaduje utility knihovnu):
<blockquote><pre>
NamingContextExt namingServiceExt = NamingContextExtHelper.narrow(orb.resolve_initial_references("NameService"));
obj = namingServiceExt.resolve_str("path/in/Naming/Service");
namingServiceExt.bind(namingServiceExt.to_name("path/in/Naming/Service"), obj);
// nebo
namingServiceExt.bind(new NameComponent[]{new NameComponent("path",""), new NameComponent("in",""), new NameComponent("Naming",""), new NameComponent("Service","")}, obj);
</pre></blockquote>
* naming services jdou propojovat (tzv. federation), pak se k nim pristupuje jako k celku
'''CORBA Trading Service'''
* podobný jako naming service, připomíná zlaté stránky telefonního seznamu
* nabízí služby spolu s referencí (IOR) a popisem, organizované do kategorií (''service offer types'')
* kategorie jsou definovány pomocí rozhraní <code>ServiceTypeRepository</code>
* aplikace exportují reference pomocí rozhraní <code>Register</code>
* rozhraní <code>Lookup</code> definuje operaci <code>query</code>, která umožňuje vyhledat službu podle nějaké podmínky
* podobně jako naming service je možné trading services propojovat
* pro obě služby existují utilitky (cmd-line i GUI) pro administraci, což redukuje kódování
* priklad v Jave:
<blockquote><pre>
Lookup lookup = LookupHelper.narrow(orb.resolve_initial_references("TradingService"));
// register type
PropStruct[] props = new PropStruct[]{new PropStruct("resolution", CORBA.INTEGER, PropertyMode.PROP_NORMAL)};
String[] superTypes = new String[]{new String("OfficeDevice")};
lookup.serviceTypeRepository.add_type("Printer", "IDL:acme.com/Equipment/Printer:1.0", props, superTypes);
// register object
Property[] properties = new Property[]{new Property("resolution", 300};
lookup.register.export(obj, "Printer", properties);
// search for it
Offer[] offers= lookup.query(
"Printer", // type name
"resolution >= 300", // constraint
"resolution", // preferred properties (influences sorting of the results)
...);
obj = offers[0].reference;
</pre></blockquote>
'''JNDI''' (Java Naming and Directory Interface)
API adresářové služby, nabízí:
* mechanismus pro navázání (''bind'') objektu na jméno
* directory lookup iface pro obecné dotazy
* rozhraní pro události, které informují klienta o změně adresářových položek
* Service Provider Interface (SPI) pro napojení jiných adresářových služeb (LDAP, CORBA naming service,...)
* příklad:
<blockquote><pre>
Object reference = myCurrentContext.lookup("com.mydomain.MyBean");
MyBean myBean = (MyBean) PortableRemoteObject.narrow(reference, MyBean.class); // this step is needed for EJB beans
</pre></blockquote>
'''UDDI''' (Universal Description Discovery and Integration)
* markup language zalozeny na XML
* register webovych sluzeb
* rozdelen na:
** white pages - prime kontakty na jednotlive sluzby / businesses
** yellow pages - sluzby jsou radene do kategorii
** green pages - technicke detaily o pristupu k dane sluzbe; jak se pripojit, atd.
* komunikace jde pres SOAP zpravy
=== Garbage collection ===
* Wikipedia: [[wen:Garbage_collection_(computer_science)|Garbage collection]], [[wen:Reference_counting|Reference counting]]
* [http://www.memorymanagement.org/glossary/ The Memory Management Glossary]
==== Výpisky ====
Garbage collection je způsob automatické správy paměti. Garbage Collector (GC) uvolňuje paměť, která již nebude použita.
* vyhody
** zamezeni dangling pointer bugu
** zamezeni double free bugu (2x uvolnena pamet)
** zamezeni leakum (nekterym)
* nevyhody
** overhead
** unpredictable
** stale zustaji logical leaks
** poor locality -> thrashing
* syntactic vs. semantic garbage (~halting problem), dá se pracovat jen se syntactic garbage
* '''reachability tracing'''
** '''mark and sweep''' – naive vs. tri-color (white-gray-black)
** moving vs. non-moving – moving přesouvá platné objekty a zahazuje celou oblast, to zjednodušuje uvolňování, snižuje fragmentaci, atd, ale musí relokovat pointry, pokud jsou v objektech obsaženy (třeba .NET). Také se tomu říká mark and compact.
** '''copying GC''' – je moving GC, který uklízí tak, že postupně kopíruje dosažitelné objetky do nové oblasti (místo obarvování). Může je i v původní paměti dočasně nechat, nebo tam nechat pointer na nová data (tzv. "broken heart") -> inkrementální GC.
** '''concurrent GC''' – běží zároveň s hlavním programem (na druhém procesoru, nebo aspoň v druhém vlákně), vyžaduje zamykání, etc.
** na půl cesty mezi stop-the-world a concurrent přístupy je '''incremental''' GC – ten přerušuje svou práci a dovoluje běh hlavního programu (mutatoru). Ale nesmi ho nechat, aby dostal nekonzistentni data, takže na chvíli povoluje i duplicity.
** '''mutátor''' reprezentuje/simuluje změny, které hlavní program dělá v paměti (tj. přesměrovává ukazatele na jiné dosažitelné objekty). Teoreticky celý program dělíme na dvě poloviny: collector a mutator. Collector zahazuje data a mutator reprezentuje všechna programová vlákna, která mu do toho lezou. Při nejjednodušší implementaci GC stop© běží vždy jen mutator nebo collector. Při increment běhají po částech, při concurrent běží najednou.
** '''finalizer''' je neco jako destruktor, ale spusteno az pri mazani objektu, coz muze bejt za dlouho; resi uvolnovani nepametovych resourcu (soubory)
* '''reference counting'''
** každý objekt má počítadlo referencí, když klesne na nulu, je '''oznacen''' pro uvolneni; je problém s cykly
** vyhody: lepsi pro real-time; snazsi implementace; efektivni pro nepametove zdroje (soubory); nema problem se skoro zaplnenou pameti
** nevyhody: vyzaduje caste updaty pocitadel (pri kazdem create, destroy, zmene reference -> problem s cache a CPU pipeline); problem s cyklickou referenci
** '''deferred increments''' odlozi zmenu counteru u lokalnich promennych na pozdeji - casto se ukaze, ze by byla zbytecna, protoze u lokalnich promennych vznikne a zanikne reference kratce po sobe
** reseni cyklu: zakazat v jazyku; ignorovat; pouzit na cykly tracing collector
** v distribuovaném prostředí je potřeba používat reference counting, nebo nějakou keepalive strategii, tj. reference musí občas objektu sdělit, že má být ještě naživu. Reference counting na distribuovaném prostředí je '''weighted'''. Při kopírování reference se jeji váha dělí na půl mezi originál a kopii a není potřeba zasílat inkrementovat pocitadlo na objektu. Pocitadlo pocita celkovou vahu, ne pocet referenci. Pocitadlo se zmeni jen při smazání reference (ale někdy je zase nutné zvýšit celkovou váhu).
=== Architektura komponentových systémů ===
* Wikipedia:
** [[wen:JavaBean|JavaBean]], [[wen:Enterprise_JavaBean|EJB]] ([[wen:Session_Bean|session bean]], [[wen:Entity_Bean|entity bean]])
** [[wen:Component_Object_Model|COM]], [[wen:Distributed_Component_Object_Model|DCOM]], [[wen:Microsoft_Transaction_Server|MTS]]
** [[wen:Architecture_description_language|ADL]] ([[wen:Wright_(ADL)|Wright]], [[wen:Darwin_(ADL)|Darwin]])
** [[wen:Unified_Modeling_Language|UML]] ([[wen:Class_diagram|class diagram]], [[wen:Sequence_diagram|sequence diagram]], [[wen:Use_case|use case]], [[wen:Use_case_diagram|use case diagram]])
* [http://www.cs.gmu.edu/~white/INFT821/Slides/Wright.ppt Wright ADL] (PPT) – prezentace o Wright
* [http://www.cs.cmu.edu/afs/cs/project/able/www/paper_abstracts/rallen_thesis.htm A Formal Approach to Software Architecture]
* Slajdy z OCS:
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/11/ocs11.pdf Beyond objects: Patterns, Components] (PDF)
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/12/ocs12.pdf SOFA 2 and Fractal component models] (PDF)
** [http://dsrg.mff.cuni.cz/teaching/ocs/lectures/06/ocs06.pdf UML and MOF] (PDF)
==== Výpisky ====
Softwarová komponenta je nezávislý kus softwaru, který se vyznačuje:
* funkcionalitou – provides/requires
* způsobem integrace – nesting (hierarchie)
* způsobem nasazení (deployment/packaging) – adresový prostor, kontejner, .jar soubor
* run-time chováním (run-time monitoring,...)
* způsobem dynamického nahrazování (rekonfigurace architektury, verzování)
Pravidla pro tyto vlastnosti jsou určena ''komponentovým modelem''.
Jde o vyšší úroveň abstrakce, než jsou objekty z OOP. Hlavním cílem je snadná opakovaná použitelnost funkcionality (a v důsledku kódu, který ji poskytuje).
'''JavaBeans'''
* motivace: jednoduchý design GUI
* BeanBox (environment, container, single address space), naming conventions for classes, publisher-subsciber
'''(D)COM'''
* motivace: interoperabilita jazyků, dynamické zjišťování rozhraní
* C++ polymorfizmus
* interface IUnknown (metody QueryInterface, AddRef, Release)
* DCOM – distribuovaný
'''EJB''' (Enterprise JavaBeans)
* motivace: jednoduché object-like komponenty pro snadný přístup do relačních databází
* Bean
** Entity (persistence) – v EJB 3.0 nahrazeno [[wen:Java Persistence API|Java Persistence API]] (persistence, obj.-rel. mapping)
** Session (stateful/stateless) – zajišťují nějakou funkcionalitu pro uživatele
* kontejner poskytuje: Security, Life-cycle, Persistence, Transactions, Remote Access (via RMI)
* EJB 3.0 jsou více lightweight, používají se [[wen: Java annotations|anotace]] (Java 5.0 feature) místo "deployment descriptors"
** inspirace v "konkurečních" projektech Hibernate (persistence a obj.-rel. mapping) a Spring Framework (business logic)
'''CCM'''
* flat model
* implicit connectors (CORBA-based communication)
* provides (facet) / requires (receptacle)
* publisher (event source) / subscriber (event sink)
'''WRIGHT'''
* ADL (architecture description language)
* formálně popisuje architekturu systému (komponenty, konektory,...)
* popisuje chování pomocí CSP-like syntaxe ([[wen:Communicating Sequential Processes|Communicating Sequential Processes]])
* umožňuje definovat a staticky kontrolovat nějaké vlastnosti systému
=== Specifikace chování systémů ===
* [http://dsrg.mff.cuni.cz/~adamek/fm/ Slajdy z předmětu Modely a verifikace chování systémů] – nejsnažší je zběžně je projít všechny (měly by stačit lekce 10 a 11)
* [[wen:Communicating sequential processes|Communicating sequential processes]]
* [http://en.wikipedia.org/wiki/Software_verification Software verification]
* [http://en.wikipedia.org/wiki/Software_testing Software testing]
=== Model checking ===
* [http://dsrg.mff.cuni.cz/~adamek/fm/ Slajdy z předmětu Modely a verifikace chování systémů] – nejsnažší je zběžně je projít všechny (měly by stačit lekce 2 až 5)
'''Kripkeho struktura'''
* AP je množina atomic propositions (logických formulí)
* Kripkeho struktura nad AP je trojice M = (S, R, L), kde
** S je konečná množina stavů
** <math>R \subseteq S \times S</math> je ''transition relation'' taková, že pro <math>\forall s \exist s' : (s, s') \in R</math>
** <math>L : S \rightarrow 2^{AP}</math> je ''labeling function''
* poznámky
** nekonečné cesty
** někdy množina iniciálních stavů S0
** AP ~ Boolean variables
'''CTL''' (Computation Tree Logic)
* A|E + X|G|F|U (next, globally, future, P until Q)
'''LTL''' (Linear Time Logic)
* jen X|G|F|U (implicitně pro všechny cesty)
* vnořování temporálních operátorů: X (X (G p)) = XXG p
'''CTL vs. LTL'''
* AG(EF p) (CTL) nemá formuli v LTL (např. G(F p) není eqvivalentní)
* FG p (LTL) nemá formuli v CTL (např. AF (AG p) není eqivalentní)
* CTL* umí obojí (path vs state formulas)
== Materiály ==
* [http://dsrg.mff.cuni.cz/teaching/ocs/ Web předmětu Objektově orientované systémy] – o heslo k materiálům si lze napsat vyučujícím
* [http://dsrg.mff.cuni.cz/~adamek/fm/ Web předmětu Modely a verifikace chování systémů]
