module Checklist
exports all
definitions

values
    -- Before Start Checklist
    -- Items in Aircraft
    -- Flight Deck... (can't check)
    fuel: ItemObject = mk_ItemObject(<SWITCH>, mk_Switch(<OFF>, false));
    pax_sign: ItemObject = mk_ItemObject(<SWITCH>, mk_Switch(<OFF>, true));
    windows: ItemObject = mk_ItemObject(<SWITCH>, mk_Switch(<ON>, false));
    -- Preflight steps
    acol: ItemObject = mk_ItemObject(<SWITCH>, mk_Switch(<OFF>, false));

    aircraft_panels: Items = {"Fuel Pump" |-> fuel, "Passenger Signs" |-> pax_sign, "Windows" |-> windows, "Anti Collision Lights" |-> acol};

    -- Checklist
    -- Flight Deck... (can't check)
    fuel_chkl: ChecklistItem = mk_ChecklistItem("Fuel Pump", <SWITCH>, <ON>, false);
    pax_sign_chkl: ChecklistItem = mk_ChecklistItem("Passenger Signs", <SWITCH>, <ON>, false);
    windows_chkl: ChecklistItem = mk_ChecklistItem("Windows", <SWITCH>, <ON>, false);
    -- Preflight steps
    acol_chkl: ChecklistItem = mk_ChecklistItem("Anti Collision Lights", <SWITCH>, <ON>, false);

    before_start_procedure: Procedure = [fuel_chkl, pax_sign_chkl, windows_chkl, acol_chkl];

    aircraft = mk_Aircraft(aircraft_panels, before_start_procedure);
types
    --@doc The dataref name in X-Plane
    Dataref = seq1 of char;

    -- Aircraft

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

	--@LF why have a type kist as a rename?
    ItemState = SwitchState; --@TODO | Button | ...

    --@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 == 
            (s.position = <MIDDLE> => s.middlePosition);

    -- Knob
    Knob :: 
        position : nat
        --@LF how can a state be an int? perhaps a proper type (i..e. subset of int range or a union?)
        states : set1 of nat
        inv k ==
            k.position in set k.states;

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

    Throttle :: 
        thrust: Lever
        reverser: Lever
        inv t ==
            (t.reverser > 0 <=> t.thrust = 0);

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

    --@doc The unique switch/knob/etc of that aircraft
    ObjectType = Switch | Knob | Throttle;                
    ItemObject ::
        type : ItemType
        object : ObjectType
        inv mk_ItemObject(type, object) ==
        	cases type: 
        		<SWITCH> -> is_Switch(object),
        		<KNOB>   -> is_Knob(object),
        		<THROTTLE>-> is_Throttle(object),
        		--<BUTTON> -> true
        		others -> true
        	end;

    --@doc Contains each ItemObject in the Aircraft, e.g. Fuel Pump switch
    Items = map Dataref to ItemObject;

    --@doc Contains the panels (all the items in the aircraft) and the procedure
    Aircraft ::
        items : Items
        procedure : Procedure
        inv mk_Aircraft(i, p) ==
        ({ x.procedure | x in seq p } subset dom i);

    -- Checklist

    --@doc Item of a checklist, e.g. Landing gear down
    ChecklistItem ::
        --@LF again, empty string here doesn't make sense.
        procedure : Dataref
        type : ItemType
        --TODO Check is not only SwitchState
        check : SwitchState
        checked : bool;

    --@doc This is an item in the aircraft that complements the item in the procedure
    ItemAndChecklistItem ::
        item : ItemObject
        checklistItem: ChecklistItem
        inv i == i.item.type = i.checklistItem.type;

    --@doc A section of a checklist, e.g. Landing Checklist
    --@LF shouldn't this be non-empty? What's the point to map a checklist name to an empty procedure? Yes.
    Procedure = seq1 of ChecklistItem
        inv p == 
            --@LF the "trick" for "false not in set S" is neat. It forces a full evaluation, rather than short circuited (i.e. stops at first false).
            --    I presume this was intended.
            false not in set { 
                let first = p(x-1).checked, second = p(x).checked in 
                	--@LF boolean values don't need equality check
                    second => first--((first = true) and (second = false))
                | x in set {2,...,len p}};

functions
    -- PROCEDURES
    --@doc Finds the index of the next item in the procedure that needs to be completed
    procedure_next_item_index: Procedure -> nat1
    procedure_next_item_index(p) ==
        hd [ x | x in set {1,...,len p} & not p(x).checked ]--p(x).checked = false]
    pre
        -- Checks procedure has not already been completed
        not procedure_completed(p)--procedure_completed(p) = false
    post
    	-- Checks that the index of the item is the next one to be completed
        --@LF your def is quite confusing (to me)
        --@LF how do you know that RESULT in inds p? Well, the definition above okay.
        --    but you can't know whether p(RESULT-1) will! What if RESULT=1? p(RESULT-1)=p(0) which is invalid!
        (not p(RESULT).checked)
    	and 
    	(RESULT > 1 => p(RESULT-1).checked)
        --p(RESULT).checked = false
        --and if RESULT > 1 then 
        --    p(RESULT-1).checked = true
        --else 
        --    true
        ;

    -- --@doc Checks if all the procedures have been completed
    -- check_all_proc_completed: Checklist -> bool
    -- check_all_proc_completed(c) ==
    --     false not in set { procedure_completed(c(x)) | x in set {1,...,len c} };

    -- --@doc Gives the index for the next procedure to complete
    -- next_procedure: Checklist -> nat1
    -- next_procedure(c) ==
    --     hd [ x | x in set {1,...,len c} & not procedure_completed(c(x))]
    -- post
    --     RESULT <= len c;

    --@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) ==
        --@LF here you have a nice lemma to prove: procedure_next_item_index(p) in set inds p! 
        --	  I think that's always true
        let procItem = p(procedure_next_item_index(p)),
        	--@LF here you can't tell whether this will be true? i.e. procItem.procedure in set dom a.items?
            item = a.items(procItem.procedure) in
            
            --TODO need to be able to check for different types of Items
            procItem.check = item.object.position
    pre
        procedure_completed(p) = false
        --@LF perhaps add 
        --and
        --p(procedure_next_item_index(p)).procedure in set dom a.items?  
        ;

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

    --@doc Completes an item in the procedure
    do_proc_item: ItemObject * ChecklistItem -> ItemAndChecklistItem
    do_proc_item(i, p) ==
        let objective = p.check,
            checkckItem = complete_item(p) in
            -- Checks if the item is in the objective desired by the checklist
            if check_item_in_position(i, objective) then
                mk_ItemAndChecklistItem(i, checkckItem)
            else
                mk_ItemAndChecklistItem(move_item(i, p.check), checkckItem)
    pre
        p.checked = false
    post
        -- Checks the item has been moved correctly
        check_item_in_position(RESULT.item, p.check);

    --@doc Completes a procedure step by step
    -- a = Aircraft
    complete_procedure: Aircraft -> Aircraft
    complete_procedure(a) ==
        let procedure = a.procedure in
            mk_Aircraft(
                a.items ++ { x.procedure |-> do_proc_item(a.items(x.procedure), x).item | x in seq procedure },
                [ complete_item(x) | x in seq procedure ]
            )
    pre
        not procedure_completed(a.procedure)
    post
        procedure_completed(RESULT.procedure);

    -- 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 Moves any type of Item
    move_item: ItemObject * ItemState -> ItemObject
    move_item(i, s) ==
        -- if is_Switch(i) then (implement later)
            let switch: Switch = i.object in
                if check_switch_onoff(switch) and (s <> <MIDDLE>) and switch.middlePosition then
                    mk_ItemObject(i.type, move_switch(move_switch(switch, <MIDDLE>), s))
                else
                    mk_ItemObject(i.type, move_switch(switch, s))
    pre
        wf_item_itemstate(i, s)
        and not check_item_in_position(i, s);
        -- and wf_switch_move(i.object, s);

    --@doc Moves a specific switch in the aircraft
    move_switch: Switch * SwitchState -> Switch
    move_switch(i, s) ==
        mk_Switch(s, i.middlePosition)
    pre
        wf_switch_move(i, s)       
    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>
    post
        -- Only one can be true at a time
        -- If the switch is in the middle position, then RESULT cannot be true
        -- If the switch is in the on/off position, then the RESULT will be true 
        (s.position = <MIDDLE>) <> RESULT;

    --@doc Checks if the item is already in position for the desired state for that item
    check_item_in_position: ItemObject * 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: ItemObject * ItemState -> bool
    wf_item_itemstate(i, s) ==
        (is_Switch(i.object) and is_SwitchState(s) and i.type = <SWITCH>)
        --TODO check that the item has not already been completed before moving item
        --TODO add other types of Items
        ;

    --@doc Checks if the move of the Switch is a valid
    wf_switch_move: Switch * SwitchState -> bool
    wf_switch_move(i, s) ==
        -- 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>;


end Checklist

/*
//@LF always a good idea to run "qc" on your model. Here is its output. PO 21 and 22 show a problem.
//@LF silly me, this was my encoding with the cases missing one pattern :-). I can see yours has no issues. Good.

> qc
PO #1, PROVABLE by finite types in 0.002s
PO #2, PROVABLE by finite types in 0.0s
PO #3, PROVABLE by finite types in 0.0s
PO #4, PROVABLE by finite types in 0.0s
PO #5, PROVABLE by finite types in 0.0s
PO #6, PROVABLE by finite types in 0.0s
PO #7, PROVABLE by finite types in 0.0s
PO #8, PROVABLE by finite types in 0.0s
PO #9, PROVABLE by finite types in 0.001s
PO #10, PROVABLE by finite types in 0.001s
PO #11, PROVABLE by direct (body is total) in 0.003s
PO #12, PROVABLE by witness s = mk_Switch(<MIDDLE>, true) in 0.001s
PO #13, PROVABLE by direct (body is total) in 0.001s
PO #14, PROVABLE by witness k = mk_Knob(1, [-2]) in 0.0s
PO #15, PROVABLE by direct (body is total) in 0.0s
PO #16, PROVABLE by witness t = 0 in 0.0s
PO #17, PROVABLE by direct (body is total) in 0.001s
PO #18, PROVABLE by witness t = mk_Throttle(0, 0) in 0.001s
PO #19, PROVABLE by direct (body is total) in 0.002s
PO #20, PROVABLE by witness i = mk_ItemObject(<KNOB>, mk_Knob(1, [-1])) in 0.002s
PO #21, FAILED in 0.002s: Counterexample: type = <BUTTON>, object = mk_Knob(1, [-1])
Causes Error 4004: No cases apply for <BUTTON> in 'Checklist' (formal/checklist.vdmsl) at line 119:13
----
ItemObject': total function obligation in 'Checklist' (formal/checklist.vdmsl) at line 118:13
(forall mk_ItemObject'(type, object):ItemObject'! &
  is_(inv_ItemObject'(mk_ItemObject'!(type, object)), bool))

PO #22, FAILED by direct in 0.005s: Counterexample: type = <BUTTON>
PO #23, PROVABLE by witness type = <KNOB>, object = mk_Knob(1, [-1]) in 0.002s
PO #24, PROVABLE by direct (body is total) in 0.001s
PO #25, PROVABLE by witness i = mk_ItemAndChecklistItem(mk_ItemObject(<KNOB>, mk_Knob(1, [-1])), mk_ChecklistItem([], <KNOB>, <MIDDLE>, true)) in 0.001s
PO #26, MAYBE in 0.003s
PO #27, MAYBE in 0.003s
PO #28, MAYBE in 0.002s
PO #29, PROVABLE by witness p = [mk_ChecklistItem([], <BUTTON>, <MIDDLE>, true)] in 0.001s
PO #30, MAYBE in 0.002s
PO #31, MAYBE in 0.001s
PO #32, MAYBE in 0.003s
PO #33, MAYBE in 0.002s
PO #34, MAYBE in 0.001s
PO #35, MAYBE in 0.002s
PO #36, MAYBE in 0.009s
PO #37, MAYBE in 0.008s
PO #38, MAYBE in 0.007s
PO #39, MAYBE in 0.009s
PO #40, MAYBE in 0.002s
PO #41, MAYBE in 0.001s
PO #42, MAYBE in 0.001s
PO #43, MAYBE in 0.002s
PO #44, MAYBE in 0.002s
PO #45, MAYBE in 0.003s
PO #46, MAYBE in 0.002s
PO #47, MAYBE in 0.002s
PO #48, MAYBE in 0.001s
PO #49, MAYBE in 0.001s
PO #50, MAYBE in 0.0s
PO #51, MAYBE in 0.0s
PO #52, MAYBE in 0.005s
PO #53, PROVABLE by trivial p in set (dom checklist) in 0.001s
PO #54, MAYBE in 0.006s
PO #55, MAYBE in 0.0s
PO #56, MAYBE in 0.001s
PO #57, MAYBE in 0.001s
PO #58, MAYBE in 0.001s
PO #59, MAYBE in 0.001s
PO #60, MAYBE in 0.001s
PO #61, MAYBE in 0.001s
PO #62, MAYBE in 0.0s
PO #63, PROVABLE by finite types in 0.001s
PO #64, PROVABLE by finite types in 0.001s
PO #65, PROVABLE by finite types in 0.001s
PO #66, MAYBE in 0.001s
> 
*/