smyalygames/checklist-tester
1
0
Fork 0
mirror of https://github.com/smyalygames/checklist-tester.git synced 2025-05-18 14:34:12 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity

feat(formal): add completing procedures with aircraft return

Browse Source
This commit is contained in:
Anthony 2024-03-28 18:33:49 +01:00
parent ba295063ca
commit 9911305bab
1 changed files with 14 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
formal/checklist.vdmsl
View File

@ -262,14 +262,20 @@ functions
n in set dom a.checklist; n in set dom a.checklist;
--@doc Completes a procedure step by step --@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: String * Aircraft -> Aircraft
complete_procedure(p, a) == complete_procedure(n, a) ==
is not yet specified 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 pre
let checklist = a.checklist in let checklist = a.checklist in
p in set dom checklist n in set dom checklist
and not procedure_completed(checklist(p)); and not procedure_completed(checklist(n))
post
procedure_completed(RESULT.checklist(n));
-- AIRCRAFT ITEMS -- AIRCRAFT ITEMS
--@doc Marks ChecklistItem as complete --@doc Marks ChecklistItem as complete
@ -284,14 +290,14 @@ functions
move_item(i, s) == move_item(i, s) ==
-- if is_Switch(i) then (implement later) -- if is_Switch(i) then (implement later)
let switch: Switch = i.object in let switch: Switch = i.object in
if check_switch_onoff(switch) and (s <> <MIDDLE>) then if check_switch_onoff(switch) and (s <> <MIDDLE>) and switch.middlePosition then
mk_ItemObject(i.type, move_switch(move_switch(switch, <MIDDLE>), s)) mk_ItemObject(i.type, move_switch(move_switch(switch, <MIDDLE>), s))
else else
mk_ItemObject(i.type, move_switch(switch, s)) mk_ItemObject(i.type, move_switch(switch, s))
pre pre
wf_item_itemstate(i, s) wf_item_itemstate(i, s)
and not check_item_in_position(i, s) and not check_item_in_position(i, s);
and (wf_switch_move(i.object, s)); -- and wf_switch_move(i.object, s);
--@doc Moves a specific switch in the aircraft --@doc Moves a specific switch in the aircraft
move_switch: Switch * SwitchState -> Switch move_switch: Switch * SwitchState -> Switch