Models the Graphical User Interface, based upon the control console of a real medical device, though the same technique can be applied to any event driven system

The Z text is illustrated with a statechart. The system design is split into largely independent subsystems which can include both data and operations on that data, (as with C++ classes).

The Console state incorporates different displays and is concerned with the dialogue from the user who enters a setting via a text input and an accept button in a dialogue box on screen.

An event occurs through a mouse click or a keystroke to change the console state.

• The disp function returns an appropriate display on event instantiation.
• A display is selected by pressing a function key to activate an event operation and if the console is not in dialogue mode.
• If a dialogue is in progress attempts to select a new display are ignored.

• Is modelled by SelectSetting (user selects setting and dialogue begins).
• As the user types in a new value each keystroke invokes GetChar.
• Finally the user may Accept the new value or Cancel the dialogue.
• If the user attempts to enter an invalid setting the system Reprompts.

• The stg function returns an appropriate setting value on event instantiation.
• SelectSetting occurs when the user clicks on a setting name displayed on screen.
• A dialogue box appears on screen and a dialogue begins with empty text.
• Typing a new value each time the user hits the alphanumeric keys causes an event to occur.
• GetChar handles that event.
• char extracts the new character and edit updates the buffer.
• When the console is not engaged in dialogue the alphanumeric characters are ignored.

• Users may Accept by clicking the accept button in the dialogue box.
• The system converts the text in the buffer to a value, which if valid is used to update the setting.
• The dialogue box disappears when the dialogue ends.
• If the value derived from the buffer is not valid, Reprompt dialogue continues.
• Alternatively the user may Cancel by clicking on an appropriate button in the dialogue box.

• The Machine state is determined by the values of its settings.
• prescribed settings download from prescriptions, measured settings are read from sensors.
• NewSetting describes the change to the machine when a new value is assigned a prescribed setting.
• Note that the system comprises both Console and Machine.
• ChangeSetting describes the change to the system when the user edits a setting.
• Other operations can be extended to show the machine state is unaffected by most Ul activity.

[DISPLAY,SETTING,VALUE,CHAR]

TEXT == seq CHAR

MODE ::= idle | dialog

BUTTON ::= accept | cancel

ÚÄConsoleÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ display : DISPLAY
³ mode : MODE
³ buffer : TEXT
³ setting : SETTING
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

[EVENT]

ÚÄEventÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œConsole
³ e? : EVENT
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

Many events are simply ignored (they do not change the Console state).

Ignore ¡ Event ™ �Console

³ disp : EVENT �‹Ž DISPLAY

ÚÄSelectDisplayÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Event
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ mode = idle
³ e? î dom disp
³ display' = disp e?
³ mode' = mode
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄIgnoreDisplayÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Ignore
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ e? î dom disp
³ mode = dialog
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

We use schema disjunction to combine the two cases.

DisplayEvent ¡ SelectDisplay ˜ IgnoreDisplay

³ stg : EVENT �‹Ž SETTING

ÚÄSelectSettingÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Event
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ mode = idle
³ e? î dom stg
³ setting' = stg e?
³ mode' = dialog
³ buffer' = í
³ display' = display
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

If a dialog is already underway, this operation is disabled.

ÚÄIgnoreSettingÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Ignore
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ e? î dom stg
³ mode = dialog
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

SettingEvent ¡ SelectSetting ˜ IgnoreSetting

ÚÄGetCharÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Event
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ mode = dialog
³ e? î dom char
³ buffer' = edit (buffer,char e?)
³ mode' = mode
³ setting' = setting
³ display' = display
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄIgnoreCharÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Ignore
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ e? î dom char
³ mode = idle
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

CharEvent ¡ GetChar ˜ IgnoreChar

³ button : EVENT �‹Ž BUTTON
³ value : TEXT �ŠŽ VALUE
³ vaild_ : SETTING ‘ŠŽ VALUE

ÚÄAcceptÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Event
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ mode = dialog
³ e? î dom button
³ button e? = accept
³ valid(setting, value buffer)
³ mode' = idle
³ display' = display
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄRepromptÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Event
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ mode = dialog
³ e? î dom button
³ button e? = accept
³ ‰ valid(setting, value buffer)
³ buffer' = buffer
³ mode' = mode
³ display' = display
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄCancelÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Event
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ mode = dialog
³ e? î dom button
³ button e? = cancel
³ mode' = idle
³ display' = display
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ButtonEvent ¡ Accept ˜ Cancel ˜ Reprompt

ÚÄMachineÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ measured,prescribed : SETTING �ŠŽ VALUE
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

The NewSetting operation describes what happens in the Machine when a new value v? is assigned to prescribed setting s?.

ÚÄSysÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ Console
³ Machine
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

ÚÄChangeSettingÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ¿
³ œSys
³ Accept
³ NewSetting
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
³ s? = setting
³ v? = value buffer
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ

SysDisplayEvent ¡ DisplayEvent ™ �Machine

SysSettingEvent ¡ SettingEvent ™ �Machine

SysCharEvent ¡ CharEvent ™ �Machine

SysButtonEvent ¡ ChangeSetting ˜ (Reprompt ™ �Machine) ˜ (Cancel ™ �Machine)