Paulo Borba e Augusto Sampaio

Centro de Informática

Universidade Federal de Pernambuco

Operadores Básicos

• CSP é uma linguagem para definição e especificação de processos

• Processos correspondem a sistemas, componentes de um sistema distribuído

• Processos comunicam-se com outros

Processos

• Realizada através de eventos de comunicação:– a chamada de um método atômico– o início ou fim da chamada de um

método não atômico– a notificação de um evento da GUI ou

de algum periférico

• Eventos são atômicos, instantâneos

Comunicação

• A comunicação só ocorre através da sincronização entre dois ou mais processos:– o mesmo evento ocorre em dois

processos ao mesmo tempo

• O alfabeto de um processo é o conjunto de todos os seus eventos:– tem que ser escolhido com cuidado

Comunicação

• O processo que não faz nada:– nunca se comunica com outros

processos– não oferece nenhum evento de

comunicação

• Representa um sistema (processo)– em deadlock, ou – sem funcionar

STOP

• Operador para construir processos:

a -> P

dado um evento a e um processo P• Oferece o evento a e espera,

indefinidamente, até que haja uma comunicação

• Depois da comunicação, comporta-se como P

• Formas inválidas: a -> b, P -> Q

Prefixo

Definindo Processos

• Declarando os eventos ou canais de comunicação: channel up, down

• Definindo (nomeando) um processo cujo alfabeto é determinado pelos eventos acima: P0 = up -> down -> up ->

down -> STOP

P1 = up -> down -> P1

P2 = up -> down -> up ->

down -> P2

• Através de equações recursivas (guardadas)

• Utilizadas para processos que – tem um comportamento repetitivo– normalmente não terminam

• Objetos em Java, por exemplo

Definições Recursivas

• Definições (equações) diferentes, processos iguais

• Operador de recursão: X.F(X) representa “o processo” definido por

P = F(P)

para uma expressão F (guardada)

• P = F(P) equivale a P = X.F(X)

Processo versus Definição do Processo

Pu = up -> Pd

Pd = down -> Pu

• Processo versus Sistema:– dois processos, um único sistema– um processo não “chama” um outro

processo, mas “comporta-se como” um outro processo

Definições Mutuamente Recursivas

• Operador para construir processos: (a1 -> P1 | ... | an -> Pn)

dado eventos diferentes a1,..., an, e processos P1, ..., Pn

• Processos que oferecem – alternativas de comportamento

– escolha de eventos

• Forma inválida: (P | Q | R)

Alternativa Guardada

• É uma abreviação para o operador de escolha externa: (a -> P | b -> Q | c -> R)

corresponde a (a -> P [] b -> Q) [] c -> R

• Exemplo:

Alternativa Guardada

channel a,bB0 = a -> B0 [] b -> B1B1 = a -> B0 [] b -> STOP

• Todo processo em CSP corresponde a uma “máquina de estados”

• Com STOP, prefixo, recursão, e alternativa guardada expressamos todas as máquinas de estados finitas e determinísticas

• Ferramentas de model checking, como FDR, verificam processos com um número finito de estados

Máquinas de Estados e CSP

• Corresponde a uma família, possivelmente infinita, de definições:COUNT(n)=

if n==0 then

(up -> COUNT(1))

else

(up -> COUNT(n+1) []

down -> COUNT(n-1))

Definições Parametrizadas

• O número de estados pode ser limitado: LCOUNT(L,n) =

(n<L & up -> LCOUNT(L,n+1))

[](n>0 & down -> LCOUNT(L,n-1))

onde

(cond & P)

corresponde a

if cond then P else STOP

Definições Parametrizadas

• Operador para construir processos: ?x:A -> P(x)

dado uma variável x, um conjunto de eventos A, e um processo P(x)

• Generalização da alternativa guardada (A pode ser infinito)

• STOP equivale a ?x:{} -> P(x)

Escolha Prefixada

• É uma abreviação para o operador indexado de escolha externa: ?x:A -> P(x)

corresponde a []x:A @ x -> P(x)

• Exemplo: Sigma = {a,b,up,down}

REPEAT =

[] x:Sigma @ x -> x -> REPEAT

Escolha Prefixada

• Canais tipados, com comunicação de dados através dos mesmos channel init:Int

NUM = {0..100}

INIT =

init?x:NUM -> LCOUNT(100,x)

• Família de eventos: c:T = {c.t | t T}

Eventos Compostos

DATA = {0,1}

channel left, right:DATA

COPY = left?x -> right!x -> COPY

Binf(s) =

if s==<> then

left?x -> Binf(<x>)

else (left?x -> Binf(s^<x>)

[]right!head(s) -> Binf(tail(s)))

Eventos Compostos

ATM1 = incard?c -> pin.fpin(c) ->

req?n -> dispense!n ->

outcard.c ->

channel incard, outcard:CARD

channel pin:PINs

channel req, dispense:WA

Exemplo

CARD = {0..9}

datatype pinnumbers = PIN.Int

fpin(c) = PIN.c

PINs = {fpin(c) | c <- CARD}

WA = {10,20,30,40,50}

Exemplo

• Do livro texto– Essenciais: 1.1.1, 1.1.2, 1.1.3– Opcionais: 1.1.5, 1.1.4

Exercícios