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 items in procedure

Browse Source
This commit is contained in:
Anthony Berg 2024-03-07 17:07:42 +00:00
parent 546aac34d0
commit 53ee06cfd6
1 changed files with 31 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
formal/checklist.vdmsl
View File

@ -78,12 +78,14 @@ types
ChecklistItem :: ChecklistItem ::
procedure : String procedure : String
type : ItemType type : ItemType
--TODO Check is not only SwitchState
check : SwitchState check : SwitchState
checked : bool; checked : bool;
--@doc A section of a checklist, e.g. Landing Checklist --@doc A section of a checklist, e.g. Landing Checklist
Procedure = seq of ChecklistItem Procedure = seq of ChecklistItem
inv p == inv p ==
len p > 0 and
false not in set { false not in set {
let first = p(x-1).checked, second = p(x).checked in let first = p(x-1).checked, second = p(x).checked in
(first = second) or ((first = true) and (second = false)) (first = second) or ((first = true) and (second = false))
@ -98,9 +100,8 @@ functions
procedure_next_index(p) == procedure_next_index(p) ==
hd [ x | x in set {1,...,len p} & p(x).checked = false] hd [ x | x in set {1,...,len p} & p(x).checked = false]
pre pre
-- Checks to prevent getting the head of an empty sequence -- Checks procedure has not already been completed
len p > 0 procedure_completed(p) = false
and procedure_completed(p) = false
post post
-- Checks that the index of the item is the next one to be completed -- Checks that the index of the item is the next one to be completed
p(RESULT).checked = false p(RESULT).checked = false
@ -114,6 +115,33 @@ functions
procedure_completed(p) == procedure_completed(p) ==
false not in set { p(x).checked | x in set {1,...,len 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 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 --@doc Find index of an item in Aircraft
index_of_item: String * Aircraft -> nat1 index_of_item: String * Aircraft -> nat1
index_of_item(i, a) == index_of_item(i, a) ==