From 273e53738dc0ee60f0b50812380545b92e146526 Mon Sep 17 00:00:00 2001
From: Anthony <smyalygames@gmail.com>
Date: Tue, 12 Mar 2024 15:02:29 +0000
Subject: [PATCH] fix(formal): add checks if item already in position

---
 formal/checklist.vdmsl | 30 ++++++++++++++++++++++++------
 1 file changed, 24 insertions(+), 6 deletions(-)

diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl
index f184114..d842617 100644
--- a/formal/checklist.vdmsl
+++ b/formal/checklist.vdmsl
@@ -141,8 +141,12 @@ functions
     --@doc Completes an Item in the procedure on the Aircraft
     do_proc_item: ChecklistItem * Aircraft -> Aircraft
     do_proc_item(p, a) ==
-        let itemIndex = index_of_item(p.procedure, a) in
-            a ++ {itemIndex |-> move_item(a(itemIndex), p.check)}
+        let itemIndex = index_of_item(p.procedure, a), item = a(itemIndex), objective = p.check in
+            -- Checks if the item is in the objective desired by the checklist
+            if check_item_in_position(item, objective) then
+                a
+            else
+                a ++ {itemIndex |-> move_item(a(itemIndex), objective)}
     pre
         p.checked = false;
 
@@ -180,10 +184,8 @@ functions
         -- if is_Switch(i) then (implement later)
             mk_Item(i.name, i.type, move_switch(i.object, s))
     pre
-        (is_Switch(i.object) and is_SwitchState(s))
-        --TODO check that the item has not already been completed before moving item
-        --TODO add other types of Items
-        ;
+        wf_item_itemstate(i, s) and
+        not check_item_in_position(i, s);
 
     --@doc Moves a specific switch in the aircraft
     move_switch: Switch * SwitchState -> Switch
@@ -210,5 +212,21 @@ functions
         let position = s.position in
             position = <OFF> or position = <ON>;
 
+    --@doc Checks if the item is already in position for the desired state for that item
+    check_item_in_position: Item * 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: Item * ItemState -> bool
+    wf_item_itemstate(i, s) ==
+        (is_Switch(i.object) and is_SwitchState(s))
+        --TODO check that the item has not already been completed before moving item
+        --TODO add other types of Items
+        ;
+
 
 end Checklist