-- Binding for videotape-style playing of a stream of data.  Communication
-- failure is not handled in this example, although it could be extended to
-- allow such failures.
--
-- $Id: videoTape.fin,v 1.1 1997/11/24 03:49:39 andyb Exp $

Binding VideoTape {

  Import RPC;

  Roles {

    Producer(DATA) {
      
      { -- receive play notification
        play?() ->   

          -- sending with sequence number generation repeating until the next
          -- pause or finished.  Guards on event occurence are prefixed and
          -- enclosed in sqare brackets.  The '*+' operator says 'iterate
          -- sequentially until the postfix iteration guard is false.'
          send!(seqnr, DATA) -> 
            [seqnr = prev.seqnr+1] send!(seqnr, DATA)
              *+[occur(finish) OR (occur(pause.receive) AND 
                 end(pause.receive) > end(play))] 
	
          -- a pause RPC can optionally occur.  The 'OR' operator has 'either
          -- or both' semantics.
          OR pause {RPC.server()}
         
       } *+[occur(finish)] -- repeating until a finish is emitted

       AND finish!()
    }


    Consumer(DATA) {

      { -- start stream, no parameters necessary
        play!() ->

        -- receiving with correct ordering and requiring a
        -- minimum frame delivery rate of 20 frames/sec
        receive?(seqnr, DATA) -> 
          [seqnr = prev.seqnr+1; now - end(prev) < 0.05] receive?(seqnr, DATA) 
            *+[occur(finish) OR (occur(pause.receive) AND 
               end(pause.receive) > end(play))]

          -- the consumer can execute a pause RPC  
          OR pause {RPC.client()}

      } *+[occur(finish)] -- repeating until a finish is received

      AND finish?()
    }
  }


  Interactions {
    { -- the play notification requires delivery
      Consumer.play -> Producer.play AND

      -- basic streaming transmission behaviour.  The '*-' indicates parallel
      -- iteration, and in this case implies that producing the next element of
      -- the stream is not dependent on the receipt of the previous element
      -- (effectively implies some form of sliding window protocol).
      {Producer.send -> Consumer.receive {*= prev} } *-

      -- the pause RPC can occur
      RPC(Consumer.stop, Producer.stop)

    } *+  -- repeat, loops guarded in roles

    AND Producer.finish -> Consumer.finish
  }
}



--
-- Revision history:
-- 
-- $Log: videoTape.fin,v $
-- Revision 1.1  1997/11/24 03:49:39  andyb
-- Initial version used for OMG/DARPA workshop position statement.
--
--