diff --git a/alarisgp-tse/docs/alaris_completeness.pvs.html b/alarisgp-tse/docs/alaris_completeness.pvs.html index 110fff2..77c9c6a 100644 --- a/alarisgp-tse/docs/alaris_completeness.pvs.html +++ b/alarisgp-tse/docs/alaris_completeness.pvs.html @@ -193,20 +193,20 @@

Source: alaris_completeness.pvs

%% % @function guard_rmode - % @description predicate that is true when the device is in paused state and not locked and not in bag mode - % @description completeness (Section 6.1 templates paper) + % @description predicate that is true when the device is in paused state and not locked and not in bag mode (Section 6.1 templates paper) % @param {state} st The state of the system % @returns {bool} % @memberof module:alaris_completeness %% -guard_rmode(st: state): boolean = - paused_state(st) & - ((topline(st) /= locked) AND - (topline(st) /= lockrate) AND - NOT((topline(st) = dispvtbi) AND - ((entrymode(st) = bagmode) OR - (entrymode(st) = tbagmode)))) - +guard_rmode(st: state): boolean = paused_state(st) & ((topline(st) /= locked) AND (topline(st) /= lockrate) AND NOT((topline(st) = dispvtbi) AND ((entrymode(st) = bagmode) OR (entrymode(st) = tbagmode)))) +%% + % @function guard_hosr + % @description predicate that is true when the device is in paused state and not locked and not in bag mode (Section 6.1 templates paper) + % @param {state} st The state of the system + % @returns {bool} + % @memberof module:alaris_completeness + %% +guard_hosr(st: state): boolean = paused_state(st) & ((topline(st) /= locked) AND (topline(st) /= lockrate) AND NOT((topline(st) = dispvtbi) AND ((entrymode(st) = bagmode) OR (entrymode(st) = tbagmode)))) %% % @function goal_rmode @@ -388,12 +388,12 @@

Source: alaris_completeness.pvs

(per_key3(st) AND goal_hosr(key3(st)))) %% -% @theorem complete_to_holdingorsetrate +% @theorem complete_to_pause % @description theorem: transition via key1 or key3 to top line display of holding or set rate, guard deals with counter examples: used in paper % @yields QED -% @stats Run time = 5061.11 secs. 18/7/17 +% @stats Run time = 4243.84 secs. 20/9/17 %% -complete_to_holdingorsetrate: THEOREM +complete_to_pause: THEOREM FORALL (pre, post: state): (init?(pre) AND post = on(pre) => complete_to_hosr(post)) AND ((state_transitions_release(pre, post) AND diff --git a/alarisgp-tse/docs/theorems-alaris_completeness.html b/alarisgp-tse/docs/theorems-alaris_completeness.html index 2bc9f85..433440d 100644 --- a/alarisgp-tse/docs/theorems-alaris_completeness.html +++ b/alarisgp-tse/docs/theorems-alaris_completeness.html @@ -39,7 +39,7 @@

Theorems: alaris_completeness

Theorems

-

complete_to_holdingorsetrate

+

complete_to_pause

theorem: transition via key1 or key3 to top line display of holding or set rate, guard deals with counter examples: used in paper
@@ -618,6 +618,44 @@
Returns:
bool +

guard_hosr(st) → {bool}

+
+ completeness (Section 6.1 templates paper) +
+
Parameters:
+ + + + + + + + + + + + + + + +
NameTypeDescription
st + state + The state of the system
+
+
Source:
+
+
+
Returns:
+
+
+ Type +
+
+ bool +
+

guard_infuse(st) → {bool}

predicate that is true when the device is infusing, the top line is not showing locked and the device is not showing VTBI in the top line in bag mode @@ -682,7 +720,7 @@
Parameters:
Source:
Returns:
diff --git a/alarisgp-tse/models/alaris_completeness.prf b/alarisgp-tse/models/alaris_completeness.prf index 12ccf87..b3cc876 100644 --- a/alarisgp-tse/models/alaris_completeness.prf +++ b/alarisgp-tse/models/alaris_completeness.prf @@ -1779,46 +1779,8 @@ (state_transitions_release const-decl "boolean" alaris_completeness_pattern nil)) shostak)) - (univ_complete_to_holdingorsetrate 0 - (univ_complete_to_holdingorsetrate-1 nil 3687849408 - ("" (skosimp*) - (("" (expand "guard_rmode") - (("" (expand "goal_hors") - (("" (flatten) - (("" (expand "paused_state") - (("" (expand "per_key1") - (("" (flatten) - (("" (split) - (("1" (split) - (("1" (propax) nil nil) - ("2" (grind) - (("1" (postpone) nil nil) - ("2" (postpone) nil nil) - ("3" (postpone) nil nil) - ("4" (postpone) nil nil) - ("5" (postpone) nil nil) - ("6" (postpone) nil nil) - ("7" (postpone) nil nil) - ("8" (postpone) nil nil) - ("9" (postpone) nil nil) - ("10" (postpone) nil nil) - ("11" (postpone) nil nil) - ("12" (postpone) nil nil)) - nil) - ("3" (postpone) nil nil) ("4" (postpone) nil nil)) - nil) - ("2" (postpone) nil nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - nil shostak)) - (complete_to_holdingorsetrate 0 - (complete_to_holdingorsetrate-1 nil 3687091004 + (complete_to_pause 0 + (complete_to_pause-1 nil 3714879602 ("" (skosimp*) (("" (split) (("1" (grind) nil nil) @@ -1827,112 +1789,110 @@ (("2" (split) (("1" (expand "per_sup") (("1" (expand "per_chevron") - (("1" (flatten) - (("1" (split) - (("1" (split) - (("1" (grind) nil nil) ("2" (grind) nil nil) - ("3" (flatten) - (("3" (split) - (("1" (grind) nil nil) ("2" (grind) nil nil)) - nil)) - nil) - ("4" (flatten) - (("4" (split) - (("1" (grind) nil nil) - ("2" (flatten) - (("2" (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("5" (grind) nil nil)) - nil) - ("2" (flatten) - (("2" (split) - (("1" (grind) nil nil) ("2" (grind) nil nil) - ("3" (flatten) - (("3" (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil) - ("4" (flatten) - (("4" (split) - (("1" (grind) nil nil) - ("2" (flatten) - (("2" - (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("5" (grind) nil nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "per_fup") - (("2" (expand "per_chevron") - (("2" (flatten) - (("2" (split) - (("1" (split) + (("1" (expand "release_sup") + (("1" (expand "release_key") + (("1" (expand "sup") (("1" (flatten) (("1" (split) - (("1" (expand "release_fup") - (("1" (expand "release_key") + (("1" (split) + (("1" (flatten) (("1" - (expand "fup") + (lift-if) (("1" - (lift-if) + (split) (("1" (split) (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_fup") - (("2" (expand "release_key") - (("2" - (expand "fup") - (("2" - (lift-if) - (("2" + ("2" + (flatten) + (("2" + (split) + (("1" (flatten) nil nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + nil + nil)) + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (flatten) + nil + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (split) (("1" (grind) nil nil) ("2" (flatten) (("2" (split) - (("1" (flatten) nil nil) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (flatten) nil nil)) + nil) ("2" (split) (("1" (grind) nil nil) - ("2" (grind) nil nil)) + ("2" + (flatten) + (("2" (grind) nil nil)) + nil)) nil)) nil)) nil)) nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_fup") - (("2" (expand "release_key") - (("2" (expand "fup") - (("2" (lift-if) + nil) + ("2" (flatten) (("2" - (flatten) + (lift-if) (("2" (split) (("1" (grind) nil nil) @@ -1940,7 +1900,14 @@ (flatten) (("2" (split) - (("1" (grind) nil nil) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (grind) nil nil)) + nil)) + nil) ("2" (split) (("1" (grind) nil nil) @@ -1957,7 +1924,7 @@ (("2" (split) (("1" - (flatten) + (grind) nil nil) ("2" @@ -1974,434 +1941,103 @@ nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil) - ("3" (grind) nil nil) - ("4" (flatten) - (("4" (split) - (("1" (grind) nil nil) - ("2" (flatten) - (("2" (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("5" (grind) nil nil)) - nil) - ("2" (flatten) - (("2" (split) - (("1" (expand "release_fup") - (("1" (expand "release_key") - (("1" (expand "fup") - (("1" - (lift-if) - (("1" - (flatten) - (("1" - (split) - (("1" + nil) + ("3" (lift-if) + (("3" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) + nil) + ("4" (grind) nil nil) + ("5" (lift-if) + (("5" + (flatten) + (("5" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (flatten) nil nil) - ("2" + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (split) - (("1" (grind) nil nil) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) ("2" - (flatten) - (("2" - (split) - (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (split) (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + (("2" + (grind) nil nil)) nil)) - nil)) - nil) - ("2" - (split) - (("1" - (grind) - nil nil) ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (flatten) nil nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" - (grind) + (propax) nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) nil)) nil)) nil)) nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_fup") - (("2" (expand "release_key") - (("2" (expand "fup") - (("2" - (lift-if) - (("2" - (flatten) - (("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" + nil) + ("2" (split) - (("1" - (flatten) - (("1" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (propax) nil nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (propax) nil nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) - nil)) - nil) - ("3" (grind) nil nil) - ("4" (flatten) - (("4" (split) - (("1" (grind) nil nil) - ("2" (flatten) - (("2" + nil) + ("2" (lift-if) + (("2" (split) + (("1" (split) (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("5" (expand "release_fup") - (("5" (expand "release_key") - (("5" (expand "fup") - (("5" - (lift-if) - (("5" + ("2" (flatten) - (("5" - (split) - (("1" - (flatten) - (("1" - (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - (("1" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (grind) - nil - nil)) - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("2" (grind) nil nil)) - nil)) - nil)) + (("2" (grind) nil nil)) + nil)) + nil) + ("2" + (flatten) + (("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (grind) nil nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("3" (expand "per_sdown") - (("3" (expand "per_chevron") - (("3" (flatten) - (("3" (split) - (("1" (split) - (("1" (expand "release_sdown") - (("1" (expand "release_key") - (("1" (expand "sdown") - (("1" (lift-if) - (("1" + nil) + ("3" (flatten) - (("1" + (("3" (split) (("1" (split) @@ -2409,101 +2045,98 @@ ("2" (flatten) (("2" - (split) - (("1" (flatten) nil nil) - ("2" + (split) + (("1" (split) (("1" (grind) nil nil) ("2" (flatten) (("2" (split) - (("1" (grind) nil nil) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (grind) + nil + nil)) + nil)) + nil) ("2" (grind) nil nil)) nil)) nil)) - nil)) + nil) + ("2" (grind) nil nil)) nil)) nil)) nil) ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (flatten) nil nil) - ("2" + (flatten) + (("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + (("2" + (grind) + nil + nil)) + nil)) + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil)) nil)) nil)) nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_sdown") - (("2" (expand "release_key") - (("2" (expand "sdown") - (("2" (lift-if) (("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("3" (expand "release_sdown") - (("3" (expand "release_key") - (("3" (expand "sdown") - (("3" (lift-if) (("3" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("4" (expand "release_sdown") - (("4" (expand "release_key") - (("4" (expand "sdown") - (("4" (lift-if) (("4" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("5" (expand "release_sdown") - (("5" (expand "release_key") - (("5" (expand "sdown") - (("5" (lift-if) (("5" (grind) nil nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_sdown") - (("2" (expand "release_key") - (("2" (expand "sdown") - (("2" (lift-if) (("2" (grind) nil nil)) nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("4" (expand "per_fdown") - (("4" (expand "per_chevron") - (("4" (flatten) - (("4" (split) - (("1" (split) - (("1" (expand "release_fdown") - (("1" (expand "release_key") - (("1" (expand "fdown") - (("1" (lift-if) - (("1" + nil) + ("4" (flatten) - (("1" + (("4" (split) (("1" (split) @@ -2512,8 +2145,7 @@ (flatten) (("2" (split) - (("1" (flatten) nil nil) - ("2" + (("1" (split) (("1" (grind) nil nil) ("2" @@ -2526,50 +2158,15 @@ ("2" (flatten) (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) + (grind) + nil nil)) nil)) nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil)) + ("2" (grind) nil nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (flatten) nil nil) + nil) ("2" (split) (("1" (grind) nil nil) @@ -2583,15 +2180,8 @@ ("2" (flatten) (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) + (grind) + nil nil)) nil)) nil) @@ -2601,15 +2191,8 @@ ("2" (flatten) (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) + (grind) + nil nil)) nil)) nil)) @@ -2618,18 +2201,75 @@ nil)) nil)) nil)) + nil) + ("2" (grind) nil nil)) + nil)) + nil) + ("5" + (flatten) + (("5" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (expand "per_fup") + (("2" (expand "per_chevron") + (("2" (expand "release_fup") + (("2" (expand "release_key") + (("2" (expand "fup") + (("2" (flatten) + (("2" (lift-if) + (("2" (split) + (("1" (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" (propax) nil nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_fdown") - (("2" (expand "release_key") - (("2" (expand "fdown") - (("2" (lift-if) - (("2" + nil) + ("2" (flatten) (("2" (split) @@ -2639,35 +2279,11 @@ (("2" (split) (("1" - (flatten) - (("1" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (propax) nil nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (grind) nil nil)) nil)) nil) ("2" @@ -2681,52 +2297,120 @@ ("2" (split) (("1" (grind) nil nil) - ("2" - (flatten) - (("2" + ("2" (grind) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" + (flatten) + (("3" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) + ("2" + (flatten) + (("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" (split) (("1" - (flatten) + (grind) nil nil) ("2" - (propax) + (flatten) + (("2" + (grind) + nil + nil)) + nil)) + nil) + ("2" + (split) + (("1" + (grind) nil + nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (flatten) + (("1" + (grind) + nil + nil)) + nil) + ("2" + (propax) + nil + nil)) + nil)) nil)) nil)) nil)) nil)) + nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) + nil) + ("4" (grind) nil nil) + ("5" + (flatten) + (("5" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) nil)) - nil)) - nil)) - nil)) - nil) - ("3" (grind) nil nil) - ("4" (flatten) - (("4" (split) - (("1" (expand "release_fdown") - (("1" (expand "release_key") - (("1" - (expand "fdown") + nil) + ("2" (flatten) + (("2" + (split) (("1" - (lift-if) - (("1" + (split) + (("1" (grind) nil nil) + ("2" (flatten) - (("1" + (("2" (split) - (("1" (grind) nil nil) + (("1" (propax) nil nil) ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) (("1" (split) (("1" (grind) nil nil) @@ -2745,177 +2429,6 @@ (("2" (split) (("1" - (flatten) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (propax) - nil - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (propax) - nil - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (propax) - nil - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (propax) - nil - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (propax) - nil - nil) - ("2" - (split) - (("1" - (grind) - nil - nil) - ("2" - (grind) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (split) (("1" (grind) @@ -2926,10 +2439,6 @@ (("2" (split) (("1" - (propax) - nil - nil) - ("2" (split) (("1" (grind) @@ -2940,6 +2449,20 @@ (("2" (split) (("1" + (split) + (("1" + (flatten) + nil + nil) + ("2" + (flatten) + (("2" + (grind) + nil + nil)) + nil)) + nil) + ("2" (split) (("1" (grind) @@ -2949,69 +2472,157 @@ (grind) nil nil)) - nil) - ("2" - (grind) - nil nil)) nil)) nil)) + nil) + ("2" + (grind) + nil nil)) nil)) nil)) + nil) + ("2" + (grind) + nil nil)) nil)) nil)) nil) ("2" - (grind) + (propax) nil nil)) - nil)) - nil)) - nil)) - nil) - ("2" (grind) nil nil)) + nil)) + nil)) + nil) + ("2" (grind) nil nil)) + nil)) nil)) nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_fdown") - (("2" (expand "release_key") - (("2" - (expand "fdown") - (("2" - (lift-if) - (("2" (grind) nil nil)) - nil)) + nil) + ("2" + (flatten) + (("2" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) + nil) + ("3" + (flatten) + (("3" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) + ("2" (grind) nil nil)) + nil)) + nil) + ("4" (grind) nil nil) + ("5" (grind) nil nil)) nil)) nil)) nil)) nil)) - nil) - ("5" (expand "release_fdown") - (("5" (expand "release_key") - (("5" (expand "fdown") - (("5" (lift-if) (("5" (grind) nil nil)) - nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" (expand "per_sdown") + (("3" (expand "per_chevron") + (("3" (expand "release_sdown") + (("3" (expand "release_key") + (("3" (expand "sdown") + (("3" (flatten) + (("3" (lift-if) + (("3" (split) + (("1" (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) + ("2" (grind) nil nil) + ("3" (grind) nil nil) + ("4" (grind) nil nil) + ("5" (grind) nil nil)) + nil) + ("2" (grind) nil nil)) nil)) nil)) nil)) - nil) - ("2" (flatten) - (("2" (split) - (("1" (expand "release_fdown") - (("1" (expand "release_key") - (("1" (expand "fdown") + nil)) + nil)) + nil)) + nil)) + nil) + ("4" (expand "per_fdown") + (("4" (expand "per_chevron") + (("4" (expand "release_fdown") + (("4" (expand "release_key") + (("4" (expand "fdown") + (("4" (flatten) + (("4" (lift-if) + (("4" (split) + (("1" (split) (("1" - (lift-if) + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil) + ("2" + (flatten) + (("2" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) + nil) + ("3" (grind) nil nil) + ("4" (grind) nil nil) + ("5" (grind) nil nil)) + nil) + ("2" (flatten) + (("2" + (split) (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" (propax) nil nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten) - (("1" + (("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" (grind) nil nil)) + nil)) + nil)) + nil) + ("3" + (flatten) + (("3" (split) (("1" (split) @@ -3020,11 +2631,86 @@ (flatten) (("2" (split) - (("1" (flatten) nil nil) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" + (grind) + nil + nil) + ("2" + (grind) + nil + nil)) + nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil) ("2" (split) (("1" (grind) nil nil) - ("2" (grind) nil nil)) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" + (grind) + nil + nil) + ("2" + (grind) + nil + nil)) + nil) + ("2" + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + (("2" + (split) + (("1" + (propax) + nil + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) nil)) nil)) nil)) @@ -3036,8 +2722,7 @@ (flatten) (("2" (split) - (("1" (flatten) nil nil) - ("2" + (("1" (split) (("1" (grind) nil nil) ("2" @@ -3053,19 +2738,36 @@ ("2" (flatten) (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) + (grind) + nil nil)) nil)) nil) ("2" + (split) + (("1" + (grind) + nil + nil) + ("2" + (flatten) + (("2" + (grind) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) + (("1" (split) (("1" (grind) @@ -3076,8 +2778,15 @@ (("2" (split) (("1" - (flatten) - nil + (split) + (("1" + (grind) + nil + nil) + ("2" + (grind) + nil + nil)) nil) ("2" (propax) @@ -3085,7 +2794,8 @@ nil)) nil)) nil)) - nil)) + nil) + ("2" (grind) nil nil)) nil)) nil)) nil)) @@ -3093,27 +2803,18 @@ nil)) nil)) nil)) - nil)) - nil)) - nil)) - nil)) - nil) - ("2" (expand "release_fdown") - (("2" (expand "release_key") - (("2" (expand "fdown") - (("2" - (lift-if) - (("2" + nil) + ("4" (flatten) - (("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) + (("4" + (split) + (("1" + (split) + (("1" (grind) nil nil) + ("2" + (flatten) + (("2" + (split) (("1" (split) (("1" (grind) nil nil) @@ -3121,77 +2822,44 @@ (flatten) (("2" (split) - (("1" (propax) nil nil) - ("2" + (("1" (split) (("1" (grind) nil nil) ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) + (grind) + nil nil)) - nil)) + nil) + ("2" (grind) nil nil)) nil)) nil)) - nil)) - nil) - ("2" + nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil) + ("2" + (flatten) + (("2" + (split) + (("1" (split) (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" (propax) nil nil) - ("2" - (split) - (("1" (grind) nil nil) - ("2" - (flatten) - (("2" - (split) - (("1" - (flatten) - nil - nil) - ("2" - (propax) - nil - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) - nil)) + ("2" (grind) nil nil)) + nil) + ("2" (grind) nil nil)) nil)) nil)) nil)) - nil)) + nil) + ("5" (grind) nil nil)) nil)) nil)) nil)) - nil) - ("3" (grind) nil nil) - ("4" (flatten) - (("4" (split) - (("1" (grind) nil nil) - ("2" (grind) nil nil)) - nil)) - nil) - ("5" (grind) nil nil)) + nil)) nil)) nil)) nil)) @@ -3208,7 +2876,12 @@ ("5" (grind) nil nil) ("6" (grind) nil nil)) nil)) nil) - ("2" (grind) nil nil)) + ("2" (flatten) + (("2" (split) + (("1" (grind) nil nil) ("2" (grind) nil nil) + ("3" (grind) nil nil)) + nil)) + nil)) nil)) nil)) nil) @@ -3227,17 +2900,7 @@ ("5" (grind) nil nil)) nil)) nil) - ("2" (flatten) - (("2" (split) - (("1" (grind) nil nil) - ("2" (flatten) - (("2" (split) - (("1" (grind) nil nil) ("2" (grind) nil nil)) - nil)) - nil) - ("3" (grind) nil nil)) - nil)) - nil)) + ("2" (grind) nil nil)) nil)) nil)) nil) @@ -3259,20 +2922,8 @@ ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil) - ("2" (flatten) - (("2" (split) - (("1" (grind) nil nil) ("2" (grind) nil nil) - ("3" (flatten) - (("3" (split) - (("1" (grind) nil nil) ("2" (grind) nil nil) - ("3" (grind) nil nil)) - nil)) - nil) - ("4" (grind) nil nil) ("5" (grind) nil nil) - ("6" (grind) nil nil) ("7" (grind) nil nil)) - nil)) - nil) - ("3" (grind) nil nil) ("4" (grind) nil nil)) + ("2" (grind) nil nil) ("3" (grind) nil nil) + ("4" (grind) nil nil)) nil)) nil)) nil) @@ -3288,40 +2939,14 @@ (("14" (flatten) (("14" (split) (("1" (grind) nil nil) - ("2" (flatten) - (("2" (expand "switch") - (("2" (lift-if) + ("2" (expand "switch") + (("2" (lift-if) + (("2" (flatten) (("2" (split) (("1" (grind) nil nil) ("2" (flatten) (("2" (split) - (("1" - (expand "switch_from_battery_low") - (("1" - (flatten) - (("1" - (lift-if) - (("1" - (split) - (("1" - (flatten) - (("1" - (lift-if) - (("1" - (split) - (("1" (flatten) nil nil) - ("2" - (flatten) - (("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) - ("2" (grind) nil nil)) - nil)) - nil)) - nil)) - nil) + (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) @@ -3341,62 +2966,63 @@ ((state_transitions_release const-decl "boolean" alaris_completeness_pattern nil) (per_chevron const-decl "bool" alaris_th nil) - (odd_minus_odd_is_even application-judgement "even_int" integers + (release_key const-decl "state" alaris_th nil) + (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) + (even_plus_even_is_even application-judgement "even_int" integers nil) - (trim_time const-decl "itimes" alaris_th nil) - (state_up_time const-decl "itimes" alaris_th nil) - (sup_case_vtbitime_ttmode const-decl "state" alaris_th nil) - (nnint_plus_posint_is_posint application-judgement "posint" - integers nil) - (odd_plus_even_is_odd application-judgement "odd_int" integers nil) - (sup_case_vtbitime_vttmode const-decl "state" alaris_th nil) - (sup_case_dispvtbi_tbagmode const-decl "state" alaris_th nil) - (mbags const-decl "nat" types_and_constants_th nil) - (sup_case_dispvtbi_bagmode const-decl "state" alaris_th nil) - (trim_vtbi const-decl "ivols" alaris_th nil) - (state_up_vtbi const-decl "ivols" alaris_th nil) - (sup_case_dispvtbi_vtmode const-decl "state" alaris_th nil) - (sup_case_infusing_NOTrlock const-decl "state" alaris_th nil) - (sup_case_options const-decl "state" alaris_th nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) - (even_plus_even_is_even application-judgement "even_int" integers + (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" + rationals nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers nil) - (real_div_nzreal_is_real application-judgement "real" reals nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) - (real_gt_is_strict_total_order name-judgement - "(strict_total_order?[real])" real_props nil) - (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" - rationals nil) - (posreal_plus_nnreal_is_posreal application-judgement "posreal" + (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) + (sup_case_holding_NOTrlock const-decl "state" alaris_th nil) + (aug_rate const-decl "pump" pump_th nil) + (state_up_rate const-decl "irates" alaris_th nil) + (trim_rate const-decl "irates" alaris_th nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) - (decrement const-decl "presstime" alaris_th nil) - (trim_rate const-decl "irates" alaris_th nil) - (state_up_rate const-decl "irates" alaris_th nil) - (aug_rate const-decl "pump" pump_th nil) - (sup_case_holding_NOTrlock const-decl "state" alaris_th nil) + (posreal_plus_nnreal_is_posreal application-judgement "posreal" + real_types nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (real_div_nzreal_is_real application-judgement "real" reals nil) (sup_case_infusingORholding_rlock const-decl "state" alaris_th nil) - (sup const-decl "state" alaris_th nil) - (release_key const-decl "state" alaris_th nil) - (release_sup const-decl "state" alaris_th nil) + (sup_case_infusing_NOTrlock const-decl "state" alaris_th nil) + (sup_case_dispvtbi_bagmode const-decl "state" alaris_th nil) + (mbags const-decl "nat" types_and_constants_th nil) + (sup_case_dispvtbi_vtmode const-decl "state" alaris_th nil) + (state_up_vtbi const-decl "ivols" alaris_th nil) + (trim_vtbi const-decl "ivols" alaris_th nil) + (sup_case_vtbitime_vttmode const-decl "state" alaris_th nil) + (odd_plus_even_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) - (int_minus_int_is_int application-judgement "int" integers nil) - (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" - real_types nil) - (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) - (nnint_times_nnint_is_nnint application-judgement "nonneg_int" - integers nil) - (even_times_int_is_even application-judgement "even_int" integers + (sup_case_vtbitime_ttmode const-decl "state" alaris_th nil) + (state_up_time const-decl "itimes" alaris_th nil) + (trim_time const-decl "itimes" alaris_th nil) + (decrement const-decl "presstime" alaris_th nil) + (odd_minus_odd_is_even application-judgement "even_int" integers nil) - (mult_divides1 application-judgement "(divides(n))" divides nil) - (mult_divides2 application-judgement "(divides(m))" divides nil) - (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) + (sup_case_dispvtbi_tbagmode const-decl "state" alaris_th nil) + (sup_case_options const-decl "state" alaris_th nil) + (sup const-decl "state" alaris_th nil) + (release_sup const-decl "state" alaris_th nil) (per_sup const-decl "bool" alaris_th nil) (fup_case_options const-decl "state" alaris_th nil) + (fup_case_dispvtbi_tbagmode const-decl "state" alaris_th nil) (state_UP_time const-decl "itimes" alaris_th nil) (fup_case_vtbitime_ttmode const-decl "state" alaris_th nil) (int_times_even_is_even application-judgement "even_int" integers @@ -3404,13 +3030,10 @@ (real_plus_real_is_real application-judgement "real" reals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (fup_case_vtbitime_vttmode const-decl "state" alaris_th nil) - (fup_case_dispvtbi_tbagmode const-decl "state" alaris_th nil) - (state_UP_vtbi const-decl "ivols" alaris_th nil) - (fup_case_dispvtbi_vtmode const-decl "state" alaris_th nil) (fup_case_dispvtbi_bagmode const-decl "state" alaris_th nil) + (fup_case_dispvtbi_vtmode const-decl "state" alaris_th nil) + (state_UP_vtbi const-decl "ivols" alaris_th nil) (fup_case_infusing_NOTrlock const-decl "state" alaris_th nil) - (release_fup const-decl "state" alaris_th nil) - (fup const-decl "state" alaris_th nil) (real_minus_real_is_real application-judgement "real" reals nil) (fup_case_holding_NOTrlock const-decl "state" alaris_th nil) (state_UP_rate const-decl "irates" alaris_th nil) @@ -3420,6 +3043,8 @@ real_types nil) (fup_case_infusingORholding_rlock const-decl "state" alaris_th nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) + (fup const-decl "state" alaris_th nil) + (release_fup const-decl "state" alaris_th nil) (per_fup const-decl "bool" alaris_th nil) (dpdtls const-decl "nat" types_and_constants_th nil) (sdown_case_options const-decl "state" alaris_th nil) @@ -3432,8 +3057,6 @@ (sdown_case_dispvtbi_vtmode const-decl "state" alaris_th nil) (sdown_case_dispvtbi_bagmode const-decl "state" alaris_th nil) (sdown_case_infusing_NOTrlock const-decl "state" alaris_th nil) - (release_sdown const-decl "state" alaris_th nil) - (sdown const-decl "state" alaris_th nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) @@ -3442,35 +3065,37 @@ (ceil_rate const-decl "irates" alaris_th nil) (sdown_case_infusingORholding_rlock const-decl "state" alaris_th nil) + (sdown const-decl "state" alaris_th nil) + (release_sdown const-decl "state" alaris_th nil) (per_sdown const-decl "bool" alaris_th nil) (fdown_case_options const-decl "state" alaris_th nil) - (fdown_case_vtbitime_vttmode const-decl "state" alaris_th nil) + (fdown_case_dispvtbi_tbagmode const-decl "state" alaris_th nil) (state_DN_time const-decl "itimes" alaris_th nil) (fdown_case_vtbitime_ttmode const-decl "state" alaris_th nil) - (fdown_case_dispvtbi_tbagmode const-decl "state" alaris_th nil) + (fdown_case_vtbitime_vttmode const-decl "state" alaris_th nil) (state_DN_vtbi const-decl "ivols" alaris_th nil) (fdown_case_dispvtbi_vtmode const-decl "state" alaris_th nil) (fdown_case_dispvtbi_bagmode const-decl "state" alaris_th nil) (fdown_case_infusing_NOTrlock const-decl "state" alaris_th nil) - (release_fdown const-decl "state" alaris_th nil) - (fdown const-decl "state" alaris_th nil) (fdown_case_holding_NOTrlock const-decl "state" alaris_th nil) (state_DN_rate const-decl "irates" alaris_th nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (fdown_case_infusingORholding_rlock const-decl "state" alaris_th nil) + (fdown const-decl "state" alaris_th nil) + (release_fdown const-decl "state" alaris_th nil) (per_fdown const-decl "bool" alaris_th nil) - (tick_case_infuse_and_infusionrateLvtbi const-decl "pump" pump_th - nil) (tick_case_infuse_and_infusionrateGEvtbi_kvoflag const-decl "pump" pump_th nil) - (tick_case_infuse_infusionrateLTvtbi const-decl "state" alaris_th - nil) (tick_case_infuse_infusionrateEQvtbi_kvoflag const-decl "state" alaris_th nil) + (tick_case_infuse_and_infusionrateLvtbi const-decl "pump" pump_th + nil) (tick_case_infuse_and_infusionrateGEvtbi_NOTkvoflag const-decl "pump" pump_th nil) + (tick_case_infuse_infusionrateLTvtbi const-decl "state" alaris_th + nil) (tick_case_infuse_infusionrateEQvtbi_notkvoflag const-decl "state" alaris_th nil) (tick_case_infuse_infusionrateLTvtbilocked const-decl "state" @@ -3584,7 +3209,7 @@ (on_case_infusionstatusNOTblank const-decl "state" alaris_th nil) (on const-decl "state" alaris_th nil) (paused_state const-decl "boolean" alaris_completeness_pattern nil) - (guard_rmode const-decl "boolean" alaris_completeness_pattern nil) + (guard_hosr const-decl "boolean" alaris_completeness_pattern nil) (goal_hosr const-decl "boolean" alaris_completeness_pattern nil) (no_button_down const-decl "bool" alaris_th nil) (per_key1 const-decl "bool" alaris_th nil) diff --git a/alarisgp-tse/models/alaris_completeness.pvs b/alarisgp-tse/models/alaris_completeness.pvs index aad528b..504da92 100644 --- a/alarisgp-tse/models/alaris_completeness.pvs +++ b/alarisgp-tse/models/alaris_completeness.pvs @@ -175,20 +175,20 @@ simple_guard_hosr(st: state): boolean = paused_state(st) %% % @function guard_rmode - % @description predicate that is true when the device is in paused state and not locked and not in bag mode - % @description completeness (Section 6.1 templates paper) + % @description predicate that is true when the device is in paused state and not locked and not in bag mode (Section 6.1 templates paper) % @param {state} st The state of the system % @returns {bool} % @memberof module:alaris_completeness %% -guard_rmode(st: state): boolean = - paused_state(st) & - ((topline(st) /= locked) AND - (topline(st) /= lockrate) AND - NOT((topline(st) = dispvtbi) AND - ((entrymode(st) = bagmode) OR - (entrymode(st) = tbagmode)))) - +guard_rmode(st: state): boolean = paused_state(st) & ((topline(st) /= locked) AND (topline(st) /= lockrate) AND NOT((topline(st) = dispvtbi) AND ((entrymode(st) = bagmode) OR (entrymode(st) = tbagmode)))) +%% + % @function guard_hosr + % @description predicate that is true when the device is in paused state and not locked and not in bag mode (Section 6.1 templates paper) + % @param {state} st The state of the system + % @returns {bool} + % @memberof module:alaris_completeness + %% +guard_hosr(st: state): boolean = paused_state(st) & ((topline(st) /= locked) AND (topline(st) /= lockrate) AND NOT((topline(st) = dispvtbi) AND ((entrymode(st) = bagmode) OR (entrymode(st) = tbagmode)))) %% % @function goal_rmode @@ -370,12 +370,12 @@ univ_complete_to_holdingorsetrate: THEOREM (per_key3(st) AND goal_hosr(key3(st)))) %% -% @theorem complete_to_holdingorsetrate +% @theorem complete_to_pause % @description theorem: transition via key1 or key3 to top line display of holding or set rate, guard deals with counter examples: used in paper % @yields QED -% @stats Run time = 5061.11 secs. 18/7/17 +% @stats Run time = 4243.84 secs. 20/9/17 %% -complete_to_holdingorsetrate: THEOREM +complete_to_pause: THEOREM FORALL (pre, post: state): (init?(pre) AND post = on(pre) => complete_to_hosr(post)) AND ((state_transitions_release(pre, post) AND