specification exa4_11[req,done] : noexit

  behaviour

    hide act1,act2,act3 in

      P1[req,act1,done]
      |[req,done]|
      P1[req,act2,done]
      |[req,done]|
      P1[req,act3,done]

  where

    process P1 [req, act, done] : noexit :=
       req; act; done;
          P1[req,act,done]
    endproc

endspec