button.mch

MACHINE button
DEFINITIONS "LibraryMeta.def"
VARIABLES
  button
INVARIANT
  button:BOOL
INITIALISATION
  button := FALSE
OPERATIONS
  press_button = PRE button=FALSE THEN
    button:=TRUE
  END;
  toggle_button = BEGIN
    button:= bool(button=FALSE)
  END;
  set_button(newVal) = PRE newVal:BOOL THEN
     button := bool(newVal=TRUE)
  END
END