module Checklist
exports all
definitions

values
    -- Before Start Checklist
    -- Items in Aircraft
    -- Flight Deck... (can't check)
    fuel: Item = mk_Item("Fuel Pump", <SWITCH>, mk_Switch(<OFF>, false));
    pax_sign: Item = mk_Item("Passenger Signs", <SWITCH>, mk_Switch(<OFF>, true));
    windows: Item = mk_Item("Windows", <SWITCH>, mk_Switch(<ON>, false));
    -- Preflight steps
    acol: Item = mk_Item("Anti Collision Lights", <SWITCH>, mk_Switch(<OFF>, false));

    aircraft: Aircraft = [fuel, pax_sign, windows, acol];

    -- Checklist
    -- Flight Deck... (can't check)
    fuel_chkl: ChecklistItem = mk_ChecklistItem(fuel.name, <SWITCH>, <ON>, false);
    pax_sign_chkl: ChecklistItem = mk_ChecklistItem(pax_sign.name, <SWITCH>, <ON>, false);
    windows_chkl: ChecklistItem = mk_ChecklistItem(windows.name, <SWITCH>, <ON>, false);
    -- Preflight steps
    acol_chkl: ChecklistItem = mk_ChecklistItem(acol.name, <SWITCH>, <ON>, false);

    before_start_procedure: Procedure = [fuel_chkl, pax_sign_chkl, windows_chkl, acol_chkl];
types
    String = seq of char;

    -- Aircraft

    -- Switches
    --@doc The state a switch can be in
    -- 1 means off
    SwitchState = <OFF> | <MIDDLE> | <ON>;

    ItemState = SwitchState;

    --@doc A switch, with the possible states it can be in, and the state that it is in
    Switch :: 
                position : SwitchState
                middlePosition : bool
                inv s == 
                    if s.middlePosition = false then 
                        s.position <> <MIDDLE>
                    else true;

    -- 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;

    --@doc Aircraft contains all the controls
    Aircraft = seq of Item;

    -- Checklist

    --@doc Item of a checklist, e.g. Landing gear down
    ChecklistItem ::
                    procedure : String
                    type : ItemType
                    --TODO Check is not only SwitchState
                    check : SwitchState
                    checked : bool;

    --@doc A section of a checklist, e.g. Landing Checklist
    Procedure = seq of ChecklistItem
        inv p == 
            len p > 0 and
            false not in set { 
                let first = p(x-1).checked, second = p(x).checked in 
                    (first = second) or ((first = true) and (second = false))
                | x in set {2,...,len p}};
    
    --@doc Full checklist, e.g. Startup, Descent, Landing Checklist
    Checklist = seq of Procedure;

functions
    -- PROCEDURES
    --@doc Finds the index of the next item in the procedure that needs to be completed
    procedure_next_index: Procedure -> nat1
    procedure_next_index(p) ==
        hd [ x | x in set {1,...,len p} & p(x).checked = false]
    pre
        -- Checks procedure has not already been completed
        procedure_completed(p) = false
    post
        -- Checks that the index of the item is the next one to be completed
        p(RESULT).checked = false
        and if RESULT > 1 then 
            p(RESULT-1).checked = true
        else 
            true;

    --@doc Checks if the procedure has been completed
    procedure_completed: Procedure -> bool
    procedure_completed(p) ==
        false not in set { p(x).checked | x in set {1,...,len p} };

    --@doc Checks if the next item in the procedure has been completed
    check_proc_item_complete: Procedure * Aircraft -> bool
    check_proc_item_complete(p, a) ==
        let procItem = p(procedure_next_index(p)),
            itemIndex = index_of_item(procItem.procedure, a),
            item = a(itemIndex) in
            
            --TODO need to be able to check for different types of Items
            procItem.check = item.object.position
    pre
        procedure_completed(p) = false;

    --@doc Marks next item in procedure as complete
    mark_proc_item_complete: Procedure -> Procedure
    mark_proc_item_complete(p) ==
        let i = procedure_next_index(p), item = p(i) in
            p ++ {i |-> complete_item(item)}
        pre
            procedure_completed(p) = false;

    --@doc Completes an Item in the procedure on the Aircraft
    do_proc_item: ChecklistItem * Aircraft -> Aircraft
    do_proc_item(p, a) ==
        let itemIndex = index_of_item(p.procedure, a), item = a(itemIndex), objective = p.check in
            -- Checks if the item is in the objective desired by the checklist
            if check_item_in_position(item, objective) then
                a
            else
                a ++ {itemIndex |-> move_item(a(itemIndex), objective)}
    pre
        p.checked = false;

    -- AIRCRAFT ITEMS
    --@doc Marks ChecklistItem as complete
    complete_item: ChecklistItem -> ChecklistItem
    complete_item(i) ==
        mk_ChecklistItem(i.procedure, i.type, i.check, true)
    pre
        i.checked = false;

    --@doc Find index of an item in Aircraft
    index_of_item: String * Aircraft -> nat1
    index_of_item(i, a) ==
        if (hd a).name = i then
            1
        else 
            index_of_item(i, tl a) + 1
    pre
        len a > 0
        -- Checks the Item being searched for is in the Aircraft
        and i in set { a(x).name | x in set {1,...,len a} }
    post
        -- Checks that the index is correct
        --TODO this does not check if it is the first item in the list
        if RESULT > 1 then
            a(RESULT).name = i
        else
            true
    measure len a;

    --@doc Moves any type of Item
    move_item: Item * ItemState -> Item
    move_item(i, s) ==
        -- if is_Switch(i) then (implement later)
            mk_Item(i.name, i.type, move_switch(i.object, s))
    pre
        wf_item_itemstate(i, s) and
        not check_item_in_position(i, s);

    --@doc Moves a specific switch in the aircraft
    move_switch: Switch * SwitchState -> Switch
    move_switch(i, s) ==
        mk_Switch(s, i.middlePosition)
    pre
        -- Checks that the switch not already in the desired state
        i.position <> s and
        -- The switch has to move one at a time
        -- Reasoning for this is that some switches cannot be moved in one quick move
        if i.middlePosition = true then
            -- Checks moving the switch away from the middle position
            (i.position = <MIDDLE> and s <> <MIDDLE>)
            -- Checks moving the siwtch to the middle position
            <> (check_switch_onoff(i) = true and s = <MIDDLE>)
        else
            check_switch_onoff(i) and s <> <MIDDLE>
        post
            RESULT.position = s;

    --@doc Checks if the switch is in the on or off position
    check_switch_onoff: Switch -> bool
    check_switch_onoff(s) ==
        let position = s.position in
            position = <OFF> or position = <ON>;

    --@doc Checks if the item is already in position for the desired state for that item
    check_item_in_position: Item * ItemState -> bool
    check_item_in_position(i, s) ==
        -- if is_Switch(i) then (implement later)
            i.object.position = s
    pre
        wf_item_itemstate(i,s);

    --@doc Checks if the Item.object is the same type for the ItemState
    wf_item_itemstate: Item * ItemState -> bool
    wf_item_itemstate(i, s) ==
        (is_Switch(i.object) and is_SwitchState(s))
        --TODO check that the item has not already been completed before moving item
        --TODO add other types of Items
        ;


end Checklist