refactor(dissertation): cleanup VDM model

2025-05-17 22:14:13 +02:00 · 2024-05-22 15:53:33 +01:00 · 2024-05-22 15:53:33 +01:00 · 19aaeedf27
commit 19aaeedf27
parent 443255342c
4 changed files with 10 additions and 127 deletions
--- a/formal/checklist.vdmsl
+++ b/formal/checklist.vdmsl
@ -35,7 +35,6 @@ types
    --@doc The state a switch can be in
    SwitchState = <OFF> | <MIDDLE> | <ON>;

-	--@LF why have a type kist as a rename?
    ItemState = SwitchState; --@TODO | Button | ...

    --@doc A switch, with the possible states it can be in, and the state that it is in
@ -93,10 +92,8 @@ types

    --@doc Item of a checklist, e.g. Landing gear down
    ChecklistItem ::
-        --@LF again, empty string here doesn't make sense.
        procedure : Dataref
        type : ItemType
-        --TODO Check is not only SwitchState
        check : SwitchState
        checked : bool;

@ -107,15 +104,12 @@ types
        inv i == i.item.type = i.checklistItem.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 == 
-            --@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
-                    second => first--((first = true) and (second = false))
+                    second => first
                | x in set {2,...,len p}};

 functions
@ -123,36 +117,16 @@ functions
    --@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]
+        hd [ x | x in set {1,...,len p} & p(x).checked = false ]
    pre
        -- Checks procedure has not already been completed
-        not procedure_completed(p)--procedure_completed(p) = false
+        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
-        ;
+    	(RESULT > 1 => p(RESULT-1).checked);

-    -- --@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
@ -162,19 +136,13 @@ functions
    --@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?  
+        and
+        p(procedure_next_item_index(p)).procedure in set dom a.items
        ;

    --@doc Marks next item in procedure as complete
@ -226,7 +194,6 @@ functions
    --@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))
@ -235,7 +202,6 @@ functions
    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
@ -260,7 +226,6 @@ functions
    --@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);
@ -268,10 +233,7 @@ functions
    --@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
-        ;
+        (is_Switch(i.object) and is_SwitchState(s) and i.type = <SWITCH>);

    --@doc Checks if the move of the Switch is a valid
    wf_switch_move: Switch * SwitchState -> bool
@ -290,83 +252,3 @@ functions


 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
-> 
-*/
--- a/pub/dissertation/chapters/appendix/database.tex
+++ b/pub/dissertation/chapters/appendix/database.tex
@ -2,7 +2,6 @@


 \begin{document}
-\section{SQL Schemas}
 \begin{listing}[!htbp]
 \inputminted[
  linenos,
--- a/pub/dissertation/dissertation.pdf
+++ b/pub/dissertation/dissertation.pdf
--- a/pub/dissertation/dissertation.tex
+++ b/pub/dissertation/dissertation.tex
@ -80,6 +80,8 @@

 \author{Anthony Berg (200871682)\\
 Supervisor: Leo Freitas\\\\
+CSC3094 - BSc Computer Science (G400)\\
+Newcastle University\\\\
 Word Count: \wordcount}
 \title{Testing Quick Reference Handbooks in Flight Simulators}

@ -135,7 +137,7 @@ with areas of improvement for me throughout the project.
 \chapter{Formal Model}
 \subfile{chapters/appendix/formal.tex}

-\chapter{Database}
+\chapter{Database Schemas}
 \subfile{chapters/appendix/database.tex}

 % References