smyalygames/checklist-tester
1
0
Fork 0
mirror of https://github.com/smyalygames/checklist-tester.git synced 2025-05-18 22:44:11 +02:00
Code Issues Actions Packages Projects Releases Wiki Activity
checklist-tester/formal/checklist.vdmsl

434 lines
17 KiB
Plaintext
Raw Blame History

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" |-> before_start_procedure});
types
--@LF can this be empty? perhaps seq1?
String = seq of char;
-- Aircraft
-- Switches
--@doc The state a switch can be in
-- 1 means off
SwitchState = <OFF> | <MIDDLE> | <ON>;
--@LF why have a type kist as a rename?
ItemState = SwitchState;
--@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 ==
--@LF boolean conditions like these are clearer described as
-- not s.middlePosition => s.position <> <MIDDLE>
-- =
-- (s.position = <MIDDLE> => s.middlePosition)
--
--
--if s.middlePosition = false then
-- s.position <> <MIDDLE>
--else true;
(s.position = <MIDDLE> => s.middlePosition);
-- Knob
Knob ::
position : nat1
--@LF how can a state be an int? perhaps a proper type (i..e. subset of int range or a union?)
states : seq1 of int
inv k ==
--@LF if k.pos <= len k.states and pos is nat1, then states better be seq1 as well?! It implicitly already is anyhow.
k.position <= len k.states;
Lever = nat
inv t == t <= 100;
Throttle ::
thrust: Lever
reverser: Lever
inv t ==
--@LF again, this is "programming" not modelling. This one won't turn out as clear as the one for Switch
-- but it is effectively this
--
-- (t.thrust > 0 <=> t.reverser = 0)
--
-- that is, if t.thurst > 0 then t.reverser = 0 and
-- and , if not (t.thurst > 0) then not t.reverser = 0
-- ==
-- if (t.thurst <= 0) then t.reverser <> 0
--
-- coming to think of this, t.reverser is already >= 0 (i.e. it's a nat?).
-- so the else is spurious (i.e. it is a good as "true"). Don't you mean
-- "t.reverser > 0"? (i.e. if thurst is <= 0, then reverser cannot be zero)?
--
-- again, this is concrete example how logic is better to illstrate issue than if-then-else.
-- arguably this is also a matter of taste. But as-is, this seems wrong.
if t.thrust > 0 then
t.reverser = 0
else
t.reverser >= 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
ItemObject ::
type : ItemType
object : Switch | Knob | Throttle
inv i ==
--@LF here I would write differently. This is protracted. I would use pattern matching
let type = i.type, object = i.object in
(type = <SWITCH> and is_Switch(object))
or (type = <KNOB> and is_Knob(object))
or (type = <THROTTLE> and is_Throttle(object));
--TODO add check for button
--@LF if type is always inline with the object, then why is it needed?
-- that is, would ItemType come from anywhere else but the way you consutrct object type?
-- this seems redudant (i.e. you just need object union type) perhaps as
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
--@LF then String defintely shouldn't be empty. Otherwise, what does it mean to map empty to something?
-- dores it really need to be string?
Items = map String to ItemObject;
--@doc Contains the panels (all the items in the aircraft) and the checklist
Aircraft ::
items : Items
checklist : Checklist;
--@LF should the domains of these two maps be equal or contained? Should the maps be non-empty?
--e.g.
-- inv mk_Aircraft(i, c) == (dom i = dom c) or (dom i subset dom c); ?
-- Checklist
--@doc Item of a checklist, e.g. Landing gear down
ChecklistItem ::
--@LF again, empty string here doesn't make sense.
procedure : String
type : ItemType
--TODO Check is not only SwitchState
check : SwitchState
checked : bool;
--@doc This is the item with the complimentary item in the chcecklist
ItemAndChecklistItem ::
item : ItemObject
--@LF this name is bad. This is not a check list but a check list item! call it checkListItem!
checklist: ChecklistItem
inv i == i.item.type = i.checklist.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 ==
--len p > 0 and
--@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
(first = second) or (first and not second)--((first = true) and (second = false))
| x in set {2,...,len p}};
--@doc Full checklist, e.g. Startup, Descent, Landing Checklist
Checklist = map String to Procedure;
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 Gets the procedure by the name, n.
get_procedure: String * Aircraft -> Procedure
get_procedure(n, a) ==
a.checklist(n)
pre
n in set dom a.checklist;
--@doc Completes a procedure step by step
-- n = Name of procedure, a = Aircraft
complete_procedure: String * Aircraft -> Aircraft
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
n in set dom checklist
and not procedure_completed(checklist(n))
post
procedure_completed(RESULT.checklist(n));
-- 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
>
*/
Reference in New Issue View Git Blame Copy Permalink