diff --git a/core/KaSa_rep/backend/ckappa_site_graph.mli b/core/KaSa_rep/backend/ckappa_site_graph.mli index 2b4405c90..a979fc749 100644 --- a/core/KaSa_rep/backend/ckappa_site_graph.mli +++ b/core/KaSa_rep/backend/ckappa_site_graph.mli @@ -43,5 +43,5 @@ val internal_pair_list_to_list : Ckappa_sig.c_site_name -> Site_graphs.KaSa_site_graph.agent_id -> Ckappa_sig.c_site_name -> - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) list list -> + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) list list -> Exception.exceptions_caught_and_uncaught * Site_graphs.KaSa_site_graph.t list diff --git a/core/KaSa_rep/frontend/cckappa_sig.ml b/core/KaSa_rep/frontend/cckappa_sig.ml index 987b54c32..aafd1c3ce 100644 --- a/core/KaSa_rep/frontend/cckappa_sig.ml +++ b/core/KaSa_rep/frontend/cckappa_sig.ml @@ -24,6 +24,7 @@ type kappa_handler = { nrules: int; nvars: int; nagents: Ckappa_sig.c_agent_name; + nguard_params: int; agents_dic: Ckappa_sig.agent_dic; agents_annotation: (string * Loc.t list) diff --git a/core/KaSa_rep/frontend/cckappa_sig.mli b/core/KaSa_rep/frontend/cckappa_sig.mli index 3ac820210..7482efcf3 100644 --- a/core/KaSa_rep/frontend/cckappa_sig.mli +++ b/core/KaSa_rep/frontend/cckappa_sig.mli @@ -24,6 +24,7 @@ type kappa_handler = { nrules: int; nvars: int; nagents: Ckappa_sig.c_agent_name; + nguard_params: int; agents_dic: Ckappa_sig.agent_dic; agents_annotation: (string * Loc.t list) diff --git a/core/KaSa_rep/frontend/ckappa_sig.ml b/core/KaSa_rep/frontend/ckappa_sig.ml index 52c7934c3..f1fd51497 100644 --- a/core/KaSa_rep/frontend/ckappa_sig.ml +++ b/core/KaSa_rep/frontend/ckappa_sig.ml @@ -34,6 +34,9 @@ type binding_state = Free | Lnk_type of agent_name * site_name type c_guard_parameter = int type c_site_or_guard_p = Site of c_site_name | Guard_p of c_guard_parameter +type c_guard_p_then_site = + int (*the first n elements are guards, the last ones are sites*) + type mixture = | SKIP of mixture | COMMA of agent * mixture @@ -192,8 +195,30 @@ let state_index_of_int (a : int) : c_state = a let int_of_state_index (a : c_state) : int = a let string_of_state_index (a : c_state) : string = string_of_int a let guard_parameter_of_int (a : int) : c_guard_parameter = a +let guard_p_then_site_of_int (a : int) : c_guard_p_then_site = a +let int_of_guard_p_then_site (a : c_guard_p_then_site) : int = a + +let guard_p_then_site_of_site (a : c_site_name) (nr_guard_p : int) : + c_guard_p_then_site = + guard_parameter_of_int (int_of_site_name a + nr_guard_p) + +let guard_p_then_site_of_guard (a : c_guard_parameter) : c_guard_p_then_site = a + +let guard_p_then_site_of_site_or_guard_p (a : c_site_or_guard_p) + (nr_guard_p : int) : c_guard_p_then_site = + match a with + | Site s -> guard_p_then_site_of_site s nr_guard_p + | Guard_p s -> guard_p_then_site_of_guard s + let int_of_guard_parameter (a : c_guard_parameter) : int = a +let site_or_guard_p_of_guard_p_then_site (a : c_guard_p_then_site) + (nr_guard_p : int) : c_site_or_guard_p = + if a < nr_guard_p then + Guard_p a + else + Site (a - nr_guard_p) + let string_of_state_index_option_min parameters a = match a with | Some a -> string_of_state_index a @@ -843,6 +868,13 @@ module Site_map_and_set = Map_wrapper.Make (SetMap.Make (struct let print = Format.pp_print_int end)) +module GuardSite_map_and_set = Map_wrapper.Make (SetMap.Make (struct + type t = c_guard_p_then_site + + let compare = compare + let print = Format.pp_print_int +end)) + type c_interface = c_port Site_map_and_set.Map.t type c_proper_agent = { @@ -932,6 +964,7 @@ let next_rule_id = succ let next_agent_id = succ let next_agent_name = succ let next_site_name = succ +let next_guard_or_site_name = succ let next_state_index = succ let compare_rule_id = compare let compare_agent_id = compare @@ -1002,6 +1035,12 @@ module Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif : and type dimension = int * int = Int_storage.Nearly_Inf_Int_Int_storage_Imperatif_Imperatif +module Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif : + Int_storage.Storage + with type key = c_agent_name * c_guard_p_then_site + and type dimension = int * int = + Int_storage.Nearly_Inf_Int_Int_storage_Imperatif_Imperatif + module Agent_type_site_quick_nearly_Inf_Int_Int_storage_Imperatif_Imperatif : Int_storage.Storage with type key = c_agent_name * c_site_name @@ -1024,6 +1063,13 @@ module Site_type_quick_nearly_Inf_Int_storage_Imperatif : Int_storage.Storage with type key = c_site_name and type dimension = int = Int_storage.Quick_key_list (Site_type_nearly_Inf_Int_storage_Imperatif) +(*guard parameters or site: the first n indexes are the guards, and the remaining are the sites*) +module GuardPOrSite_nearly_Inf_Int_storage_Imperatif : + Int_storage.Storage + with type key = c_guard_p_then_site + and type dimension = int = + Int_storage.Nearly_inf_Imperatif + (*state*) module State_index_nearly_Inf_Int_storage_Imperatif : Int_storage.Storage with type key = c_state and type dimension = int = @@ -1252,7 +1298,7 @@ end)) module Views_bdu : Mvbdu_wrapper.Mvbdu - with type key = c_site_name + with type key = c_guard_p_then_site and type value = c_state with type mvbdu = Mvbdu_wrapper.Mvbdu.mvbdu = Mvbdu_wrapper.Mvbdu diff --git a/core/KaSa_rep/frontend/ckappa_sig.mli b/core/KaSa_rep/frontend/ckappa_sig.mli index 01b817565..cf438c539 100644 --- a/core/KaSa_rep/frontend/ckappa_sig.mli +++ b/core/KaSa_rep/frontend/ckappa_sig.mli @@ -34,6 +34,7 @@ type c_link_value type c_counter_name type c_guard_parameter type c_site_or_guard_p = Site of c_site_name | Guard_p of c_guard_parameter +type c_guard_p_then_site (****************************************************************************) @@ -55,8 +56,8 @@ val dummy_link_value : c_link_value val dummy_site_name_1 : c_site_name val dummy_site_name_minus1 : c_site_name val next_link_value : c_link_value -> c_link_value -val fst_site : c_site_name -val snd_site : c_site_name +val fst_site : c_guard_p_then_site (*rTODO maybe add nr_guard_params?*) +val snd_site : c_guard_p_then_site val dummy_state_index_1 : c_state val string_of_agent_name : c_agent_name -> string val int_of_agent_name : c_agent_name -> int @@ -70,8 +71,19 @@ val state_index_of_int : int -> c_state val int_of_state_index : c_state -> int val string_of_state_index : c_state -> string val guard_parameter_of_int : int -> c_guard_parameter +val guard_p_then_site_of_int : int -> c_guard_p_then_site +val int_of_guard_p_then_site : c_guard_p_then_site -> int +val guard_p_then_site_of_site : c_site_name -> int -> c_guard_p_then_site +val guard_p_then_site_of_guard : c_guard_parameter -> c_guard_p_then_site + +val guard_p_then_site_of_site_or_guard_p : + c_site_or_guard_p -> int -> c_guard_p_then_site + val int_of_guard_parameter : c_guard_parameter -> int +val site_or_guard_p_of_guard_p_then_site : + c_guard_p_then_site -> int -> c_site_or_guard_p + val string_of_state_index_option_min : Remanent_parameters_sig.parameters -> c_state option -> string @@ -91,6 +103,7 @@ val next_agent_id : c_agent_id -> c_agent_id val next_agent_name : c_agent_name -> c_agent_name val next_rule_id : c_rule_id -> c_rule_id val next_site_name : c_site_name -> c_site_name +val next_guard_or_site_name : c_guard_p_then_site -> c_guard_p_then_site val next_state_index : c_state -> c_state val pred_site_name : c_site_name -> c_site_name val pred_agent_name : c_agent_name -> c_agent_name @@ -375,6 +388,9 @@ module SiteOrGuard_map_and_set : module Site_map_and_set : Map_wrapper.S_with_logs with type elt = c_site_name +module GuardSite_map_and_set : + Map_wrapper.S_with_logs with type elt = c_guard_p_then_site + type c_interface = c_port Site_map_and_set.Map.t type c_proper_agent = { @@ -485,6 +501,11 @@ module Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif : with type key = c_agent_name * c_site_name and type dimension = int * int +module Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif : + Int_storage.Storage + with type key = c_agent_name * c_guard_p_then_site + and type dimension = int * int + module Agent_type_site_quick_nearly_Inf_Int_Int_storage_Imperatif_Imperatif : Int_storage.Storage with type key = c_agent_name * c_site_name @@ -501,6 +522,11 @@ module Site_type_nearly_Inf_Int_storage_Imperatif : module Site_type_quick_nearly_Inf_Int_storage_Imperatif : Int_storage.Storage with type key = c_site_name and type dimension = int +module GuardPOrSite_nearly_Inf_Int_storage_Imperatif : + Int_storage.Storage + with type key = c_guard_p_then_site + and type dimension = int + module State_index_nearly_Inf_Int_storage_Imperatif : Int_storage.Storage with type key = c_state and type dimension = int @@ -586,7 +612,9 @@ module AgentsSitePState_map_and_set : with type elt = c_agent_id * c_agent_name * c_site_name * pair_of_states module Views_bdu : - Mvbdu_wrapper.Mvbdu with type key = c_site_name and type value = c_state + Mvbdu_wrapper.Mvbdu + with type key = c_guard_p_then_site + and type value = c_state module Views_intbdu : Mvbdu_wrapper.Internalized_mvbdu diff --git a/core/KaSa_rep/frontend/handler.ml b/core/KaSa_rep/frontend/handler.ml index 32c7baacf..cf6344c00 100644 --- a/core/KaSa_rep/frontend/handler.ml +++ b/core/KaSa_rep/frontend/handler.ml @@ -16,6 +16,7 @@ let local_trace = false let nrules _parameter _error handler = handler.Cckappa_sig.nrules let nvars _parameter _error handler = handler.Cckappa_sig.nvars let nagents _parameter _error handler = handler.Cckappa_sig.nagents +let get_nr_guard_parameters handler = handler.Cckappa_sig.nguard_params let check_pos parameter ka_pos ml_pos message error error' = match ml_pos with @@ -620,6 +621,19 @@ let string_of_site_contact_map ?(ml_pos = None) ?(ka_pos = None) ?(message = "") in error, print_site_contact_map site_type +let string_of_site_or_guard_contact_map ?(ml_pos = None) ?(ka_pos = None) + ?(message = "") parameter error handler_kappa agent_name site_or_guard_int = + let nr_guard_params = get_nr_guard_parameters handler_kappa in + match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_or_guard_int + nr_guard_params + with + | Ckappa_sig.Site s -> + string_of_site_contact_map ~ml_pos ~ka_pos ~message parameter error + handler_kappa agent_name s + | Ckappa_sig.Guard_p g -> + string_of_guard g handler_kappa.Cckappa_sig.guard_parameters error + let print_labels parameters error handler couple = let _ = Quark_type.Labels.dump_couple parameters error handler couple in error diff --git a/core/KaSa_rep/frontend/handler.mli b/core/KaSa_rep/frontend/handler.mli index f68739b60..c1fb54149 100644 --- a/core/KaSa_rep/frontend/handler.mli +++ b/core/KaSa_rep/frontend/handler.mli @@ -249,6 +249,17 @@ val string_of_site_contact_map : Ckappa_sig.c_site_name -> Exception_without_parameter.exceptions_caught_and_uncaught * string +val string_of_site_or_guard_contact_map : + ?ml_pos:(string * int * int * int) option -> + ?ka_pos:Loc.t option -> + ?message:string -> + Remanent_parameters_sig.parameters -> + Exception_without_parameter.exceptions_caught_and_uncaught -> + Cckappa_sig.kappa_handler -> + Quark_type.agent_quark -> + Ckappa_sig.c_guard_p_then_site -> + Exception_without_parameter.exceptions_caught_and_uncaught * string + val string_of_site_in_natural_language : Remanent_parameters_sig.parameters -> Exception_without_parameter.exceptions_caught_and_uncaught -> diff --git a/core/KaSa_rep/frontend/list_tokens.ml b/core/KaSa_rep/frontend/list_tokens.ml index 435f9beb7..fe6bf32ea 100644 --- a/core/KaSa_rep/frontend/list_tokens.ml +++ b/core/KaSa_rep/frontend/list_tokens.ml @@ -53,6 +53,7 @@ let empty_handler parameters error = Cckappa_sig.nvars = 0; Cckappa_sig.nagents = Ckappa_sig.dummy_agent_name; Cckappa_sig.nrules = 0; + Cckappa_sig.nguard_params = 0; Cckappa_sig.agents_dic = Ckappa_sig.Dictionary_of_agents.init (); Cckappa_sig.agents_annotation = agent_annotation; Cckappa_sig.interface_constraints = int_constraints; @@ -506,8 +507,16 @@ let scan_compil parameters error compil = let remanent = scan_perts scan_tested_mixture parameters remanent compil.Ast.perturbations in - let remanent = + let error, remanent = scan_rules scan_tested_mixture parameters remanent compil.Ast.rules in + let remanent = + ( error, + { + remanent with + Cckappa_sig.nguard_params = + List.length remanent.Cckappa_sig.guard_parameters; + } ) + in let remanent = reverse_agents_annotation parameters remanent in remanent diff --git a/core/KaSa_rep/reachability_analysis/bdu_static_views.ml b/core/KaSa_rep/reachability_analysis/bdu_static_views.ml index 3cc4e46e8..ee1b5a0eb 100644 --- a/core/KaSa_rep/reachability_analysis/bdu_static_views.ml +++ b/core/KaSa_rep/reachability_analysis/bdu_static_views.ml @@ -23,7 +23,8 @@ type bdu_analysis_static_pattern = { (*pattern*) store_proj_bdu_test_restriction_pattern: (Covering_classes_type.cv_id - * Ckappa_sig.c_state Cckappa_sig.interval Ckappa_sig.Site_map_and_set.Map.t) + * Ckappa_sig.c_state Cckappa_sig.interval + Ckappa_sig.GuardSite_map_and_set.Map.t) list; } @@ -53,8 +54,10 @@ type bdu_analysis_static = { Ckappa_sig.Views_bdu.mvbdu Covering_classes_type.AgentsCV_setmap.Map.t Ckappa_sig.Rule_setmap.Map.t; site_to_renamed_site_list: - (Covering_classes_type.cv_id * Ckappa_sig.c_site_name) list - Ckappa_sig.Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif.t; + (Covering_classes_type.cv_id * Ckappa_sig.c_guard_p_then_site) list + Ckappa_sig + .Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif + .t; } (***************************************************************************) @@ -63,7 +66,8 @@ type bdu_analysis_static = { let init_bdu_analysis_static parameters error = let error, init_site_to_renamed_site_list = - Ckappa_sig.Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif + Ckappa_sig + .Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif .create parameters error (0, 0) in let init_bdu_analysis_static = @@ -120,17 +124,20 @@ let add_dependency_triple_bdu parameters handler error error, handler, store_result let add_dependency_site parameters map_new_index_forward site state - (error, store_result) = + nr_guard_params (error, store_result) = let error, site' = match Ckappa_sig.SiteOrGuard_map_and_set.Map.find_option parameters error site map_new_index_forward with | error, None -> - Exception.warn parameters error __POS__ Exit Ckappa_sig.dummy_site_name + Exception.warn parameters error __POS__ Exit + (Ckappa_sig.guard_p_then_site_of_site Ckappa_sig.dummy_site_name + nr_guard_params) | error, Some s -> error, s in - Ckappa_sig.Site_map_and_set.Map.add parameters error site' state store_result + Ckappa_sig.GuardSite_map_and_set.Map.add parameters error site' state + store_result let to_site_or_guard_map parameters error site_map = Ckappa_sig.Site_map_and_set.Map.fold @@ -141,7 +148,7 @@ let to_site_or_guard_map parameters error site_map = (error, Ckappa_sig.SiteOrGuard_map_and_set.Map.empty) let get_pair_cv_map_with_missing_association_creation parameters error agent - triple_list = + triple_list nr_guard_params = List.fold_left (fun (error, current_list) (cv_id, list, set) -> let error, (map_new_index_forward, _) = @@ -161,21 +168,22 @@ let get_pair_cv_map_with_missing_association_creation parameters error agent port.Cckappa_sig.site_state.Cckappa_sig.max ) with | Some a, Some b when a = b -> - add_dependency_site parameters map_new_index_forward site a m + add_dependency_site parameters map_new_index_forward site a + nr_guard_params m | Some _, Some _ | None, _ | _, None -> raise Exit) (fun site -> match site with | Ckappa_sig.Site _ -> add_dependency_site parameters map_new_index_forward site - Ckappa_sig.dummy_state_index + Ckappa_sig.dummy_state_index nr_guard_params | Ckappa_sig.Guard_p _ -> add_dependency_site parameters map_new_index_forward site - Ckappa_sig.dummy_state_index_true + Ckappa_sig.dummy_state_index_true nr_guard_params (*rTODO does that mean that all parameters are true?*)) - set agent_interface Ckappa_sig.Site_map_and_set.Map.empty + set agent_interface Ckappa_sig.GuardSite_map_and_set.Map.empty with Exit -> Exception.warn parameters error __POS__ Exit - Ckappa_sig.Site_map_and_set.Map.empty + Ckappa_sig.GuardSite_map_and_set.Map.empty in let error = Exception.check_point Exception.warn parameters error error' __POS__ @@ -185,7 +193,7 @@ let get_pair_cv_map_with_missing_association_creation parameters error agent (error, []) triple_list let collect_bdu_creation_restriction_map parameters handler error rule_id rule - store_remanent_triple store_result = + store_remanent_triple store_result nr_guard_params = (*-----------------------------------------------------------------*) Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.fold parameters error @@ -209,7 +217,7 @@ let collect_bdu_creation_restriction_map parameters handler error rule_id rule (*get map restriction from covering classes*) let error, get_pair_list = get_pair_cv_map_with_missing_association_creation parameters - error agent triple_list + error agent triple_list nr_guard_params in (*----------------------------------------------------------*) (*fold a list and get a pair of site and state and rule_id*) @@ -217,7 +225,7 @@ let collect_bdu_creation_restriction_map parameters handler error rule_id rule List.fold_left (fun (error, handler, store_result) (cv_id, map_res) -> let pair_list = - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' state current_list -> (site', state) :: current_list) map_res [] @@ -246,7 +254,7 @@ let collect_bdu_creation_restriction_map parameters handler error rule_id rule (*projection with rule_id*) let collect_proj_bdu_creation_restriction_map parameters handler_bdu error - rule_id rule store_remanent_triple store_result = + rule_id rule store_remanent_triple store_result nr_guard_params = let store_init_bdu_creation_restriction_map = Covering_classes_type.AgentRuleCV_setmap.Map.empty in @@ -254,7 +262,7 @@ let collect_proj_bdu_creation_restriction_map parameters handler_bdu error collect_bdu_creation_restriction_map (* collect should work directly on the partitioned map (store_result) *) parameters handler_bdu error rule_id rule store_remanent_triple - store_init_bdu_creation_restriction_map + store_init_bdu_creation_restriction_map nr_guard_params in let error, handler_bdu, bdu_true = Ckappa_sig.Views_bdu.mvbdu_true parameters handler_bdu error @@ -282,7 +290,7 @@ let collect_proj_bdu_creation_restriction_map parameters handler_bdu error (*modification rule with creation rules*) let get_pair_cv_map_with_restriction_modification parameters error agent - triple_list = + triple_list nr_guard_params = List.fold_left (fun (error, current_list) (cv_id, list, set) -> (*-----------------------------------------------------------*) @@ -306,22 +314,24 @@ let get_pair_cv_map_with_restriction_modification parameters error agent in let error, site' = Ckappa_sig.SiteOrGuard_map_and_set.Map.find_default_without_logs - parameters error Ckappa_sig.dummy_site_name site - map_new_index_forward + parameters error + (Ckappa_sig.guard_p_then_site_of_site Ckappa_sig.dummy_site_name + nr_guard_params) + site map_new_index_forward in let error, map_res = - Ckappa_sig.Site_map_and_set.Map.add parameters error site' state - store_result + Ckappa_sig.GuardSite_map_and_set.Map.add parameters error site' + state store_result in error, map_res) - set agent_interface Ckappa_sig.Site_map_and_set.Map.empty + set agent_interface Ckappa_sig.GuardSite_map_and_set.Map.empty in error, (cv_id, map_res) :: current_list) (error, []) triple_list let collect_modif_list_restriction_map parameters handler error rule_id rule (*store_new_index_pair_map*) - store_remanent_triple store_result = + store_remanent_triple store_result nr_guard_params = let add_link error (agent_id, agent_type, rule_id, cv_id) list_a store_result = (*the association must be unique *) @@ -357,20 +367,20 @@ let collect_modif_list_restriction_map parameters handler error rule_id rule (*get map restriction from covering classes*) let error, get_pair_list = get_pair_cv_map_with_restriction_modification parameters error - agent_modif triple_list + agent_modif triple_list nr_guard_params in (*-----------------------------------------------------------------*) (*fold a list and get a pair of site and state and rule_id*) let error, handler, store_result = List.fold_left (fun (error, handler, store_result) (cv_id, map_res) -> - if Ckappa_sig.Site_map_and_set.Map.is_empty map_res then + if Ckappa_sig.GuardSite_map_and_set.Map.is_empty map_res then error, handler, store_result else ( (*get a list of pair (site, state) in a map of new indexes of site.*) let error, pair_list = - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' state (error, current_list) -> match state with | Some state -> @@ -404,7 +414,7 @@ let collect_modif_list_restriction_map parameters handler error rule_id rule (**************************************************************************) (*build bdu for potential side effects*) -let get_triple_map parameters error pair_list triple_list = +let get_triple_map parameters error pair_list triple_list nr_guard_params = List.fold_left (fun (error, current_list) (cv_id, list, set) -> (*-------------------------------------------------------*) @@ -422,21 +432,23 @@ let get_triple_map parameters error pair_list triple_list = then ( let error, site' = Ckappa_sig.SiteOrGuard_map_and_set.Map.find_default_without_logs - parameters error Ckappa_sig.dummy_site_name + parameters error + (Ckappa_sig.guard_p_then_site_of_site + Ckappa_sig.dummy_site_name nr_guard_params) (Ckappa_sig.Site site) map_new_index_forward in let error, old = - Ckappa_sig.Site_map_and_set.Map.find_default_without_logs + Ckappa_sig.GuardSite_map_and_set.Map.find_default_without_logs parameters error [] site' map_res in let error, map_res = - Ckappa_sig.Site_map_and_set.Map.add_or_overwrite parameters + Ckappa_sig.GuardSite_map_and_set.Map.add_or_overwrite parameters error site' (state :: old) map_res in error, map_res ) else error, map_res) - (error, Ckappa_sig.Site_map_and_set.Map.empty) + (error, Ckappa_sig.GuardSite_map_and_set.Map.empty) pair_list in (*------------------------------------------------------*) @@ -445,14 +457,14 @@ let get_triple_map parameters error pair_list triple_list = Exit in ( error, - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' list_state list -> (cv_id, site', list_state) :: list) map_res current_list )) (error, []) triple_list -let store_bdu_potential_restriction_map_aux parameters handler error - (*store_new_index_pair_map*) - store_remanent_triple store_potential_side_effects store_result = +let store_bdu_potential_restriction_map_aux parameters handler nr_guard_params + error (*store_new_index_pair_map*) store_remanent_triple + store_potential_side_effects store_result = let error, handler, bdu_false = Ckappa_sig.Views_bdu.mvbdu_false parameters handler error in @@ -484,6 +496,7 @@ let store_bdu_potential_restriction_map_aux parameters handler error if agent_type' = agent_type then ( let error, get_triple_list = get_triple_map parameters error pair_list triple_list + nr_guard_params in (*---------------------------------------------------------*) let error, handler, store_result = @@ -528,12 +541,12 @@ let store_bdu_potential_restriction_map_aux parameters handler error (*************************************************************************) (*build bdu_potential in the case of binding*) -let store_bdu_potential_effect_restriction_map parameters handler error - (*store_new_index_pair_map*) - store_remanent_triple store_potential_side_effects store_result = +let store_bdu_potential_effect_restriction_map parameters handler + nr_guard_params error (*store_new_index_pair_map*) store_remanent_triple + store_potential_side_effects store_result = let error', (handler, store_result) = - store_bdu_potential_restriction_map_aux parameters handler error - (*store_new_index_pair_map*) + store_bdu_potential_restriction_map_aux parameters handler nr_guard_params + error (*store_new_index_pair_map*) store_remanent_triple store_potential_side_effects store_result in let error = @@ -542,7 +555,7 @@ let store_bdu_potential_effect_restriction_map parameters handler error error, (handler, store_result) let collect_site_to_renamed_site_list parameters error store_remanent_triple - output = + nr_guard_params output = Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.fold parameters error (fun parameters error agent_type' triple_list output -> @@ -551,15 +564,16 @@ let collect_site_to_renamed_site_list parameters error store_remanent_triple let rec aux error site list output = match list with | [] -> error, output - | Ckappa_sig.Guard_p _ :: t -> - (*rTODO what is this for?*) - aux error site t output - | Ckappa_sig.Site h :: t -> + | h :: t -> + let h = + Ckappa_sig.guard_p_then_site_of_site_or_guard_p h + nr_guard_params + in let key = agent_type', h in let error, old = match Ckappa_sig - .Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif + .Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif .unsafe_get parameters error key output with | error, None -> error, [] @@ -568,29 +582,32 @@ let collect_site_to_renamed_site_list parameters error store_remanent_triple let new_list = (cv_id, site) :: old in let error, output = Ckappa_sig - .Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif + .Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif .set parameters error key new_list output in - let site' = Ckappa_sig.next_site_name site in + let site' = Ckappa_sig.next_guard_or_site_name site in aux error site' t output in - aux error Ckappa_sig.dummy_site_name_1 list output) + aux error + (Ckappa_sig.guard_p_then_site_of_site Ckappa_sig.dummy_site_name_1 + nr_guard_params) + list output) (error, output) triple_list) store_remanent_triple output (**************************************************************************) (*projection with rule_id*) -let collect_proj_bdu_potential_restriction_map parameters handler error - (*store_new_index_pair_map*) - store_remanent_triple store_potential_side_effects store_result = +let collect_proj_bdu_potential_restriction_map parameters handler + nr_guard_params error (*store_new_index_pair_map*) store_remanent_triple + store_potential_side_effects store_result = let store_init_bdu_potential_restriction_map = Covering_classes_type.AgentSiteRuleCV_setmap.Map.empty in let error, (handler, store_bdu_potential_restriction_map) = (* this function should work directly on the partitioned map (store_result) *) - store_bdu_potential_effect_restriction_map parameters handler error - (*store_new_index_pair_map*) + store_bdu_potential_effect_restriction_map parameters handler + nr_guard_params error (*store_new_index_pair_map*) store_remanent_triple store_potential_side_effects store_init_bdu_potential_restriction_map in @@ -620,7 +637,8 @@ let collect_proj_bdu_potential_restriction_map parameters handler error (**************************************************************************) -let get_pair_cv_map_with_restriction_views parameters error agent triple_list = +let get_pair_cv_map_with_restriction_views parameters error agent triple_list + nr_guard_params = List.fold_left (fun (error, current_list) (cv_id, list, set) -> (*----------------------------------------------------------*) @@ -638,14 +656,17 @@ let get_pair_cv_map_with_restriction_views parameters error agent triple_list = let state = port.Cckappa_sig.site_state in let error, site' = Ckappa_sig.SiteOrGuard_map_and_set.Map.find_default parameters - error Ckappa_sig.dummy_site_name site map_new_index_forward + error + (Ckappa_sig.guard_p_then_site_of_site Ckappa_sig.dummy_site_name + nr_guard_params) + site map_new_index_forward in let error, map_res = - Ckappa_sig.Site_map_and_set.Map.add parameters error site' state - store_result + Ckappa_sig.GuardSite_map_and_set.Map.add parameters error site' + state store_result in error, map_res) - set agent_interface Ckappa_sig.Site_map_and_set.Map.empty + set agent_interface Ckappa_sig.GuardSite_map_and_set.Map.empty in let error = Exception.check_point Exception.warn parameters error error' __POS__ @@ -654,12 +675,15 @@ let get_pair_cv_map_with_restriction_views parameters error agent triple_list = error, (cv_id, map_res) :: current_list) (error, []) triple_list -let collect_bdu_test_restriction_map parameters _handler_kappa handler error +let collect_bdu_test_restriction_map parameters handler_kappa handler error rule_id rule (*store_new_index_pair_map*) store_remanent_triple store_result = let error, handler, bdu_false = Ckappa_sig.Views_bdu.mvbdu_false parameters handler error in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters handler_kappa + in (*let (map_new_index_forward, _) = store_new_index_pair_map in*) (*-----------------------------------------------------------------*) Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.fold parameters @@ -706,17 +730,17 @@ let collect_bdu_test_restriction_map parameters _handler_kappa handler error (*get map restriction from covering classes*) let error, get_pair_list = get_pair_cv_map_with_restriction_views parameters error agent - triple_list + triple_list nr_guard_params in (*-----------------------------------------------------------------*) let error, handler, store_result = List.fold_left (fun (error, handler, store_result) (cv_id, map_res) -> - if Ckappa_sig.Site_map_and_set.Map.is_empty map_res then + if Ckappa_sig.GuardSite_map_and_set.Map.is_empty map_res then error, handler, store_result else ( let error, pair_list = - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' state (error, current_list) -> let pair_list = (site', (state.Cckappa_sig.min, state.Cckappa_sig.max)) @@ -787,7 +811,7 @@ let collect_proj_bdu_test_restriction parameters handler_kappa handler error let collect_proj_bdu_test_restriction_pattern parameters error (pattern : Cckappa_sig.mixture) (*store_new_index_pair_map*) - store_remanent_triple store_result = + store_remanent_triple store_result nr_guard_params = (*let (map_new_index_forward, _) = store_new_index_pair_map in*) let error, store_result = Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.fold parameters @@ -813,7 +837,7 @@ let collect_proj_bdu_test_restriction_pattern parameters error in let error, get_pair_list = get_pair_cv_map_with_restriction_views parameters error agent - triple_list + triple_list nr_guard_params in error, get_pair_list) pattern.Cckappa_sig.views store_result @@ -833,22 +857,27 @@ let scan_rule_static parameters log_info error handler_kappa handler_bdu (StoryProfiling.Scan_rule_static (Ckappa_sig.int_of_rule_id rule_id)) None log_info in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters handler_kappa + in (*------------------------------------------------------------------------*) let (error, handler_bdu), store_proj_bdu_creation_restriction_map = collect_proj_bdu_creation_restriction_map parameters handler_bdu error rule_id rule (*store_new_index_pair_map*) store_remanent_triple store_result.store_proj_bdu_creation_restriction_map + nr_guard_params in (*-----------------------------------------------------------------------*) let error, (handler_bdu, store_modif_list_restriction_map) = collect_modif_list_restriction_map parameters handler_bdu error rule_id rule (*store_new_index_pair_map*) store_remanent_triple store_result.store_modif_list_restriction_map + nr_guard_params in (*-----------------------------------------------------------------------*) let (error, handler_bdu), store_proj_bdu_potential_restriction_map = - collect_proj_bdu_potential_restriction_map parameters handler_bdu error - (*store_new_index_pair_map*) + collect_proj_bdu_potential_restriction_map parameters handler_bdu + nr_guard_params error (*store_new_index_pair_map*) store_remanent_triple store_potential_side_effects store_result.store_proj_bdu_potential_restriction_map in @@ -880,6 +909,9 @@ let scan_rule_static parameters log_info error handler_kappa handler_bdu let scan_rule_set parameters log_info handler_bdu error handler_kappa compiled store_potential_side_effects store_remanent_triple = let error, init = init_bdu_analysis_static parameters error in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters handler_kappa + in let error, (handler_bdu, log_info, store_results) = Ckappa_sig.Rule_nearly_Inf_Int_storage_Imperatif.fold parameters error (fun parameters error rule_id rule (handler_bdu, log_info, store_result) -> @@ -894,7 +926,7 @@ let scan_rule_set parameters log_info handler_bdu error handler_kappa compiled in let error, site_to_renamed_site_list = collect_site_to_renamed_site_list parameters error store_remanent_triple - store_results.site_to_renamed_site_list + nr_guard_params store_results.site_to_renamed_site_list in ( error, (handler_bdu, log_info, { store_results with site_to_renamed_site_list }) ) @@ -905,18 +937,19 @@ let scan_rule_set parameters log_info handler_bdu error handler_kappa compiled let scan_rule_static_pattern parameters (*store_new_index_pair_map*) - store_remanent_triple error rule store_result = + store_remanent_triple error rule store_result nr_guard_params = let error, store_proj_bdu_test_restriction_pattern = collect_proj_bdu_test_restriction_pattern parameters error rule.Cckappa_sig.rule_lhs (*pattern*) (*store_new_index_pair_map*) store_remanent_triple store_result.store_proj_bdu_test_restriction_pattern + nr_guard_params in error, { store_proj_bdu_test_restriction_pattern } let scan_rule_set_pattern parameters error (*store_new_index_pair_map*) - store_remanent_triple compiled = + store_remanent_triple compiled nr_guard_params = let init = init_bdu_analysis_static_pattern in let error, store_results = Ckappa_sig.Rule_nearly_Inf_Int_storage_Imperatif.fold parameters error @@ -925,7 +958,7 @@ let scan_rule_set_pattern parameters error scan_rule_static_pattern parameters (*store_new_index_pair_map*) store_remanent_triple error rule.Cckappa_sig.e_rule_c_rule - store_result + store_result nr_guard_params in error, store_result) compiled.Cckappa_sig.rules init diff --git a/core/KaSa_rep/reachability_analysis/common_map.ml b/core/KaSa_rep/reachability_analysis/common_map.ml index af1d9832b..464fa99d3 100644 --- a/core/KaSa_rep/reachability_analysis/common_map.ml +++ b/core/KaSa_rep/reachability_analysis/common_map.ml @@ -217,17 +217,18 @@ let new_index_pair_map parameters error l = Ckappa_sig.SiteOrGuard_map_and_set.Map.add parameters error h k map1 in let error, map2 = - Ckappa_sig.Site_map_and_set.Map.add parameters error k h map2 + Ckappa_sig.GuardSite_map_and_set.Map.add parameters error k h map2 in aux tl - (Ckappa_sig.site_name_of_int (Ckappa_sig.int_of_site_name k + 1)) + (Ckappa_sig.guard_p_then_site_of_int + (Ckappa_sig.int_of_guard_p_then_site k + 1)) map1 map2 error in let error', (map1, map2) = aux l - (Ckappa_sig.site_name_of_int 1) + (Ckappa_sig.guard_p_then_site_of_int 1) Ckappa_sig.SiteOrGuard_map_and_set.Map.empty - Ckappa_sig.Site_map_and_set.Map.empty error + Ckappa_sig.GuardSite_map_and_set.Map.empty error in let error = Exception.check_point Exception.warn parameters error error' __POS__ Exit diff --git a/core/KaSa_rep/reachability_analysis/covering_classes_main.ml b/core/KaSa_rep/reachability_analysis/covering_classes_main.ml index 6b4959dce..b694cfd24 100644 --- a/core/KaSa_rep/reachability_analysis/covering_classes_main.ml +++ b/core/KaSa_rep/reachability_analysis/covering_classes_main.ml @@ -15,6 +15,8 @@ let trace = false (*******************************************************************************) +let get_nr_guard_parameters kappa_handler = + kappa_handler.Cckappa_sig.nguard_params let compare_unit_covering_class_id _ _ = Covering_classes_type.dummy_cv_id @@ -474,7 +476,7 @@ let scan_rule_set_remanent parameters error handler rules = (*clean the covering classes, removed duplicate of covering classes*) let error, store_remanent_dic = clean_classes parameters error covering_class modified_map - (List.length handler.guard_parameters) + (get_nr_guard_parameters handler) in (*---------------------------------------------------------------*) (*compute the number of covering classes*) @@ -714,7 +716,10 @@ let scan_predicate_covering_classes parameters error handler_kappa compil = let error, last_site = Handler.last_site_of_agent parameters error handler_kappa ag in - let size_map1 = 1 + Ckappa_sig.int_of_site_name last_site in + let nr_guard_parameters = get_nr_guard_parameters handler_kappa in + let size_map1 = + 1 + Ckappa_sig.int_of_site_name last_site + nr_guard_parameters + in let size_map2 = 1 + List.length list in let error, array = List.fold_left @@ -722,32 +727,34 @@ let scan_predicate_covering_classes parameters error handler_kappa compil = let rec aux acc k map1 map2 error = match acc with | [] -> error, (map1, map2) - | Ckappa_sig.Guard_p _ :: tl -> - aux tl k map1 map2 error (*rTODO??*) - | Ckappa_sig.Site h :: tl -> + | h :: tl -> + let h_int = + Ckappa_sig.guard_p_then_site_of_site_or_guard_p h + nr_guard_parameters + in let error, map1 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.set - parameters error h k map1 + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.set + parameters error h_int k map1 in let error, map2 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.set + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.set parameters error k h map2 in aux tl - (Ckappa_sig.site_name_of_int - (Ckappa_sig.int_of_site_name k + 1)) + (Ckappa_sig.guard_p_then_site_of_int + (Ckappa_sig.int_of_guard_p_then_site k + 1)) map1 map2 error in let error, map1 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.create + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.create parameters error size_map1 in let error, map2 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.create + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.create parameters error size_map2 in let error, (map1, map2) = - aux list (Ckappa_sig.site_name_of_int 1) map1 map2 error + aux list (Ckappa_sig.guard_p_then_site_of_int 1) map1 map2 error in Covering_classes_type.Cv_id_nearly_Inf_Int_storage_Imperatif.set parameters error cv_id (map1, map2) array) diff --git a/core/KaSa_rep/reachability_analysis/covering_classes_type.ml b/core/KaSa_rep/reachability_analysis/covering_classes_type.ml index a10a81cfd..d0ba12853 100644 --- a/core/KaSa_rep/reachability_analysis/covering_classes_type.ml +++ b/core/KaSa_rep/reachability_analysis/covering_classes_type.ml @@ -113,7 +113,7 @@ module AgentsCV_setmap = SetMap.Make (struct end) module AgentSiteCV_setmap = SetMap.Make (struct - type t = Ckappa_sig.c_agent_name * Ckappa_sig.c_site_name * cv_id + type t = Ckappa_sig.c_agent_name * Ckappa_sig.c_guard_p_then_site * cv_id let compare = compare let print _ _ = () @@ -140,7 +140,7 @@ end) module AgentSiteRuleCV_setmap = SetMap.Make (struct type t = Ckappa_sig.c_agent_name - * Ckappa_sig.c_site_name + * Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_rule_id * cv_id @@ -180,10 +180,10 @@ type predicate_covering_classes = { list Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.t; site_correspondence: - (Ckappa_sig.c_site_name - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.t - * Ckappa_sig.c_site_name - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.t) + (Ckappa_sig.c_guard_p_then_site + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.t + * Ckappa_sig.c_site_or_guard_p + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.t) Cv_id_nearly_Inf_Int_storage_Imperatif.t Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.t; } diff --git a/core/KaSa_rep/reachability_analysis/covering_classes_type.mli b/core/KaSa_rep/reachability_analysis/covering_classes_type.mli index ce03383de..b9a51832a 100644 --- a/core/KaSa_rep/reachability_analysis/covering_classes_type.mli +++ b/core/KaSa_rep/reachability_analysis/covering_classes_type.mli @@ -74,7 +74,8 @@ module AgentsCV_setmap : module AgentSiteCV_setmap : SetMap.S - with type elt = Ckappa_sig.c_agent_name * Ckappa_sig.c_site_name * cv_id + with type elt = + Ckappa_sig.c_agent_name * Ckappa_sig.c_guard_p_then_site * cv_id module AgentRuleCV_setmap : SetMap.S @@ -92,7 +93,7 @@ module AgentSiteRuleCV_setmap : SetMap.S with type elt = Ckappa_sig.c_agent_name - * Ckappa_sig.c_site_name + * Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_rule_id * cv_id @@ -109,13 +110,14 @@ module Project2bdu_potential : SetMap.Projection2 with type elt_a = Ckappa_sig.c_agent_name - * Ckappa_sig.c_site_name + * Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_rule_id * cv_id and type elt_b = Ckappa_sig.c_rule_id and type 'a map_a = 'a AgentSiteRuleCV_setmap.Map.t and type 'a map_b = 'a Ckappa_sig.Rule_setmap.Map.t - and type elt_c = Ckappa_sig.c_agent_name * Ckappa_sig.c_site_name * cv_id + and type elt_c = + Ckappa_sig.c_agent_name * Ckappa_sig.c_guard_p_then_site * cv_id and type 'a map_c = 'a AgentSiteCV_setmap.Map.t module Project2_bdu_views : @@ -155,10 +157,10 @@ type predicate_covering_classes = { list Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.t; site_correspondence: - (Ckappa_sig.c_site_name - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.t - * Ckappa_sig.c_site_name - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.t) + (Ckappa_sig.c_guard_p_then_site + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.t + * Ckappa_sig.c_site_or_guard_p + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.t) Cv_id_nearly_Inf_Int_storage_Imperatif.t Ckappa_sig.Agent_type_quick_nearly_Inf_Int_storage_Imperatif.t; } diff --git a/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml b/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml index 591573908..f247b935c 100644 --- a/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml +++ b/core/KaSa_rep/reachability_analysis/translation_in_natural_language.ml @@ -15,24 +15,28 @@ let trace = false let _ = trace +let get_nr_guard_parameters kappa_handler = + kappa_handler.Cckappa_sig.nguard_params + type token = - | Range of Ckappa_sig.c_site_name * Ckappa_sig.c_state list + (*rTODO maybe change this*) + | Range of Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state list | Equiv of - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) - * (Ckappa_sig.c_site_name * Ckappa_sig.c_state) + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) + * (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) | Imply of - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) - * (Ckappa_sig.c_site_name * Ckappa_sig.c_state) + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) + * (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) | Partition of - (Ckappa_sig.c_site_name * (Ckappa_sig.c_state * token list) list) + (Ckappa_sig.c_guard_p_then_site * (Ckappa_sig.c_state * token list) list) | No_known_translation of - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) list list + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) list list type rename_sites = Remanent_parameters_sig.parameters -> Exception.exceptions_caught_and_uncaught -> - Ckappa_sig.Site_map_and_set.Map.elt -> - Exception.exceptions_caught_and_uncaught * Ckappa_sig.Site_map_and_set.Map.elt + Ckappa_sig.c_guard_p_then_site -> + Exception.exceptions_caught_and_uncaught * Ckappa_sig.c_guard_p_then_site (****************************************************************************) @@ -439,54 +443,85 @@ let rec print ?beginning_of_sentence:(beggining = true) "" in let log = Remanent_parameters.get_logger parameters in + let nr_guard_params = get_nr_guard_parameters handler_kappa in let error, () = match translation with | Range (site_type, state_list) -> - if dim_min <= 1 then ( - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - let error, t = - Site_graphs.KaSa_site_graph.add_site parameters error handler_kappa - agent_id site_type t - in - let error = - Site_graphs.KaSa_site_graph.print log parameters error t - in - let () = Loggers.fprintf log " => " in - let should_use_bracket = - match state_list with - | [] | [ _ ] -> false - | _ :: _ -> true - in - let () = if should_use_bracket then Loggers.fprintf log "[ " in - let error, _bool = - List.fold_left - (fun (error, bool) state -> - let () = if bool then Loggers.fprintf log " v " in - let error, t = - Site_graphs.KaSa_site_graph.add_state parameters error - handler_kappa agent_id site_type state t + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_type + nr_guard_params + with + | Guard_p _ -> error, () (*rTODO print guards*) + | Site site_type -> + if dim_min <= 1 then ( + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> + let error, t = + Site_graphs.KaSa_site_graph.add_site parameters error + handler_kappa agent_id site_type t + in + let error = + Site_graphs.KaSa_site_graph.print log parameters error t + in + let () = Loggers.fprintf log " => " in + let should_use_bracket = + match state_list with + | [] | [ _ ] -> false + | _ :: _ -> true + in + let () = if should_use_bracket then Loggers.fprintf log "[ " in + let error, _bool = + List.fold_left + (fun (error, bool) state -> + let () = if bool then Loggers.fprintf log " v " in + let error, t = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site_type state t + in + let error = + Site_graphs.KaSa_site_graph.print log parameters error t + in + error, true) + (error, false) state_list + in + let () = if should_use_bracket then Loggers.fprintf log " ]" in + let () = Loggers.print_newline log in + error, () + | Remanent_parameters_sig.Natural_language -> + let error', site_string = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type site_type + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let rec aux list error = + match list with + | [] -> Exception.warn parameters error __POS__ Exit () + | [ state ] -> + let error', state_string = + Handler.string_of_state_fully_deciphered parameters error + handler_kappa agent_type site_type state in let error = - Site_graphs.KaSa_site_graph.print log parameters error t + Exception.check_point Exception.warn parameters error error' + __POS__ Exit in - error, true) - (error, false) state_list - in - let () = if should_use_bracket then Loggers.fprintf log " ]" in - let () = Loggers.print_newline log in - error, () - | Remanent_parameters_sig.Natural_language -> - let error', site_string = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type site_type - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let rec aux list error = - match list with + error, Loggers.fprintf log " and %s.%s" state_string endofline + | state :: tail -> + let error', state_string = + Handler.string_of_state_fully_deciphered parameters error + handler_kappa agent_type site_type state + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let () = Loggers.fprintf log " %s," state_string in + aux tail error + in + (match state_list with | [] -> Exception.warn parameters error __POS__ Exit () | [ state ] -> let error', state_string = @@ -497,39 +532,101 @@ let rec print ?beginning_of_sentence:(beggining = true) Exception.check_point Exception.warn parameters error error' __POS__ Exit in - error, Loggers.fprintf log " and %s.%s" state_string endofline - | state :: tail -> - let error', state_string = + ( error, + Loggers.fprintf log "%s%s %sis always %s.%s" + (Remanent_parameters.get_prefix parameters) + (cap site_string) (in_agent agent_string) state_string + endofline ) + | [ state1; state2 ] -> + let error', state_string1 = Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site_type state + handler_kappa agent_type site_type state1 in let error = Exception.check_point Exception.warn parameters error error' __POS__ Exit in - let () = Loggers.fprintf log " %s," state_string in - aux tail error - in - (match state_list with - | [] -> Exception.warn parameters error __POS__ Exit () - | [ state ] -> - let error', state_string = - Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site_type state + let error', state_string2 = + Handler.string_of_state_fully_deciphered parameters error + handler_kappa agent_type site_type state2 + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + ( error, + Loggers.fprintf log "%s%s %sranges over %s and %s.%s" + (Remanent_parameters.get_prefix parameters) + (cap site_string) (in_agent agent_string) state_string1 + state_string2 endofline ) + | list -> + let () = + Loggers.fprintf log "%s%s %sranges over" + (Remanent_parameters.get_prefix parameters) + (cap site_string) (in_agent agent_string) + in + aux list error) + ) else + error, ()) + | Equiv ((site1, state1), (site2, state2)) -> + (match + ( Ckappa_sig.site_or_guard_p_of_guard_p_then_site site1 nr_guard_params, + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site2 nr_guard_params + ) + with + | Guard_p _, _ -> error, () (*rTODO print guards*) + | _, Guard_p _ -> error, () + | Site site1, Site site2 -> + if dim_min <= 2 then ( + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> + let error, t' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site1 state1 t + in + let error, t'' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site2 state2 t + in + let error = + Site_graphs.KaSa_site_graph.print + (Remanent_parameters.get_logger parameters) + parameters error t' + in + let () = + Loggers.fprintf + (Remanent_parameters.get_logger parameters) + " <=> " + in + let error = + Site_graphs.KaSa_site_graph.print + (Remanent_parameters.get_logger parameters) + parameters error t'' + in + let () = + Loggers.print_newline (Remanent_parameters.get_logger parameters) + in + error, () + | Remanent_parameters_sig.Natural_language -> + let error', site_string1 = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type site1 in let error = Exception.check_point Exception.warn parameters error error' __POS__ Exit in - ( error, - Loggers.fprintf log "%s%s %sis always %s.%s" - (Remanent_parameters.get_prefix parameters) - (cap site_string) (in_agent agent_string) state_string endofline - ) - | [ state1; state2 ] -> let error', state_string1 = Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site_type state1 + handler_kappa agent_type site1 state1 + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let error', site_string2 = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type site2 in let error = Exception.check_point Exception.warn parameters error error' @@ -537,224 +634,164 @@ let rec print ?beginning_of_sentence:(beggining = true) in let error', state_string2 = Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site_type state2 + handler_kappa agent_type site2 state2 in let error = Exception.check_point Exception.warn parameters error error' __POS__ Exit in ( error, - Loggers.fprintf log "%s%s %sranges over %s and %s.%s" - (Remanent_parameters.get_prefix parameters) - (cap site_string) (in_agent agent_string) state_string1 - state_string2 endofline ) - | list -> - let () = - Loggers.fprintf log "%s%s %sranges over" + Loggers.fprintf + (Remanent_parameters.get_logger parameters) + "%s%s%s is %s, if and only if, %s is %s.%s" (Remanent_parameters.get_prefix parameters) - (cap site_string) (in_agent agent_string) - in - aux list error) - ) else - error, () - | Equiv ((site1, state1), (site2, state2)) -> - if dim_min <= 2 then ( - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - let error, t' = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site1 state1 t - in - let error, t'' = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site2 state2 t - in - let error = - Site_graphs.KaSa_site_graph.print - (Remanent_parameters.get_logger parameters) - parameters error t' - in - let () = - Loggers.fprintf (Remanent_parameters.get_logger parameters) " <=> " - in - let error = - Site_graphs.KaSa_site_graph.print - (Remanent_parameters.get_logger parameters) - parameters error t'' - in - let () = - Loggers.print_newline (Remanent_parameters.get_logger parameters) - in - error, () - | Remanent_parameters_sig.Natural_language -> - let error', site_string1 = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type site1 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let error', state_string1 = - Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site1 state1 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let error', site_string2 = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type site2 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let error', state_string2 = - Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site2 state2 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - ( error, - Loggers.fprintf - (Remanent_parameters.get_logger parameters) - "%s%s%s is %s, if and only if, %s is %s.%s" - (Remanent_parameters.get_prefix parameters) - (cap (in_agent_comma agent_string)) - site_string1 state_string1 site_string2 state_string2 endofline ) - ) else - error, () + (cap (in_agent_comma agent_string)) + site_string1 state_string1 site_string2 state_string2 endofline + ) + ) else + error, ()) | Imply ((site1, state1), (site2, state2)) -> - if dim_min <= 2 then ( - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - let error, t = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site1 state1 t - in - let error, t' = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site2 state2 t - in - let error = - Site_graphs.KaSa_site_graph.print - (Remanent_parameters.get_logger parameters) - parameters error t - in - let () = - Loggers.fprintf (Remanent_parameters.get_logger parameters) " => " - in - let error = - Site_graphs.KaSa_site_graph.print - (Remanent_parameters.get_logger parameters) - parameters error t' - in - let () = - Loggers.print_newline (Remanent_parameters.get_logger parameters) - in - error, () - | Remanent_parameters_sig.Natural_language -> - let error', site_string1 = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type site1 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let error', state_string1 = - Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site1 state1 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let error', site_string2 = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type site2 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - let error', state_string2 = - Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type site2 state2 - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - ( error, - Loggers.fprintf - (Remanent_parameters.get_logger parameters) - "%s%s%s is %s whenever %s is %s.%s" - (Remanent_parameters.get_prefix parameters) - (cap (in_agent_comma agent_string)) - site_string2 state_string2 site_string1 state_string1 endofline ) - ) else - error, () - | Partition (v, list) -> - (*let () = - Loggers.fprintf log - "%s%s%s" (Remanent_parameters.get_prefix parameters) - (cap (in_agent_colon agent_string)) endofline - in*) - let error, site_string = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type v - in - let parameters = Remanent_parameters.update_prefix parameters tab in - let error = - List.fold_left - (fun error (a, list) -> - let error, parameters = - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Natural_language -> - let error, state_string = - Handler.string_of_state_fully_deciphered parameters error - handler_kappa agent_type v a - in - let () = - Loggers.fprintf log "%swhen %s is equal to %s, then:%s%s" - (Remanent_parameters.get_prefix parameters) - site_string state_string endofline beginenumeration - in - let parameters = - Remanent_parameters.update_prefix parameters - (tab ^ beginenum ^ " ") - in - error, parameters - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - error, parameters + (match + ( Ckappa_sig.site_or_guard_p_of_guard_p_then_site site1 nr_guard_params, + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site2 nr_guard_params + ) + with + | Guard_p _, _ -> error, () (*rTODO print guards*) + | _, Guard_p _ -> error, () + | Site site1, Site site2 -> + if dim_min <= 2 then ( + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> + let error, t = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site1 state1 t in let error, t' = Site_graphs.KaSa_site_graph.add_state parameters error - handler_kappa agent_id v a t + handler_kappa agent_id site2 state2 t in let error = - List.fold_left - (fun error token -> - let error = - print ~beginning_of_sentence:false ~prompt_agent_type:false - ~html_mode ~show_dep_with_dimmension_higher_than:0 - parameters handler_kappa error agent_string agent_type - agent_id token t' - in - let () = Loggers.fprintf log "%s" endenum in - error) - error list + Site_graphs.KaSa_site_graph.print + (Remanent_parameters.get_logger parameters) + parameters error t in - let () = Loggers.fprintf log "%s" endenumeration in - error) - error list - in - error, () + let () = + Loggers.fprintf (Remanent_parameters.get_logger parameters) " => " + in + let error = + Site_graphs.KaSa_site_graph.print + (Remanent_parameters.get_logger parameters) + parameters error t' + in + let () = + Loggers.print_newline (Remanent_parameters.get_logger parameters) + in + error, () + | Remanent_parameters_sig.Natural_language -> + let error', site_string1 = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type site1 + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let error', state_string1 = + Handler.string_of_state_fully_deciphered parameters error + handler_kappa agent_type site1 state1 + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let error', site_string2 = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type site2 + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let error', state_string2 = + Handler.string_of_state_fully_deciphered parameters error + handler_kappa agent_type site2 state2 + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + ( error, + Loggers.fprintf + (Remanent_parameters.get_logger parameters) + "%s%s%s is %s whenever %s is %s.%s" + (Remanent_parameters.get_prefix parameters) + (cap (in_agent_comma agent_string)) + site_string2 state_string2 site_string1 state_string1 endofline + ) + ) else + error, ()) + | Partition (v, list) -> + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site v nr_guard_params + with + | Guard_p _ -> error, () (*rTODO print guards*) + | Site v -> + (*let () = + Loggers.fprintf log + "%s%s%s" (Remanent_parameters.get_prefix parameters) + (cap (in_agent_colon agent_string)) endofline + in*) + let error, site_string = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type v + in + let parameters = Remanent_parameters.update_prefix parameters tab in + let error = + List.fold_left + (fun error (a, list) -> + let error, parameters = + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Natural_language -> + let error, state_string = + Handler.string_of_state_fully_deciphered parameters error + handler_kappa agent_type v a + in + let () = + Loggers.fprintf log "%swhen %s is equal to %s, then:%s%s" + (Remanent_parameters.get_prefix parameters) + site_string state_string endofline beginenumeration + in + let parameters = + Remanent_parameters.update_prefix parameters + (tab ^ beginenum ^ " ") + in + error, parameters + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> + error, parameters + in + let error, t' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id v a t + in + let error = + List.fold_left + (fun error token -> + let error = + print ~beginning_of_sentence:false + ~prompt_agent_type:false ~html_mode + ~show_dep_with_dimmension_higher_than:0 parameters + handler_kappa error agent_string agent_type agent_id + token t' + in + let () = Loggers.fprintf log "%s" endenum in + error) + error list + in + let () = Loggers.fprintf log "%s" endenumeration in + error) + error list + in + error, ()) | No_known_translation list -> (match Remanent_parameters.get_backend_mode parameters with | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> @@ -776,8 +813,14 @@ let rec print ?beginning_of_sentence:(beggining = true) let error, t' = List.fold_left (fun (error, t) (site, state) -> - Site_graphs.KaSa_site_graph.add_state parameters error - handler_kappa agent_id site state t) + match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site + nr_guard_params + with + | Guard_p _ -> error, t (*rTODO print guards*) + | Site site -> + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site state t) (error, t) state_list in let error = @@ -804,30 +847,48 @@ let rec print ?beginning_of_sentence:(beggining = true) let rec aux l error = match l with | [ (a, _) ] -> - let error, string = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type a - in - let () = Loggers.fprintf log ", and %s, " string in - error, () + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site a + nr_guard_params + with + | Guard_p _ -> error, () (*rTODO print guards*) + | Site a -> + let error, string = + Handler.string_of_site_in_natural_language parameters + error handler_kappa agent_type a + in + let () = Loggers.fprintf log ", and %s, " string in + error, ()) | [] -> Exception.warn parameters error __POS__ Exit () | (a, _) :: b -> - let error, string = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type a - in - let () = Loggers.fprintf log ", %s" string in - aux b error + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site a + nr_guard_params + with + | Guard_p _ -> error, () (*rTODO print guards*) + | Site a -> + let error, string = + Handler.string_of_site_in_natural_language parameters + error handler_kappa agent_type a + in + let () = Loggers.fprintf log ", %s" string in + aux b error) in match head with | [] | [ _ ] -> Exception.warn parameters error __POS__ Exit () | (a, _) :: b -> - let error, string = - Handler.string_of_site_in_natural_language parameters error - handler_kappa agent_type a - in - let () = Loggers.fprintf log "%s" string in - aux b error + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site a + nr_guard_params + with + | Guard_p _ -> error, () (*rTODO print guards*) + | Site a -> + let error, string = + Handler.string_of_site_in_natural_language parameters error + handler_kappa agent_type a + in + let () = Loggers.fprintf log "%s" string in + aux b error) in let () = Loggers.fprintf log @@ -842,35 +903,41 @@ let rec print ?beginning_of_sentence:(beggining = true) let error, bool = List.fold_left (fun (error, bool) (site_type, state) -> - let error', site_string = - Handler.string_of_site parameters error handler_kappa - agent_type site_type - in - let error = - Exception.check_point Exception.warn parameters error - error' __POS__ Exit - in - let error', state_string = - Handler.string_of_state_fully_deciphered parameters - error handler_kappa agent_type site_type state - in - let error = - Exception.check_point Exception.warn parameters error - error' __POS__ Exit - in - (*---------------------------------------------*) - let () = - if bool then - Loggers.fprintf log "," - else - Loggers.fprintf log "%s%s(" - (Remanent_parameters.get_prefix parameters) - agent_string - in - let () = - Loggers.fprintf log "%s%s" site_string state_string - in - error, true) + match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site + site_type nr_guard_params + with + | Guard_p _ -> error, bool (*rTODO print guards*) + | Site site_type -> + let error', site_string = + Handler.string_of_site parameters error + handler_kappa agent_type site_type + in + let error = + Exception.check_point Exception.warn parameters + error error' __POS__ Exit + in + let error', state_string = + Handler.string_of_state_fully_deciphered parameters + error handler_kappa agent_type site_type state + in + let error = + Exception.check_point Exception.warn parameters + error error' __POS__ Exit + in + (*---------------------------------------------*) + let () = + if bool then + Loggers.fprintf log "," + else + Loggers.fprintf log "%s%s(" + (Remanent_parameters.get_prefix parameters) + agent_string + in + let () = + Loggers.fprintf log "%s%s" site_string state_string + in + error, true) (error, false) l in (*----------------------------------------------------*) @@ -889,146 +956,175 @@ let rec print ?beginning_of_sentence:(beggining = true) let rec convert_views_internal_constraints_list_aux ~show_dep_with_dimmension_higher_than:dim_min parameters handler_kappa error agent_string agent_type agent_id translation t current_list = + let nr_guard_params = get_nr_guard_parameters handler_kappa in let error, current_list = match translation with | Range (site_type, state_list) -> - if dim_min <= 1 then ( - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - (*hyp*) - (*-----------------------------------------------------*) - let error, t = - Site_graphs.KaSa_site_graph.add_site parameters error handler_kappa - agent_id site_type t - in - let error'', refinement = - List.fold_left - (fun (error, c_list) state -> - let error', t' = - Site_graphs.KaSa_site_graph.add_state parameters error - handler_kappa agent_id site_type state t - in - let error = - Exception.check_point Exception.warn parameters error error' - __POS__ Exit - in - error, t' :: c_list) - (error, []) state_list - in - let lemma = { Public_data.hyp = t; Public_data.refinement } in - let current_list = lemma :: current_list in - let error = - Exception.check_point Exception.warn parameters error error'' - __POS__ Exit - in - error, current_list - | Remanent_parameters_sig.Natural_language -> + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_type + nr_guard_params + with + | Guard_p _ -> error, current_list (*rTODO guards*) + | Site site_type -> + if dim_min <= 1 then ( + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> + (*hyp*) + (*-----------------------------------------------------*) + let error, t = + Site_graphs.KaSa_site_graph.add_site parameters error + handler_kappa agent_id site_type t + in + let error'', refinement = + List.fold_left + (fun (error, c_list) state -> + let error', t' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site_type state t + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + error, t' :: c_list) + (error, []) state_list + in + let lemma = { Public_data.hyp = t; Public_data.refinement } in + let current_list = lemma :: current_list in + let error = + Exception.check_point Exception.warn parameters error error'' + __POS__ Exit + in + error, current_list + | Remanent_parameters_sig.Natural_language -> + (*let _ = + Loggers.fprintf (Remanent_parameters.get_logger parameters) "Natural_language\n" + in*) + error, current_list + ) else (*let _ = - Loggers.fprintf (Remanent_parameters.get_logger parameters) "Natural_language\n" + Loggers.fprintf (Remanent_parameters.get_logger parameters) "test\n" in*) - error, current_list - ) else - (*let _ = - Loggers.fprintf (Remanent_parameters.get_logger parameters) "test\n" - in*) - error, current_list + error, current_list) | Equiv ((site1, state1), (site2, state2)) -> - if dim_min <= 2 then ( - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - let error', t' = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site1 state1 t - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - (*--------------------------------------------------*) - let error''', t'' = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site2 state2 t - in - let error = - Exception.check_point Exception.warn parameters error error''' - __POS__ Exit - in - (*--------------------------------------------------*) - let lemma = - { Public_data.hyp = t'; Public_data.refinement = [ t'' ] } - in - let current_list = lemma :: current_list in - error, List.rev current_list - | Remanent_parameters_sig.Natural_language -> error, current_list - ) else - error, current_list - | Imply ((site1, state1), (site2, state2)) -> - if dim_min <= 2 then ( - match Remanent_parameters.get_backend_mode parameters with - | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> - let error', t = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site1 state1 t - in - let error = - Exception.check_point Exception.warn parameters error error' __POS__ - Exit - in - (*--------------------------------------------------*) - let error''', t' = - Site_graphs.KaSa_site_graph.add_state parameters error handler_kappa - agent_id site2 state2 t - in - let error = - Exception.check_point Exception.warn parameters error error''' - __POS__ Exit - in - (*--------------------------------------------------*) - let lemma = - { - (*Remanent_state.hyp = site_graph ; - Remanent_state.refinement = [site_graph']*) - Public_data.hyp = t; - Public_data.refinement = [ t' ]; - } - in - let current_list = lemma :: current_list in - error, List.rev current_list - | Remanent_parameters_sig.Natural_language -> error, current_list - ) else - error, current_list - | Partition (site_type, list) -> - let error, current_list = - List.fold_left - (fun (error, current_list) (state, list) -> + (match + ( Ckappa_sig.site_or_guard_p_of_guard_p_then_site site1 nr_guard_params, + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site2 nr_guard_params + ) + with + | Guard_p _, _ -> error, current_list (*rTODO guards*) + | _, Guard_p _ -> error, current_list (*rTODO guards*) + | Site site1, Site site2 -> + if dim_min <= 2 then ( + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> let error', t' = Site_graphs.KaSa_site_graph.add_state parameters error - handler_kappa agent_id site_type state t + handler_kappa agent_id site1 state1 t in let error = Exception.check_point Exception.warn parameters error error' __POS__ Exit in - let error'', current_list = - List.fold_left - (fun (error, current_list) token -> - convert_views_internal_constraints_list_aux - ~show_dep_with_dimmension_higher_than:0 parameters - handler_kappa error agent_string agent_type agent_id token - t' current_list) - (error, current_list) list + (*--------------------------------------------------*) + let error''', t'' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site2 state2 t in let error = - Exception.check_point Exception.warn parameters error error'' + Exception.check_point Exception.warn parameters error error''' __POS__ Exit in - (*let _ = - Loggers.fprintf (Remanent_parameters.get_logger parameters) "test1\n" - in*) - error, current_list) - (error, current_list) list - in - error, current_list + (*--------------------------------------------------*) + let lemma = + { Public_data.hyp = t'; Public_data.refinement = [ t'' ] } + in + let current_list = lemma :: current_list in + error, List.rev current_list + | Remanent_parameters_sig.Natural_language -> error, current_list + ) else + error, current_list) + | Imply ((site1, state1), (site2, state2)) -> + (match + ( Ckappa_sig.site_or_guard_p_of_guard_p_then_site site1 nr_guard_params, + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site2 nr_guard_params + ) + with + | Guard_p _, _ -> error, current_list (*rTODO guards*) + | _, Guard_p _ -> error, current_list (*rTODO guards*) + | Site site1, Site site2 -> + if dim_min <= 2 then ( + match Remanent_parameters.get_backend_mode parameters with + | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> + let error', t = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site1 state1 t + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + (*--------------------------------------------------*) + let error''', t' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site2 state2 t + in + let error = + Exception.check_point Exception.warn parameters error error''' + __POS__ Exit + in + (*--------------------------------------------------*) + let lemma = + { + (*Remanent_state.hyp = site_graph ; + Remanent_state.refinement = [site_graph']*) + Public_data.hyp = t; + Public_data.refinement = [ t' ]; + } + in + let current_list = lemma :: current_list in + error, List.rev current_list + | Remanent_parameters_sig.Natural_language -> error, current_list + ) else + error, current_list) + | Partition (site_type, list) -> + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_type + nr_guard_params + with + | Guard_p _ -> error, current_list (*rTODO guards*) + | Site site_type -> + let error, current_list = + List.fold_left + (fun (error, current_list) (state, list) -> + let error', t' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site_type state t + in + let error = + Exception.check_point Exception.warn parameters error error' + __POS__ Exit + in + let error'', current_list = + List.fold_left + (fun (error, current_list) token -> + convert_views_internal_constraints_list_aux + ~show_dep_with_dimmension_higher_than:0 parameters + handler_kappa error agent_string agent_type agent_id token + t' current_list) + (error, current_list) list + in + let error = + Exception.check_point Exception.warn parameters error error'' + __POS__ Exit + in + (*let _ = + Loggers.fprintf (Remanent_parameters.get_logger parameters) "test1\n" + in*) + error, current_list) + (error, current_list) list + in + error, current_list) | No_known_translation list -> (match Remanent_parameters.get_backend_mode parameters with | Remanent_parameters_sig.Kappa | Remanent_parameters_sig.Raw -> @@ -1039,15 +1135,21 @@ let rec convert_views_internal_constraints_list_aux let error, t' = List.fold_left (fun (error, t') (site, state) -> - let error', t' = - Site_graphs.KaSa_site_graph.add_state parameters error - handler_kappa agent_id site state t' - in - let error = - Exception.check_point Exception.warn parameters error - error' __POS__ Exit - in - error, t') + match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site + nr_guard_params + with + | Guard_p _ -> error, t' (*rTODO guards*) + | Site site -> + let error', t' = + Site_graphs.KaSa_site_graph.add_state parameters error + handler_kappa agent_id site state t' + in + let error = + Exception.check_point Exception.warn parameters error + error' __POS__ Exit + in + error, t') (error, t) state_list in let refinement = t' :: current_list in @@ -1079,11 +1181,17 @@ let convert_views_internal_constraints_list let error = Exception.check_point Exception.warn parameters error error' __POS__ Exit in + let nr_guard_params = get_nr_guard_parameters handler_kappa in let error, t = match translation with | Range (site, _) -> - Site_graphs.KaSa_site_graph.add_site parameters error handler_kappa - agent_id site t + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site nr_guard_params + with + | Guard_p _ -> error, t (*rTODO guards*) + | Site site -> + Site_graphs.KaSa_site_graph.add_site parameters error handler_kappa + agent_id site t) | Equiv _ | Imply _ | Partition _ | No_known_translation _ -> error, t in convert_views_internal_constraints_list_aux diff --git a/core/KaSa_rep/reachability_analysis/translation_in_natural_language.mli b/core/KaSa_rep/reachability_analysis/translation_in_natural_language.mli index e43d7f110..f13336cc0 100644 --- a/core/KaSa_rep/reachability_analysis/translation_in_natural_language.mli +++ b/core/KaSa_rep/reachability_analysis/translation_in_natural_language.mli @@ -13,23 +13,23 @@ * under the terms of the GNU Library General Public License *) type token = - | Range of Ckappa_sig.c_site_name * Ckappa_sig.c_state list + | Range of Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state list | Equiv of - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) - * (Ckappa_sig.c_site_name * Ckappa_sig.c_state) + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) + * (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) | Imply of - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) - * (Ckappa_sig.c_site_name * Ckappa_sig.c_state) + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) + * (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) | Partition of - (Ckappa_sig.c_site_name * (Ckappa_sig.c_state * token list) list) + (Ckappa_sig.c_guard_p_then_site * (Ckappa_sig.c_state * token list) list) | No_known_translation of - (Ckappa_sig.c_site_name * Ckappa_sig.c_state) list list + (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) list list type rename_sites = Remanent_parameters_sig.parameters -> Exception.exceptions_caught_and_uncaught -> - Ckappa_sig.Site_map_and_set.Map.elt -> - Exception.exceptions_caught_and_uncaught * Ckappa_sig.Site_map_and_set.Map.elt + Ckappa_sig.c_guard_p_then_site -> + Exception.exceptions_caught_and_uncaught * Ckappa_sig.c_guard_p_then_site val non_relational : Remanent_parameters_sig.parameters -> diff --git a/core/KaSa_rep/reachability_analysis/views_domain.ml b/core/KaSa_rep/reachability_analysis/views_domain.ml index d8a321751..fe781b5c6 100644 --- a/core/KaSa_rep/reachability_analysis/views_domain.ml +++ b/core/KaSa_rep/reachability_analysis/views_domain.ml @@ -307,12 +307,15 @@ module Domain = struct let dynamic = set_log_info log_info dynamic in let dynamic = set_mvbdu_handler handler_bdu dynamic in let static = set_domain_static result static in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in (*-----------------------------------------------------------------------*) (*pattern*) (*-----------------------------------------------------------------------*) let error, result = Bdu_static_views.scan_rule_set_pattern parameters error remanent_triple - compiled + compiled nr_guard_params in let static = set_domain_static_pattern result static in error, static, dynamic @@ -522,12 +525,12 @@ module Domain = struct match cv_id_array_opt with | None -> let error, map1 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.create parameters - error 0 + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.create + parameters error 0 in let error, map2 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.create parameters - error 0 + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.create + parameters error 0 in Exception.warn parameters error __POS__ Exit (map1, map2) | Some cv_id_array -> @@ -538,11 +541,11 @@ module Domain = struct (match pair_opt with | None -> let error, map1 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.create + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.create parameters error 0 in let error, map2 = - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.create + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.create parameters error 0 in Exception.warn parameters error __POS__ Exit (map1, map2) @@ -717,22 +720,22 @@ module Domain = struct (fun (error, bool) (site_type, state) -> let error, site_type = match - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.get - parameters error site_type map2 + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif + .get parameters error site_type map2 with | error, None -> Exception.warn parameters error __POS__ Exit - Ckappa_sig.dummy_site_name + (Ckappa_sig.Site Ckappa_sig.dummy_site_name) | error, Some i -> error, i in (*----------------------------------------------------*) let error, site_string = try - Handler.string_of_site parameters error handler_kappa - ~state agent_type site_type + Handler.string_of_site_or_guard parameters error + handler_kappa ~state agent_type site_type with _ -> Exception.warn parameters error __POS__ Exit - (Ckappa_sig.string_of_site_name site_type) + (Ckappa_sig.string_of_site_or_guard site_type) in (*-----------------------------------------------------*) let () = @@ -838,7 +841,7 @@ module Domain = struct (*build bdu restriction for initial state *) let bdu_build static dynamic error - (pair_list : (Ckappa_sig.c_site_name * Ckappa_sig.c_state) list) = + (pair_list : (Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) list) = let parameters = get_parameter static in let handler = get_mvbdu_handler dynamic in let error, handler, bdu_result = @@ -853,6 +856,9 @@ module Domain = struct let build_init_restriction static dynamic error init_state = let parameters = get_parameter static in let store_remanent_triple = get_remanent_triple static in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters (get_kappa_handler static) + in let error, (dynamic, event_list) = Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.fold parameters error @@ -874,13 +880,13 @@ module Domain = struct let error, get_pair_list = Bdu_static_views .get_pair_cv_map_with_missing_association_creation parameters - error agent triple_list + error agent triple_list nr_guard_params in let error, (dynamic, event_list) = List.fold_left (fun (error, (dynamic, event_list)) (cv_id, map_res) -> let error, pair_list = - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' state (error, current_list) -> let pair_list = (site', state) :: current_list in error, pair_list) @@ -965,35 +971,42 @@ module Domain = struct (*****************************************************************) (*MOVE in static?*) - let get_new_site_name parameters error site_name + let get_new_site_name parameters error site_name nr_guard_parameters (*store_new_index_pair_map*) map1 = let error, new_site_name = match - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.get parameters + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.get parameters error site_name map1 with | error, None -> - Exception.warn parameters error __POS__ Exit Ckappa_sig.dummy_site_name + Exception.warn parameters error __POS__ Exit + (Ckappa_sig.guard_p_then_site_of_site Ckappa_sig.dummy_site_name + nr_guard_parameters) | error, Some i -> error, i in error, new_site_name (*MOVE?*) - let is_new_site_name parameters error site_name map1 = + let is_new_site_name parameters error site_name map1 nr_guard_parameters = match - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.unsafe_get - parameters error site_name map1 + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.unsafe_get + parameters error + (Ckappa_sig.guard_p_then_site_of_site site_name nr_guard_parameters) + map1 with | error, None -> error, false | error, Some _ -> error, true (*****************************************************************) - let step_list_empty _kappa_handler dynamic parameters error agent_id - agent_type site_name cv_list fixpoint_result proj_bdu_test_restriction - bdu_false bdu_true site_correspondence = + let step_list_empty kappa_handler dynamic parameters error agent_id agent_type + site_name cv_list fixpoint_result proj_bdu_test_restriction bdu_false + bdu_true site_correspondence = (*------------------------------------------------------------*) + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in let error, dynamic, bdu = List.fold_left (fun (error, dynamic, bdu) cv_id -> @@ -1002,7 +1015,7 @@ module Domain = struct cv_id site_correspondence in let error, new_site_name = - get_new_site_name parameters error site_name map1 + get_new_site_name parameters error site_name nr_guard_params map1 in (*--------------------------------------------------------------*) (* fetch the bdu for the agent type and the cv_id in @@ -1086,6 +1099,9 @@ module Domain = struct let precondition_empty_step_list kappa_handler parameters error dynamic rule_id path store_agent_name bdu_false bdu_true store_covering_classes_id site_correspondence fixpoint_result proj_bdu_test_restriction = + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in let error, agent_type = match Ckappa_sig.RuleAgent_map_and_set.Map.find_option_without_logs parameters @@ -1127,8 +1143,10 @@ module Domain = struct (*---------------------------------------------------------------------*) let error, dynamic, new_answer = step_list_empty kappa_handler dynamic parameters error - path.Communication.agent_id agent_type path.Communication.site cv_list - fixpoint_result proj_bdu_test_restriction bdu_false bdu_true + path.Communication.agent_id agent_type + (Ckappa_sig.guard_p_then_site_of_site path.Communication.site + nr_guard_params) + cv_list fixpoint_result proj_bdu_test_restriction bdu_false bdu_true (*store_new_index_pair_map*) site_correspondence in @@ -1277,6 +1295,12 @@ module Domain = struct where (agent_type_in, site_in) is the information of the last agent, and (agent_type', site_in) is the information of the agent of the pattern *) + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in + let to_guard_or_site s = + Ckappa_sig.guard_p_then_site_of_site s nr_guard_params + in let error, (agent_type', site_out, site_in, agent_type_in) = get_tuple_pattern error path agent_type in @@ -1344,7 +1368,9 @@ module Domain = struct get_list_of_sites_correspondence_map parameters error agent_type_in cv_id site_correspondence_map in - let error, b = is_new_site_name parameters error site_in map1 in + let error, b = + is_new_site_name parameters error site_in map1 nr_guard_params + in let error, bdu_X = match Covering_classes_type.AgentCV_map_and_set.Map @@ -1356,7 +1382,9 @@ module Domain = struct in let handler = Analyzer_headers.get_mvbdu_handler dynamic in let error, new_site_name_z = - get_new_site_name parameters error site_path map1 + get_new_site_name parameters error + (to_guard_or_site site_path) + nr_guard_params map1 in let error, handler, singleton = Ckappa_sig.Views_bdu.build_variables_list parameters handler @@ -1366,7 +1394,8 @@ module Domain = struct if b then ( (*site y is in CV, *) let error, new_site_name_y = - get_new_site_name parameters error site_in map1 + get_new_site_name parameters error + (to_guard_or_site site_in) nr_guard_params map1 in let error, handler, mvbdu_B_y = Ckappa_sig.Views_bdu @@ -1386,7 +1415,7 @@ module Domain = struct let error, handler, new_site_name_1 = Ckappa_sig.Views_bdu.build_renaming_list parameters handler error - [ new_site_name_z, site_path ] + [ new_site_name_z, to_guard_or_site site_path ] in let error, handler, bdu_renamed = Ckappa_sig.Views_bdu.mvbdu_rename parameters handler error @@ -2009,7 +2038,7 @@ module Domain = struct (************************************************************************) let build_bdu_test_pattern parameters error pattern site_correspondence - dynamic = + dynamic nr_guard_params = Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.fold parameters error (fun parameters error _agent_id agent (dynamic, current_list) -> @@ -2021,17 +2050,17 @@ module Domain = struct let agent_type = agent.Cckappa_sig.agent_name in let error, get_pair_list = Bdu_static_views.get_pair_cv_map_with_restriction_views parameters - error agent site_correspondence + error agent site_correspondence nr_guard_params in (*build bdu_test*) let error, (dynamic, list) = List.fold_left (fun (error, (dynamic, current_list)) (_cv_id, map_res) -> - if Ckappa_sig.Site_map_and_set.Map.is_empty map_res then + if Ckappa_sig.GuardSite_map_and_set.Map.is_empty map_res then error, (dynamic, current_list) else ( let error, pair_list = - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' state (error, current_list) -> let pair_list = (site', (state.Cckappa_sig.min, state.Cckappa_sig.max)) @@ -2056,12 +2085,18 @@ module Domain = struct error, (dynamic, list)) pattern.Cckappa_sig.views (dynamic, []) - let precondition_empty_aux parameters error path pattern dynamic bdu_false - bdu_true site_correspondence site_correspondence_map fixpoint_result - cv_list = + let precondition_empty_aux parameters error path pattern kappa_handler dynamic + bdu_false bdu_true site_correspondence site_correspondence_map + fixpoint_result cv_list = + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in + let to_guard_or_site s = + Ckappa_sig.guard_p_then_site_of_site s nr_guard_params + in let error, (dynamic, list) = build_bdu_test_pattern parameters error pattern site_correspondence - dynamic + dynamic nr_guard_params in (*--------------------------------------------------*) let error, dynamic, bdu = @@ -2075,7 +2110,9 @@ module Domain = struct cv_id site_correspondence_map in let error, new_site_name = - get_new_site_name parameters error site_name map1 + get_new_site_name parameters error + (to_guard_or_site site_name) + nr_guard_params map1 in let error, bdu_X = match @@ -2103,7 +2140,7 @@ module Domain = struct let error, handler, new_site_name_1 = Ckappa_sig.Views_bdu.build_renaming_list parameters handler error - [ new_site_name, site_name ] + [ new_site_name, to_guard_or_site site_name ] in let error, handler, bdu_renamed = Ckappa_sig.Views_bdu.mvbdu_rename parameters handler error @@ -2138,9 +2175,10 @@ module Domain = struct in error, (dynamic, Usual_domains.Val (List.rev state_lists)) - let precondition_empty_pattern parameters error path pattern dynamic bdu_false - bdu_true store_agent_name_from_pattern site_correspondence - site_correspondence_map store_covering_classes_id fixpoint_result = + let precondition_empty_pattern parameters error path pattern kappa_handler + dynamic bdu_false bdu_true store_agent_name_from_pattern + site_correspondence site_correspondence_map store_covering_classes_id + fixpoint_result = let error, agent_type = match Ckappa_sig.Agent_id_map_and_set.Map.find_option_without_logs parameters @@ -2174,9 +2212,9 @@ module Domain = struct in (*step list empty*) let error, (dynamic, new_answer) = - precondition_empty_aux parameters error path pattern dynamic bdu_false - bdu_true site_correspondence site_correspondence_map fixpoint_result - cv_list + precondition_empty_aux parameters error path pattern kappa_handler dynamic + bdu_false bdu_true site_correspondence site_correspondence_map + fixpoint_result cv_list in error, dynamic, new_answer @@ -2196,6 +2234,9 @@ module Domain = struct let site_correspondence = get_remanent_triple static in let site_correspondence_map = get_site_correspondence_array static in let store_covering_classes_id = get_covering_classes_id static in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in (*---------------------------------------------------------*) (* Why an arbitrary patterns would be stored in that map *) (* For each view, you have to collect the set of sites *) @@ -2231,17 +2272,18 @@ module Domain = struct in let error, get_pair_list = Bdu_static_views.get_pair_cv_map_with_restriction_views - parameters error agent site_correspondence + parameters error agent site_correspondence nr_guard_params in (*build bdu_test*) let error, dynamic = List.fold_left (fun (error, dynamic) (cv_id, map_res) -> - if Ckappa_sig.Site_map_and_set.Map.is_empty map_res then + if Ckappa_sig.GuardSite_map_and_set.Map.is_empty map_res + then error, dynamic else ( let error, pair_list = - Ckappa_sig.Site_map_and_set.Map.fold + Ckappa_sig.GuardSite_map_and_set.Map.fold (fun site' state (error, current_list) -> let pair_list = ( site', @@ -2395,9 +2437,10 @@ module Domain = struct | [] -> let error, dynamic, new_answer = precondition_empty_pattern parameters error path pattern - dynamic bdu_false bdu_true store_agent_name_from_pattern - site_correspondence site_correspondence_map - store_covering_classes_id fixpoint_result + kappa_handler dynamic bdu_false bdu_true + store_agent_name_from_pattern site_correspondence + site_correspondence_map store_covering_classes_id + fixpoint_result in let error = scan_bot ~also_scan_top:false __POS__ parameters error @@ -2672,9 +2715,14 @@ module Domain = struct let apply_one_side_effect static dynamic error _rule_id (_, (agent_name, site, state)) precondition = let parameters = get_parameter static in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters (get_kappa_handler static) + in + let site = Ckappa_sig.guard_p_then_site_of_site site nr_guard_params in let error, site_to_site_list = get_site_to_renamed_site_list static error in let error, site_list_opt = - Ckappa_sig.Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif + Ckappa_sig + .Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif .unsafe_get parameters error (agent_name, site) site_to_site_list in let site_list = @@ -2760,9 +2808,12 @@ module Domain = struct (**************************************************************************) let smash_map decomposition ~show_dep_with_dimmension_higher_than:_dim_min - parameters handler error _handler_kappa + parameters handler error handler_kappa (*store_new_index_pair_map*) site_correspondence result = + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters handler_kappa + in let error', handler, mvbdu_true = Ckappa_sig.Views_bdu.mvbdu_true parameters handler error in @@ -2779,12 +2830,12 @@ module Domain = struct let rename_site parameters error site_type = let error, site_type = match - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif.get + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif.get parameters error site_type map2 with | error, None -> Exception.warn parameters error __POS__ Exit - Ckappa_sig.dummy_site_name_minus1 + (Ckappa_sig.Site Ckappa_sig.dummy_site_name_minus1) | error, Some i -> error, i in error, site_type @@ -2805,7 +2856,11 @@ module Domain = struct List.fold_left (fun (error, list) i -> let error, new_name = rename_site parameters error i in - error, (i, new_name) :: list) + ( error, + ( i, + Ckappa_sig.guard_p_then_site_of_site_or_guard_p new_name + nr_guard_params ) + :: list )) (error, []) (List.rev list) in let error, handler, hconsed_asso = @@ -2854,6 +2909,9 @@ module Domain = struct let stabilise_bdu_update_map_gen_decomposition decomposition ~smash ~show_dep_with_dimmension_higher_than:dim_min parameters handler error handler_kappa site_correspondence result = + let nr_guard_parameters = + Covering_classes_main.get_nr_guard_parameters handler_kappa + in let log = Remanent_parameters.get_logger parameters in if smash then ( let error', handler, output = @@ -2958,13 +3016,18 @@ module Domain = struct let rename_site parameters error site_type = let error, site_type = match - Ckappa_sig.Site_type_nearly_Inf_Int_storage_Imperatif + Ckappa_sig.GuardPOrSite_nearly_Inf_Int_storage_Imperatif .get parameters error site_type map2 with | error, None -> Exception.warn parameters error __POS__ Exit - Ckappa_sig.dummy_site_name_minus1 - | error, Some i -> error, i + (Ckappa_sig.guard_p_then_site_of_site + Ckappa_sig.dummy_site_name_minus1 + nr_guard_parameters) + | error, Some i -> + ( error, + Ckappa_sig.guard_p_then_site_of_site_or_guard_p i + nr_guard_parameters ) in error, site_type in @@ -3001,7 +3064,7 @@ module Domain = struct match translation with | Translation_in_natural_language.Range (x, _) -> let error, x = - Handler.string_of_site_contact_map parameters error + Handler.string_of_site_or_guard_contact_map parameters error handler_kappa agent_id x in error, (agent_string, x) @@ -3287,6 +3350,9 @@ module Domain = struct let kappa_handler = get_kappa_handler static in let handler = get_mvbdu_handler dynamic in let parameters = get_parameter static in + let nr_guard_params = + Covering_classes_main.get_nr_guard_parameters kappa_handler + in let contact_map = Preprocess.init_contact_map in (*-----------------------------------------------*) let error, (handler, contact_map) = @@ -3305,62 +3371,72 @@ module Domain = struct match list_of_states with | [] -> error, (handler, contact_map) | [ (site_type, _) ] :: _ -> - let error, contact_map = - Preprocess.declare_site parameters error ag_type site_type - contact_map - in - let error, site = - Handler.translate_site parameters error kappa_handler - ag_type site_type - in - (match site with - | Ckappa_sig.Internal _ -> + (match + Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_type + nr_guard_params + with + | Ckappa_sig.Guard_p _ -> error, (handler, contact_map) + | Ckappa_sig.Site site_type -> let error, contact_map = - List.fold_left - (fun (error, contact_map) l -> - match l with - | [ (site_type', state) ] when site_type' = site_type - -> - Preprocess.add_internal_state_in_contact_map - parameters error (ag_type, site_type) state - contact_map - | [] | _ :: _ -> - Exception.warn parameters error __POS__ Exit - contact_map) - (error, contact_map) list_of_states + Preprocess.declare_site parameters error ag_type site_type + contact_map in - error, (handler, contact_map) - | Ckappa_sig.Counter _ -> error, (handler, contact_map) - | Ckappa_sig.Binding _ -> - let error, contact_map = - List.fold_left - (fun (error, contact_map) l -> - match l with - | [ (site_type', state) ] when site_type' = site_type - -> - if state = Ckappa_sig.state_index_of_int 0 then - (* we ignore free sites *) - error, contact_map - else ( - let error, dual = - Handler.dual parameters error kappa_handler - ag_type site_type state - in - match dual with - | None -> - Exception.warn parameters error __POS__ Exit - contact_map - | Some (ag_type', site_type', _) -> - Preprocess.add_link_in_contact_map parameters - error (ag_type, site_type) - (ag_type', site_type') contact_map - ) - | [] | _ :: _ -> - Exception.warn parameters error __POS__ Exit - contact_map) - (error, contact_map) list_of_states + let error, site = + Handler.translate_site parameters error kappa_handler + ag_type site_type in - error, (handler, contact_map)) + (match site with + | Ckappa_sig.Internal _ -> + let error, contact_map = + List.fold_left + (fun (error, contact_map) l -> + match l with + | [ (site_type', state) ] + when site_type' + = Ckappa_sig.guard_p_then_site_of_site + site_type nr_guard_params -> + Preprocess.add_internal_state_in_contact_map + parameters error (ag_type, site_type) state + contact_map + | [] | _ :: _ -> + Exception.warn parameters error __POS__ Exit + contact_map) + (error, contact_map) list_of_states + in + error, (handler, contact_map) + | Ckappa_sig.Counter _ -> error, (handler, contact_map) + | Ckappa_sig.Binding _ -> + let error, contact_map = + List.fold_left + (fun (error, contact_map) l -> + match l with + | [ (site_type', state) ] + when site_type' + = Ckappa_sig.guard_p_then_site_of_site + site_type nr_guard_params -> + if state = Ckappa_sig.state_index_of_int 0 then + (* we ignore free sites *) + error, contact_map + else ( + let error, dual = + Handler.dual parameters error kappa_handler + ag_type site_type state + in + match dual with + | None -> + Exception.warn parameters error __POS__ Exit + contact_map + | Some (ag_type', site_type', _) -> + Preprocess.add_link_in_contact_map parameters + error (ag_type, site_type) + (ag_type', site_type') contact_map + ) + | [] | _ :: _ -> + Exception.warn parameters error __POS__ Exit + contact_map) + (error, contact_map) list_of_states + in + error, (handler, contact_map))) | _ :: _ -> Exception.warn parameters error __POS__ Exit (handler, contact_map))