Update user doc for choose op

doc/usr/source/2_input/1_lustre.rst

@@ -1077,10 +1077,84 @@ stateful. Therefore, a frame block initialization cannot contain any ``pre`` or
 operators. This restriction also ensures that initializations are never undefined.
 
 Nondeterministic choice operator
-----------------------------------
-The expression ``choose { var: ty | expression }`` evaluates to a variable
-``var`` that of type ``ty`` that satisfies ``expression``. For example,
-``choose { y: int | y < 50 }`` nondeterminsitically evaluates to 
-some value less than 50. The body ``expression`` can
-reference variable ``var`` as well as any inputs, outputs, or locals 
-that are currently in scope.
+--------------------------------
+There are situations in the design of reactive systems where
+nondeterministic behaviors must be modeled.
+Kind 2 offers a convenient binder of the form
+``choose { x: T | P(x) }`` which denotes an arbitrary stream of
+values of type ``T`` each satisfying the predicate ``P``.
+In the expression above ``x`` is a locally bound variable of type ``T``,
+and ``P(x)`` is a Boolean expression that typically, 
+but not necessarily, contains ``x``. The expression ``P(x)``
+may also contain any input, output, or local variable that
+are in the scope of the ``choose`` expression.
+The following example shows a component using the ``choose``
+operator to define a local stream ``l`` of arbitrary odd values.
+
+.. code-block:: none
+
+   node N(y: int) returns (z:int);
+   (*@contract
+     assume "y is odd" y mod 2 = 1;
+     guarantee "z is even" z mod 2 = 0;
+   *)
+     var l: int;
+   let
+     l = choose { x: int | x mod 2 = 1 };
+     z = y + l;
+   tel
+
+A challenge for the user with the use of ``choose`` expressions arises if
+the specified condition is inconsistent, or more generally, unrealizable.
+In that case, the system model may be satisfied by no execution trace.
+As a consequence, any property, even an inconsistent one, would be trivially
+satisfied by the (inconsistent) system model.
+For instance, the condition of the ``choose`` operator in the node of
+the following example is inconsistent, and thus, there is no realization of
+the system model. As a result, Kind 2 proves the property P1 valid.
+
+.. code-block:: none
+
+   node N(y: int) returns (z: int);
+     var l: int;
+   let
+     l = choose { x : int | x < 0 and x > 0 };
+     z = y + l;
+     check "P1" z > 0 and z < 0;
+   tel
+
+This problem is mitigated by the possibility for
+the user to check that the predicate ``P(x)`` in
+the ``choose`` expression is realizable.
+This is possible because, for each ``choose`` expression occurring in
+a model, Kind 2 introduces an internal imported node whose
+contract restricts the values of the returned output using
+the given predicate as a guarantee.
+The user can take advantage of this fact to detect issues with
+the conditions of ``choose`` expressions by enabling 
+Kind 2's functionality that checks
+the :ref:`realizability of contracts<9_other/11_contract_checks>` of
+imported nodes. When this functionality is enabled, Kind 2 is able to
+detect the problem illustrated in the example above.
+
+It is worth mentioning that Kind 2 does not consider the surrounding
+context when checking the realizability of the introduced imported node.
+Because of this limitation, some checks may fail even if,
+in a broader context where all constraints included in
+the model are considered, the imported node would actually be considered
+realizable. To mitigate this issue, Kind 2 offers an extended version of
+the binder, ``choose { x: T | P(x) assuming Q }``, that
+allows the user to specify an assumption ``Q`` that
+should be taken into account in the realizability check.
+For instance, the realizability check for the ``choose`` expression
+in the following example would fail if the assumption ``a <= b`` 
+was not included.
+
+.. code-block:: none
+
+   node N(a: int) returns (z: int);
+   var b: int;
+   let
+     b = a + 10;
+     z = choose { x: int | a <= x and x <= b assuming a<=b };
+   tel