Add > as syntactic sugar for >= in counters

core/KaSa_rep/frontend/prepreprocess.ml

@@ -256,6 +256,7 @@ let translate_counter_test test =
   match test with
   | Ast.CEQ i -> Ckappa_sig.CEQ i
   | Ast.CGTE i -> Ckappa_sig.CGTE i
+  | Ast.CGT i -> Ckappa_sig.CGTE (i+1)
   | Ast.CVAR x -> Ckappa_sig.CVAR x
   | Ast.CLTE _i -> failwith "CLTE not yet implemented" (* TODO *)
 

core/grammar/ast.ml

@@ -23,11 +23,7 @@ type port = {
   port_link_mod: int Loc.annoted option option;
 }
 
-(* 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? *)
-
-type counter_test = CEQ of int | CGTE of int | CLTE of int | CVAR of string
+type counter_test = CEQ of int | CGTE of int | CLTE of int  | CGT of int | CVAR of string
 
 type counter = {
   counter_name: string Loc.annoted;
@@ -249,6 +245,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
+  | CGT x, _ -> Format.fprintf f ">%i" x
   | CLTE x, _ -> Format.fprintf f "<=%i" x
   | CVAR x, _ -> Format.fprintf f "=%s" x
 
@@ -285,6 +282,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 ]
+  | CGT x -> `Assoc [ "test", `String "gt"; "val", `Int x ]
   | CLTE x -> `Assoc [ "test", `String "lte"; "val", `Int x ]
   | CVAR x -> `Assoc [ "test", `String "eq"; "val", `String x ]
 
@@ -295,6 +293,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 "gt" ]
+  | `Assoc [ "test", `String "gt"; "val", `Int x ] -> 
+     CGT x
   | `Assoc [ ("val", `Int x); ("test", `String "gle") ]
   | `Assoc [ ("test", `String "gle"); ("val", `Int x) ] ->
     CLTE x

core/grammar/ast.mli

@@ -27,7 +27,7 @@ type port = {
  * - 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_test = CEQ of int | CGTE of int | CGT of int | CLTE of int | CVAR of string
 
 type counter = {
   counter_name: string Loc.annoted;

core/grammar/counters_compiler.ml

@@ -209,7 +209,7 @@ let counters_signature s agents =
         | Ast.Counter c -> c :: acc
         | Ast.Port _ -> acc)
       [] sites'
-
+    
 (** [split_cvar_counter_in_rules_per_value var_name annot counter_delta counter_def] translates a counter CVAR whose value acts upon the rate expression into a rule per possible value, that are selected by a CEQ expression.
  * *)
 let split_cvar_counter_in_rules_per_value (var_name : string) (annot : Loc.t)
@@ -218,7 +218,7 @@ 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.CLTE _, _) | Some (Ast.CVAR _, _)
+    | None | Some (Ast.CGTE _, _) | Some (Ast.CGT _,_) | Some (Ast.CLTE _, _) | Some (Ast.CVAR _, _)
       ->
       raise
         (ExceptionDefn.Malformed_Decl
@@ -278,6 +278,9 @@ let split_counter_variables_into_separate_rules ~warning rules signatures =
                  Loc.get_annot c.counter_name ))
       | Some (Ast.CLTE _value, _annot) ->
         failwith "not implemented" (* TODO NOW *)
+      | Some (Ast.CGT _,pos) ->
+          raise (ExceptionDefn.Internal_Error
+            ("Counter "^(fst c.Ast.count_nme)^" should not have a > test by now", pos))
       | Some (Ast.CGTE value, annot) ->
         if value + delta < 0 then
           raise
@@ -471,6 +474,151 @@ let split_counter_variables_into_separate_rules ~warning ~debug_mode
   );
   { compil with Ast.rules }
 
+let with_counters c =
+  let with_counters_mix mix =
+    List.exists
+      (function
+        | Ast.Absent _ -> false
+        | Ast.Present (_,ls,_) ->
+        List.exists (function Ast.Counter _ -> true | Ast.Port _ -> false) ls)
+      mix in
+  with_counters_mix c.Ast.signatures
+
+let replace_greater_than c =
+  let process_mix =
+    let process_site = function
+      | Ast.Port _
+      | Ast.Counter Ast.{count_test = None; _}
+      | Ast.Counter Ast.{count_test = Some (CEQ _,_); _}
+      | Ast.Counter Ast.{count_test = Some (CVAR _,_); _}
+      | Ast.Counter Ast.{count_test = Some (CGTE _,_); _} as s -> s
+      | Ast.Counter Ast.{count_test = Some (CGT i,p); count_nme; count_delta} ->
+          Ast.Counter Ast.{count_nme; count_delta; count_test = Some (CGTE (i+1), p)}
+    in
+    let process_agent = function
+      | Ast.Absent _ as a -> a
+      | Ast.Present (n, ss, m) ->
+          Ast.Present (n, List.map process_site ss, m)
+    in
+    List.map (fun ags -> List.map process_agent ags)
+  in
+  let rec process_alg = function
+    | Alg_expr.STATE_ALG_OP _, _
+    | Alg_expr.ALG_VAR _, _
+    | Alg_expr.TOKEN_ID _, _
+    | Alg_expr.CONST _, _ as a -> a
+    | Alg_expr.BIN_ALG_OP (o, a1, a2), p ->
+        Alg_expr.BIN_ALG_OP (o, process_alg a1, process_alg a2), p
+    | Alg_expr.UN_ALG_OP (o, a), p ->
+        Alg_expr.UN_ALG_OP (o, process_alg a), p
+    | Alg_expr.IF (b, a1, a2), p ->
+        Alg_expr.IF (process_bool b, process_alg a1, process_alg a2), p
+    | Alg_expr.DIFF_TOKEN (a, id), p ->
+        Alg_expr.DIFF_TOKEN (process_alg a, id), p
+    | Alg_expr.KAPPA_INSTANCE m, p ->
+        Alg_expr.KAPPA_INSTANCE (process_mix m), p
+    | Alg_expr.DIFF_KAPPA_INSTANCE (a, m), p ->
+        Alg_expr.DIFF_KAPPA_INSTANCE (process_alg a, process_mix m), p
+  and process_bool = function
+    | Alg_expr.TRUE, _
+    | Alg_expr.FALSE, _ as b -> b
+    | Alg_expr.BIN_BOOL_OP (o, b1, b2), p ->
+        Alg_expr.BIN_BOOL_OP (o, process_bool b1, process_bool b2), p
+    | Alg_expr.UN_BOOL_OP (o, b), p ->
+        Alg_expr.UN_BOOL_OP (o, process_bool b), p
+    | Alg_expr.COMPARE_OP (o, a1, a2), p ->
+        Alg_expr.COMPARE_OP (o, process_alg a1, process_alg a2), p
+  in
+  let process_rule (r, l) =
+    let rewrite =
+      match r.Ast.rewrite with
+      | Ast.Edit e -> Ast.Edit Ast.{e with mix = process_mix e.mix}
+      | Ast.Arrow a -> Ast.Arrow Ast.{a with lhs = process_mix a.lhs}
+    in
+    let k_def = process_alg r.Ast.k_def in
+    let k_un =
+      match r.Ast.k_un with
+      | None -> None
+      | Some (alg, None) -> Some (process_alg alg, None)
+      | Some (alg1, Some alg2) -> Some (process_alg alg1, Some (process_alg alg2))
+    in
+    let k_op =
+      match r.Ast.k_op with
+      | None -> None
+      | Some alg -> Some (process_alg alg)
+    in
+    let k_op_un =
+      match r.Ast.k_op_un with
+      | None -> None
+      | Some (alg, None) -> Some (process_alg alg, None)
+      | Some (alg1, Some alg2) -> Some (process_alg alg1, Some (process_alg alg2))
+    in
+    (Ast.{r with rewrite; k_def; k_un; k_op; k_op_un}, l)
+  in
+
+  let process_rule_stmt (s, r) = s, process_rule r in
+  let process_variable_def (s, a) = s, process_alg a in
+  let process_init = function
+    | a, Ast.INIT_TOK t -> process_alg a, Ast.INIT_TOK t
+    | a, Ast.INIT_MIX m -> process_alg a, Ast.INIT_MIX m
+  in
+
+  let process_pexpr = function
+    | Primitives.Str_pexpr _ as e -> e
+    | Primitives.Alg_pexpr a -> Primitives.Alg_pexpr (process_alg a)
+  in
+  let process_pexprs = List.map process_pexpr in
+
+  let process_perturbation ((n, bool1, mods, bool2), l) =
+    let bool1 =
+      match bool1 with
+      | None -> None
+      | Some b -> Some (process_bool b)
+    in
+    let bool2 =
+      match bool2 with
+      | None -> None
+      | Some b -> Some (process_bool b)
+    in
+    let process_modif_expr = function
+      | Ast.PLOTENTRY | Ast.CFLOWLABEL _ | Ast.CFLOWMIX _ as e -> e
+      | Ast.APPLY (a, r) -> Ast.APPLY (process_alg a, process_rule r)
+      | Ast.UPDATE (p, a) -> Ast.UPDATE (p, process_alg a)
+      | Ast.STOP ps -> Ast.STOP (process_pexprs ps)
+      | Ast.SNAPSHOT (b, ps) -> Ast.SNAPSHOT (b, process_pexprs ps)
+      | Ast.PRINT (ps1, ps2) -> Ast.PRINT (process_pexprs ps1, process_pexprs ps2)
+      | Ast.DIN (k, ps) -> Ast.DIN (k, process_pexprs ps)
+      | Ast.DINOFF ps -> Ast.DINOFF (process_pexprs ps)
+      | Ast.SPECIES_OF (b, ps, p) -> Ast.SPECIES_OF (b, process_pexprs ps, p)
+    in
+    let mods = List.map process_modif_expr mods in
+    ((n, bool1, mods, bool2), l)
+  in
+
+  Ast.{c with
+     init = List.map process_init c.init;
+     observables = List.map process_alg c.observables;
+     variables = List.map process_variable_def c.variables;
+     perturbations = List.map process_perturbation c.perturbations;
+     rules = List.map process_rule_stmt c.rules;
+  }
+
+
+let compile ~warning ~debugMode c =
+  if (with_counters c) then
+    let c = replace_greater_than c in
+    let rules =
+      remove_variable_in_counters ~warning c.Ast.rules c.Ast.signatures in
+    let () =
+      if debugMode then
+        let () = Format.printf "@.ast rules@." in
+        List.iter (fun (s,(r,_)) ->
+            let label = match s with None -> "" | Some (l,_) -> l in
+            Format.printf "@.%s = %a" label Ast.print_ast_rule r)
+          rules in
+    ({c with Ast.rules},true)
+  else (c,false)
+
 let make_counter_agent sigs (is_first, (dst, ra_erased)) (is_last, equal) i j
     loc (created : bool) : LKappa.rule_agent =
   let counter_agent_info = Signature.get_counter_agent_info sigs in
@@ -630,6 +778,12 @@ let counter_becomes_port (sigs : Signature.s) (ra : LKappa.rule_agent)
                 conditions after rule splitting",
              Loc.get_annot counter_test ))
     | Ast.CEQ j -> j, true
+    | Ast.CGT j ->  
+       raise (ExceptionDefn.Internal_Error
+               ( "Counter "
+             ^ Loc.v counter.Ast.counter_name
+             ^ " should not have a > test by now", Loc.get_annot counter_test))
+
     | Ast.CGTE j -> j, false
     | Ast.CLTE _j -> failwith "not implemented" (* TODO now *)
   in
@@ -688,7 +842,7 @@ let compile_counter_in_rule_agent (sigs : Signature.s)
     LKappa.rule_mixture * Raw_mixture.t * int =
   let (incrs, lnk_nb') : (LKappa.rule_mixture * Raw_mixture.t) list * int =
     Tools.array_fold_lefti
-      (fun id (acc_incrs, lnk_nb) -> function
+    (fun id (acc_incrs, lnk_nb) -> function
         | None -> acc_incrs, lnk_nb
         | Some (counter, _) ->
           let new_incrs, new_lnk_nb =
@@ -702,6 +856,7 @@ let compile_counter_in_rule_agent (sigs : Signature.s)
     List.fold_left (fun (als, bls) (a, b) -> a @ als, b @ bls) ([], []) incrs
   in
   als, bls, lnk_nb'
+
 
 (** Compiles the counter value change in the right hand side of a rule into dummy chain changes *)
 let compile_counter_in_raw_agent (sigs : Signature.s)
@@ -751,9 +906,9 @@ let rule_agent_has_counters (rule_agent : LKappa.rule_agent)
  * both with counter information, and returns two mixtures for a new rule without counters, having compiled the counter logic inside the rule.
  *
  * - adds increment agents to the rule_agent mixture
-   - adds increment agents to the raw mixture
-   - links the agents in the mixture(lhs,rhs,mix) or in the raw mixture(created)
-     to the increments *)
+ * - adds increment agents to the raw mixture
+ * - links the agents in the mixture(lhs,rhs,mix) or in the raw mixture(created)
+ *   to the increments *)
 let compile_counter_in_rule (sigs : Signature.s)
     (mix : rule_mixture_with_agent_counters)
     (created : raw_mixture_with_agent_counters) :

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) }
+  | GREATER annot INT { (Ast.CGT $3,rhs_pos 3) }
   | SMALLER annoted EQUAL annoted INT { (Ast.CLTE $5,rhs_pos 5) }
   | EQUAL annoted ID { (Ast.CVAR $3,rhs_pos 3) }
   ;

core/grammar/lKappa_compiler.ml

@@ -1919,7 +1919,7 @@ let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) =
             acc
           else
             (agent_name, counter_name, ref 0) :: acc
-        | Some (Ast.CEQ _) | Some (Ast.CGTE _) | Some (Ast.CVAR _) | None -> acc)
+        | Some (Ast.CEQ _ | Ast.CGT _ | Ast.CGTE _ | Ast.CVAR _) | None -> acc)
   in
 
   (* Create opposite counters that have the same tests *)
@@ -1969,7 +1969,7 @@ let translate_clte_into_cgte (ast_compil : Ast.parsing_compil) =
                   match
                     counter_test |> Option_util.unsome_or_raise |> Loc.v
                   with
-                  | CGTE _ | CLTE _ | CVAR _ ->
+                  | CGT _ | CGTE _ | CLTE _ | CVAR _ ->
                     raise
                       (ExceptionDefn.Malformed_Decl
                          ( "Counter should have CEQ test value in signature \

tests/integration/compiler/counters_greater_than/README

@@ -0,0 +1 @@
+"${KAPPABIN}"KaSim -l 1 -seed 442310228 -d output counters_greater_than.ka -syntax 4 || true

tests/integration/compiler/counters_greater_than/counters_greater_than.ka

@@ -0,0 +1,13 @@
+%agent:	A(c{=0 / +=3})
+
+%init: 1 A(c{=0})
+%init: 1 A(c{=1})
+%init: 1 A(c{=2})
+
+'greater_than_edit' A(c{>0/+=1}) @ 1
+
+'greater_than_arrow' A(c{>0}) -> A(c{+=1}) @ 1
+
+%obs: A1 |A(c{=0})|
+%obs: A2 |A(c{>0})|
+%obs: A3 |A(c{>=0})|

tests/integration/compiler/counters_greater_than/output/LOG.ref

@@ -0,0 +1,21 @@
+Parsing counters_greater_than.ka...
+done
++ simulation parameters
++ Sanity checks
++ Compiling...
++ Building initial simulation conditions...
+	 -variable declarations
+	 -rules
+	 -interventions
+	 -observables
+	 -update_domain construction
+	 9 (sub)observables 5 navigation steps
+	 -initial conditions
++ Building initial state (9 agents)
+Done
++ Command line to rerun is: 'KaSim' '-l' '1' '-seed' '442310228' '-d' 'output' 'counters_greater_than.ka' '-syntax' '4'
+______________________________________________________________________
+#################
+Counter c of agent A reached maximum
+#####################################################
+Simulation ended

tests/integration/compiler/counters_greater_than/output/counter_perturbation.ka.ref

@@ -0,0 +1,7 @@
+// Snapshot [Event: 3]
+%def: "T0" "0.35709268540166106"
+
+%init: 1 /*1 agents*/ A(c{=4})
+%init: 1 /*1 agents*/ A(c{=2})
+%init: 1 /*1 agents*/ A(c{=0})
+

tests/integration/compiler/counters_greater_than/output/data.csv.ref

@@ -0,0 +1,3 @@
+# Output of 'KaSim' '-l' '1' '-seed' '442310228' '-d' 'output' 'counters_greater_than.ka' '-syntax' '4'
+"[T]","A1","A2","A3"
+0.,1,2,3

tests/integration/compiler/counters_greater_than/output/inputs.ka.ref

@@ -0,0 +1,29 @@
+%def: "seed" "442310228"
+%def: "dumpIfDeadlocked" "true"
+%def: "maxConsecutiveClash" "3"
+%def: "progressBarSize" "70"
+%def: "progressBarSymbol" "#"
+%def: "plotPeriod" "1" "t.u."
+%def: "outputFileName" "data.csv"
+
+
+%agent: A(c{=0/+=3})
+
+%var:/*0*/ 'A1' |A(c{=0})|
+%var:/*1*/ 'A2' |A(c{=1})|
+%var:/*2*/ 'A3' |A(c{=0})|
+%plot: [T]
+%plot: A1
+%plot: A2
+%plot: A3
+
+'greater_than_edit' A(c{>=1/+=1}) @ 1
+'greater_than_arrow' A(c{>=1/+=1}) @ 1
+
+/*0*/%mod: (|A(c{=4})| = 1) do $PRINTF ""; $PRINTF "Counter c of agent A reached maximum"; $STOP "counter_perturbation.ka"; repeat [false]
+
+%init: 1 A(c{=0})
+%init: 1 A(c{=1})
+%init: 1 A(c{=2})
+
+%mod: [E] = 3 do $STOP;

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 719, 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 841, File "crash.ka", line 4, characters 5-69:: missaligned rule: the rule is ignored; exception:Exit