Skip to content

Commit

Permalink
changed type of bdu to an int type whose first n numbers represent th…
Browse files Browse the repository at this point in the history
…e guards and the remaining numbers represent the sites
  • Loading branch information
reb-ddm committed Jan 9, 2025
1 parent 63e0d7e commit abfb1c6
Show file tree
Hide file tree
Showing 16 changed files with 1,030 additions and 693 deletions.
2 changes: 1 addition & 1 deletion core/KaSa_rep/backend/ckappa_site_graph.mli
Original file line number Diff line number Diff line change
Expand Up @@ -43,5 +43,5 @@ val internal_pair_list_to_list :
Ckappa_sig.c_site_name ->
Site_graphs.KaSa_site_graph.agent_id ->
Ckappa_sig.c_site_name ->
(Ckappa_sig.c_site_name * Ckappa_sig.c_state) list list ->
(Ckappa_sig.c_guard_p_then_site * Ckappa_sig.c_state) list list ->
Exception.exceptions_caught_and_uncaught * Site_graphs.KaSa_site_graph.t list
1 change: 1 addition & 0 deletions core/KaSa_rep/frontend/cckappa_sig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ type kappa_handler = {
nrules: int;
nvars: int;
nagents: Ckappa_sig.c_agent_name;
nguard_params: int;
agents_dic: Ckappa_sig.agent_dic;
agents_annotation:
(string * Loc.t list)
Expand Down
1 change: 1 addition & 0 deletions core/KaSa_rep/frontend/cckappa_sig.mli
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ type kappa_handler = {
nrules: int;
nvars: int;
nagents: Ckappa_sig.c_agent_name;
nguard_params: int;
agents_dic: Ckappa_sig.agent_dic;
agents_annotation:
(string * Loc.t list)
Expand Down
48 changes: 47 additions & 1 deletion core/KaSa_rep/frontend/ckappa_sig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,9 @@ type binding_state = Free | Lnk_type of agent_name * site_name
type c_guard_parameter = int
type c_site_or_guard_p = Site of c_site_name | Guard_p of c_guard_parameter

type c_guard_p_then_site =
int (*the first n elements are guards, the last ones are sites*)

type mixture =
| SKIP of mixture
| COMMA of agent * mixture
Expand Down Expand Up @@ -192,8 +195,30 @@ let state_index_of_int (a : int) : c_state = a
let int_of_state_index (a : c_state) : int = a
let string_of_state_index (a : c_state) : string = string_of_int a
let guard_parameter_of_int (a : int) : c_guard_parameter = a
let guard_p_then_site_of_int (a : int) : c_guard_p_then_site = a
let int_of_guard_p_then_site (a : c_guard_p_then_site) : int = a

let guard_p_then_site_of_site (a : c_site_name) (nr_guard_p : int) :
c_guard_p_then_site =
guard_parameter_of_int (int_of_site_name a + nr_guard_p)

let guard_p_then_site_of_guard (a : c_guard_parameter) : c_guard_p_then_site = a

let guard_p_then_site_of_site_or_guard_p (a : c_site_or_guard_p)
(nr_guard_p : int) : c_guard_p_then_site =
match a with
| Site s -> guard_p_then_site_of_site s nr_guard_p
| Guard_p s -> guard_p_then_site_of_guard s

let int_of_guard_parameter (a : c_guard_parameter) : int = a

let site_or_guard_p_of_guard_p_then_site (a : c_guard_p_then_site)
(nr_guard_p : int) : c_site_or_guard_p =
if a < nr_guard_p then
Guard_p a
else
Site (a - nr_guard_p)

let string_of_state_index_option_min parameters a =
match a with
| Some a -> string_of_state_index a
Expand Down Expand Up @@ -843,6 +868,13 @@ module Site_map_and_set = Map_wrapper.Make (SetMap.Make (struct
let print = Format.pp_print_int
end))

module GuardSite_map_and_set = Map_wrapper.Make (SetMap.Make (struct
type t = c_guard_p_then_site

let compare = compare
let print = Format.pp_print_int
end))

type c_interface = c_port Site_map_and_set.Map.t

type c_proper_agent = {
Expand Down Expand Up @@ -932,6 +964,7 @@ let next_rule_id = succ
let next_agent_id = succ
let next_agent_name = succ
let next_site_name = succ
let next_guard_or_site_name = succ
let next_state_index = succ
let compare_rule_id = compare
let compare_agent_id = compare
Expand Down Expand Up @@ -1002,6 +1035,12 @@ module Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif :
and type dimension = int * int =
Int_storage.Nearly_Inf_Int_Int_storage_Imperatif_Imperatif

module Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif :
Int_storage.Storage
with type key = c_agent_name * c_guard_p_then_site
and type dimension = int * int =
Int_storage.Nearly_Inf_Int_Int_storage_Imperatif_Imperatif

module Agent_type_site_quick_nearly_Inf_Int_Int_storage_Imperatif_Imperatif :
Int_storage.Storage
with type key = c_agent_name * c_site_name
Expand All @@ -1024,6 +1063,13 @@ module Site_type_quick_nearly_Inf_Int_storage_Imperatif :
Int_storage.Storage with type key = c_site_name and type dimension = int =
Int_storage.Quick_key_list (Site_type_nearly_Inf_Int_storage_Imperatif)

(*guard parameters or site: the first n indexes are the guards, and the remaining are the sites*)
module GuardPOrSite_nearly_Inf_Int_storage_Imperatif :
Int_storage.Storage
with type key = c_guard_p_then_site
and type dimension = int =
Int_storage.Nearly_inf_Imperatif

(*state*)
module State_index_nearly_Inf_Int_storage_Imperatif :
Int_storage.Storage with type key = c_state and type dimension = int =
Expand Down Expand Up @@ -1252,7 +1298,7 @@ end))

module Views_bdu :
Mvbdu_wrapper.Mvbdu
with type key = c_site_name
with type key = c_guard_p_then_site
and type value = c_state
with type mvbdu = Mvbdu_wrapper.Mvbdu.mvbdu =
Mvbdu_wrapper.Mvbdu
Expand Down
34 changes: 31 additions & 3 deletions core/KaSa_rep/frontend/ckappa_sig.mli
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ type c_link_value
type c_counter_name
type c_guard_parameter
type c_site_or_guard_p = Site of c_site_name | Guard_p of c_guard_parameter
type c_guard_p_then_site

(****************************************************************************)

Expand All @@ -55,8 +56,8 @@ val dummy_link_value : c_link_value
val dummy_site_name_1 : c_site_name
val dummy_site_name_minus1 : c_site_name
val next_link_value : c_link_value -> c_link_value
val fst_site : c_site_name
val snd_site : c_site_name
val fst_site : c_guard_p_then_site (*rTODO maybe add nr_guard_params?*)
val snd_site : c_guard_p_then_site
val dummy_state_index_1 : c_state
val string_of_agent_name : c_agent_name -> string
val int_of_agent_name : c_agent_name -> int
Expand All @@ -70,8 +71,19 @@ val state_index_of_int : int -> c_state
val int_of_state_index : c_state -> int
val string_of_state_index : c_state -> string
val guard_parameter_of_int : int -> c_guard_parameter
val guard_p_then_site_of_int : int -> c_guard_p_then_site
val int_of_guard_p_then_site : c_guard_p_then_site -> int
val guard_p_then_site_of_site : c_site_name -> int -> c_guard_p_then_site
val guard_p_then_site_of_guard : c_guard_parameter -> c_guard_p_then_site

val guard_p_then_site_of_site_or_guard_p :
c_site_or_guard_p -> int -> c_guard_p_then_site

val int_of_guard_parameter : c_guard_parameter -> int

val site_or_guard_p_of_guard_p_then_site :
c_guard_p_then_site -> int -> c_site_or_guard_p

val string_of_state_index_option_min :
Remanent_parameters_sig.parameters -> c_state option -> string

Expand All @@ -91,6 +103,7 @@ val next_agent_id : c_agent_id -> c_agent_id
val next_agent_name : c_agent_name -> c_agent_name
val next_rule_id : c_rule_id -> c_rule_id
val next_site_name : c_site_name -> c_site_name
val next_guard_or_site_name : c_guard_p_then_site -> c_guard_p_then_site
val next_state_index : c_state -> c_state
val pred_site_name : c_site_name -> c_site_name
val pred_agent_name : c_agent_name -> c_agent_name
Expand Down Expand Up @@ -375,6 +388,9 @@ module SiteOrGuard_map_and_set :

module Site_map_and_set : Map_wrapper.S_with_logs with type elt = c_site_name

module GuardSite_map_and_set :
Map_wrapper.S_with_logs with type elt = c_guard_p_then_site

type c_interface = c_port Site_map_and_set.Map.t

type c_proper_agent = {
Expand Down Expand Up @@ -485,6 +501,11 @@ module Agent_type_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif :
with type key = c_agent_name * c_site_name
and type dimension = int * int

module Agent_type_guard_or_site_nearly_Inf_Int_Int_storage_Imperatif_Imperatif :
Int_storage.Storage
with type key = c_agent_name * c_guard_p_then_site
and type dimension = int * int

module Agent_type_site_quick_nearly_Inf_Int_Int_storage_Imperatif_Imperatif :
Int_storage.Storage
with type key = c_agent_name * c_site_name
Expand All @@ -501,6 +522,11 @@ module Site_type_nearly_Inf_Int_storage_Imperatif :
module Site_type_quick_nearly_Inf_Int_storage_Imperatif :
Int_storage.Storage with type key = c_site_name and type dimension = int

module GuardPOrSite_nearly_Inf_Int_storage_Imperatif :
Int_storage.Storage
with type key = c_guard_p_then_site
and type dimension = int

module State_index_nearly_Inf_Int_storage_Imperatif :
Int_storage.Storage with type key = c_state and type dimension = int

Expand Down Expand Up @@ -586,7 +612,9 @@ module AgentsSitePState_map_and_set :
with type elt = c_agent_id * c_agent_name * c_site_name * pair_of_states

module Views_bdu :
Mvbdu_wrapper.Mvbdu with type key = c_site_name and type value = c_state
Mvbdu_wrapper.Mvbdu
with type key = c_guard_p_then_site
and type value = c_state

module Views_intbdu :
Mvbdu_wrapper.Internalized_mvbdu
Expand Down
14 changes: 14 additions & 0 deletions core/KaSa_rep/frontend/handler.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ let local_trace = false
let nrules _parameter _error handler = handler.Cckappa_sig.nrules
let nvars _parameter _error handler = handler.Cckappa_sig.nvars
let nagents _parameter _error handler = handler.Cckappa_sig.nagents
let get_nr_guard_parameters handler = handler.Cckappa_sig.nguard_params

let check_pos parameter ka_pos ml_pos message error error' =
match ml_pos with
Expand Down Expand Up @@ -620,6 +621,19 @@ let string_of_site_contact_map ?(ml_pos = None) ?(ka_pos = None) ?(message = "")
in
error, print_site_contact_map site_type

let string_of_site_or_guard_contact_map ?(ml_pos = None) ?(ka_pos = None)
?(message = "") parameter error handler_kappa agent_name site_or_guard_int =
let nr_guard_params = get_nr_guard_parameters handler_kappa in
match
Ckappa_sig.site_or_guard_p_of_guard_p_then_site site_or_guard_int
nr_guard_params
with
| Ckappa_sig.Site s ->
string_of_site_contact_map ~ml_pos ~ka_pos ~message parameter error
handler_kappa agent_name s
| Ckappa_sig.Guard_p g ->
string_of_guard g handler_kappa.Cckappa_sig.guard_parameters error

let print_labels parameters error handler couple =
let _ = Quark_type.Labels.dump_couple parameters error handler couple in
error
Expand Down
11 changes: 11 additions & 0 deletions core/KaSa_rep/frontend/handler.mli
Original file line number Diff line number Diff line change
Expand Up @@ -249,6 +249,17 @@ val string_of_site_contact_map :
Ckappa_sig.c_site_name ->
Exception_without_parameter.exceptions_caught_and_uncaught * string

val string_of_site_or_guard_contact_map :
?ml_pos:(string * int * int * int) option ->
?ka_pos:Loc.t option ->
?message:string ->
Remanent_parameters_sig.parameters ->
Exception_without_parameter.exceptions_caught_and_uncaught ->
Cckappa_sig.kappa_handler ->
Quark_type.agent_quark ->
Ckappa_sig.c_guard_p_then_site ->
Exception_without_parameter.exceptions_caught_and_uncaught * string

val string_of_site_in_natural_language :
Remanent_parameters_sig.parameters ->
Exception_without_parameter.exceptions_caught_and_uncaught ->
Expand Down
11 changes: 10 additions & 1 deletion core/KaSa_rep/frontend/list_tokens.ml
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ let empty_handler parameters error =
Cckappa_sig.nvars = 0;
Cckappa_sig.nagents = Ckappa_sig.dummy_agent_name;
Cckappa_sig.nrules = 0;
Cckappa_sig.nguard_params = 0;
Cckappa_sig.agents_dic = Ckappa_sig.Dictionary_of_agents.init ();
Cckappa_sig.agents_annotation = agent_annotation;
Cckappa_sig.interface_constraints = int_constraints;
Expand Down Expand Up @@ -506,8 +507,16 @@ let scan_compil parameters error compil =
let remanent =
scan_perts scan_tested_mixture parameters remanent compil.Ast.perturbations
in
let remanent =
let error, remanent =
scan_rules scan_tested_mixture parameters remanent compil.Ast.rules
in
let remanent =
( error,
{
remanent with
Cckappa_sig.nguard_params =
List.length remanent.Cckappa_sig.guard_parameters;
} )
in
let remanent = reverse_agents_annotation parameters remanent in
remanent
Loading

0 comments on commit abfb1c6

Please sign in to comment.