Ticket #1363: Update inv related to BrowsePathResult / Remaining

In the component translate_browse_path_result_1 :
- The inv "c_ExpandedNodeId_indet /: ran(BrowsePathResult)" is not
  necessary as we have "ran(BrowsePathResult) <:
  dom(conv_ExpandedNodeId_NodeId)". Indeed, the latter is a subset of
  t_ExpandedNodeId. An assertion "ran(BrowsePathResult) <:
  t_ExpandedNodeId" is added to facilitate automated proof.
- The inv related to the codomain of BrowsePathRemainingNodeId shall be
  enhanced by specifying that ran(BrowsePathRemainingNodeId) is a subset
  of t_ExpandedNodeId. This new invariant is true by construction of
  BrowsePathRemainingNodeId and needed by operations, for example,
  free_BrowsePathRemaining. This latter requires that the nodeId to be
  freed belongs to t_ExpandedNodeId.

bsrc/translate_browse_path_result_1.mch

@@ -40,8 +40,8 @@ DEFINITIONS
         size(BrowsePathRemainingNodeId) <= k_n_BrowsePathResPerElt_max  &
         size(BrowsePathRemainingNodeId)  = size(BrowsePathRemainingIndex) &
 
-        c_ExpandedNodeId_indet /: ran(BrowsePathResult) &
-        ran(BrowsePathResult) <: dom(conv_ExpandedNodeId_NodeId)
+        ran(BrowsePathResult) <: dom(conv_ExpandedNodeId_NodeId) &
+        ran(BrowsePathRemainingNodeId) <: t_ExpandedNodeId
 
 ABSTRACT_VARIABLES
     d_variables
@@ -49,6 +49,9 @@ ABSTRACT_VARIABLES
 INVARIANT
     d_invariant
 
+ASSERTIONS
+    ran(BrowsePathResult) <: t_ExpandedNodeId
+
 INITIALISATION
     BrowsePathResult := {} ||
     BrowsePathRemainingNodeId := {} ||