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

feat(formal): add checklist procedure values

Browse Source
This commit is contained in:
Anthony 2024-02-27 17:09:39 +00:00
parent 9f1ea3691e
commit 1354906b57
1 changed files with 30 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
formal/checklist.vdmsl
View File

@ -4,14 +4,25 @@ definitions
values values
-- Before Start Checklist -- Before Start Checklist
-- Items in Aircraft
-- Flight Deck... (can't check) -- Flight Deck... (can't check)
fuel: Item = mk_Item("Fuek Pump", <SWITCH>, mk_Switch(1, [1, 2])); fuel: Item = mk_Item("Fuek Pump", <SWITCH>, mk_Switch(<OFF>, false));
pax_sign: Item = mk_Item("Passenger Signs", <SWITCH>, mk_Switch(1, [1, 2, 3])); pax_sign: Item = mk_Item("Passenger Signs", <SWITCH>, mk_Switch(<OFF>, true));
windows: Item = mk_Item("Windows", <SWITCH>, mk_Switch(2, [1, 2])); windows: Item = mk_Item("Windows", <SWITCH>, mk_Switch(<ON>, false));
-- Preflight steps -- Preflight steps
acol: Item = mk_Item("Anti Collision Lights", <SWITCH>, mk_Switch(1, [1, 2])); acol: Item = mk_Item("Anti Collision Lights", <SWITCH>, mk_Switch(<OFF>, false));
aircraft: Aircraft = [fuel, pax_sign, windows, acol]; 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 types
String = seq of char; String = seq of char;
@ -20,14 +31,16 @@ types
-- Switches -- Switches
--@doc The state a switch can be in --@doc The state a switch can be in
-- 1 means off -- 1 means off
SwitchState = nat1 SwitchState = <OFF> | <MIDDLE> | <ON>;
inv s == s <= 3;
--@doc A switch, with the possible states it can be in, and the state that it is in --@doc A switch, with the possible states it can be in, and the state that it is in
Switch :: Switch ::
position : nat1 position : SwitchState
states : seq of SwitchState middlePosition : bool
inv s == s.position <= len s.states; inv s ==
if s.middlePosition = false then
s.position <> <MIDDLE>
else true;
-- Knob -- Knob
Knob :: Knob ::
@ -64,24 +77,22 @@ types
--@doc Item of a checklist, e.g. Landing gear down --@doc Item of a checklist, e.g. Landing gear down
ChecklistItem :: ChecklistItem ::
procedure : String procedure : String
item : Item type : ItemType
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 == check_procedure_order_complete(p); inv p ==
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 --@doc Full checklist, e.g. Startup, Descent, Landing Checklist
Checklist = seq of Procedure; Checklist = seq of Procedure;
functions functions
--@doc Checks that each item in the checklist are completed in order
check_procedure_order_complete: Procedure -> bool
check_procedure_order_complete(p) ==
false not in set {
p(x-1).checked = p(x).checked or
(p(x-1).checked = true and p(x).checked = false)
| x in set {1,...,len p}
};
end Checklist end Checklist