minor changes (refactored function name)

haslab · Sep 28, 2017 · d7e5ef6 · d7e5ef6
1 parent bd8747d
commit d7e5ef6
Show file tree

Hide file tree

Showing 4 changed files with 826 additions and 1,163 deletions.
diff --git a/alarisgp-tse/docs/alaris_completeness.pvs.html b/alarisgp-tse/docs/alaris_completeness.pvs.html
@@ -193,20 +193,20 @@ <h1 class="page-title">Source: alaris_completeness.pvs</h1>
 
 %%
   % @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 @@ <h1 class="page-title">Source: alaris_completeness.pvs</h1>
 	 (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
@@ -39,7 +39,7 @@ <h1 class="page-title">Theorems: alaris_completeness</h1>
                 </div>
 
                 <h3 class="subsection-title">Theorems</h3>
-                <h4 class="name" id="~complete_to_holdingorsetrate"><span class="type-signature"> </span>complete_to_holdingorsetrate<span class="signature"></span><span class="type-signature"></span></h4>
+                <h4 class="name" id="~complete_to_pause"><span class="type-signature"> </span>complete_to_pause<span class="signature"></span><span class="type-signature"></span></h4>
                 <div class="description">
                     theorem: transition via key1 or key3 to top line display of holding or set rate, guard deals with counter examples: used in paper
                 </div>
@@ -618,6 +618,44 @@ <h5>Returns:</h5>
                         <span class="param-type">bool</span>
                     </dd>
                 </dl>
+                <h4 class="name" id=".guard_hosr"><span class="type-signature"> </span>guard_hosr<span class="signature">(st)</span><span class="type-signature"> &rarr; {bool}</span></h4>
+                <div class="description">
+                    completeness (Section 6.1 templates paper)
+                </div>
+                <h5>Parameters:</h5>
+                <table class="params">
+                    <thead>
+                        <tr>
+                            <th>Name</th>
+                            <th>Type</th>
+                            <th class="last">Description</th>
+                        </tr>
+                    </thead>
+                    <tbody>
+                        <tr>
+                            <td class="name"><code>st</code></td>
+                            <td class="type">
+                                <span class="param-type">state</span>
+                            </td>
+                            <td class="description last">The state of the system</td>
+                        </tr>
+                    </tbody>
+                </table>
+                <dl class="details">
+                    <dt class="tag-source">Source:</dt>
+                    <dd class="tag-source"><ul class="dummy"><li>
+                        <a href="alaris_completeness.pvs.html">alaris_completeness.pvs</a>, <a href="alaris_completeness.pvs.html#line191">line 191</a>
+                    </li></ul></dd>
+                </dl>
+                <h5>Returns:</h5>
+                <dl>
+                    <dt>
+                        Type
+                    </dt>
+                    <dd>
+                        <span class="param-type">bool</span>
+                    </dd>
+                </dl>
                 <h4 class="name" id=".guard_infuse"><span class="type-signature"> </span>guard_infuse<span class="signature">(st)</span><span class="type-signature"> &rarr; {bool}</span></h4>
                 <div class="description">
                     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 @@ <h5>Parameters:</h5>
                 <dl class="details">
                     <dt class="tag-source">Source:</dt>
                     <dd class="tag-source"><ul class="dummy"><li>
-                        <a href="alaris_completeness.pvs.html">alaris_completeness.pvs</a>, <a href="alaris_completeness.pvs.html#line184">line 184</a>
+                        <a href="alaris_completeness.pvs.html">alaris_completeness.pvs</a>, <a href="alaris_completeness.pvs.html#line183">line 183</a>
                     </li></ul></dd>
                 </dl>
                 <h5>Returns:</h5>