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 [Select] Expand

[PRE X>0 THEN y=y/xEND](y>1), [CHOICE SS:= SS U{xx} ||| bb:=TRUE OR bb:=FALSE ](xx patri SS)
----------------------------------------------------------------------------------------------------


----------------------------------------------------------------------------------------------------
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 [Select] Expand

[ANY vv WHERE vv>xx A vv (patri) N THEN xx:=vv END] (xx (patri) ss)

14.06.2010, 20:54:41

Code [Select] Expand

[@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
----------------------------------------------------------------------------------------------------


18.06.2010, 12:18:25
B stroj

Code [Select] Expand

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

EDIT od kOsTi-ho: k 1. obrazku: pri p7: este musi ist z t3 do p7 hrana

[Faust]

ake je heslo do moodlu?

[jan]

ake je heslo do moodlu?

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

[Faust]

do kedy treba koreckovi poslat ten "referat" ?

[azalie]

cawko. mam dotaz. co treba psiat k tymto teoretickym otazkam???

B jazyk, definicia vlatnosti
sysntax struktury MASCHINE N(p) a jeho vlastnosti
Jazyk ,,guarded commands".
Sémantika Machine N(p):štruktúra povinného dôkazu korektnosti špecifikácie stroja Machine N(p).(Proof Obligation for
Machine N(p)
Mechanizmus ";" dokaz jeho korektnosti, platnosti pre vlastnosti 1-4

Neviem kde najdem odpoved v tom koreckovom PDF. dik za odpoved

[Faust]

mna by zaujimalo ake boli otazky na 1.termine, moze niekto napisat? dik

[Faust]

btw kde najdem teoriu k tejto otazke? vektorove aditivne systemy. Vztah VAS a petriho sieti ..v tych podkladoch od korecka tam take nieje ak sa nemylim

[jan]

Heslo do moodle: jahodka

Skúška: otázky boli tie čo sú hore
Zadanie: každý mal urobiť referát na nejakú tému (napr. Petriho siete v biochémii)
DU: Urobiť B-MACHINE ten čo je dole
K cvičeniu: na cvičení sa chodí k tabuli, kto chce. Systém  je taký, že za aktivitu je napr. 10 bodov, smerodajné je koľko krát bol maximálne niekto pri tabuli, keď to bude napr. 5, tak sa vypočíta cena jedného počítania pri tabuli ako 10/5=2 body. Takže ten čo bol pri tabuli tých 5 krát, dostane full, čiže 10 bodov a keď sa niekomu nechcelo a bol tam len raz, dostane 2 body (1 účasť x 2 body = 2 body).

Príprava na skúšku:
- Základným učebným materiálom je [1], toto treba prečítať celé, kapitoly 2.6.2, 2.6.3, väčšinu kapitoly 2.7 a v kapitole 3.3 "Príkaz DO" som ja osobne preskočil.
- Z literatúry [2] treba hlavne kapitoly 3 (tá je ale preložená v literatúre [1]) a asi 4 a 7.
- Z literatúry [3] treba tiež len niečo, podľa toho čo povie na prednáške.
- Literatúra [4]. Toto si treba pozrieť a použiť na doplnenie informácií, ktoré nie sú v [1][2][3], ale väčšna je v [1], keďže Ing. Korečko písal [1] podľa prednášok Prof. Hudáka a Prof. Hudák tieto materiály [4] používa na prednáškach.
- Čo sa týka príkladov, na cvičení sa počítajú príklady z [5] + treba vedieť urobiť kód B-MACHINE (viď. dole) + nakresliť PS obedujúcich filozofov (odrázok hore).

Archív zo všetkými materiálmi:
http://www.uloz.to/9389262/zhrnutie-rar

Učebné materiály

Zo stránky Ing. Korečka (http://hornad.fei.tuke.sk/~korecko/fss/):
[1] SK_FSpodklady.pdf - http://hornad.fei.tuke.sk/~korecko/fss/SK_FSpodklady.pdf
[2] Materiál k jednej prednáške - An Introduction to the Theoretical Aspects of Coloured Petri Nets - http://hornad.fei.tuke.sk/~korecko/fss/CPNtheory.pdf

Doplňujúce materiály od Prof. Hudáka (v archíve):
[3] Materiál k jednej prednáške - Štefan Hudák - Rozšírenia Petriho Sietí - habilitačná práca.pdf (https://docs.google.com/leaf?id=0B9X-L5lO6y2YOWVmZjhkMDctOWIzZC00Njc2LTkyNmEtZjdhNWU2OTNiMWJm&hl=en_US&authkey=CMyAtZsG)

Z moodlu od Prof. Hudáka (aj v archíve)
[4] - 6 súborov pdf

Na cvičenie (len v archíve):
[5] cvika2007 zosvetlene.pdf

Možno sa tiež zíde (len v archíve):
[6] prednasky2007.pdf

Okruhy otázok:
[7] Tematické okruhy ku skúške z predmetu Formálne špecifikácie systémov; akad. rok 2010/2011 - FSSTemySkOtazok.doc
[8] Teoretické otázky pre študentov ŠpZ - http://hornad.fei.tuke.sk/~korecko/fss/FSS_SpZ_teoretOtazky.pdf

Potrebný softvér:

B-MACHINE
[9] ProB - http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download
[10] Atelier B - http://www.atelierb.eu/index-en.php

Petriho siete
[11] PNtool 2 (školský projekt) - http://hornad.fei.tuke.sk/~korecko/fss/index.html

Farebne Petriho siete
[12] CPN tools - http://cpntools.org/


príklad B-MACHINE z cvičenia:

vysvetlenie zápisu B-MACHINE(abstraktného stroja) a jeho klauzúl (CONSTRAINTS, ...) je v literatúre [1] na stranách 61-64

Code [Select] Expand


MACHINE Scalar( max_val )

CONSTRAINTS max_val:NAT & max_val>=0

ABSTRACT_VARIABLES val

INVARIANT  val : 0 .. 10

INITIALISATION val := 0

OPERATIONS

    retVal <-- getVal =
    BEGIN
        retVal := val
    END ;

    setVal ( amount ) =
    PRE amount : NAT THEN
        IF amount <= max_val & amount >= 0 THEN val := amount END
    END ;

    incVal ( amount ) =
    PRE amount : NAT THEN
        IF val < max_val THEN val := val + 1 END
    END ;

    decVal ( amount ) =
    PRE amount : NAT THEN
        IF val > 0 THEN val := val - 1 END
    END ;

    maximum <-- maxVal ( xx ) =
    PRE xx : INT THEN
        IF xx > val THEN maximum := xx ELSE maximum := val END
    END ;

    incORdecVal ( amount ) =
    PRE amount : NAT THEN
               CHOICE
                   IF val > 0 THEN val := val - 1 END
               OR
                   IF val < max_val THEN val := val + 1 END
               END
    END
END