Reintroduce 'any' operator

This reverts commit c854bb9.

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

@@ -1075,3 +1075,94 @@ cannot be placed within if statements or frame blocks.
 Since an initialization only defines a variable at the first timestep, it need not be 
 stateful. Therefore, a frame block initialization cannot contain any ``pre`` or ``->`` 
 operators. This restriction also ensures that initializations are never undefined.
+
+Nondeterministic choice operator
+--------------------------------
+There are situations in the design of reactive systems where
+nondeterministic behaviors must be modeled.
+Kind 2 offers a convenient binder of the form
+``any { x: T | P(x) }`` which denotes an arbitrary stream of
+values of type ``T`` satisfying the predicate ``P``.
+In the expression above ``x`` is a locally bound variable of
+Lustre type ``T``, and ``P(x)`` is a Lustre 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 ``any`` expression.
+The following example shows a component using the ``any``
+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 = any { x: int | x mod 2 = 1 };
+     z = y + l;
+   tel
+
+In addition, the ``any`` operator can take any Lustre type as argument.
+For instance, the expression ``any int`` is also accepted
+and denotes an arbitrary stream of values of type ``int``.
+
+A challenge for the user with the use of ``any`` 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 ``any`` 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 = any { 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 ``any`` expression is realizable.
+This is possible because, for each ``any`` 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 ``any`` 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, ``any { 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 ``any`` 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 = any { x: int | a <= x and x <= b assuming a<=b };
+     check z>=a+10 => z=b;
+   tel
+
+Moreover, Kind 2 checks that any specified assumption in
+a ``any`` expression holds when model checking the component.

src/lustre/lustreLexer.mll

@@ -287,6 +287,10 @@ let keyword_table = mk_hashtbl [
   "with", WITH ;
   "div", INTDIV ;
   "mod", MOD ;
+
+  (* 'Any' operator *)
+  "any", ANY ;
+  "assuming", ASSUMING ;
 
   (* Clock operators *)
   "when", WHEN ;

src/lustre/lustreParser.messages

@@ -2864,8 +2864,17 @@ one_expr: ASSUME LPARAMBRACKET SUBRANGE LSQBRACKET ASSUME COMMA ASSUME COMMA
 
 Syntax Error!
 
+one_expr: ANY XOR
 
+Syntax Error!
+
+one_expr: ANY LCURLYBRACKET XOR
+
+Syntax Error!
+
+one_expr: ANY LCURLYBRACKET ASSUME COLON ASSUME BAR XOR
 
+Syntax Error!
 
 one_expr: ASSUME BAR XOR
 
@@ -2875,13 +2884,37 @@ one_expr: ASSUME BAR DECIMAL WEAKLY
 
 Syntax Error!
 
+one_expr: ANY LCURLYBRACKET ASSUME COLON ASSUME BAR DECIMAL WEAKLY
+
+Syntax Error!
+
+one_expr: ANY LCURLYBRACKET ASSUME XOR
+
+Syntax Error!
+
+one_expr: ANY LCURLYBRACKET ASSUME COLON XOR
+
+Syntax Error!
+
+one_expr: ANY LCURLYBRACKET ASSUME COLON ASSUME WHEN
 
+Syntax Error!
 
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY XOR
 
+Syntax Error!
 
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY LCURLYBRACKET XOR
 
+Syntax Error!
 
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY LCURLYBRACKET ASSUME COLON ASSUME BAR XOR
+
+Syntax Error!
 
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY LCURLYBRACKET ASSUME COLON ASSUME BAR DECIMAL WEAKLY
+
+Syntax Error!
 
 main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ASSUME BAR XOR
 
@@ -2891,12 +2924,33 @@ main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ASSUME BAR
 
 Syntax Error!
 
+one_expr: ANY LCURLYBRACKET ASSUME COLON ASSUME BAR ASSUME ASSUMING XOR
+
+Syntax Error!
+
+one_expr: ANY LCURLYBRACKET ASSUME COLON ASSUME BAR ASSUME ASSUMING DECIMAL WEAKLY
 
+Syntax Error!
 
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY LCURLYBRACKET ASSUME COLON ASSUME BAR ASSUME ASSUMING XOR
 
+Syntax Error!
 
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY LCURLYBRACKET ASSUME COLON ASSUME BAR ASSUME ASSUMING DECIMAL WEAKLY
 
+Syntax Error!
 
+one_expr: ANY ASSUME WEAKLY
+
+Syntax Error!
+
+one_expr: ANY ASSUME CARET DECIMAL WEAKLY
+
+Syntax Error!
+
+main: FUNCTION ASSUME LPAREN RPAREN RETURNS LPAREN RPAREN LET ASSERT ANY ASSUME RPARAMBRACKET
+
+Syntax Error!
 
 main: PARAM XOR
 
@@ -2933,7 +2987,3 @@ Syntax Error!
 main: PARAM ASSUME COLON ASSUME AND
 
 Syntax Error!
-
-one_expr: ASSUME LPARAMBRACKET ASSUME RSQBRACKET
-
-Syntax Error!

src/lustre/lustreParser.mly

@@ -132,6 +132,7 @@ let mk_span start_pos end_pos =
 %token CHECK
 %token REACHABLE
 %token PROVIDED
+%token ASSUMING
 %token INVARIANT
 %token FROM
 %token AT
@@ -155,6 +156,7 @@ let mk_span start_pos end_pos =
 %token HASH
 %token FORALL
 %token EXISTS
+%token ANY
 
 (* Tokens for relations *)
 %token LTE
@@ -217,6 +219,7 @@ let mk_span start_pos end_pos =
 %nonassoc INT REAL 
 %nonassoc NOT
 %nonassoc BVNOT 
+%nonassoc ANY
 %left CARET 
 %left LSQBRACKET DOT DOTPERCENT
 
@@ -939,12 +942,12 @@ pexpr(Q):
     { A.TernaryOp (mk_pos $startpos, A.Ite, e1, e2, e3) }
 
   (* 'Any' operation *)
-  (*| ANY; LCURLYBRACKET; id = typed_ident; BAR; e = pexpr(Q); RCURLYBRACKET
+  | ANY; LCURLYBRACKET; id = typed_ident; BAR; e = pexpr(Q); RCURLYBRACKET
     { A.AnyOp (mk_pos $startpos, id, e, None) } 
   | ANY; LCURLYBRACKET; id = typed_ident; BAR; e1 = pexpr(Q); ASSUMING; e2 = pexpr(Q); RCURLYBRACKET
     { A.AnyOp (mk_pos $startpos, id, e1, Some e2) } 
   | ANY; ty = lustre_type;
-    { A.AnyOp (mk_pos $startpos, (mk_pos $startpos, HString.mk_hstring "_", ty), Const(mk_pos $startpos, True), None)}*)
+    { A.AnyOp (mk_pos $startpos, (mk_pos $startpos, HString.mk_hstring "_", ty), Const(mk_pos $startpos, True), None)}
 
   (* Recursive node call *)
   | WITH; pexpr(Q); THEN; pexpr(Q); ELSE; pexpr(Q) 

src/lustre/lustreTypeChecker.ml

@@ -309,7 +309,7 @@ let rec infer_const_attr ctx exp =
   | Activate (_, i, _, _, _)
   | RestartEvery (_, i, _, _)
   | Call (_, i, _) -> (
-    let err = error exp "node call" in
+    let err = error exp "node call or any operator" in
     match lookup_node_ty ctx i with
     | Some (TArr (_, _, exp_ret_tys)) -> (
       match exp_ret_tys with
@@ -1507,7 +1507,7 @@ and check_const_integer_expr ctx kind e =
   match infer_type_expr ctx e with
   | Error (`LustreTypeCheckerError (pos, UnboundNodeName _)) ->
     type_error pos
-      (ExpectedConstant (kind, "node call"))
+      (ExpectedConstant (kind, "node call or any operator"))
   | Ok ty ->
     let* eq = eq_lustre_type ctx ty (LA.Int (LH.pos_of_expr e)) in
     if eq then

tests/ounit/lustre/testLustreFrontend.ml

@@ -599,6 +599,14 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [
     match load_file "./lustreTypeChecker/open_interval.lus" with
     | Error (`LustreTypeCheckerError (_, IntervalMustHaveBound)) -> true
     | _ -> false);
+  mk_test "test nondeterministic choice type error" (fun () ->
+    match load_file "./lustreTypeChecker/nondeterministic_choice.lus" with
+    | Error (`LustreTypeCheckerError (_, ExpectedIntegerTypes _)) -> true
+    | _ -> false);
+  mk_test "test nondeterministic choice type error 2" (fun () ->
+    match load_file "./lustreTypeChecker/nondeterministic_choice_2.lus" with
+    | Error (`LustreTypeCheckerError (_, UnificationFailed _)) -> true
+    | _ -> false);
   mk_test "test temporal op in const" (fun () ->
     match load_file "./lustreSyntaxChecks/const_not_const.lus" with
     | Error (`LustreTypeCheckerError (_, ExpectedConstant _)) -> true

tests/regression/success/choose_simple.lus

@@ -0,0 +1,13 @@
+const x1: int = 0;
+
+node main (a: int) returns (y, z: int); 
+var x2, b: int;
+let 
+  x2 = any {x: int | x > x1 };
+  y = any { x: int | x + x2 < 50 };
+  check y < 100;
+
+  b = a + 10;
+  z = any { x: int | a <= x and x <= b assuming a<=b };
+  check a <= z and z <= b;
+tel;