Redes de Petri
1° Exercício




Modele dois processos concorrentes entre si.
Cada processo é cíclico e compostos por
apenas três atividades.
Estes processos compartilham entre si dois
recursos.
Um modelo em redes de Petri para este
problema é apresentado no próximo slide.
Redes de Petri
1° Exercício

Para as redes mostradas no proximo slide
analisem as seguintes propriedades:
–
–
–
–
–
•
Boundedness
Deadlock freedom
Liveness
Reversibilidade
Conservação
Como os modelos são de pequenas dimensões,
sugiro o seguinte:
1.
2.
3.
Inicialmente, de maneira informal (simulação
exaustiva), vocês devem analisar a existência das
propriedades.
Após isto, utilizando a ferramenta INA, vocês devem
fazer a análise formal de maneira automática.
Comparem ambos os resultados.
Redes de Petri
1° Exercício

N1

N2
Redes de Petri
1° Exercício

N3

N4
p0
p0
t0
t0
p3
t2
t4
p2
p1
p3
p1
t2
t3
t1
p2
t1
t3
Redes de Petri
2° Exercício
Para a rede de Petri obtida para o modelo FSP seguinte e mostrada no proximo slide, analise as mesmas propriedades do 1ºexercício.
MAKE_A = (makeA->ready->used->MAKE_A).
MAKE_B = (makeB->ready->used->MAKE_B).
ASSEMBLE = (ready->assemble->used->ASSEMBLE).
||FACTORY = (MAKE_A || MAKE_B || ASSEMBLE).
Redes de Petri
2° Exercício - Solução
MakeA
MakeB
makeA
Assemble
makeB
ready
assemble
used
Jantar dos Filósofos
3° Exercício
Analise as propriedades referidas no 1º
Exercício para a rede de Petri dos
filósofos.
3
2
2
1
3
A rede é mostrada no slide seguinte.
4
1
4
0
0
começa
pensar
Jantar dos Filósofos
pensando 3° Exercício - Solução
começa ter fome
garfo 2
Filósofo 3
comendo
pensando
com fome
com fome
começa
comer
começa
pensar
comendo
começa ter fome
começa
comer
Filósofo 2
comendo
começa
comer
com fome
garfo 3
garfo 1
começa ter fome
pensando
começa
pensar
Filósofo 1
Download

aulapratica6