specification PBL4 [push,on,off] : noexit

  library BOOLEAN endlib 

  behaviour

    hide msg in

    PBL_BODY[push,msg]
    |[msg]|
    LIGHT2[msg,on,off](false of BOOL)

  where

    process PBL_BODY [push,msg] : noexit :=

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

    endproc

    process LIGHT2 [msg,on,off] (status:BOOL) : noexit :=

       msg ?output:BOOL;
       (
        [ (status eq (false of BOOL)) and (output eq (true of BOOL)) ]
           -> on; LIGHT2 [msg,on,off](true of BOOL)
        []
        [ (status eq (true of BOOL)) and (output eq (false of BOOL)) ]
           -> off; LIGHT2 [msg,on,off](false of BOOL)
       )

    endproc

endspec