Merge pull request #1035 from daniel-larraz/disable-any-op

Temporarily deactivate 'any' operator before release

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

@@ -1075,94 +1075,3 @@ 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,10 +287,6 @@ 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,17 +2864,8 @@ 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
 
@@ -2884,37 +2875,13 @@ 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
 
@@ -2924,33 +2891,12 @@ 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
 
@@ -2987,3 +2933,7 @@ Syntax Error!
 main: PARAM ASSUME COLON ASSUME AND
 
 Syntax Error!
+
+one_expr: ASSUME LPARAMBRACKET ASSUME RSQBRACKET
+
+Syntax Error!

src/lustre/lustreParser.mly

@@ -132,7 +132,6 @@ let mk_span start_pos end_pos =
 %token CHECK
 %token REACHABLE
 %token PROVIDED
-%token ASSUMING
 %token INVARIANT
 %token FROM
 %token AT
@@ -156,7 +155,6 @@ let mk_span start_pos end_pos =
 %token HASH
 %token FORALL
 %token EXISTS
-%token ANY
 
 (* Tokens for relations *)
 %token LTE
@@ -219,7 +217,6 @@ let mk_span start_pos end_pos =
 %nonassoc INT REAL 
 %nonassoc NOT
 %nonassoc BVNOT 
-%nonassoc ANY
 %left CARET 
 %left LSQBRACKET DOT DOTPERCENT
 
@@ -942,12 +939,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

@@ -317,7 +317,7 @@ let rec infer_const_attr ctx exp =
   | Activate (_, i, _, _, _)
   | RestartEvery (_, i, _, _)
   | Call (_, i, _) -> (
-    let err = error exp "node call or any operator" in
+    let err = error exp "node call" in
     match lookup_node_ty ctx i with
     | Some (TArr (_, _, exp_ret_tys)) -> (
       match exp_ret_tys with
@@ -1537,7 +1537,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 or any operator"))
+      (ExpectedConstant (kind, "node call"))
   | 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

@@ -603,14 +603,6 @@ 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