From 9911305babffd56ccdb051d5d28d875a6de73696 Mon Sep 17 00:00:00 2001 From: Anthony Date: Thu, 28 Mar 2024 18:33:49 +0100 Subject: [PATCH] feat(formal): add completing procedures with aircraft return --- formal/checklist.vdmsl | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl index d119e36..b74004a 100644 --- a/formal/checklist.vdmsl +++ b/formal/checklist.vdmsl @@ -262,14 +262,20 @@ functions n in set dom a.checklist; --@doc Completes a procedure step by step - -- p = Name of procedure, a = Aircraft + -- n = Name of procedure, a = Aircraft complete_procedure: String * Aircraft -> Aircraft - complete_procedure(p, a) == - is not yet specified + complete_procedure(n, a) == + let procedure = get_procedure(n, a) in + mk_Aircraft( + a.items ++ { x.procedure |-> do_proc_item(a.items(x.procedure), x).item | x in seq procedure }, + a.checklist ++ { n |-> [ complete_item(x) | x in seq procedure ] } + ) pre let checklist = a.checklist in - p in set dom checklist - and not procedure_completed(checklist(p)); + n in set dom checklist + and not procedure_completed(checklist(n)) + post + procedure_completed(RESULT.checklist(n)); -- AIRCRAFT ITEMS --@doc Marks ChecklistItem as complete @@ -284,14 +290,14 @@ functions move_item(i, s) == -- if is_Switch(i) then (implement later) let switch: Switch = i.object in - if check_switch_onoff(switch) and (s <> ) then + if check_switch_onoff(switch) and (s <> ) and switch.middlePosition then mk_ItemObject(i.type, move_switch(move_switch(switch, ), 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)); + 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