diff --git a/core/KaSa_rep/frontend/prepreprocess.ml b/core/KaSa_rep/frontend/prepreprocess.ml index de09d0174..b45a9f28d 100644 --- a/core/KaSa_rep/frontend/prepreprocess.ml +++ b/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 *) diff --git a/core/grammar/ast.ml b/core/grammar/ast.ml index bdb032a33..e43a04ae8 100644 --- a/core/grammar/ast.ml +++ b/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 diff --git a/core/grammar/ast.mli b/core/grammar/ast.mli index f6358a70a..17fd7beb4 100644 --- a/core/grammar/ast.mli +++ b/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; diff --git a/core/grammar/counters_compiler.ml b/core/grammar/counters_compiler.ml index 81253db9b..2777a5bb3 100644 --- a/core/grammar/counters_compiler.ml +++ b/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) : diff --git a/core/grammar/kparser4.mly b/core/grammar/kparser4.mly index 3bed553a1..8d42f4461 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) } + | 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) } ; diff --git a/core/grammar/lKappa_compiler.ml b/core/grammar/lKappa_compiler.ml index f6631c926..595bd6fe8 100644 --- a/core/grammar/lKappa_compiler.ml +++ b/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 \ diff --git a/tests/integration/compiler/counters_greater_than/README b/tests/integration/compiler/counters_greater_than/README new file mode 100644 index 000000000..3ea45aa8c --- /dev/null +++ b/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 diff --git a/tests/integration/compiler/counters_greater_than/counters_greater_than.ka b/tests/integration/compiler/counters_greater_than/counters_greater_than.ka new file mode 100644 index 000000000..feeb52571 --- /dev/null +++ b/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})| diff --git a/tests/integration/compiler/counters_greater_than/output/LOG.ref b/tests/integration/compiler/counters_greater_than/output/LOG.ref new file mode 100644 index 000000000..0d1acd601 --- /dev/null +++ b/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 diff --git a/tests/integration/compiler/counters_greater_than/output/counter_perturbation.ka.ref b/tests/integration/compiler/counters_greater_than/output/counter_perturbation.ka.ref new file mode 100644 index 000000000..052f27738 --- /dev/null +++ b/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}) + diff --git a/tests/integration/compiler/counters_greater_than/output/data.csv.ref b/tests/integration/compiler/counters_greater_than/output/data.csv.ref new file mode 100644 index 000000000..6155b607c --- /dev/null +++ b/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 diff --git a/tests/integration/compiler/counters_greater_than/output/error.log.ref b/tests/integration/compiler/counters_greater_than/output/error.log.ref new file mode 100644 index 000000000..e69de29bb diff --git a/tests/integration/compiler/counters_greater_than/output/inputs.ka.ref b/tests/integration/compiler/counters_greater_than/output/inputs.ka.ref new file mode 100644 index 000000000..7c3683d23 --- /dev/null +++ b/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; diff --git a/tests/integration/compiler/site_mismatch/output/LOG.ref b/tests/integration/compiler/site_mismatch/output/LOG.ref index 28c6fc2ce..8e5b78f86 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 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