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