specification PBL3 [push,on,off] : noexit

  library BOOLEAN endlib 

  behaviour

    hide msg in

    PBL_BODY[push,msg]
    |[msg]|
    LIGHT[msg,on,off]

  where

    process PBL_BODY [push,msg] : noexit :=

       push; msg !(true of BOOL);
       push; msg !(false of BOOL);
          PBL_BODY[push,msg]

    endproc

    process LIGHT [msg,on,off] : noexit :=

       msg ?output:BOOL;
       (
        [ output eq (true of BOOL) ] -> on;exit
        []
        [ output eq (false of BOOL) ] -> off;exit
       )
        >> LIGHT [msg,on,off]

    endproc

endspec