-- The specification of the example "press delete button", to motivate
-- the application of CSP
-- Author: H. Shi
-- Date: 2006-05-08


-- Definition of datatypes
-- -----------------------
datatype MOUSE_BUTTON = depress | release | move_off
datatype DELETE_BUTTON = highlight | remove_highlight
datatype TEXT = change | not_change

-- Specification of channels
-- -------------------------
channel mouse: MOUSE_BUTTON
channel delete: DELETE_BUTTON
channel text: TEXT
channel do_delete

-- Sepcification of system components
-- ----------------------------------
User = mouse.depress -> 
       (mouse.release -> SKIP
        []
        mouse.move_off -> mouse.release -> SKIP)

Screen = delete.highlight -> delete.remove_highlight ->
         (text.change -> SKIP [] SKIP)

Dialog = mouse.depress -> delete.highlight ->
         (mouse.release -> do_delete
                        -> delete.remove_highlight -> SKIP
          []
          mouse.move_off -> delete.remove_highlight
                         -> mouse.release -> SKIP)

Application = do_delete -> text.change -> SKIP
              []
              SKIP

-- Specification of the interaction between the components
-- -------------------------------------------------------
SYS = ((User [|{| mouse |}|] Dialog)
      [|{| delete |}|] Screen)
      [|{| text, do_delete |}|] Application


SCREEN_HIT = mouse.depress -> delete.highlight 
          -> mouse.release -> do_delete
          -> delete.remove_highlight
          -> text.change -> SKIP

SCREEN_MISS = mouse.depress -> delete.highlight 
           -> mouse.move_off -> delete.remove_highlight
           -> mouse.release -> SKIP

-- Asserts
-- -------

assert SYS [T= SCREEN_HIT
assert SYS [T= SCREEN_MISS