From 54d786ddb47a45aea6f275e85688b5cf1b9b165f Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 25 Apr 2024 11:34:52 +0200 Subject: [PATCH] add support for using forall index in linear constraint --- src/lib/Templates.ml | 10 +++++++++- tests/testcases/templates/syntatic_check.imi | 9 +++++---- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/lib/Templates.ml b/src/lib/Templates.ml index ddf60e892..54c6ef144 100644 --- a/src/lib/Templates.ml +++ b/src/lib/Templates.ml @@ -84,7 +84,15 @@ let instantiate_convex_predicate (param_map : var_map) (inv : convex_predicate) let rec instantiate_linear_term (param_map : var_map) (term : unexpanded_linear_term) : unexpanded_linear_term = match term with - | Unexpanded_constant _ | Unexpanded_variable (_, Var_name _) -> term + | Unexpanded_constant _ -> term + | Unexpanded_variable (c, Var_name name) -> begin + match Hashtbl.find_opt param_map name with + | None -> Unexpanded_variable (c, Var_name name) + | Some (Arg_name name') -> Unexpanded_variable (c, Var_name name') + | Some (Arg_int i_val) -> Unexpanded_constant i_val + | Some (Arg_float f_val) -> Unexpanded_constant f_val + | Some (Arg_bool _) -> failwith "[instantiate_linear_term]: boolean variable in linear constraint." + end | Unexpanded_variable (c, Var_array_access (arr_name, index)) -> let index' = instantiate_discrete_arithmetic_expression param_map index in Unexpanded_variable (c, Var_array_access (arr_name, index')) diff --git a/tests/testcases/templates/syntatic_check.imi b/tests/testcases/templates/syntatic_check.imi index c7f57c37e..80dee5832 100644 --- a/tests/testcases/templates/syntatic_check.imi +++ b/tests/testcases/templates/syntatic_check.imi @@ -13,7 +13,7 @@ template p(i : int) actions: acts[2 * i]; -loc A: invariant x[i] <= params[2 * i] +loc A: invariant x[i] <= params[i] when id = IDLE do { x[i] := 0 } sync acts[2 * i] goto req; loc req: invariant x[i] <= k @@ -28,17 +28,18 @@ loc cs: invariant True end -forall i in [0, 2]: instantiate p[i] := p(i); +forall i in [0, 1]: instantiate p[i] := p(i); init := { discrete = + forall i in [0, 1]: loc[p[i]] := A, id := IDLE, ; continuous = - x[0] = 0 - & x[1] = 0 + forall i in [0, 1]: x[i] = i & + forall i in [0, 1]: params[i] >= 0 ; }