Remove inverted counters from snapshot

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

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 =

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
 

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

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;
   |]

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 ->

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 "@[<v>%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 "@[<hv 2>%%agent:@ %a(@[%a@])@]"
              (Signature.print_agent sigs)
              ag

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})