From 16d922ccc10382ceef998636ff790afa4c30bde4 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 26 Dec 2023 18:50:46 -0600 Subject: [PATCH] Reintroduce 'any' operator This reverts commit c854bb95830810e63447a218852e959179f5ab03. --- doc/usr/source/2_input/1_lustre.rst | 91 ++++++++++++++++++++++ src/lustre/lustreLexer.mll | 4 + src/lustre/lustreParser.messages | 58 +++++++++++++- src/lustre/lustreParser.mly | 7 +- src/lustre/lustreTypeChecker.ml | 4 +- tests/ounit/lustre/testLustreFrontend.ml | 8 ++ tests/regression/success/choose_simple.lus | 13 ++++ 7 files changed, 177 insertions(+), 8 deletions(-) create mode 100644 tests/regression/success/choose_simple.lus diff --git a/doc/usr/source/2_input/1_lustre.rst b/doc/usr/source/2_input/1_lustre.rst index 89437c250..6078c38c0 100644 --- a/doc/usr/source/2_input/1_lustre.rst +++ b/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. diff --git a/src/lustre/lustreLexer.mll b/src/lustre/lustreLexer.mll index a98ffdf96..1ad008a86 100644 --- a/src/lustre/lustreLexer.mll +++ b/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 ; diff --git a/src/lustre/lustreParser.messages b/src/lustre/lustreParser.messages index 190e0f547..ee6c9b31b 100644 --- a/src/lustre/lustreParser.messages +++ b/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! diff --git a/src/lustre/lustreParser.mly b/src/lustre/lustreParser.mly index ff57720ac..87b711a72 100644 --- a/src/lustre/lustreParser.mly +++ b/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) diff --git a/src/lustre/lustreTypeChecker.ml b/src/lustre/lustreTypeChecker.ml index 703aa51e2..205d1bdd6 100644 --- a/src/lustre/lustreTypeChecker.ml +++ b/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 diff --git a/tests/ounit/lustre/testLustreFrontend.ml b/tests/ounit/lustre/testLustreFrontend.ml index d5654dd34..471d67c34 100644 --- a/tests/ounit/lustre/testLustreFrontend.ml +++ b/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 diff --git a/tests/regression/success/choose_simple.lus b/tests/regression/success/choose_simple.lus new file mode 100644 index 000000000..87cd0cc9e --- /dev/null +++ b/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;