From 3c74237a6f5acc60111ca05c6afa5249dec934a1 Mon Sep 17 00:00:00 2001 From: Ethel Morgan Date: Thu, 6 Jul 2023 17:48:01 +0100 Subject: [PATCH] Add > as syntactic sugar for >= in counters --- core/KaSa_rep/frontend/prepreprocess.ml | 1 + core/grammar/ast.ml | 6 +- core/grammar/ast.mli | 2 +- core/grammar/counters_compiler.ml | 134 +++++++++++++++++- core/grammar/kparser4.mly | 1 + core/grammar/lKappa_compiler.ml | 3 + .../compiler/counters_greater_than/README | 1 + .../counters_greater_than.ka | 13 ++ .../counters_greater_than/output/LOG.ref | 21 +++ .../output/counter_perturbation.ka.ref | 7 + .../counters_greater_than/output/data.csv.ref | 3 + .../output/error.log.ref | 0 .../output/inputs.ka.ref | 29 ++++ .../compiler/site_mismatch/output/LOG.ref | 2 +- 14 files changed, 218 insertions(+), 5 deletions(-) create mode 100644 tests/integration/compiler/counters_greater_than/README create mode 100644 tests/integration/compiler/counters_greater_than/counters_greater_than.ka create mode 100644 tests/integration/compiler/counters_greater_than/output/LOG.ref create mode 100644 tests/integration/compiler/counters_greater_than/output/counter_perturbation.ka.ref create mode 100644 tests/integration/compiler/counters_greater_than/output/data.csv.ref create mode 100644 tests/integration/compiler/counters_greater_than/output/error.log.ref create mode 100644 tests/integration/compiler/counters_greater_than/output/inputs.ka.ref diff --git a/core/KaSa_rep/frontend/prepreprocess.ml b/core/KaSa_rep/frontend/prepreprocess.ml index 4cb1a9175c..cb21863bd6 100644 --- a/core/KaSa_rep/frontend/prepreprocess.ml +++ b/core/KaSa_rep/frontend/prepreprocess.ml @@ -342,6 +342,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 let fst_opt a_opt = diff --git a/core/grammar/ast.ml b/core/grammar/ast.ml index a2934f3583..ea9ebd32d6 100644 --- a/core/grammar/ast.ml +++ b/core/grammar/ast.ml @@ -23,7 +23,7 @@ type port = { port_lnk_mod: int Locality.annot option option; } -type counter_test = CEQ of int | CGTE of int | CVAR of string +type counter_test = CEQ of int | CGTE of int | CGT of int | CVAR of string type counter = { count_nme: string Locality.annot; @@ -244,6 +244,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 | CVAR x, _ -> Format.fprintf f "=%s" x let print_counter_delta test f (delta,_) = @@ -278,12 +279,15 @@ let string_option_annot_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 ] | CVAR x -> `Assoc [ "test", `String "eq"; "val", `String x ] let counter_test_of_json = function | `Assoc [ "test", `String "eq"; "val", `Int x ] | `Assoc [ "val", `Int x; "test", `String "eq" ] -> CEQ x | `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 [ "test", `String "eq"; "val", `String x ] | `Assoc [ "val", `String x; "test", `String "eq" ] -> CVAR x | x -> diff --git a/core/grammar/ast.mli b/core/grammar/ast.mli index 3f310d293e..33283ee3b4 100644 --- a/core/grammar/ast.mli +++ b/core/grammar/ast.mli @@ -21,7 +21,7 @@ type port = { port_lnk_mod: int Locality.annot option option; } -type counter_test = CEQ of int | CGTE of int | CVAR of string +type counter_test = CEQ of int | CGTE of int | CGT of int | CVAR of string type counter = { count_nme: string Locality.annot; diff --git a/core/grammar/counters_compiler.ml b/core/grammar/counters_compiler.ml index 296ed845c8..eb61015f12 100644 --- a/core/grammar/counters_compiler.ml +++ b/core/grammar/counters_compiler.ml @@ -172,7 +172,7 @@ let enumerate_counter_tests x a ((delta,_) as count_delta) c' = let (max,_) = c'.Ast.count_delta in let min = match c'.Ast.count_test with - None| Some (Ast.CGTE _,_)| Some (Ast.CVAR _,_) -> + None| Some (Ast.CGTE _,_) | Some (Ast.CGT _,_) | Some (Ast.CVAR _,_) -> raise (ExceptionDefn.Malformed_Decl ("Invalid counter signature - have to specify min bound", @@ -222,6 +222,9 @@ let remove_variable_in_counters ~warning rules signatures = | Ast.Counter c -> let (delta,_) = c.Ast.count_delta in match c.Ast.count_test with + | Some (Ast.CGT _,pos) -> + raise (ExceptionDefn.Internal_Error + ("Counter "^(fst c.Ast.count_nme)^" should not have a > test by now", pos)) | Some (Ast.CEQ v,_) -> if (delta >0 || abs(delta) <= v) then [(Ast.Counter c,[])] else @@ -316,8 +319,129 @@ let with_counters c = 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 () = @@ -457,6 +581,9 @@ let remove_counter_agent sigs ag lnk_nb = ("Counter "^s^" should have a test by now",pos)) | (Some (test,pos')), delta -> match test with + | Ast.CGT _ -> + raise (ExceptionDefn.Internal_Error + ("Counter "^(fst counter.Ast.count_nme)^" should not have a > test by now", pos')) | Ast.CEQ j -> (counter_becomes_port sigs ag.ra id delta pos true j lnk_nb)::acc_incrs, @@ -487,8 +614,11 @@ let remove_counter_created_agent sigs ag lnk_nb = (Signature.print_agent sigs) raw_ag.Raw_mixture.a_type in LKappa.not_enough_specified ~status:"counter" ~side:"left" agent_name c.Ast.count_nme - | Some (test,_) -> + | Some (test,pos) -> match test with + | Ast.CGT _ -> + raise (ExceptionDefn.Internal_Error + ("Counter "^(fst c.Ast.count_nme)^" should not have a > test by now", pos)) | Ast.CEQ j -> let p = Raw_mixture.VAL lnk in let () = ports.(p_id) <- p in diff --git a/core/grammar/kparser4.mly b/core/grammar/kparser4.mly index 890407146d..b84ff7be41 100644 --- a/core/grammar/kparser4.mly +++ b/core/grammar/kparser4.mly @@ -129,6 +129,7 @@ counter_modif: counter_test: | EQUAL annot INT { (Ast.CEQ $3,rhs_pos 3) } | GREATER annot EQUAL annot INT { (Ast.CGTE $5,rhs_pos 5) } + | GREATER annot INT { (Ast.CGT $3,rhs_pos 3) } | EQUAL annot ID { (Ast.CVAR $3,rhs_pos 3) } ; diff --git a/core/grammar/lKappa_compiler.ml b/core/grammar/lKappa_compiler.ml index ff6dff6f83..0ff2d0ce7b 100644 --- a/core/grammar/lKappa_compiler.ml +++ b/core/grammar/lKappa_compiler.ml @@ -1277,6 +1277,9 @@ let create_t sites incr_info = | Ast.CGTE _ -> raise (ExceptionDefn.Internal_Error ("Counter should not have >= in signature",pos)) + | Ast.CGT _ -> + raise (ExceptionDefn.Internal_Error + ("Counter should not have > in signature",pos)) | Ast.CEQ j -> (c.Ast.count_nme, (NamedDecls.create [||], diff --git a/tests/integration/compiler/counters_greater_than/README b/tests/integration/compiler/counters_greater_than/README new file mode 100644 index 0000000000..3ea45aa8c1 --- /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 0000000000..feeb525719 --- /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 0000000000..0d1acd601b --- /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 0000000000..052f27738e --- /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 0000000000..6155b607c0 --- /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 0000000000..e69de29bb2 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 0000000000..7c3683d232 --- /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 762122c5f0..8e5b78f862 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 840, 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