checklist-tester/formal/checklist.vdmsl

module Checklist
exports all
definitions

values

types
    String = seq of char;

    -- Aircraft

    -- Switches
    --@doc The state a switch can be in
    SwitchState = nat
        inv s == s <= 3;

    --@doc A switch, with the possible states it can be in, and the state that it is in
    Switch :: 
                position : nat1
                states : seq of SwitchState
                inv s == s.position <= len s.states;

    -- Knob
    Knob :: 
            position : nat1
            states : seq of int
            inv k == k.position <= len k.states;

    Lever = nat
        inv t == t <= 100;

    Throttle :: 
                thrust: Lever
                reverser: Lever
                inv t ==
                    if t.thrust > 0 then
                        t.reverser = 0
                    else 
                        t.reverser >= 0;

    --@doc The type that the action of the button is
    ItemType = <SWITCH> | <KNOB> | <BUTTON>;

    --@doc Item of a checklist, e.g. Landing gear down
    Item ::
            name : String
            type : ItemType
            object : Switch | Knob | Throttle;

    -- Checklist

    --@doc Item of a checklist, e.g. Landing gear down
    ChecklistItem ::
                    procedure : String
                    item : Item
                    checked : bool;

    --@doc A section of a checklist, e.g. Landing Checklist
    Section = seq of ChecklistItem;

    --@doc Full checklist, e.g. Startup, Descent, Landing Checklist
    Checklist = seq of Section;

functions

end Checklist