specification PBL [push,on,off] : noexit

  behaviour

    PBL_BODY[push,on,off]

  where

    process PBL_BODY [push,out1,out2] : noexit :=

       push; out1; push; out2;
          PBL_BODY[push,out1,out2]

    endproc

endspec