diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f986cc99d..7a7ce2600 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -59,7 +59,7 @@ jobs:
           sudo apt-get install --yes gnuplot-nox \
             poppler-utils graphviz texlive-latex-recommended \
             texlive-fonts-recommended texlive-pictures tex4ht
-          opam install --yes dune num yojson lwt fmt logs re \
+          opam install --yes dune num yojson result lwt fmt logs re \
             cohttp-lwt-unix atdgen
           pip install nose
       - name: Make Kappa
diff --git a/core/KaSa_rep/frontend/prepreprocess.ml b/core/KaSa_rep/frontend/prepreprocess.ml
index d9b20cf3c..de09d0174 100644
--- a/core/KaSa_rep/frontend/prepreprocess.ml
+++ b/core/KaSa_rep/frontend/prepreprocess.ml
@@ -257,6 +257,7 @@ let translate_counter_test test =
   | Ast.CEQ i -> Ckappa_sig.CEQ i
   | Ast.CGTE i -> Ckappa_sig.CGTE i
   | Ast.CVAR x -> Ckappa_sig.CVAR x
+  | Ast.CLTE _i -> failwith "CLTE not yet implemented" (* TODO *)
 
 let fst_opt a_opt =
   match a_opt with
diff --git a/core/dataStructures/loc.ml b/core/dataStructures/loc.ml
index 1a43de468..f31ed9407 100644
--- a/core/dataStructures/loc.ml
+++ b/core/dataStructures/loc.ml
@@ -12,6 +12,8 @@ type 'a annoted = 'a * t
 
 let v (v, _) = v
 let get_annot (_, annot) = annot
+let copy_annot (_, loc) a = a, loc
+let map_annot f (a, loc) = f a, loc
 
 let of_pos start_location end_location =
   let () =
diff --git a/core/dataStructures/loc.mli b/core/dataStructures/loc.mli
index e0d41f1af..c147c0469 100644
--- a/core/dataStructures/loc.mli
+++ b/core/dataStructures/loc.mli
@@ -19,6 +19,12 @@ val v : 'a annoted -> 'a
 val get_annot : 'a annoted -> t
 (** Extract annotation from Loc.annoted *)
 
+val copy_annot : 'b annoted -> 'a -> 'a annoted
+(** Create annoted variable with same annotation as existing variable *)
+
+val map_annot : ('a -> 'b) -> 'a annoted -> 'b annoted
+(** Apply operation on variable and keep annotation *)
+
 val of_pos : Lexing.position -> Lexing.position -> t
 val dummy : t
 val annot_with_dummy : 'a -> 'a annoted
diff --git a/core/grammar/ast.ml b/core/grammar/ast.ml
index cb4e8677c..bdb032a33 100644
--- a/core/grammar/ast.ml
+++ b/core/grammar/ast.ml
@@ -24,20 +24,19 @@ type port = {
 }
 
 (* TODO change name, CVAR is not a test? *)
+(* TODO discriminate between counter definition and counter test ? *)
+(* TODO: change this to CTYPE = CTEST (CTESTTYPE * int) | CVAR string? *)
 
-(** What test is done by the counter expression
- * - CEQ: If counter value is equal to the specified value
- * - CGTE: If counter value is greater or equal to the specified value
- * - CVAR: Not a test, but defines a variable to be used in the rule rates *)
-type counter_test = CEQ of int | CGTE of int | CVAR of string
+type counter_test = CEQ of int | CGTE of int | CLTE of int | CVAR of string
 
 type counter = {
   counter_name: string Loc.annoted;
   counter_test: counter_test Loc.annoted option;
-      (** In a rule: what test is done, in an agent declaration: the initial value *)
+      (** In a rule: what test is done, in an agent declaration: the min value, in an init declaration: the init value, None if absent *)
   counter_delta: int Loc.annoted;
-      (** In a rule: change in counter value, in an agent declaration: max value of the counter *)
+      (** In a rule: change in counter value, in an agent declaration: max value of the counter, 0 if absent *)
 }
+(** Counter syntax from AST, present in 3 contexts with different meanings: agent definition, species init declaration, rule *)
 
 type site = Port of port | Counter of counter
 type agent_mod = NoMod | Erase | Create
@@ -46,6 +45,7 @@ type agent =
   | Present of string Loc.annoted * site list * agent_mod
   | Absent of Loc.t
 
+(* TODO: document why list list *)
 type mixture = agent list list
 
 type edit_notation = {
@@ -249,6 +249,7 @@ let print_ast_port f p =
 let print_counter_test f = function
   | CEQ x, _ -> Format.fprintf f "=%i" x
   | CGTE x, _ -> Format.fprintf f ">=%i" x
+  | CLTE x, _ -> Format.fprintf f "<=%i" x
   | CVAR x, _ -> Format.fprintf f "=%s" x
 
 let print_counter_delta test f (delta, _) =
@@ -284,6 +285,7 @@ let string_option_annoted_of_json filenames =
 let counter_test_to_json = function
   | CEQ x -> `Assoc [ "test", `String "eq"; "val", `Int x ]
   | CGTE x -> `Assoc [ "test", `String "gte"; "val", `Int x ]
+  | CLTE x -> `Assoc [ "test", `String "lte"; "val", `Int x ]
   | CVAR x -> `Assoc [ "test", `String "eq"; "val", `String x ]
 
 let counter_test_of_json = function
@@ -293,6 +295,9 @@ let counter_test_of_json = function
   | `Assoc [ ("val", `Int x); ("test", `String "gte") ]
   | `Assoc [ ("test", `String "gte"); ("val", `Int x) ] ->
     CGTE x
+  | `Assoc [ ("val", `Int x); ("test", `String "gle") ]
+  | `Assoc [ ("test", `String "gle"); ("val", `Int x) ] ->
+    CLTE x
   | `Assoc [ ("test", `String "eq"); ("val", `String x) ]
   | `Assoc [ ("val", `String x); ("test", `String "eq") ] ->
     CVAR x
diff --git a/core/grammar/ast.mli b/core/grammar/ast.mli
index 17dfe6663..f6358a70a 100644
--- a/core/grammar/ast.mli
+++ b/core/grammar/ast.mli
@@ -22,7 +22,12 @@ type port = {
 }
 (** Describe a port from an agent. [_int] references the internal state of the port, [_link], the possible links that can be made to this port, [_mod] to the changes in a rule that would be made to the state, used only in edit_notation  *)
 
-type counter_test = CEQ of int | CGTE of int | CVAR of string
+(** What test is done by the counter expression
+ * - CEQ: If counter value is equal to the specified value
+ * - CGTE: If counter value is greater or equal to the specified value
+ * - CLTE: If counter value is less or equal to the specified value
+ * - CVAR: Not a test, but defines a variable to be used in the rule rates *)
+type counter_test = CEQ of int | CGTE of int | CLTE of int | CVAR of string
 
 type counter = {
   counter_name: string Loc.annoted;
diff --git a/core/grammar/counters_compiler.ml b/core/grammar/counters_compiler.ml
index bafc63bf4..81253db9b 100644
--- a/core/grammar/counters_compiler.ml
+++ b/core/grammar/counters_compiler.ml
@@ -218,7 +218,8 @@ let split_cvar_counter_in_rules_per_value (var_name : string) (annot : Loc.t)
   let max_value : int = Loc.v counter_def.counter_delta in
   let min_value : int =
     match counter_def.counter_test with
-    | None | Some (Ast.CGTE _, _) | Some (Ast.CVAR _, _) ->
+    | None | Some (Ast.CGTE _, _) | Some (Ast.CLTE _, _) | Some (Ast.CVAR _, _)
+      ->
       raise
         (ExceptionDefn.Malformed_Decl
            ( "Invalid counter signature - have to specify min bound",
@@ -275,6 +276,8 @@ let split_counter_variables_into_separate_rules ~warning rules signatures =
             (ExceptionDefn.Malformed_Decl
                ( "Counter " ^ Loc.v c.counter_name ^ " becomes negative",
                  Loc.get_annot c.counter_name ))
+      | Some (Ast.CLTE _value, _annot) ->
+        failwith "not implemented" (* TODO NOW *)
       | Some (Ast.CGTE value, annot) ->
         if value + delta < 0 then
           raise
@@ -557,7 +560,7 @@ let rec add_incr (i : int) (first_link : int) (last_link : int) (delta : int)
   )
 
 let rec link_incr (sigs : Signature.s) (i : int) (nb : int)
-    (ag_info : (int * int) * bool) (equal : bool) (lnk : int) (loc : Loc.t)
+    (ag_info : (int * int) * bool) (equal : bool) (link : int) (loc : Loc.t)
     (delta : int) : LKappa.rule_mixture =
   if i = nb then
     []
@@ -565,38 +568,73 @@ let rec link_incr (sigs : Signature.s) (i : int) (nb : int)
     let is_first = i = 0 in
     let is_last = i = nb - 1 in
     let ra_agent =
-      make_counter_agent sigs (is_first, ag_info) (is_last, equal) (lnk + i)
-        (lnk + i + 1)
+      make_counter_agent sigs (is_first, ag_info) (is_last, equal) (link + i)
+        (link + i + 1)
         loc (delta > 0)
     in
-    ra_agent :: link_incr sigs (i + 1) nb ag_info equal lnk loc delta
+    ra_agent :: link_incr sigs (i + 1) nb ag_info equal link loc delta
   )
 
 let rec erase_incr (sigs : Signature.s) (i : int) (incrs : LKappa.rule_mixture)
-    (delta : int) (lnk : int) : LKappa.rule_mixture =
+    (delta : int) (link : int) : LKappa.rule_mixture =
   let counter_agent_info = Signature.get_counter_agent_info sigs in
   let port_b = fst counter_agent_info.ports in
   match incrs with
   | incr :: incr_s ->
     if i = abs delta then (
       let before, _ = incr.LKappa.ra_ports.(port_b) in
-      incr.LKappa.ra_ports.(port_b) <- before, LKappa.Linked lnk;
+      incr.LKappa.ra_ports.(port_b) <- before, LKappa.Linked link;
       incr :: incr_s
     ) else (
       Array.iteri
         (fun i (a, _) -> incr.LKappa.ra_ports.(i) <- a, LKappa.Erased)
         incr.LKappa.ra_ports;
       let rule_agent = { incr with LKappa.ra_erased = true } in
-      rule_agent :: erase_incr sigs (i + 1) incr_s delta lnk
+      rule_agent :: erase_incr sigs (i + 1) incr_s delta link
     )
   | [] -> []
 
+(** Returns mixtures for agent with site changed from counter to port, as well as new [link_nb] after previous additions
+ * Used by [compile_counter_in_rule_agent]*)
 let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
-    (p_id : int) ((delta, loc_delta) : int Loc.annoted) (loc : Loc.t)
-    (equal : bool) (test : int) (start_link_nb : int) :
-    LKappa.rule_mixture * Raw_mixture.t =
+    (p_id : int) (counter : Ast.counter) (start_link_nb : int) :
+    (LKappa.rule_mixture * Raw_mixture.t) * int =
+  (* Returns positive part of value *)
+  let positive_part (i : int) : int =
+    if i < 0 then
+      0
+    else
+      i
+  in
+
+  let loc : Loc.t = Loc.get_annot counter.Ast.counter_name in
+  let (delta, loc_delta) : int * Loc.t = counter.Ast.counter_delta in
+  let counter_test : Ast.counter_test Loc.annoted =
+    Option_util.unsome_or_raise
+      ~excep:
+        (ExceptionDefn.Internal_Error
+           ( "Counter "
+             ^ Loc.v counter.Ast.counter_name
+             ^ " should have a test by now",
+             loc ))
+      counter.Ast.counter_test
+  in
+  let (test, equal) : int * bool =
+    match Loc.v counter_test with
+    | Ast.CVAR _ ->
+      raise
+        (ExceptionDefn.Internal_Error
+           ( "Counter "
+             ^ Loc.v counter.Ast.counter_name
+             ^ " defines a variable, which should have been replaced by CEQ \
+                conditions after rule splitting",
+             Loc.get_annot counter_test ))
+    | Ast.CEQ j -> j, true
+    | Ast.CGTE j -> j, false
+    | Ast.CLTE _j -> failwith "not implemented" (* TODO now *)
+  in
   let start_link_for_created : int = start_link_nb + test + 1 in
-  let lnk_for_erased : int = start_link_nb + abs delta in
+  let link_for_erased : int = start_link_nb + abs delta in
   let ag_info : (int * int) * bool =
     (p_id, ra.LKappa.ra_type), ra.LKappa.ra_erased
   in
@@ -606,7 +644,7 @@ let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
   in
   let adjust_delta : LKappa.rule_mixture =
     if delta < 0 then
-      erase_incr sigs 0 test_incr delta lnk_for_erased
+      erase_incr sigs 0 test_incr delta link_for_erased
     else
       test_incr
   in
@@ -628,14 +666,16 @@ let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
     else if delta > 0 then
       LKappa.Linked start_link_for_created
     else
-      LKappa.Linked lnk_for_erased
+      LKappa.Linked link_for_erased
   in
   let counter_agent_info = Signature.get_counter_agent_info sigs in
   let port_b : int = fst counter_agent_info.ports in
   ra.LKappa.ra_ports.(p_id) <-
     ( (LKappa.LNK_VALUE (start_link_nb, (port_b, counter_agent_info.id)), loc),
       switch );
-  adjust_delta, created
+  let new_link_nb : int = start_link_nb + 1 + test + positive_part delta in
+
+  (adjust_delta, created), new_link_nb
 
 (** Compiles the counter precondition in a left hand side mixture of a rule into a mixture which tests dummy positions
  * rule_agent_ - agent with counters in a rule
@@ -646,52 +686,16 @@ let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
 let compile_counter_in_rule_agent (sigs : Signature.s)
     (rule_agent_ : LKappa.rule_agent with_agent_counters) (lnk_nb : int) :
     LKappa.rule_mixture * Raw_mixture.t * int =
-  (* Returns positive part of value *)
-  let positive_part (i : int) : int =
-    if i < 0 then
-      0
-    else
-      i
-  in
-
   let (incrs, lnk_nb') : (LKappa.rule_mixture * Raw_mixture.t) list * int =
     Tools.array_fold_lefti
       (fun id (acc_incrs, lnk_nb) -> function
         | None -> acc_incrs, lnk_nb
         | Some (counter, _) ->
-          let loc = Loc.get_annot counter.Ast.counter_name in
-          let test =
-            Option_util.unsome_or_raise
-              ~excep:
-                (ExceptionDefn.Internal_Error
-                   ( "Counter "
-                     ^ Loc.v counter.Ast.counter_name
-                     ^ " should have a test by now",
-                     loc ))
-              counter.Ast.counter_test
+          let new_incrs, new_lnk_nb =
+            counter_becomes_port sigs rule_agent_.agent id counter lnk_nb
           in
-          let delta = counter.Ast.counter_delta in
-          (match Loc.v test with
-          | Ast.CEQ j ->
-            ( counter_becomes_port sigs rule_agent_.agent id delta loc true j
-                lnk_nb
-              :: acc_incrs,
-              lnk_nb + 1 + j + positive_part (Loc.v delta) )
-            (* JF: link ids were colliding after counter decrementations -> I do not think that we should add delta when negative *)
-          | Ast.CGTE j ->
-            ( counter_becomes_port sigs rule_agent_.agent id delta loc false j
-                lnk_nb
-              :: acc_incrs,
-              lnk_nb + 1 + j + positive_part (Loc.v delta) )
-            (* JF: link ids were colliding after counter decrementations -> I do not think that we should add delta when negative *)
-          | Ast.CVAR _ ->
-            raise
-              (ExceptionDefn.Internal_Error
-                 ( "Counter "
-                   ^ Loc.v counter.Ast.counter_name
-                   ^ " defines a variable, which should have been replaced by \
-                      CEQ conditions after rule splitting",
-                   Loc.get_annot test ))))
+          new_incrs :: acc_incrs, new_lnk_nb
+        (* JF: link ids were colliding after counter decrementations -> I do not think that we should add delta when negative *))
       ([], lnk_nb) rule_agent_.counters
   in
   let (als, bls) : LKappa.rule_mixture * Raw_mixture.t =
@@ -720,19 +724,19 @@ let compile_counter_in_raw_agent (sigs : Signature.s)
             agent_name c.Ast.counter_name
         | Some (test, _) ->
           (match test with
-          | Ast.CEQ j ->
-            let p = Raw_mixture.VAL lnk_nb in
-            let () = ports.(p_id) <- p in
-            let incrs = add_incr 0 lnk_nb (lnk_nb + j) (j + 1) true sigs in
-            acc @ incrs, lnk_nb + j + 1
-          | Ast.CGTE _ | Ast.CVAR _ ->
+          | Ast.CGTE _ | Ast.CLTE _ | Ast.CVAR _ ->
             let agent_name =
               Format.asprintf "@[%a@]"
                 (Signature.print_agent sigs)
                 raw_agent.Raw_mixture.a_type
             in
             LKappa.raise_not_enough_specified ~status:"counter" ~side:"left"
-              agent_name c.Ast.counter_name)))
+              agent_name c.Ast.counter_name
+          | Ast.CEQ j ->
+            let p = Raw_mixture.VAL lnk_nb in
+            let () = ports.(p_id) <- p in
+            let incrs = add_incr 0 lnk_nb (lnk_nb + j) (j + 1) true sigs in
+            acc @ incrs, lnk_nb + j + 1)))
     ([], lnk_nb) raw_agent_.counters
 
 let raw_agent_has_counters (ag_ : 'a with_agent_counters) : bool =
diff --git a/core/grammar/kappaParser.mly b/core/grammar/kappaParser.mly
index ae798518c..c370ee69b 100644
--- a/core/grammar/kappaParser.mly
+++ b/core/grammar/kappaParser.mly
@@ -448,6 +448,7 @@ interface_expression:
 counter_test:
    | TYPE INT { Some (Ast.CEQ $2,rhs_pos 2)}
    | TYPE GREATER INT { Some (Ast.CGTE $3,rhs_pos 3)}
+   | TYPE SMALLER INT { Some (Ast.CLTE $3,rhs_pos 3)}
    | TYPE ID { Some (Ast.CVAR $2,rhs_pos 2)}
 
 port_expression:
diff --git a/core/grammar/kparser4.mly b/core/grammar/kparser4.mly
index d3ea9a589..3bed553a1 100644
--- a/core/grammar/kparser4.mly
+++ b/core/grammar/kparser4.mly
@@ -129,6 +129,7 @@ counter_modif:
 counter_test:
   | EQUAL annoted INT { (Ast.CEQ $3,rhs_pos 3) }
   | GREATER annoted EQUAL annoted INT { (Ast.CGTE $5,rhs_pos 5) }
+  | SMALLER annoted EQUAL annoted INT { (Ast.CLTE $5,rhs_pos 5) }
   | EQUAL annoted ID { (Ast.CVAR $3,rhs_pos 3) }
   ;
 
diff --git a/core/grammar/lKappa_compiler.ml b/core/grammar/lKappa_compiler.ml
index f9736a99d..f6631c926 100644
--- a/core/grammar/lKappa_compiler.ml
+++ b/core/grammar/lKappa_compiler.ml
@@ -1637,7 +1637,7 @@ let prepare_agent_sig ~(sites : Ast.site list) :
             :: acc_site_sigs,
             acc_counter_names )
         | Counter c ->
-          (* Here, only CEQ tests are accepted *)
+          (* We are reading here a signature, only CEQ tests are accepted *)
           (match c.counter_test with
           | None ->
             let n, pos = c.counter_name in
@@ -1654,6 +1654,10 @@ let prepare_agent_sig ~(sites : Ast.site list) :
               raise
                 (ExceptionDefn.Internal_Error
                    ("Counter should not have >= in signature", pos))
+            | CLTE _ ->
+              raise
+                (ExceptionDefn.Internal_Error
+                   ("Counter should not have <= in signature", pos))
             | CEQ j ->
               ( ( c.counter_name,
                   {
@@ -1856,8 +1860,358 @@ type ast_compiled_data = {
      * (syntactic sugar on mixture are not) *)
 }
 
+(** 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].
+ * Each delta [+ delta] is translated into a [- delta] *)
+let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) =
+  let counter_fold (f : 'a list -> string -> Ast.counter -> 'a list) : 'a list =
+    List.fold_left
+      (fun acc1 rule_def ->
+        let rule : Ast.rule = rule_def |> snd |> Loc.v in
+        match rule.rewrite with
+        | Ast.Edit _ -> acc1 (* no counter test allowed in edit rule *)
+        | Ast.Arrow content ->
+          List.fold_left
+            (fun acc2 agent_list ->
+              List.fold_left
+                (fun acc3 agent ->
+                  match agent with
+                  | Ast.Absent _ -> acc3
+                  | Ast.Present (agent_name, site_list, _) ->
+                    List.fold_left
+                      (fun acc4 site ->
+                        match site with
+                        | Ast.Port _ -> acc4
+                        | Counter counter -> f acc4 (Loc.v agent_name) counter)
+                      acc3 site_list)
+                acc2 agent_list)
+            acc1 content.lhs)
+      [] 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
+          raise
+            (ExceptionDefn.Malformed_Decl
+               ( "cannot end counter name by \"" ^ 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
+        | Some (Ast.CLTE _) ->
+          if
+            List.exists
+              (fun (agent_name2, counter_name2, _) ->
+                String.equal agent_name agent_name2
+                && String.equal counter_name counter_name2)
+              acc
+          then
+            acc
+          else
+            (agent_name, counter_name, ref 0) :: acc
+        | Some (Ast.CEQ _) | Some (Ast.CGTE _) | Some (Ast.CVAR _) | None -> acc)
+  in
+
+  (* Create opposite counters that have the same tests *)
+  let signatures : Ast.agent list =
+    List.map
+      (fun agent ->
+        match agent with
+        | Ast.Absent _ -> agent
+        | Present (agent_name_, site_list, agent_mod) ->
+          let agent_name = Loc.v agent_name_ in
+          let counters_with_clte_tests_from_agent :
+              (string * string * int ref) list =
+            List.filter
+              (fun (agent_name_counter, _, _) ->
+                agent_name = agent_name_counter)
+              counters_with_clte_tests
+          in
+          let new_counter_sites : Ast.site list =
+            List.fold_left
+              (fun acc (_, counter_name, sum_bounds_ref) ->
+                (* Find counter to invert *)
+                let counter_orig : Ast.counter =
+                  List.find_map
+                    (fun site ->
+                      match site with
+                      | Ast.Port _ -> None
+                      | Counter counter ->
+                        if Loc.v counter.counter_name = counter_name then
+                          Some counter
+                        else
+                          None)
+                    site_list
+                  |> Option_util.unsome_or_raise
+                in
+
+                (* Make inverted counter declaration *)
+                let counter_name : string Loc.annoted =
+                  Loc.map_annot
+                    (fun name -> inverted_counter_name name)
+                    counter_orig.counter_name
+                in
+                let counter_test = counter_orig.counter_test in
+                let counter_delta = counter_orig.counter_delta in
+
+                (* Write in sum_bounds_ref the sum of the counter bounds above *)
+                let inf_bound =
+                  match
+                    counter_test |> Option_util.unsome_or_raise |> Loc.v
+                  with
+                  | CGTE _ | CLTE _ | CVAR _ ->
+                    raise
+                      (ExceptionDefn.Malformed_Decl
+                         ( "Counter should have CEQ test value in signature \
+                            statement",
+                           Loc.get_annot counter_name ))
+                  | CEQ value -> value
+                in
+                let sup_bound = Loc.v counter_delta in
+                sum_bounds_ref := inf_bound + sup_bound;
+
+                Ast.Counter { counter_name; counter_test; counter_delta } :: acc)
+              [] counters_with_clte_tests_from_agent
+          in
+
+          Ast.Present (agent_name_, site_list @ new_counter_sites, agent_mod))
+      ast_compil.signatures
+  in
+
+  (* In rules, we need to replace the counter tests and the counter modifications *)
+  let replace_counter_by_invert (mix : Ast.mixture) : Ast.mixture =
+    List.map
+      (fun agent_list ->
+        List.map
+          (fun agent ->
+            match agent with
+            | Ast.Absent _ -> agent
+            | Present (agent_name_, site_list, agent_mod) ->
+              let agent_name : string = Loc.v agent_name_ in
+              let counters_with_clte_tests_from_agent :
+                  (string * string * int ref) list =
+                List.filter
+                  (fun (agent_name_counter, _, _) ->
+                    agent_name = agent_name_counter)
+                  counters_with_clte_tests
+              in
+              (* Add delta to counter as opposite deltas to counter_delta *)
+              let (added_sites, site_list_with_opposite_deltas) :
+                  Ast.site list * Ast.site list =
+                List.fold_left_map
+                  (fun acc site ->
+                    match site with
+                    | Ast.Port _ -> acc, site
+                    | Counter counter ->
+                      (match
+                         List.find_opt
+                           (fun (_, name, _) ->
+                             String.equal (Loc.v counter.counter_name) name)
+                           counters_with_clte_tests_from_agent
+                       with
+                      | None -> acc, site
+                      | Some (_, _, sum_bounds_ref) ->
+                        (* As we know that this counter uses a CLTE test, We introduce the inverted counter *)
+                        (* [clte_value_or_none] discriminates the case where this site in this expression has a CLTE test *)
+                        let clte_value_or_none =
+                          match counter.counter_test with
+                          | None -> None
+                          | Some test ->
+                            (match Loc.v test with
+                            | Ast.CEQ _ | CGTE _ | CVAR _ -> None
+                            | Ast.CLTE value -> Some value)
+                        in
+                        (match clte_value_or_none with
+                        | None ->
+                          (* If there is a test, it doesn't need inversion: we add inverted counter without test *)
+                          if Loc.v counter.counter_delta == 0 then
+                            acc, site
+                          else (
+                            (* If the counter value is changing, we need to add it to the inverted counter *)
+                            let inverted_counter_site =
+                              Ast.Counter
+                                {
+                                  counter_name =
+                                    Loc.map_annot inverted_counter_name
+                                      counter.counter_name;
+                                  counter_test = None;
+                                  counter_delta =
+                                    Loc.map_annot
+                                      (fun delta -> -delta)
+                                      counter.counter_delta;
+                                }
+                            in
+                            inverted_counter_site :: acc, site
+                          )
+                        | Some value ->
+                          (* The test is CLTE, we invert it *)
+
+                          (* Site with inverted counter with CGTE test instead of CLTE test *)
+                          let new_site =
+                            Ast.Counter
+                              {
+                                counter_name =
+                                  Loc.map_annot inverted_counter_name
+                                    counter.counter_name;
+                                counter_test =
+                                  Some
+                                    (Ast.CGTE (!sum_bounds_ref - value)
+                                    |> Loc.copy_annot
+                                         (Option_util.unsome_or_raise
+                                            counter.counter_test));
+                                counter_delta =
+                                  Loc.map_annot
+                                    (fun delta -> -delta)
+                                    counter.counter_delta;
+                              }
+                          in
+                          if Loc.v counter.counter_delta == 0 then
+                            acc, new_site
+                          else (
+                            (* If the counter value is changing, we need to add it to the original counter too *)
+                            let original_counter_site =
+                              Ast.Counter { counter with counter_test = None }
+                            in
+                            original_counter_site :: acc, new_site
+                          ))))
+                  [] site_list
+              in
+              let new_site_list : Ast.site list =
+                site_list_with_opposite_deltas @ added_sites
+              in
+              Ast.Present (agent_name_, new_site_list, agent_mod))
+          agent_list)
+      mix
+  in
+  let rules : (string Loc.annoted option * Ast.rule Loc.annoted) list =
+    List.map
+      (fun rule_def ->
+        ( fst rule_def,
+          Loc.map_annot
+            (fun (rule : Ast.rule) ->
+              let rewrite =
+                match rule.rewrite with
+                | Edit content ->
+                  Ast.Edit
+                    { content with mix = replace_counter_by_invert content.mix }
+                | Arrow content ->
+                  Arrow
+                    {
+                      content with
+                      lhs = replace_counter_by_invert content.lhs;
+                      rhs = replace_counter_by_invert content.rhs;
+                    }
+              in
+              { rule with rewrite })
+            (snd rule_def) ))
+      ast_compil.rules
+  in
+
+  let add_inverted_counter_to_init_mixture (mix : Ast.mixture) : Ast.mixture =
+    List.map
+      (fun agent_list ->
+        List.map
+          (fun agent ->
+            match agent with
+            | Ast.Absent _ -> agent
+            | Present (agent_name_, site_list, agent_mod) ->
+              let agent_name : string = Loc.v agent_name_ in
+              let counters_with_clte_tests_from_agent :
+                  (string * string * int ref) list =
+                List.filter
+                  (fun (agent_name_counter, _, _) ->
+                    agent_name = agent_name_counter)
+                  counters_with_clte_tests
+              in
+              (* Add delta to counter as opposite deltas to counter_delta *)
+              let added_sites : Ast.site list =
+                List.fold_left
+                  (fun acc site ->
+                    match site with
+                    | Ast.Port _ -> acc
+                    | Counter counter ->
+                      (match
+                         List.find_opt
+                           (fun (_, name, _) ->
+                             String.equal (Loc.v counter.counter_name) name)
+                           counters_with_clte_tests_from_agent
+                       with
+                      | None -> acc
+                      | Some (_, _, sum_bounds_ref) ->
+                        (* As we know that this counter uses a CLTE test, We introduce the inverted counter *)
+                        (match counter.counter_test with
+                        | None ->
+                          raise
+                            (ExceptionDefn.Malformed_Decl
+                               ( "Counter should have CEQ test value in init \
+                                  statement",
+                                 Loc.get_annot counter.counter_name ))
+                        | Some test ->
+                          (match Loc.v test with
+                          | Ast.CGTE _ | CLTE _ | CVAR _ ->
+                            raise
+                              (ExceptionDefn.Malformed_Decl
+                                 ( "Counter should have CEQ test value in init \
+                                    statement",
+                                   Loc.get_annot test ))
+                          | Ast.CEQ value ->
+                            if Loc.v counter.counter_delta <> 0 then
+                              raise
+                                (ExceptionDefn.Malformed_Decl
+                                   ( "Counter delta should be 0 in init \
+                                      statement",
+                                     Loc.get_annot test ))
+                            else
+                              Ast.Counter
+                                {
+                                  counter_name =
+                                    Loc.map_annot inverted_counter_name
+                                      counter.counter_name;
+                                  counter_test =
+                                    Some
+                                      (Loc.copy_annot test
+                                         (Ast.CEQ (!sum_bounds_ref - value)));
+                                  counter_delta =
+                                    counter.counter_delta
+                                    (* 0 with annot as tested above *);
+                                }
+                              :: acc))))
+                  [] site_list
+              in
+              let new_site_list : Ast.site list = site_list @ added_sites in
+              Ast.Present (agent_name_, new_site_list, agent_mod))
+          agent_list)
+      mix
+  in
+  let init : (Ast.mixture, Ast.mixture, string) Ast.init_statement list =
+    List.map
+      (fun (quantity_alg_expr, init_kind) ->
+        ( quantity_alg_expr,
+          match init_kind with
+          | Ast.INIT_TOK _ -> init_kind
+          | INIT_MIX mix_ ->
+            INIT_MIX (Loc.map_annot add_inverted_counter_to_init_mixture mix_) ))
+      ast_compil.init
+  in
+
+  { ast_compil with signatures; rules; init }
+
 let compil_of_ast ~warning ~debug_mode ~syntax_version ~var_overwrite ast_compil
     =
+  (* TODO test this *)
+  (* Translate CLTE tests in ast_compil into CGTE tests *)
+  let ast_compil = translate_clte_into_cgte ast_compil in
+
   let has_counters = Counters_compiler.has_counters ast_compil in
   let agent_sig_is_implicit =
     ast_compil.Ast.signatures = [] && ast_compil.Ast.tokens = []
diff --git a/core/term/lKappa.ml b/core/term/lKappa.ml
index 4e8f766ca..ab2fab47a 100644
--- a/core/term/lKappa.ml
+++ b/core/term/lKappa.ml
@@ -192,18 +192,16 @@ let print_rule_intf ~noCounters sigs ~show_erased ~ltypes ag_ty f
                  Mods.DynArray.get counters.Raw_mixture.rank root
                in
                if is_counter' && not noCounters then (
-                 let () =
-                   Format.fprintf f "%t%a{%a%a}"
-                     (if empty then
-                        Pp.empty
-                      else
-                        Pp.space)
-                     (Signature.print_site sigs ag_ty)
-                     i print_counter_test
-                     (c - 1, eq)
-                     (print_counter_delta created_counters j)
-                     switch
-                 in
+                 Format.fprintf f "%t%a{%a%a}"
+                   (if empty then
+                      Pp.empty
+                    else
+                      Pp.space)
+                   (Signature.print_site sigs ag_ty)
+                   i print_counter_test
+                   (c - 1, eq)
+                   (print_counter_delta created_counters j)
+                   switch;
                  true
                ) else
                  false
diff --git a/core/term/raw_mixture.mli b/core/term/raw_mixture.mli
index 16b1f609d..288ea813a 100644
--- a/core/term/raw_mixture.mli
+++ b/core/term/raw_mixture.mli
@@ -27,6 +27,7 @@ val print :
 val to_json : t -> Yojson.Basic.t
 val of_json : Yojson.Basic.t -> t
 
+(* TODO Change this to have equal bool as sum type *)
 type incr_t = {
   father: int Mods.DynArray.t;
   rank: (int * (bool * bool)) Mods.DynArray.t;
diff --git a/tests/integration/compiler/counters_smaller_than/README b/tests/integration/compiler/counters_smaller_than/README
new file mode 100644
index 000000000..3e10065cf
--- /dev/null
+++ b/tests/integration/compiler/counters_smaller_than/README
@@ -0,0 +1,2 @@
+#Command-line:
+"${KAPPABIN}"KaSim -l 1 counters_smaller_than.ka -seed 23014 -d output -syntax 4 || true
diff --git a/tests/integration/compiler/counters_smaller_than/counters_smaller_than.ka b/tests/integration/compiler/counters_smaller_than/counters_smaller_than.ka
new file mode 100644
index 000000000..1b2a9d07c
--- /dev/null
+++ b/tests/integration/compiler/counters_smaller_than/counters_smaller_than.ka
@@ -0,0 +1,21 @@
+%agent: A(c{=0 / += 7})
+%agent: B()
+
+'rule_a' A(c{<=2}) -> A(c{+=1}) @ 1
+'rule_b' A(c{>=5}) -> A(c{-=1}) @ 1
+'rule_c' A(c{=3}) -> A(c{+=1}) @ 1
+'rule_aa' A(c{<=1}),. -> ., B() @ 0.2
+
+%init: 10 A(c{=0})
+%init: 10 A(c{=7})
+
+// %obs: 'A' |A()|
+%obs: 'B' |B()|
+%obs: 'A0' |A(c{=0})|
+%obs: 'A1' |A(c{=1})|
+%obs: 'A2' |A(c{=2})|
+%obs: 'A3' |A(c{=3})|
+%obs: 'A4' |A(c{=4})|
+%obs: 'A5' |A(c{=5})|
+%obs: 'A6' |A(c{=6})|
+%obs: 'A7' |A(c{=7})|
diff --git a/tests/integration/compiler/counters_smaller_than/output/LOG.ref b/tests/integration/compiler/counters_smaller_than/output/LOG.ref
new file mode 100644
index 000000000..2c9d6f0d4
--- /dev/null
+++ b/tests/integration/compiler/counters_smaller_than/output/LOG.ref
@@ -0,0 +1,19 @@
+Parsing counters_smaller_than.ka...
+done
++ simulation parameters
++ Sanity checks
++ Compiling...
++ Building initial simulation conditions...
+	 -variable declarations
+	 -rules
+	 -interventions
+	 -observables
+	 -update_domain construction
+	 28 (sub)observables 58 navigation steps
+	 -initial conditions
++ Building initial state (200 agents)
+Done
++ Command line to rerun is: 'KaSim' '-l' '1' 'counters_smaller_than.ka' '-seed' '23014' '-d' 'output' '-syntax' '4'
+______________________________________________________________________
+######################################################################
+Simulation ended
diff --git a/tests/integration/compiler/counters_smaller_than/output/data.csv.ref b/tests/integration/compiler/counters_smaller_than/output/data.csv.ref
new file mode 100644
index 000000000..4a807970b
--- /dev/null
+++ b/tests/integration/compiler/counters_smaller_than/output/data.csv.ref
@@ -0,0 +1,4 @@
+# Output of 'KaSim' '-l' '1' 'counters_smaller_than.ka' '-seed' '23014' '-d' 'output' '-syntax' '4'
+"[T]","B","A0","A1","A2","A3","A4","A5","A6","A7"
+0.,0,10,0,0,0,0,0,0,10
+1.,2,3,2,2,0,1,2,3,5
diff --git a/tests/integration/compiler/counters_smaller_than/output/error.log.ref b/tests/integration/compiler/counters_smaller_than/output/error.log.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/integration/compiler/counters_smaller_than/output/inputs.ka.ref b/tests/integration/compiler/counters_smaller_than/output/inputs.ka.ref
new file mode 100644
index 000000000..836df5b98
--- /dev/null
+++ b/tests/integration/compiler/counters_smaller_than/output/inputs.ka.ref
@@ -0,0 +1,44 @@
+%def: "seed" "23014"
+%def: "dumpIfDeadlocked" "true"
+%def: "maxConsecutiveClash" "3"
+%def: "progressBarSize" "70"
+%def: "progressBarSymbol" "#"
+%def: "plotPeriod" "1" "t.u."
+%def: "outputFileName" "data.csv"
+
+
+%agent: A(c{=0/+=7} c__inverted{=0/+=7})
+%agent: B()
+
+%var:/*0*/ 'B' |B()|
+%var:/*1*/ 'A0' |A(c{=0})|
+%var:/*2*/ 'A1' |A(c{=1})|
+%var:/*3*/ 'A2' |A(c{=2})|
+%var:/*4*/ 'A3' |A(c{=3})|
+%var:/*5*/ 'A4' |A(c{=4})|
+%var:/*6*/ 'A5' |A(c{=5})|
+%var:/*7*/ 'A6' |A(c{=6})|
+%var:/*8*/ 'A7' |A(c{=7})|
+%plot: [T]
+%plot: B
+%plot: A0
+%plot: A1
+%plot: A2
+%plot: A3
+%plot: A4
+%plot: A5
+%plot: A6
+%plot: A7
+
+'rule_a' A(c{>=0/+=1} c__inverted{>=5/+=-1}) @ 1
+'rule_b' A(c{>=5/+=-1} c__inverted{>=0/+=1}) @ 1
+'rule_c' A(c{=3/+=1} c__inverted{>=1/+=-1}) @ 1
+'rule_aa' A(c[#] c__inverted{>=6})-, B()+ @ 0.2
+
+/*0*/%mod: (|A(c__inverted{=8})| = 1) do $PRINTF ""; $PRINTF "Counter c__inverted of agent A reached maximum"; $STOP "counter_perturbation.ka"; repeat [false]
+/*1*/%mod: (|A(c{=8})| = 1) do $PRINTF ""; $PRINTF "Counter c of agent A reached maximum"; $STOP "counter_perturbation.ka"; repeat [false]
+
+%init: 10 A(c{=0} c__inverted{=7})
+%init: 10 A(c{=7} c__inverted{=0})
+
+%mod: [E] = 19 do $STOP;
diff --git a/tests/integration/compiler/site_mismatch/output/LOG.ref b/tests/integration/compiler/site_mismatch/output/LOG.ref
index 59227f230..28c6fc2ce 100644
--- a/tests/integration/compiler/site_mismatch/output/LOG.ref
+++ b/tests/integration/compiler/site_mismatch/output/LOG.ref
@@ -73,4 +73,4 @@ every agent may occur in the model
 ------------------------------------------------------------
 
 Some exceptions have been raised
-error: file_name: core/KaSa_rep/frontend/prepreprocess.ml; message: line 718, File "crash.ka", line 4, characters 5-69:: missaligned rule: the rule is ignored; exception:Exit
+error: file_name: core/KaSa_rep/frontend/prepreprocess.ml; message: line 719, File "crash.ka", line 4, characters 5-69:: missaligned rule: the rule is ignored; exception:Exit