Modelagem em CSP através da
Function: Single Left/Right
Consolidation
Aluno: Leandro Santana de Melo.
Professor: Dr. Alexandre Cabral Mota
Recife, Agosto de 2014
Agenda

O que é Function
Consolidation;
Single
Left/Rigth

Modelagem da Function Single Left/Rigth
Consolidation em CSP.
2
O que é Function Single Left/Rigth
Consolidation

Nada mais é do que um sistema onde
acontece uma consolidação de um
seletor para esquerda/direta.
3
O que é Function Single Left/Rigth
Consolidation
4
O que é Function Single Left/Rigth
Consolidation

Quando o Seletor estiver na posição
Esquerda/Direita,
acontece
uma
liberação de sinal para 3 canais.

Cada canal recebe um valor true/false
dependendo da sua condição: Ou seja,
se estiver na posição Esquerda é
liberado um sinal para o canal1,
canal2, canal3. E se ele estiver na
posição direita acontecera a mesma
coisa.
5
O que é Function Single Left/Rigth
Consolidation
Cada
um desses canais possuem um;
 Validade
de confirmação;
Valor de confirmação;
Validade de direta;
Valor direita;
Validade esquerda;
Valor esquerda.
6
O que é Function Single Left/Rigth
Consolidation
 Pois
bem, quando o seletor estiver na
posição mencionada anteriormente,
será emitido valores booleanos do tipo
true para:
Validade de Confirmação;
Valor de Confirmação;
Valor direito e validade direito.
Já para Valor e Validade esquerdo o
valor Booleano será false
A mesma coisa caso estever na
direita

7
O que é Function Single Left/Rigth
Consolidation

E o computador recebe os sinais do
canal 1, canal 2, canal 3.
8
Modelagem da Function Single
Left/Rigth Consolidation em
CSP.

channel left, right, confirmation: Bool

datatype CHType = CH1 | CH2 | CH3

datatype CommandType = LEFT | RIGHT | CONFIRMATION

datatype CommandValueType = VALUE | VALIDITY | CONSOLIDATED

channel ch_left_value, ch_left_validity, ch_left_conf, ch_right_value,
ch_right_validity, ch_right_conf: CHType.Bool

channel ch: CHType.CommandType.CommandValueType.Bool

-- ch_left_value.CH1.true -----> ch.CH1.LEFT.VALUE.true

channel validity_more_than1

channel decide : Bool

channel left_value, left_validity : Bool
9
Modelagem da Function Single
Left/Rigth Consolidation em
CSP.

CH(i) =

let

READ =

left?l -> right?r -> confirmation?c -> PROCESS_OUTPUT(l,r,c)

PROCESS_OUTPUT(l,r,c) =

decide?vld -> PROCESS_OUTPUT_CH(ch_left_value, ch_left_validity, l, vld);

decide?vld -> PROCESS_OUTPUT_CH(ch_right_value, ch_right_validity, r, vld)

PROCESS_OUTPUT_CH(ve, vy, vl, vld) =

if vld then

ve.i.vl -> PROCESS_OUTPUT_VLD(vy, vld)

else

ve.i?vl -> PROCESS_OUTPUT_VLD(vy, vld)

PROCESS_OUTPUT_VLD(vy, vld) =

vy.i.vld -> SKIP

within READ \ {|decide|}

CHS = ||| i : CHType @ CH(i)
10
Modelagem da Function Single
Left/Rigth Consolidation em
CSP.

COMPUTER =

let

cv(vl,vld) = if vld then vl else false

within

ch_left_value.CH1?vlch1 -> ch_left_validity.CH1?vldch1 ->

ch_left_value.CH2?vlch2 -> ch_left_validity.CH2?vldch2 ->

ch_left_value.CH3?vlch3 -> ch_left_validity.CH3?vldch3 ->SKIP
11