Introdução aos Formalismos
para Modelagem de Sistemas
Concorrentes
Por
Paulo Maciel
Centro de Informática
Universidade Federal de Pernambuco
Objetivo
Apresentar alguns formalismos para a
modelagem de sistemas concorrentes.
Descrever as principais características
destes modelos.
Modelagem de Problemas.
Ressaltar as pontencialidades destes
modelos.
Metodologia
Aulas expositivas
Seminários onde serão discutidos em sala os assuntos sugeridos.
Para cada um dos temas será fornecido material de estudo.
Aulas práticas.
Desenvolvimento de estudo de casos.
Bibliografia Básica
Intoduction to Discrete Event Systems, Cassandras
and Lafortune,
Lafortune, Kluwer,
Kluwer, 2008.
Concurrency: State Models & Java Programs, 2nd
Edition byJeff MageeandJeff Kramer John Wiley &
Sons 2006
Uma Introdução às Redes de Petri. Paulo Maciel,
Maciel,
Rafael Lins,
Lins, Paulo Cunha, Escola de Computação,
Computação,
1996.
Lectures Notes on Petri Nets I, Basic Models.
Springer Verlag,
Verlag, 1998.
Lectures Notes on Petri Nets II, Applications.
Springer Verlag,
Verlag, 1998.
Avaliação
Listas
Seminários
Trabalho Final (draft de artigo)
artigo)
Classificação dos Modelos
O que é um sistema?
O que é um modelo?
1
Classificação dos Sistemas
Estáticos
Dinâmicos Variantes no Tempo
Invariantes Estado Contínuo
Estado Discreto
Tempo Discreto
Tempo Contínuo
Classificação dos Sistemas
Estáticos
Dinâmicos
Não--Temporais Invariantes no Tempo Variantes no Tempo
Não
Determinísticos
Probabilístico
Eventos Discretos
Estado Contínuo
Contínuos
Estado Discreto
Tempo Discreto
Tempo Contínuo
Determinísticos
Classificação dos Modelos
Modelos Baseados em Estado
– Consideram apenas os estados para modelar e se referir as
propriedades do sistema.
– Maioria das lógicas temporais, autômatos
Modelos Baseados em Ações
– Consideram apenas as ações para modelar e se referir as
propriedades dos sistemas.
– As álgebras de processos: CCS, CSP, COSY, FSP
Motivação
Considere uma situação onde se deseja representar de forma
precisa o comportamento de um sistema de manufatura,
manufatura,
responsável pela fabricação de três tipos de produtos
diferentes.
A realização das atividades de manufatura de cada produto é
denominada um processo. Estes processos podem ser
executado paralelamente.
paralelamente.
O ambiente de manufatura disponibiliza três máquinas
(recursos) para realização das atividades dos processos.
Cada par de processos compartilha entre si uma máquina.
máquina.
E cada processo precisa simultaneamente de duas máquinas
para realização de uma determinada atividade.
Modelos Heterogêneos
– Consideram ações e estados.
– Redes de Petri
Motivação
Motivação
Estrutura do Problema
Processo
3
M3
M2
Processo
1
Probabilístico
Processo
2
M1
O Problema Jantar dos Filósofos
G2
P3
Filósofos
• Pensam
•Tem fome
•Comem
G3
P1
P2
G1
Como especificar
adequadamente
este problema de
forma que o
modelo obtido não
trave (deadlock) e
que todos os
filósofos tenham
oportunidade de
comer ?
2
Apresentacão
LTS – Sistema de Transição Rotulado,
Máquinas ou Autômatos (Labeled Transitions
Systems)
FSP – Finite Sequential Process
Redes de Petri
Apresentacão
Máquinas de Estados Finitos
LTS – Sistema de Transição Rotulado
CSP – Communicating Sequential Process
Estruturas Traces
Redes de Petri
(Finite State Machines)
(Labeled Transitions Systems)
Máquinas de Estados
Máquinas de Estados,
Autômatos ou
Sistemas de Transição
Rotulados
Máquina de Estados Determinística
Máquina de Estados NãoNão-Determinística
Máquina de Estados Finitos NãoNãoDeterminísitca
Máquinas de Estados Finitos Determinística
– Máquina de Estados Finitos Determinística
com Entradas e Saídas
Máquina de Estados
Determinística
SM= (S,E,f,Γ
(S,E,f,Γ, s0,Sm)
– S – Conjunto de estados
– s0 ∈ S– Estado inicial
– E – Alfabeto (conjunto de eventos)
– f : S × E → S – Função de próximo estado
– Γ : S → 2E – Função dos eventos factíveis
– Sm ⊆ S - Conjunto de estados marcados
Máquina de Estados
Determinística
S={s0,s1}, E={a,b}, f(s0,a) = s1,
f(s0,b) = s0, f(s1,a)=s1, f(s1,b)=s0,
Γ(s0) = {a,b}, Γ(s1) = {a,b}, Sm={s1}
b
s0
a
b
s1
a
3
Máquina de Estados
Determinística
Máquina de Estados
Determinística
Linguagem Gerada
L(SM) = {st ∈ E* | f(s0, st) é definida}
se f for uma função total então L(SM) = E*
Linguagem Marcada
Lm(SM) = {st ∈ L(SM) | f(s0, st) ∈ Sm}
b
L(SM1) = L(SM2)
Lm(SM1) = Lm(SM2)
a
s0
a
s1
b
Duas Máquinas de Estados SM1 e SM2
são ditas equivalentes se
Lm(SM) = {a, aa, ba, aaa, aba, ....}
L(SM)= E*
Máquina de Estados
Determinística
SM1
a
s0
Máquina de Estados
Determinística
a
s1
b
s0
s1
b
s2
b
a
L(SM1) = L(SM2)
Lm(SM1)=Lm(SM2)
Máquina de Estados
Determinística
1
s0
1
s1
3
1
2
1
2
E = {1,2,3}
2,3
s2
3
b
a
s4
g
•Alcançabilidade - Um
estado sn é alcançável de
s0 se existe um
conjunto de eventos
que realizados a partir de
s0 levam a sn.
s4 ∈R(s0)
s0 ∉ R(s4)
Máquina de Estados
Determinística
Detector de Seqüência 123
2,3
•Livelock - Estados s3, s4
s3
s2
a
s5
a
s0
a
•Deadlock - Estado s5
g
s1
a
g
SM2
SM
s3
Podemos modelar este problema
com um automata (máquina)
Sistema de Fila
de estados infinitos.
Neste ambiente, os usuários Os eventos que dirigem o sistema
chegam e solicitam acesso a são:
um servidor. Caso o servidor
esteja ocupado, os usuários a : chegada de um usuário
d: saída de um usuário
devem aguardar na
Portanto,
fila.Quando o usuário
completa a operação
E={a,d}
solicitada, ele sai do sistema S={0,1,2,...}
e o próximo usuário da fila é
f(s,a) = s+1, ∀ s≥0
servido imediatamente.
f(s,d) = ss-1, se s>0
Γ(s) = {a,d}, ∀ s>0
Γ(0) = {a}
4
Máquina de Estados
Determinística
Máquina de Estados
Determinística
Sistema de Fila
Sistema de Fila
E={a,d}
S={0,1,2,...}
f(s,a) = s+1, ∀ s≥0
f(s,d) = ss-1, se s>0
Γ(s) = {a,d}, ∀ s>0
Γ(0) = {a}
d
a
a
s0
a
a
s1
a
s2
d
s3
d
d
...
d
Para este mesmo sistema, vamos
focar o estado do servidor.
Vamos assumir que o servidor
pode estar desocupado (I
(I),
ocupado (B
(B) ou quebrado (D
(D).
Assumi--se que quando o
Assumi
servidor está quebrado, o
usuário em serviço é perdido.
Portanto, após o reparo, o
servidor está desocupado. Os
eventos são: serviço começa
(a), serviço finaliza (b
(b),
servidor quebra (l
(l) e servidor é
reparado (n
(n).
.
Máquina de Estados
Determinística
Sistema de Fila
E={a,b,l,n}
S={I,B,D}
f(I,a) = B, f(B,b) = I,
f(D,n) = I, f(B,l) = D,
Γ(I) = {a}, Γ(B) = {b,l},
Γ(D) = {n}
B
b
Máquina de Estados NãoNãoDeterminística
SMnd= (S,E ∪ {ε},F,
,F,Γ
Γ, s0,Sm)
S={0,1}
E={a,b}
F(0,a) = {0,1}
F(1,b) = {0}
Γ(0) = {a}
Γ(1) = {b}
S – Conjunto de estados
s0 ∈ S– Estado inicial
E – Alfabeto (conjunto de eventos)
F : S × E × S – Relação de próximos estados
Γ : S → 2E - Função dos eventos factíveis
Sm ⊆ S - Conjunto de estados marcados
Por quê utilizar?
1. Desconhecimento sobre determinadas atividades ou necessidade de
abstração
2. É possível obter um automata de menor número de estados.
l
D
E={a,b,l,n}
S={I,B,D}
f(I,a) = B, f(B,b) = I,
f(D,n) = I, f(B,l) = D,
Γ(I) = {a}, Γ(B) = {b,l},
Γ(D) = {n}
SMnd= (S,E∪
(S,E∪{ε},F,
,F,Γ
Γ, s0,Sm)
–
–
–
–
–
–
a
I
n
d
Máquina de Estados NãoNãoDeterminística
.
a
Máquina de Estados NãoNãoDeterminística
Máquina determinísitca equivalente
SMnd= (S,E,f,Γ
(S,E,f,Γ, s0,Sm)
a
S={A,B}
a
AI
1
B
E={a,b}
b
f(A,a) = B
f(B,a) = A, f(B,b) = A
Γ(A) = {a}
Máquinas não-determinísticas podem ser
convertidas em máquinas deteminísticas.
Γ(B) = {a,b}
a
a
0I
1
b
5
Máquina de Estados
-Algumas OperaçõesOperaçõesPartes Acessíveis (Reachable)
SM= (S,E,f,
(S,E,f, s0,Sm)
Rc(SM)=(Src,E,frc, s0, Smrc)
f(s0,st) esteja
Src={s ∈ S | ∃ st ∈ E* que f(s
definida}
Smrc= Sm∩ Src
frc=f| Src × E → Src é a função f com o domínio
restrito a (Src,E)
Máquina de Estados
-Algumas OperaçõesOperações Composição Paralela
SM1= (S1,E1,f1,Γ1, s01,Sm1)
SM2= (S2,E2,f2,Γ2, s02,Sm2)
SM1|| SM2=Rc(S1× S2, E1 ∪ E2,f1||2, Γ1||2, (s01, s02), Sm1× Sm2)
(f1(s1,e), f2(s2,e)) se e ∈ Γ1(s1)∩Γ2(s2)
f1||2((s1, s2),e) = (f1(s1,e), s2))
se e ∈ Γ1(s1)\ E2
(s1,f2(s2,e))
se e ∈ Γ2(s2)\ E1
indefinido
caso contrário
Γ1||2(s1, s2)={
)={Γ
Γ1(s1) ∩ Γ2(s2)} ∪ {Γ1(s1)\ E2} ∪ {Γ2(s2)\ E1}
Nós vamos assumir que as máquinas tratadas aqui são acessíveis.
Máquina de Estados
-Algumas OperaçõesOperaçõesComposição Paralela
a
a
X
Y
a,g
g
b
Z
Máquina de Estados
-Algumas OperaçõesOperações Composição
S={X,Y,Z}, E={a,b,g},
f(X,a) = X, f(X,g) = Z,
f(Y,a)=X, f(Y,b)=Y,
f(Z,b)=Z,
b f(Z,a)=f(Z,g)=Y
Γ(X) = {a,g}, Γ(Y) = {a,b},
Γ(Z) = {a,b,g}
Sm={X,Z}
S={s0,s1}, E={a,b}, f(s0,a) = s1,
f(s0,b) = s0, f(s1,a)=s1, f(s1,b)=s0,
Γ(s0) = {a,b}, Γ(s1) = {a,b}, Sm={s1}
b
s0
Máquina de Estados
-Algumas OperaçõesOperações
Composição Paralela
b
b
X,0
g
Z,0
a
a
X,1
X
b
g
Z,1
X
a
a
g
Y,0
a
b
a,g
Y,1
S={(X,0),(X,1),(Y,0),(Y,1),(Z,0),(Z,1)},
E={a,b,g},
f((X,0),a) = (X,1), f((X,0),g) = (Z,0),
f((X,1),a) = (X,1), f((X,1),g) = (Z,1),
f((Y,0),a)=(X,1), f((Y,0),b)=(Y,0),
f((Y,1),a)=(X,1), f((Y,1),b)=(Y,0),
f((Z,0),b)=(Z,0),
f((Z,0),a)=f((Z,1),g)= f((Z,1),a)=
(Y,1)
f((Z,1),b)= (Z,0)
Γ(X,0) = Γ(X,1) = {a,g},
Γ(Y,0) = Γ(Y,1) = {a,b},
Γ(Z,0) = Γ(Z,1) = {a,b,g}
Sm={(X,1),(Z,1)}
Paralela
a
b
s1
a
Máquina de Estados
-Algumas OperaçõesOperações
Composição Paralela
Se E1 = E2, todos os eventos de SM1||SM2
serão sincronizados
Se E1 ∩ E2 = ∅, não se tem eventos
sincronizados. TemTem-se a concorrência, com
nenhum sincronismo (interleaving dos
eventos de SM1 e SM2)
6
Máquina de Estados
-Algumas OperaçõesOperações-
Máquina de Estados
- Problema dos Filósofos -
Produto
SM1= (S1,E1,f1,Γ1, s01,Sm1)
SM2= (S2,E2,f2,Γ2, s02,Sm2)
SM1× SM2=Rc(S1× S2, E1 ∩ E2,f1×2, Γ1×2, (s01, s02), Sm1× Sm2)
(f1(s1,e), f2(s2,e)) se e ∈ Γ1(s1)∩Γ2(s2)
f1×2((s1, s2),e) =
indefinido
caso contrário
Suponhamos dois Filósofos P1 e P2. Cada filósofo ou está
pensando ou comendo. Os eventos i fj significam o filósofo i
pega o garfo j e os evento j f significam o filósofo j libera os
garfos.
P2
P1
1f1 1I1 1f2
2f1 2I1 2f2
1T
2T
X
1E
X
2E
1f
2f
1f2 1I2 1f1
2f2 2I2 2f1
Γ1×2(s1, s2)=
)=Γ
Γ 1( s 1) ∩ Γ 2( s 2)
1A
X
Máquina de Estados
- Problema dos Filósofos 1f
1f2
(1T,2T,1A,2A)
1f1
X
1f2
2f1
2f2
2f
2f2
1f1
1f1
(1E,2T,1U,2U)
Exercício: construir um
Deadlock modelo que não tenha
deadlock
(1T,2E,1U,2U)
Finite State Machine
Modelo Mealy
1/F
s0
1/F
s1
3/F
2/F
I = {1,2,3}
O={F,T}
1/F
2/F
1/F
2,3/F
s2
3/T
2U
SM= (S,I,O,f,h)
Finite State Machine
Detector de Seqüência 123
2,3/F
1f,2f
– S – Conjunto de Estados
– s0 ∈ S– Estado inicial
– I – Alfabeto de entrada
– O – Alfabeto de saída
– f : S × I → S – Função de próximo estado
– h: S × I → O – Função de saída
(1I2,2I1,1U,2U)
(1I1,2I2,1U,2U)
2f1
1f,2f
1f2,2f2
2A
X
1U
Finite State Machine
Modelo Mealy
2f1
1f2
2f2
1f1,2f1
Linguagem Gerada
L(SM) = {ik ∈ I | f é definida}
b
s3
s0
a
b
s1
a
L(SM) = {a, aa, ba, aaa, aba, ....}
Duas Máquinas de Estados SM1 e SM2 são ditas equivalentes se
L(SM1) = L(SM2)
7
Máquinas de Estados Finitos
Modelo Mealy
Máquinas de Estados Finitos
Modelo Mealy
Edfícil
I={a1,a2,a3}
ANDAR DESEJADO
O={d2,d1,p,s1,s2}
a1/p
a3
DE ANDARES
a2
a2/s1
S1
DIREÇÃO E
NÚMERO
a2/p
S2
a1/d1
O={d2,d1,p,s1,s2}
I={a1,a2,a3}
DIREÇÃO E
NÚMERO
S3
ANDAR DESEJADO
a3/p
DE ANDARES
a1
E
Máquinas de Estados Finitos
Modelo Moore
Máquinas de Estados Finitos
Modelo Moore
a1
a1
FSM= (S,I,O,f,h)
– S – Conjunto de Estados
– s0 ∈ S– Estado inicial
– I – Alfabeto de entrada
– O – Alfabeto de saída
– f : S × I → S – Função de próximo estado
– h: S → O – Função de saída
S11 /d2
S21 /d1
a2
a1
a1
S12 /d1
a3
a1
a1
S13 /p
a3
a1
a2
a3
a3
a2
S22 /p
a2
a2
S31 /p
a2
a3
S32 /s1
a3
a3
S23 /s1
a2
S33 /s2
a1
a3
Máquinas de Estados Finitos
– Dificuldades na modelagem direta da concorrência.
Sistema de Transição Rotulado
(Labeled Transition System)
Criação de processos
sincronização
– Impossibilidade de representação de sistemas acom
número infinito de estados.
– A análise de propriedades interessantes são
decidíveis
8
Sistema de Transição Rotulado
TS = (S,s0,L,tran)
Finite State Process
(FSP)
– S – Conjunto de Estados
– s0 – Estado inicial
– L – Conjunto de rótulos
a
– tran ⊆ S × L × S, normalmente indicada por s →
s’
Modelando Processos
Modelos serão descritos por Labelled
Transition Systems LTS.
Serão descritos textualmente através finite
state processes (FSP)
Ferramenta LTSA .
♦ LTS - forma gráfica
modelando processos
Um processo é a execução de programa seqüencial.
Modelaremos utlizando LTS que muda de estado pela
execução de ações atômicas.
on
0
♦ FSP - forma algébrica
1
off
on
off
on
off
on
off
……….
FSP - Prefixação
Se x é uma ação e P um processo então (x-> P)
descreve um processo que inicialmente executa a
ação x e comporta-se exatamente como descrito
pelo processo P.
ONESHOT = (once -> STOP).
once
0
ONESHOT state
machine
1
Convenção: ações começam com letras minúsculas e
PROCESSOS com letras maiúsculas
a light
switch LTS
a seqüência de
ações ou trace
FSP - Prefixação & Recursão
Comportamento Repetitivo - Usas-se recursão:
SWITCH = OFF,
OFF
= (on -> ON),
ON
= (off-> OFF).
Forma mais sucinta:
on
0
SWITCH = OFF,
OFF
= (on ->(off->OFF)).
1
off
Outra vez:
SWITCH = (on->off->SWITCH).
9
animação usando LTSA
FSP - Prefixação
Modelo FSP de um semáforo :
O animador LTSA pode
ser usado para produzir
um trace.
TRAFFICLIGHT = (red->orange->green>orange
-> TRAFFICLIGHT).
LTS gerado utilizando LTSA:
Escolha das ações
elegíveis.
red
.
0
orange
1
green
2
3
on
0
1
Trace:
orange
red
orange
green
orange
red
orange
gree
n …
off
FSP - Escolha
FSP - choice
Modelo FSP of uma máquina de venda :
Se x e y são ações então (x-> P | y-> Q)
descreve um processo que inicialmente executa
x or y. Após a primeira ação ter ocorrido, o
comportamento subseqüente é descrito po P se ta
primeira ação foi x e Q se foi y.
DRINKS = (red->coffee->DRINKS
|blue->tea->DRINKS
).
blue
LTS gerado usando-se
LTSA:
red
0
1
2
Quem o que fez a escolha ?
Quais são os traces possíveis?
coffee
tea
FSP - Processos e Ações
Indexadas
Escolha NãoNão-Determinística
Processo (x-> P | x -> Q) descreve um processo
que executa x e então comporta-se como P ou Q.
COIN = (toss->HEADS|toss->TAILS),
toss
HEADS= (heads->COIN),
TAILS= (tails->COIN).
toss
0
Quais são os possíveis
1
2
buffer que recebe como entrada um valor entre 0 e
3 e então fornece como saída:
BUFF = (in[i:0..3]->out[i]-> BUFF).
Equivale a
BUFF = (in[0]->out[0]->BUFF
|in[1]->out[1]->BUFF
|in[2]->out[2]->BUFF
|in[3]->out[3]->BUFF
Ou através de).
parâmetros de processos com valor
default:
BUFF(N=3) = (in[i:0..N]->out[i]-> BUFF).
heads
traces ?
tails
10
FSP - Ações Guardadas
A escolha (when B x -> P | y -> Q) significa
que quando a guarda B é verdadeira então as
ações x e y são ambas elegíveis, caso contrário, se
B is falso, então a ação x não pode ser escolhida.
Sistema de Transição Rotulado
Sejam dois processos concorrentes A e B
Processo A{
Processo B {
Enquanto C=T {
e1
e2
}
e3
e5
COUNT (N=3)
= COUNT[0],
COUNT[i:0..N] = (when(i<N) inc->COUNT[i+1]
|when(i>0) dec->COUNT[i-1]
).
inc
0
inc
1
dec
inc
2
dec
3
}
}
dec
Sistema de Transição Rotulado
e4
e5
Sistema de Transição Rotulado
Se A e B são dois processos, então (A||B)
representa a execução concorrente de A e B.
e2
s0
e3
e1
Processo A =
(e1 -> e2 -> Process A)
Processo B =
(e4 -> e5 - Process B)
s1
e4 e2
s3
e4
e3
s4
Process C = ((Process A || Process B) -> Process C )
s5
e4
s6
e1
e5
s7
Composição Paralela
Interleaving de Ações
Se VERTV e CONVERSA são dois processos,
então (VERTV||CONVERSA) representa a
execução concorrente de VERTV e CONVERSA.
O operador || é o operador de composição
paralela.
VERTV = (ver->STOP).
CONVERSA = (pensa->conversa->STOP).
||CONVERSA_VERTV = (VERTV
pensa
conversa
ver
pensa
ver
conversa
ver
pensa
conversa
Composição Paralela
Interleaving de Ações
ver
pensa
VERTV
0
1
0
ver
1
2 estados
2
3 estados
ver
CONVERSA_VERTV
|| CONVERSA).
Os traces
possíveis são
resultados do
interleaving de
ações.
conversa
CONVERSA
VERTV
pensa
conversa
0
1
2
(0,0)
(0,1)
(0,2)
CONVERSA
ver
3
(1,2)
4
5
(1,1)
(1,0)
conversa
pensa
2 x 3 estados
11
Modelando Interações
Ações Compartilhadas
Modelando Interações
Ações Compartilhadas
Se processoes em uma composição têm ações em comum, estas
ações são ditas compartilhadas.
3 estados
MAKERv2 = (make->ready->used->MAKERv2).
3 estados
USERv2 = (ready->use->used ->USERv2).
Ações compartilhadas modelam as interações entre processos.
Enquanto ações não compartilhadas podem ser
arbitrariamente interleaved , ações compartilhadas devem ser
executadas ao mesmo tempo por todos os processos.
MAKER = (make->ready->MAKER).
USER = (ready->use->USER).
||MAKER_USER = (MAKER || USER).
MAKER
sincroniza-se
com USER
quando ready.
Modelando Interações
Múltiplos Processos
||MAKER_USERv2 = (MAKERv2 || USERv2).
make
ready
0
MAKE_A
= (makeA->ready->used->MAKE_A).
MAKE_B
= (makeB->ready->used->MAKE_B).
ASSEMBLE = (ready->assemble->used->ASSEMBLE).
1
2
makeA
a.on
b.on
b:SWITCH
0
0
1
2
1
4
0
1
a.off
assemble
3
Interação
restringe o
comportamento
global
a:P prefixa cada rótulo associado a uma ação do alfabeto P
com a.
SWITCH = (on->off->SWITCH).
Duas instâncias de switch ||TWO_SWITCH = (a:SWITCH ||
process:
b:SWITCH).
a:SWITCH
ready
4 estados
3
used
||FACTORY = (MAKE_A || MAKE_B || ASSEMBLE).
makeA
use
Nomeação de Processo
Sincronização Múltipla:
makeB
3 x 3
estados?
5
makeB
b.off
Um array de instâncias do processo switch:
||SWITCHES(N=3) = (forall[i:1..N]
s[i]:SWITCH).
||SWITCHES(N=3) = (s[i:1..N]:SWITCH).
used
Nomeação de processo por um
conjunto de rótulos prefixos
{a1,..,ax}::P substitui todo rótulo associado a uma
ação no alfabeto de P com os rótulos a1.n,…,ax.n.
Posteriormente, toda ação (n->X) na definição de
P será substituída pelas transições ({a1.n,…,ax.n} >X).
RESOURCE = (acquire->release->RESOURCE).
USER = (acquire->use->release->USER).
||RESOURCE_SHARE = (a:USER || b:USER
|| {a,b}::RESOURCE).
Rótulos Prefixados a
Processos
a.acquire
a.use
b.acquire
a:USER
0
1
b.use
b:USER
2
0
1
a.release
b.release
Como se garante que um
usuário solicita um
recurso é o mesmo que o
libera ?
b.acquire
a.acquire
{a,b}::RESOURCE
a.acquire
0
b.acquire
b.use
a.use
RESOURCE_SHARE
0
2
1
2
3
4
1
a.release
b.release
b.release
a.release
12
Renomeação de Ações
Funções de renomeação são usadas para mudar os
nomes das ações. A forma geral é:
/{newlabel_1/oldlabel_1,… newlabel_n/oldlabel_n}.
Renomeação de Ações
||CLIENT_SERVER = (CLIENT || SERVER)
/{call/request, reply/wait}.
call
reply
0
O renomeação garante que processos
compostos se sincronizarão em uma ação
em particular.
1
CLIENT_SERVER
Algumas vezes é importante mostra as áções que não
são silents.
Quand aplicado ao processo P, o
operador de interface @{a1..ax} esconde
todas as ações exceto as presentes no
conjunto a1..ax.
service
1
2
reply
continue
call
0
Qunado apliado a um processo P, o operador hiding
\{a1..ax} remove os nomes das ações a1..ax do
alfabeto de P e torna estas ações "silent". Estas
ações são rotuladas por tau. Ações Silent em
processos diferentes não são compartilhadas.
0
2
service
1
CLIENT = (call->wait->continue->CLIENT).
SERVER = (request->service->reply->SERVER).
Tornando Internas (hiding
(hiding)) as
Ações-- Abstração para Redução de
Ações
Complexidade
call
SERVER
CLIENT
reply
2
3
continue
Tornando Internas (hiding
(hiding)) as
Ações
As seguintes definições são equivalentes:
USER = (acquire->use->release->USER)
\{use}.
USER = (acquire->use->release->USER)
@{acquire,release}.
A minimização remove as
acquire
0
ações silents produzindo
um LTS com
açõesobesrváveis.
tau
1
2
acquire
release
0
1
release
13