From 84274f47494afa8a370db6ad00a571e3410b7934 Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 16 May 2024 16:24:47 +0200 Subject: [PATCH 1/7] exists examples --- tests/testcases/templates/properties/fischer.imiprop | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tests/testcases/templates/properties/fischer.imiprop b/tests/testcases/templates/properties/fischer.imiprop index 14745573..d4ab7635 100644 --- a/tests/testcases/templates/properties/fischer.imiprop +++ b/tests/testcases/templates/properties/fischer.imiprop @@ -5,4 +5,10 @@ (* property := #synth AGnot(forall i in [0, N - 1]: (forall j in [0, N - 1]: loc[p[i]] <> cs)) *) (* Works -> True || False is outside of forall *) -property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False) +(* property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False) *) + +(* Works *) +(* property := #synth AGnot(exists i in [0, N - 1]: (forall i in [0, N - 1]: loc[p[i]] <> cs) && True || False) *) + +(* Works *) +property := #synth AGnot(True && exists i in [0, N - 1]: (loc[p[i]] = cs && loc[p[i]] <> cs) || False) From 8a8a2bdb2da2e5a504aa89300388a4284811f4f4 Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 16 May 2024 16:26:05 +0200 Subject: [PATCH 2/7] Infrastructure for parsing exists. --- src/lib/ParsingStructure.mli | 2 ++ src/lib/PropertyLexer.mll | 1 + src/lib/PropertyParser.mly | 10 +++++++++- 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/src/lib/ParsingStructure.mli b/src/lib/ParsingStructure.mli index d247fe42..55f93919 100644 --- a/src/lib/ParsingStructure.mli +++ b/src/lib/ParsingStructure.mli @@ -445,6 +445,8 @@ type unexpanded_parsed_state_predicate_factor = (* The forall is in this level so we can use it on both sides of `AND` and `OR` *) | Unexpanded_Parsed_forall_simple_predicate of forall_index_data * unexpanded_parsed_simple_predicate | Unexpanded_Parsed_forall_state_predicate of forall_index_data * unexpanded_parsed_state_predicate + | Unexpanded_Parsed_exists_simple_predicate of forall_index_data * unexpanded_parsed_simple_predicate + | Unexpanded_Parsed_exists_state_predicate of forall_index_data * unexpanded_parsed_state_predicate and unexpanded_parsed_state_predicate_term = | Unexpanded_Parsed_state_predicate_term_AND of unexpanded_parsed_state_predicate_term * unexpanded_parsed_state_predicate_term diff --git a/src/lib/PropertyLexer.mll b/src/lib/PropertyLexer.mll index 54eefc66..75e92e6d 100644 --- a/src/lib/PropertyLexer.mll +++ b/src/lib/PropertyLexer.mll @@ -98,6 +98,7 @@ rule token = parse | "before" { CT_BEFORE } | "eventually" { CT_EVENTUALLY } | "everytime" { CT_EVERYTIME } + | "exists" { CT_EXISTS } | "False" { CT_FALSE } | "forall" { CT_FORALL } | "happened" { CT_HAPPENED } diff --git a/src/lib/PropertyParser.mly b/src/lib/PropertyParser.mly index bf00c136..71af4622 100644 --- a/src/lib/PropertyParser.mly +++ b/src/lib/PropertyParser.mly @@ -59,7 +59,7 @@ let resolve_property l = CT_BCBORDER CT_BCLEARN CT_BCRANDOM CT_BCRANDOMSEQ CT_BCSHUFFLE CT_BEFORE CT_COVERCARTOGRAPHY CT_DEADLOCKFREE - CT_E CT_EF CT_EF_timed CT_EFpmax CT_EFpmin CT_EFtmin CT_EG CT_EVENTUALLY CT_EVERYTIME CT_EXEMPLIFY CT_EXHIBIT + CT_E CT_EF CT_EF_timed CT_EFpmax CT_EFpmin CT_EFtmin CT_EG CT_EVENTUALLY CT_EVERYTIME CT_EXEMPLIFY CT_EXHIBIT CT_EXISTS CT_FALSE CT_FORALL CT_HAPPENED CT_HAS CT_IF CT_IMCONVEX CT_IMK CT_IMUNION CT_IN CT_INFCYCLE CT_INFCYCLETHROUGH CT_INFINITY CT_IS @@ -462,6 +462,8 @@ state_predicate_factor: | LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_state_predicate $2 } | forall_common_prefix simple_predicate { Unexpanded_Parsed_forall_simple_predicate ($1, $2) } | forall_common_prefix LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_forall_state_predicate ($1, $3) } + | exists_common_prefix simple_predicate { Unexpanded_Parsed_exists_simple_predicate ($1, $2) } + | exists_common_prefix LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_exists_state_predicate ($1, $3) } ; @@ -809,3 +811,9 @@ forall_common_prefix: { { forall_index_name = $2; forall_lb = $5; forall_ub = $7} } + +exists_common_prefix: + | CT_EXISTS NAME CT_IN LSQBRA arithmetic_expression COMMA arithmetic_expression RSQBRA COLON + { + { forall_index_name = $2; forall_lb = $5; forall_ub = $7} + } From 234c9ccac27b301410f5f9dd72cbf9d3b57577db Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 16 May 2024 16:26:24 +0200 Subject: [PATCH 3/7] Expanding exists. --- src/lib/Templates.ml | 71 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 67 insertions(+), 4 deletions(-) diff --git a/src/lib/Templates.ml b/src/lib/Templates.ml index 3ab3f171..3f12d0a8 100644 --- a/src/lib/Templates.ml +++ b/src/lib/Templates.ml @@ -585,6 +585,7 @@ and instantiate_state_factor (param_map: var_map): unexpanded_parsed_state_predi | Unexpanded_Parsed_state_predicate_factor_NOT f -> Unexpanded_Parsed_state_predicate_factor_NOT (instantiate_state_factor param_map f) | Unexpanded_Parsed_simple_predicate spred -> Unexpanded_Parsed_simple_predicate (instantiate_simple_predicate param_map spred) | Unexpanded_Parsed_state_predicate pred -> Unexpanded_Parsed_state_predicate (instantiate_state_predicate param_map pred) + (* TODO: merge next 4 branches *) | Unexpanded_Parsed_forall_state_predicate (index_data, pred) -> let binded_name = index_data.forall_index_name in let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in @@ -600,15 +601,30 @@ and instantiate_state_factor (param_map: var_map): unexpanded_parsed_state_predi | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> let binded_name = index_data.forall_index_name in let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in - (* Here we remove the binde to allow the inner forall to rebind it. *) - (* This means that if the user had something like `forall i in [0, 1]: (forall i in [0, 1]: (p(i)) && q(i))`, the inner one will be - substituted first, and the outer one will substitute only `q(i)` *) Hashtbl.remove param_map binded_name; let r = Unexpanded_Parsed_forall_simple_predicate (index_data, instantiate_simple_predicate param_map spred) in begin match prev_binded_value_opt with | Some v -> Hashtbl.add param_map binded_name v; r | None -> r end + | Unexpanded_Parsed_exists_state_predicate (index_data, pred) -> + let binded_name = index_data.forall_index_name in + let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in + Hashtbl.remove param_map binded_name; + let r = Unexpanded_Parsed_exists_state_predicate (index_data, instantiate_state_predicate param_map pred) in + begin match prev_binded_value_opt with + | Some v -> Hashtbl.add param_map binded_name v; r + | None -> r + end + | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) -> + let binded_name = index_data.forall_index_name in + let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in + Hashtbl.remove param_map binded_name; + let r = Unexpanded_Parsed_exists_simple_predicate (index_data, instantiate_simple_predicate param_map spred) in + begin match prev_binded_value_opt with + | Some v -> Hashtbl.add param_map binded_name v; r + | None -> r + end let expand_loc_pred (g_decls: variable_declarations): unexpanded_parsed_loc_predicate -> parsed_loc_predicate = function | Unexpanded_Parsed_loc_predicate_EQ (aut_name, loc) -> Parsed_loc_predicate_EQ (expand_name_or_access g_decls aut_name, loc) @@ -633,7 +649,7 @@ and expand_state_term (g_decls: variable_declarations): unexpanded_parsed_state_ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_parsed_state_predicate_factor): parsed_state_predicate_factor = match factor with - (* TODO: Refactor the next two branches *) + (* TODO: merge next 4 branches *) | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> begin let indices = indices_from_forall_index_data g_decls index_data in (* Here we reverse the list to preserve the order of the index after the fold *) @@ -686,6 +702,53 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par in List.fold_left fold_fun (Parsed_state_predicate pred_i) is end + | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) -> begin + let indices = indices_from_forall_index_data g_decls index_data in + match List.rev indices with + | [] -> failwith "error or vacuity?" + | i :: is -> + (* Compute the disjunction of spred instantiated with each idx in (i::is) *) + let instantiate_spred_with idx = + let param_map_idx = gen_aux_var_tbl idx index_data in + instantiate_simple_predicate param_map_idx spred |> + expand_simple_predicate g_decls + in + let spred_i = instantiate_spred_with i in + let state_pred_of_simple_pred p = + Parsed_state_predicate_term (Parsed_state_predicate_factor (Parsed_simple_predicate p)) + in + let fold_fun acc idx = + let spred_idx = instantiate_spred_with idx in + let spred_idx_state = state_pred_of_simple_pred spred_idx in + match acc with + | Parsed_state_predicate p -> + Parsed_state_predicate (Parsed_state_predicate_OR (spred_idx_state, p)) + | Parsed_simple_predicate p -> + let p_state= state_pred_of_simple_pred p in + Parsed_state_predicate (Parsed_state_predicate_OR (spred_idx_state, p_state)) + | _ -> failwith "[expand_state_factor]: unreachable" + in + List.fold_left fold_fun (Parsed_simple_predicate spred_i) is + end + | Unexpanded_Parsed_exists_state_predicate (index_data, pred) -> begin + let indices = indices_from_forall_index_data g_decls index_data in + match List.rev indices with + | [] -> failwith "error or vacuity?" + | i :: is -> + let instantiate_pred_with idx = + let param_map_idx = gen_aux_var_tbl idx index_data in + instantiate_state_predicate param_map_idx pred |> + expand_state_predicate g_decls + in + let pred_i = instantiate_pred_with i in + let fold_fun acc idx = + let pred_idx = instantiate_pred_with idx in + match acc with + | Parsed_state_predicate p -> Parsed_state_predicate (Parsed_state_predicate_OR (pred_idx, p)) + | _ -> failwith "[expand_state_factor]: unreachable" + in + List.fold_left fold_fun (Parsed_state_predicate pred_i) is + end | Unexpanded_Parsed_state_predicate_factor_NOT f -> Parsed_state_predicate_factor_NOT (expand_state_factor g_decls f) | Unexpanded_Parsed_simple_predicate spred -> Parsed_simple_predicate (expand_simple_predicate g_decls spred) | Unexpanded_Parsed_state_predicate pred -> Parsed_state_predicate (expand_state_predicate g_decls pred) From ea1db49fd2ea28f91fd3bc15b27cb8899ee1f929 Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 30 May 2024 22:42:03 +0200 Subject: [PATCH 4/7] Refactor on expand_state_factor --- src/lib/Templates.ml | 46 +++++++++++++++++--------------------------- 1 file changed, 18 insertions(+), 28 deletions(-) diff --git a/src/lib/Templates.ml b/src/lib/Templates.ml index 3f12d0a8..b6ec9b4e 100644 --- a/src/lib/Templates.ml +++ b/src/lib/Templates.ml @@ -648,6 +648,16 @@ and expand_state_term (g_decls: variable_declarations): unexpanded_parsed_state_ | Unexpanded_Parsed_state_predicate_factor f -> Parsed_state_predicate_factor (expand_state_factor g_decls f) and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_parsed_state_predicate_factor): parsed_state_predicate_factor = + let instantiate_spred_with index_data spred idx = + let param_map_idx = gen_aux_var_tbl idx index_data in + instantiate_simple_predicate param_map_idx spred |> + expand_simple_predicate g_decls + in + let instantiate_pred_with index_data pred idx = + let param_map_idx = gen_aux_var_tbl idx index_data in + instantiate_state_predicate param_map_idx pred |> + expand_state_predicate g_decls + in match factor with (* TODO: merge next 4 branches *) | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> begin @@ -657,15 +667,10 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par | [] -> failwith "error or vacuity?" | i :: is -> (* Compute the conjunction of spred instantiated with each idx in (i::is) *) - let instantiate_spred_with idx = - let param_map_idx = gen_aux_var_tbl idx index_data in - instantiate_simple_predicate param_map_idx spred |> - expand_simple_predicate g_decls - in let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in - let spred_i = instantiate_spred_with i in + let spred_i = instantiate_spred_with index_data spred i in let fold_fun acc idx = - let spred_idx = instantiate_spred_with idx in + let spred_idx = instantiate_spred_with index_data spred idx in let spred_idx_term = term_of_simple_pred spred_idx in match acc with | Parsed_state_predicate (Parsed_state_predicate_term t) -> @@ -682,15 +687,10 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par match List.rev indices with | [] -> failwith "error or vacuity?" | i :: is -> - let instantiate_pred_with idx = - let param_map_idx = gen_aux_var_tbl idx index_data in - instantiate_state_predicate param_map_idx pred |> - expand_state_predicate g_decls - in - let pred_i = instantiate_pred_with i in + let pred_i = instantiate_pred_with index_data pred i in let term_of_state_pred p = Parsed_state_predicate_factor (Parsed_state_predicate p) in let fold_fun acc idx = - let pred_idx = instantiate_pred_with idx in + let pred_idx = instantiate_pred_with index_data pred idx in let pred_idx_term = term_of_state_pred pred_idx in match acc with | Parsed_state_predicate (Parsed_state_predicate_term t) -> @@ -708,17 +708,12 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par | [] -> failwith "error or vacuity?" | i :: is -> (* Compute the disjunction of spred instantiated with each idx in (i::is) *) - let instantiate_spred_with idx = - let param_map_idx = gen_aux_var_tbl idx index_data in - instantiate_simple_predicate param_map_idx spred |> - expand_simple_predicate g_decls - in - let spred_i = instantiate_spred_with i in + let spred_i = instantiate_spred_with index_data spred i in let state_pred_of_simple_pred p = Parsed_state_predicate_term (Parsed_state_predicate_factor (Parsed_simple_predicate p)) in let fold_fun acc idx = - let spred_idx = instantiate_spred_with idx in + let spred_idx = instantiate_spred_with index_data spred idx in let spred_idx_state = state_pred_of_simple_pred spred_idx in match acc with | Parsed_state_predicate p -> @@ -735,14 +730,9 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par match List.rev indices with | [] -> failwith "error or vacuity?" | i :: is -> - let instantiate_pred_with idx = - let param_map_idx = gen_aux_var_tbl idx index_data in - instantiate_state_predicate param_map_idx pred |> - expand_state_predicate g_decls - in - let pred_i = instantiate_pred_with i in + let pred_i = instantiate_pred_with index_data pred i in let fold_fun acc idx = - let pred_idx = instantiate_pred_with idx in + let pred_idx = instantiate_pred_with index_data pred idx in match acc with | Parsed_state_predicate p -> Parsed_state_predicate (Parsed_state_predicate_OR (pred_idx, p)) | _ -> failwith "[expand_state_factor]: unreachable" From b543561261045d9892caac335e5553d03cbd1ade Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 30 May 2024 22:53:17 +0200 Subject: [PATCH 5/7] Show a warning if the range of forall/exists is empty. --- src/lib/Templates.ml | 19 +++++++++++++------ .../templates/properties/fischer.imiprop | 3 +++ 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/lib/Templates.ml b/src/lib/Templates.ml index b6ec9b4e..6d6a5bd8 100644 --- a/src/lib/Templates.ml +++ b/src/lib/Templates.ml @@ -1,5 +1,6 @@ open ParsingStructure;; open ParsingStructureUtilities;; +open ImitatorUtilities;; (* Utilities *) @@ -124,7 +125,10 @@ let indices_from_forall_index_data g_decls forall_index_data = let { forall_index_name = _; forall_lb; forall_ub } = forall_index_data in let forall_lb_val = eval_parsed_arithmetic_expr g_decls forall_lb |> NumConst.to_bounded_int in let forall_ub_val = eval_parsed_arithmetic_expr g_decls forall_ub |> NumConst.to_bounded_int in - List.init (forall_ub_val - forall_lb_val + 1) (fun i -> i + forall_lb_val) + if forall_ub_val < forall_lb_val then + [] + else + List.init (forall_ub_val - forall_lb_val + 1) (fun i -> i + forall_lb_val) let gen_aux_var_tbl i index_data = Hashtbl.of_seq (List.to_seq [(index_data.forall_index_name, Arg_int (NumConst.numconst_of_int i))]) @@ -659,12 +663,12 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par expand_state_predicate g_decls in match factor with - (* TODO: merge next 4 branches *) | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> begin let indices = indices_from_forall_index_data g_decls index_data in (* Here we reverse the list to preserve the order of the index after the fold *) match List.rev indices with - | [] -> failwith "error or vacuity?" + | [] -> print_warning "Trying to expand a forall with an empty range."; + Parsed_simple_predicate Parsed_state_predicate_true | i :: is -> (* Compute the conjunction of spred instantiated with each idx in (i::is) *) let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in @@ -685,7 +689,8 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par | Unexpanded_Parsed_forall_state_predicate (index_data, pred) -> begin let indices = indices_from_forall_index_data g_decls index_data in match List.rev indices with - | [] -> failwith "error or vacuity?" + | [] -> print_warning "Trying to expand a forall with an empty range."; + Parsed_simple_predicate Parsed_state_predicate_true | i :: is -> let pred_i = instantiate_pred_with index_data pred i in let term_of_state_pred p = Parsed_state_predicate_factor (Parsed_state_predicate p) in @@ -705,7 +710,8 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) -> begin let indices = indices_from_forall_index_data g_decls index_data in match List.rev indices with - | [] -> failwith "error or vacuity?" + | [] -> print_warning "Trying to expand an exists with an empty range."; + Parsed_simple_predicate Parsed_state_predicate_false | i :: is -> (* Compute the disjunction of spred instantiated with each idx in (i::is) *) let spred_i = instantiate_spred_with index_data spred i in @@ -728,7 +734,8 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par | Unexpanded_Parsed_exists_state_predicate (index_data, pred) -> begin let indices = indices_from_forall_index_data g_decls index_data in match List.rev indices with - | [] -> failwith "error or vacuity?" + | [] -> print_warning "Trying to expand an exists with an empty range."; + Parsed_simple_predicate Parsed_state_predicate_false | i :: is -> let pred_i = instantiate_pred_with index_data pred i in let fold_fun acc idx = diff --git a/tests/testcases/templates/properties/fischer.imiprop b/tests/testcases/templates/properties/fischer.imiprop index d4ab7635..080dc42d 100644 --- a/tests/testcases/templates/properties/fischer.imiprop +++ b/tests/testcases/templates/properties/fischer.imiprop @@ -12,3 +12,6 @@ (* Works *) property := #synth AGnot(True && exists i in [0, N - 1]: (loc[p[i]] = cs && loc[p[i]] <> cs) || False) + +(* Empty range raises a warning *) +(* property := #synth AGnot(True && exists i in [100, N - 1]: (loc[p[i]] = cs && loc[p[i]] <> cs) || False) *) From b81dcf814af76eec085c7da7f77ddff19b83ad61 Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Thu, 30 May 2024 23:09:25 +0200 Subject: [PATCH 6/7] More refactor on expand_state_factor. --- src/lib/Templates.ml | 85 ++++++++++++++++++++------------------------ 1 file changed, 39 insertions(+), 46 deletions(-) diff --git a/src/lib/Templates.ml b/src/lib/Templates.ml index 6d6a5bd8..8e84065b 100644 --- a/src/lib/Templates.ml +++ b/src/lib/Templates.ml @@ -662,36 +662,40 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par instantiate_state_predicate param_map_idx pred |> expand_state_predicate g_decls in - match factor with - | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> begin - let indices = indices_from_forall_index_data g_decls index_data in - (* Here we reverse the list to preserve the order of the index after the fold *) - match List.rev indices with + let apply_fn_in_forall_range index_data fn = + let indices = indices_from_forall_index_data g_decls index_data in + match List.rev indices with | [] -> print_warning "Trying to expand a forall with an empty range."; Parsed_simple_predicate Parsed_state_predicate_true - | i :: is -> - (* Compute the conjunction of spred instantiated with each idx in (i::is) *) - let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in - let spred_i = instantiate_spred_with index_data spred i in - let fold_fun acc idx = - let spred_idx = instantiate_spred_with index_data spred idx in - let spred_idx_term = term_of_simple_pred spred_idx in - match acc with - | Parsed_state_predicate (Parsed_state_predicate_term t) -> - Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, t))) - | Parsed_simple_predicate p -> (* Only first iteration of fold, after that I know for sure is a term *) - let p_term = term_of_simple_pred p in - Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, p_term))) - | _ -> failwith "[expand_state_factor]: unreachable" - in - List.fold_left fold_fun (Parsed_simple_predicate spred_i) is - end - | Unexpanded_Parsed_forall_state_predicate (index_data, pred) -> begin - let indices = indices_from_forall_index_data g_decls index_data in - match List.rev indices with - | [] -> print_warning "Trying to expand a forall with an empty range."; - Parsed_simple_predicate Parsed_state_predicate_true - | i :: is -> + | i :: is -> fn i is + in + let apply_fn_in_exists_range index_data fn = + let indices = indices_from_forall_index_data g_decls index_data in + match List.rev indices with + | [] -> print_warning "Trying to expand an exists with an empty range."; + Parsed_simple_predicate Parsed_state_predicate_false + | i :: is -> fn i is + in + match factor with + | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> + apply_fn_in_forall_range index_data (fun i is -> + (* Compute the conjunction of spred instantiated with each idx in (i::is) *) + let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in + let spred_i = instantiate_spred_with index_data spred i in + let fold_fun acc idx = + let spred_idx = instantiate_spred_with index_data spred idx in + let spred_idx_term = term_of_simple_pred spred_idx in + match acc with + | Parsed_state_predicate (Parsed_state_predicate_term t) -> + Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, t))) + | Parsed_simple_predicate p -> (* Only first iteration of fold, after that I know for sure is a term *) + let p_term = term_of_simple_pred p in + Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, p_term))) + | _ -> failwith "[expand_state_factor]: unreachable" + in + List.fold_left fold_fun (Parsed_simple_predicate spred_i) is) + | Unexpanded_Parsed_forall_state_predicate (index_data, pred) -> + apply_fn_in_forall_range index_data (fun i is -> let pred_i = instantiate_pred_with index_data pred i in let term_of_state_pred p = Parsed_state_predicate_factor (Parsed_state_predicate p) in let fold_fun acc idx = @@ -705,14 +709,9 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (pred_idx_term, p_term))) | _ -> failwith "[expand_state_factor]: unreachable" in - List.fold_left fold_fun (Parsed_state_predicate pred_i) is - end - | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) -> begin - let indices = indices_from_forall_index_data g_decls index_data in - match List.rev indices with - | [] -> print_warning "Trying to expand an exists with an empty range."; - Parsed_simple_predicate Parsed_state_predicate_false - | i :: is -> + List.fold_left fold_fun (Parsed_state_predicate pred_i) is) + | Unexpanded_Parsed_exists_simple_predicate (index_data, spred) -> + apply_fn_in_exists_range index_data (fun i is -> (* Compute the disjunction of spred instantiated with each idx in (i::is) *) let spred_i = instantiate_spred_with index_data spred i in let state_pred_of_simple_pred p = @@ -729,14 +728,9 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par Parsed_state_predicate (Parsed_state_predicate_OR (spred_idx_state, p_state)) | _ -> failwith "[expand_state_factor]: unreachable" in - List.fold_left fold_fun (Parsed_simple_predicate spred_i) is - end - | Unexpanded_Parsed_exists_state_predicate (index_data, pred) -> begin - let indices = indices_from_forall_index_data g_decls index_data in - match List.rev indices with - | [] -> print_warning "Trying to expand an exists with an empty range."; - Parsed_simple_predicate Parsed_state_predicate_false - | i :: is -> + List.fold_left fold_fun (Parsed_simple_predicate spred_i) is) + | Unexpanded_Parsed_exists_state_predicate (index_data, pred) -> + apply_fn_in_exists_range index_data (fun i is -> let pred_i = instantiate_pred_with index_data pred i in let fold_fun acc idx = let pred_idx = instantiate_pred_with index_data pred idx in @@ -744,8 +738,7 @@ and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_par | Parsed_state_predicate p -> Parsed_state_predicate (Parsed_state_predicate_OR (pred_idx, p)) | _ -> failwith "[expand_state_factor]: unreachable" in - List.fold_left fold_fun (Parsed_state_predicate pred_i) is - end + List.fold_left fold_fun (Parsed_state_predicate pred_i) is) | Unexpanded_Parsed_state_predicate_factor_NOT f -> Parsed_state_predicate_factor_NOT (expand_state_factor g_decls f) | Unexpanded_Parsed_simple_predicate spred -> Parsed_simple_predicate (expand_simple_predicate g_decls spred) | Unexpanded_Parsed_state_predicate pred -> Parsed_state_predicate (expand_state_predicate g_decls pred) From f8d18f9bb6bd24ca1c33c54fe4463a0ae5c4ad1a Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Fri, 31 May 2024 00:06:54 +0200 Subject: [PATCH 7/7] Documentation forall/exists in properties file. --- doc/IMITATOR-user-manual.tex | 31 ++++++++++++++++++++++++------- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/doc/IMITATOR-user-manual.tex b/doc/IMITATOR-user-manual.tex index 121fd100..28e46cb9 100644 --- a/doc/IMITATOR-user-manual.tex +++ b/doc/IMITATOR-user-manual.tex @@ -2114,13 +2114,30 @@ \section{Model templates}\label{section:templates} \end{example} \paragraph{Templates in properties} -The \styleIMI{forall} construction can also be used in properties. -Below is an example of property using such a syntax (unrelated to the former model example). -Note that \styleIMI{NB} is a constant defined in the model, leading to an easy specification of properties. -\begin{IMITATORproperty} -property := #synth EF(forall i in [0, NB - 1]: loc[train[i]] = train_End); -\end{IMITATORproperty} +The \styleIMI{forall} construction can also be used in properties. We also added the analogous \styleIMI{exists} construct, +which creates a disjunction instead of a conjunction. The user can nest \styleIMI{forall} and \styleIMI{exists} +in any way he wants. The syntax is exactly the same as for the models. but it has +lower precedence in comparison to all the other logical operators. This means that, unless the user enclose +the predicate inside the forall with parenthesis, only the first statement will be considered as part of +the \styleIMI{forall}/\styleIMI{exists}. + + +\begin{example} + Below is an example of property using such a syntax (unrelated to the former model example). It clarifies the precedence and what can be done with nesting. + Note that \styleIMI{NB} is a constant defined in the model, leading to an easy specification of properties. + + \begin{IMITATORproperty} + (* True || False is outside of the forall *) + property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False) + + (* True || False is inside of the forall *) + property := #synth AGnot(forall i in [0, N - 1]: (loc[p[i]] <> cs && True || False)) + + (* Nesting *) + property := #synth AGnot(exists i in [0, N - 1]: (forall i in [0, N - 1]: loc[p[i]] <> cs) && True || False) + \end{IMITATORproperty} +\end{example} @@ -5757,7 +5774,7 @@ \section{Grammar of the property file}\label{section:grammar-property} $|$ & \styleIMI{PRPC} \styleIMI{(} \nt{state\_predicate} \styleIMI{,} \nt{hyper\_rectangle} \nt{step\_opt} \styleIMI{)} \\ % PTG - $|$ & \styleIMI{Win(} \nt{state\_predicate} \styleIMI{)} \\ + $|$ & \styleIMI{Win(} \nt{state\_predicate} \styleIMI{)} \\ % Observer pattern $|$ & \styleIMI{pattern(} \nt{pattern} \styleIMI{)} \\