FEI archív 2010/2011 > 4. ročník
FŠS - Formálne špecifikácie systémov
jan:
Zhrnutie príspevkov z minulého roka
----------------------------------------------------------------------------------------------------
skuska
----------------------------------------------------------------------------------------------------
21.05.2010, 11:16:22
Otazky cca:
1. uvod FM, sucasnost, priklady, motivacia
2. zivost, RP
3. nakreslit PS pre obedujucich filozofov, s tym ze tam moze dochadzat k deadlocku a neberu sa obe vidlicky naraz....
4. nejake vyratanie pre-podmienok
----------------------------------------------------------------------------------------------------
01.06.2010, 08:15:36
prva skupina :
1) PN - marking, realizacia prechodu, jazyky PN
2) B jazyk, definicia vlatnosti
3) S invariant pre RW problem
4) Vytvorte B specifikaciu vypoctoveho strediska s jednym pocitacom
druha skupina :
1) vektorove aditivne systemy. Vztah VAS a petriho sieti
2) sysntax struktury MASCHINE N(p) a jeho vlastnosti
3) vypocitajte najslabsie prepodmienky
4)pre kapacitno obmedzenu PS najdite jazykovo ekvivalentnu PS bez kapacitneho obmedzenia
- a dokazat jej s- invariant
----------------------------------------------------------------------------------------------------
15.06.2010, 14:48:33
T1: Jazyk „guarded commands“.
T2: Sémantika Machine N(p):štruktúra povinného dôkazu korektnosti špecifikácie stroja Machine N(p).(Proof Obligation for
Machine N(p)
P1: Urcit najslabsie prepodmienky pre nejake vyrazy (; , ||)
P2: Urcit T-invarianty PN.
teoria
1- Mechanizmus ";" dokaz jeho korektnosti, platnosti pre vlastnosti 1-4
2- Kompozicne mechanizmy EXTENDS a INCLUDES
priklady
1- T-invarianty PN (bola siet ako pre readers-writers len torchu upravena)
2- nepamatam presne ale cosi ako:
vytvorit B stroj, kt. ma operacie
- ak xx patri do mnoziny ss (ta ma byt z N) vrati TRUE
- nedeterministicky bud prida xx do ss vrati TRUE alebo neurobi nic vrati FALSE
----------------------------------------------------------------------------------------------------
21.05.2010, 14:19:32 Doplnim, ze priklady na prepodmienky boli tie co boli na cviku,
--- Code: ---[PRE X>0 THEN y=y/xEND](y>1), [CHOICE SS:= SS U{xx} ||| bb:=TRUE OR bb:=FALSE ](xx patri SS)
--- End code ---
----------------------------------------------------------------------------------------------------
----------------------------------------------------------------------------------------------------
na stiahnutie
----------------------------------------------------------------------------------------------------
26.05.2010, 17:06:37 tie otazky nie su kompletne...to su otazky len pre externistov
28.05.2010, 11:23:55 pdf + prednasky + web + rozne vygooglene clanky (dijkstra, murata a pod)
28.05.2010, 12:19:48 http://www.uloz.to/4946538/fss2007.rar
prednasky a cvika z roku 2007...skoro je to rovnake ako toho roku...ako obsahovo je to to iste...len
nieco je tam naviac, kedze oni to mali este ako povinny predmet
----------------------------------------------------------------------------------------------------
28.05.2010, 17:33:06 TOTO JE ZLE ti filozofi co ste mali mat ze po jednom beru vidlicku a moze dochadzat k deadlocku
by mali vyzerat nejak takto: http://img338.imageshack.us/img338/7171/filozofipojednomberulyz.jpg
30.05.2010, 09:47:11 Zadanie bolo, ze musi to byt nedeterministicke a nesmie zobrat dve vidlicky naraz. Teda bud vezme
najprv pravu a potom lavu, alebo naopak Tu je cast riesenia pre 1 filozofa http://i49.tinypic.com/mmy328.jpg
----------------------------------------------------------------------------------------------------
14.06.2010, 15:46:41 taketo nieco asi http://i47.tinypic.com/15f1uyp.jpg
14.06.2010, 19:57:19 este je tam malicky nedostatok.... tam pri p7: este musi ist z t3 do p7 hrana
14.06.2010, 20:23:38 rozdelenie bodov teoria-priklady 25 25 10 10 tusim
----------------------------------------------------------------------------------------------------
11.06.2010, 12:50:32
http://ibn.sk/images/na%20skuske%201.jpg nejde
http://ibn.sk/images/na%20skuske%202.jpg nejde
konkretne toto bolo minule ...
----------------------------------------------------------------------------------------------------
14.06.2010, 15:35:22
X1 = kX2 + X4
X3 = X2 + X4
toto sme si vyjadrili z rovnice Ct.X=0
14.06.2010, 15:38:24
ked si vsimnes tie dve premenne x1 a x3 sa daju vypocitat pomocou x2 a x4..tak si zostavis tabulku:
x1 x2 x3 x4
X1 0 0
X2 0 1
X3 1 0
X4 1 1
a pomocou tych dvoch rovnic dopocitas x1 a x3..potom len skrtnes zavisle riadky a ostanu ti tie dva co si uviedol
14.06.2010, 15:54:18 premenne su dve takze mozu mat pri dvoch moznostiach styri rozne hodnoty a to bud 00 alebo 01 alebo
10 alebo 11
----------------------------------------------------------------------------------------------------
14.06.2010, 20:33:26 vie niketo vypocitat tie prepodmienky ?
--- Code: ---[ANY vv WHERE vv>xx A vv (patri) N THEN xx:=vv END] (xx (patri) ss)
--- End code ---
14.06.2010, 20:54:41
--- Code: ---[@vv.(vv>xx a vv patri N -> xx:=vv)](xx patri ss)
pre vsetky vv: (vv>xx a vv patri N) -> [xx:=vv](xx patri ss)
pre vsetky vv: (vv>xx a vv patri N) -> vv patri ss
--- End code ---
----------------------------------------------------------------------------------------------------
18.06.2010, 12:18:25
B stroj
--- Code: ---MACHINE Stroj()
VARIABLES ss
INVARIANT ss patri N
INITIALISATION ss=prazdna mnozina
OPERATIONS
b <- Test(xx) =
PRE xx patri N
THEN
IF xx patri ss THEN b := TRUE ELSE b:=FALSE END
END
b<- Nedeterm(xx) =
PRE xx patri N
THEN
CHOICE ss := ss zjednotenie {xx} || b:= TRUE OR b:=FALSE END
END
END
--- End code ---
EDIT od kOsTi-ho: k 1. obrazku: pri p7: este musi ist z t3 do p7 hrana
Faust:
ake je heslo do moodlu?
jan:
--- Quote from: Faust on 02.03.2011, 17:20:12 ---ake je heslo do moodlu?
--- End quote ---
jahodka
Faust:
vdaka
jan:
FSS - Štefan Hudák - Rozšírenia Petriho Sietí - habilitačná práca.pdf
https://docs.google.com/leaf?id=0B9X-L5lO6y2YOWVmZjhkMDctOWIzZC00Njc2LTkyNmEtZjdhNWU2OTNiMWJm&hl=en&authkey=CMyAtZsG
Navigácia
[0] Index správ
[#] Ďalšia strana
Go to full version