Madiel de Souza Conserva Filho / bts

Blame view

BRIC/cspFiles/Comportamento.csp 253 Bytes
edit raw normal view history
eeb5cac08   Madiel de Souza Conserva Filho   first 
1
2
3
4
5
6
7
8
9
10
11
 
  
  datatype Direction = req | ack
  Value = {0..3}
  channel wrt : Direction.Value
  channel rd : Direction.Value
  
  Cell = 
    let CellState(val) =
      rd.req?dumb -> rd.ack!val -> CellState(val) [] wrt.req?x -> wrt.ack.x -> CellState(x)
    within
      CellState(0)