From d0e8f3b206b019134379fddaff0e8c56b89a4594 Mon Sep 17 00:00:00 2001 From: Antoine Pouille Date: Thu, 7 Mar 2024 13:51:44 +0100 Subject: [PATCH] Remove inverted counters from snapshot --- core/grammar/lKappa_compiler.ml | 16 ++- core/siteGraphs/edges.ml | 20 ++- core/siteGraphs/signature.ml | 2 + core/siteGraphs/signature.mli | 3 + core/siteGraphs/snapshot.ml | 127 ++++++++++-------- core/siteGraphs/snapshot.mli | 1 + core/term/contact_map.ml | 2 +- .../counters_create/output/error.log.ref | 2 +- 8 files changed, 102 insertions(+), 71 deletions(-) diff --git a/core/grammar/lKappa_compiler.ml b/core/grammar/lKappa_compiler.ml index f6631c926..0094bb0e6 100644 --- a/core/grammar/lKappa_compiler.ml +++ b/core/grammar/lKappa_compiler.ml @@ -1860,6 +1860,9 @@ type ast_compiled_data = { * (syntactic sugar on mixture are not) *) } +let inverted_counter_name (name : string) : string = + name ^ Signature.inverted_counter_suffix + (** Evaluates to a ast_compil where clte tests have been changed to cgte tests. * For this, for each counter where a CLTE test is present, whose values are in [\[a, b\]], initialized at [i] and add a new counter belonging in [a, b] initialized at [a+b-i]. * Each test [> value] is then translated into a test to the "inverted" counter as [< a+b-value]. @@ -1890,21 +1893,20 @@ let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) = [] ast_compil.rules in - let inverted_counter_suffix = "__inverted" in - let inverted_counter_name (name : string) : string = - name ^ inverted_counter_suffix - in - (* Find counters that have CLTE tests, and build list: agent_name, counter_name, sum_bounds_ref list. * sum_bounds_ref is then filled when reading the signature and used to specify for inverted counter init value or test value as [sum_bounds_ref - value] *) let counters_with_clte_tests : (string * string * int ref) list = counter_fold (fun acc agent_name counter -> let counter_name = Loc.v counter.counter_name in (* Forbid prefix to avoid nonsense in counter definition *) - if String.ends_with ~suffix:inverted_counter_suffix counter_name then + if + String.ends_with ~suffix:Signature.inverted_counter_suffix + counter_name + then raise (ExceptionDefn.Malformed_Decl - ( "cannot end counter name by \"" ^ inverted_counter_suffix ^ "\"", + ( "cannot end counter name by \"" + ^ Signature.inverted_counter_suffix ^ "\"", Loc.get_annot counter.counter_name )); (* Return counter name along with matching agent_name *) match Option_util.map Loc.v counter.counter_test with diff --git a/core/siteGraphs/edges.ml b/core/siteGraphs/edges.ml index f1d3d0325..94030778e 100644 --- a/core/siteGraphs/edges.ml +++ b/core/siteGraphs/edges.ml @@ -567,8 +567,12 @@ let get_connected_component ag graph = | Some ccs -> Mods.DynArray.get ccs ag) (** The snapshot machinery *) -let one_connected_component sigs ty node graph = - let rec build id acc known = function +let one_connected_component (sigs : Signature.s) (ty : int) (node : int) + (graph : tables) : Snapshot.cc_node array = + let rec build (id : int) + (acc : (int * int * (Edge.t option * int option) list) list) + (known : int Mods.IntMap.t) : (int * int) list -> Snapshot.cc_node array = + function | [] -> Tools.array_rev_map_of_list (fun (node_id_in_witness, node_type, sites) -> @@ -636,28 +640,32 @@ let species ~debug_mode sigs root graph = let () = Cache.reset (fst tables.caches) in specie -let rec aux_build_snapshot raw sigs tables ccs node = +let rec aux_build_snapshot (raw : bool) (sigs : Signature.s) (tables : tables) + (ccs : Snapshot.t) (node : int) : Snapshot.t = if node = Mods.DynArray.length tables.sort then ( + (* We went through all nodes, we return the full snapshot *) let () = Cache.reset (fst tables.caches) in ccs ) else if Cache.test (fst tables.caches) node then + (* Already in cache, we continue to the next node *) aux_build_snapshot raw sigs tables ccs (succ node) else ( match Mods.DynArray.get tables.sort node with | None -> aux_build_snapshot raw sigs tables ccs (succ node) - | Some ty -> + | Some (ty : int) -> let out = one_connected_component sigs ty node tables in aux_build_snapshot raw sigs tables (Snapshot.increment_in_snapshot ~raw sigs out ccs) (succ node) ) -let build_snapshot ~raw sigs graph = +let build_snapshot ~(raw : bool) (sigs : Signature.s) (graph : t) : Snapshot.t = match graph.tables with | None -> assert false | Some tables -> aux_build_snapshot raw sigs tables Snapshot.empty 0 -let build_user_snapshot ~debug_mode ~raw sigs graph = +let build_user_snapshot ~(debug_mode : bool) ~(raw : bool) (sigs : Signature.s) + (graph : t) : (int * User_graph.connected_component) list = Snapshot.export ~debug_mode ~raw sigs (build_snapshot ~raw sigs graph) let debug_print f graph = diff --git a/core/siteGraphs/signature.ml b/core/siteGraphs/signature.ml index 96e4ef077..fe3224559 100644 --- a/core/siteGraphs/signature.ml +++ b/core/siteGraphs/signature.ml @@ -236,6 +236,8 @@ let get_counter_agent_info sigs = | None -> failwith "No counter agent" | Some counter_agent_info -> counter_agent_info +let inverted_counter_suffix : string = "__inverted" + let print_agent sigs f ag_ty = Format.pp_print_string f @@ agent_of_num ag_ty sigs diff --git a/core/siteGraphs/signature.mli b/core/siteGraphs/signature.mli index da2a872a2..c27622be4 100644 --- a/core/siteGraphs/signature.mli +++ b/core/siteGraphs/signature.mli @@ -88,6 +88,9 @@ type counter_agent_info = { id: int; arity: int; ports: int * int } val get_counter_agent_info : s -> counter_agent_info (** [counter_agent agent_sigs] *) +val inverted_counter_suffix : string +(** Suffix added to counter names to make an inverted counter name when needed for a <= test *) + (** {2 I/O} *) val print_agent : s -> Format.formatter -> int -> unit diff --git a/core/siteGraphs/snapshot.ml b/core/siteGraphs/snapshot.ml index 1a30e628d..f58c1edee 100644 --- a/core/siteGraphs/snapshot.ml +++ b/core/siteGraphs/snapshot.ml @@ -126,13 +126,15 @@ let rec counter_value cc (nid, sid) count = )) count ag.node_sites -let cc_to_user_cc ~debug_mode ~raw sigs cc = - let r = Renaming.empty () in - let cc_list, indexes, _ = +let cc_to_user_cc ?(keep_inverted_counters : bool = false) ~debug_mode ~raw sigs + cc = + let r : Renaming.t = Renaming.empty () in + let (cc_list_without_counters, indexes, _) : cc_node list * Renaming.t * int = Tools.array_fold_lefti (fun i (acc, indexes, pos) ag -> - match Signature.ports_if_counter_agent sigs ag.node_type with - | None -> + if Signature.is_counter_agent sigs ag.node_type then + acc, indexes, pos + else ( let indexes' = if i = pos then indexes @@ -146,13 +148,74 @@ let cc_to_user_cc ~debug_mode ~raw sigs cc = ) in ag :: acc, indexes', pos + 1 - | Some _ -> acc, indexes, pos) + )) ([], r, 0) cc in - let cc_without_counters = Array.of_list (List.rev cc_list) in + let cc_without_counters : cc_node array = + Array.of_list (List.rev cc_list_without_counters) + in [| Array.map (fun ag -> + let node_sites_all : User_graph.cc_site array = + Array.mapi + (fun id si -> + { + User_graph.site_name = + Format.asprintf "%a" + (Signature.print_site sigs ag.node_type) + id; + User_graph.site_type = + (let port_states = + match si.site_state with + | None -> Some [] + | Some s -> + Some + [ + Format.asprintf "%a" + (Signature.print_internal_state sigs ag.node_type + id) + s; + ] + in + match si.site_link with + | None -> + User_graph.Port + { + User_graph.port_links = User_graph.LINKS []; + User_graph.port_states; + } + | Some (dn_id, s) -> + let dn_id' = + try Renaming.apply ~debug_mode indexes dn_id + with Renaming.Undefined | Invalid_argument _ -> dn_id + in + if Signature.is_counter_agent sigs cc.(dn_id).node_type + then + User_graph.Counter (counter_value cc (dn_id, s) 0) + else + User_graph.Port + { + User_graph.port_links = + User_graph.LINKS [ (0, dn_id'), s ]; + User_graph.port_states; + }); + }) + ag.node_sites + in + let node_sites : User_graph.cc_site array = + if keep_inverted_counters then + node_sites_all + else + (* Remove inverted counters from user snapshot *) + node_sites_all |> Array.to_list + |> List.filter (fun (site : User_graph.cc_site) : bool -> + not + (String.ends_with ~suffix:Signature.inverted_counter_suffix + site.site_name)) + |> Array.of_list + in + Some { User_graph.node_id = @@ -162,55 +225,7 @@ let cc_to_user_cc ~debug_mode ~raw sigs cc = None); User_graph.node_type = Format.asprintf "%a" (Signature.print_agent sigs) ag.node_type; - User_graph.node_sites = - Array.mapi - (fun id si -> - { - User_graph.site_name = - Format.asprintf "%a" - (Signature.print_site sigs ag.node_type) - id; - User_graph.site_type = - (let port_states = - match si.site_state with - | None -> Some [] - | Some s -> - Some - [ - Format.asprintf "%a" - (Signature.print_internal_state sigs - ag.node_type id) - s; - ] - in - match si.site_link with - | None -> - User_graph.Port - { - User_graph.port_links = User_graph.LINKS []; - User_graph.port_states; - } - | Some (dn_id, s) -> - let dn_id' = - try Renaming.apply ~debug_mode indexes dn_id - with Renaming.Undefined | Invalid_argument _ -> - dn_id - in - (match - Signature.ports_if_counter_agent sigs - cc.(dn_id).node_type - with - | None -> - User_graph.Port - { - User_graph.port_links = - User_graph.LINKS [ (0, dn_id'), s ]; - User_graph.port_states; - } - | Some _ -> - User_graph.Counter (counter_value cc (dn_id, s) 0))); - }) - ag.node_sites; + User_graph.node_sites; }) cc_without_counters; |] diff --git a/core/siteGraphs/snapshot.mli b/core/siteGraphs/snapshot.mli index 71f9c69cf..077a1bf28 100644 --- a/core/siteGraphs/snapshot.mli +++ b/core/siteGraphs/snapshot.mli @@ -21,6 +21,7 @@ type connected_component = cc_node array type t val cc_to_user_cc : + ?keep_inverted_counters:bool -> debug_mode:bool -> raw:bool -> Signature.s -> diff --git a/core/term/contact_map.ml b/core/term/contact_map.ml index bf6fa6db0..125ba0b52 100644 --- a/core/term/contact_map.ml +++ b/core/term/contact_map.ml @@ -67,7 +67,7 @@ let of_yojson (a : Yojson.Basic.t) = let print_kappa ~noCounters sigs f c = Format.fprintf f "@[%a@]" (Pp.array Pp.space (fun ag f intf -> - if Signature.ports_if_counter_agent sigs ag = None || noCounters then + if (not (Signature.is_counter_agent sigs ag)) || noCounters then Format.fprintf f "@[%%agent:@ %a(@[%a@])@]" (Signature.print_agent sigs) ag diff --git a/tests/integration/simulation/counters_create/output/error.log.ref b/tests/integration/simulation/counters_create/output/error.log.ref index 55a24aebb..356df5364 100644 --- a/tests/integration/simulation/counters_create/output/error.log.ref +++ b/tests/integration/simulation/counters_create/output/error.log.ref @@ -63,5 +63,5 @@ Domain: 3 -2(c[a.!__counter_agent-5])->() 2) Intial graph; - %init: 1 A(c{=0} c__inverted{=10}) + %init: 1 A(c{=0})