specification PBL2 [push,output] : noexit

  library BOOLEAN endlib 

  behaviour

    PBL_BODY[push,output]

  where

    process PBL_BODY [push,output] : noexit :=

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

    endproc

endspec