example4.rcp

channels: a, b

enum msgvals {get, msg1, msg2}

message-structure: MSG : msgvals
communication-variables: asgn : bool

agent Buffer
        local:  m1 : int, m2 : int
        init:  m1 == 0 && m2 == 0
        relabel:
            asgn <- false
        receive-guard: TRUE

        repeat: (
                    <(m1 > 0)> *! (TRUE)
                    (MSG := msg1)[m1:= m1 - 1]

                    +

                    <(m2 > 0)> *! (TRUE)
                    (MSG := msg2)[m2:= m2 - 1]

                    +

                    <(m1 > 0)> b? [m1:= m1 + 1]

                    +

                    <(m2 > 0)> b? [m2:= m2 + 1]


)

agent Producer
        local: size : int, no : int
        init: size == 4 && no == 0
        relabel:
            asgn <- false
        receive-guard: TRUE

        repeat: (

                    <TRUE> b! (TRUE)
                    (MSG := msg1)[]

                    +

                    <TRUE> b! (TRUE)
                    (MSG := msg2)[]

)

system = Buffer(one,TRUE) | Producer(two,TRUE) | Producer(three,TRUE)