Skip to content

Commit

Permalink
add sum type of site and guard
Browse files Browse the repository at this point in the history
  • Loading branch information
reb-ddm committed Jan 8, 2025
1 parent d1e81e7 commit 63e0d7e
Show file tree
Hide file tree
Showing 11 changed files with 216 additions and 95 deletions.
38 changes: 38 additions & 0 deletions core/KaSa_rep/frontend/ckappa_sig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,8 @@ type c_rule_id = int
type c_link_value = int
type c_counter_name = int
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 mixture =
| SKIP of mixture
Expand Down Expand Up @@ -158,6 +160,8 @@ let c_rule_id_of_string s =
let dummy_agent_name = 0
let dummy_site_name = 0
let dummy_state_index = 0
let dummy_state_index_true = 1
let dummy_state_index_false = 2
let dummy_rule_id = 0
let dummy_agent_id = 0
let dummy_site_name_1 = 1
Expand All @@ -179,9 +183,16 @@ let next_link_value (i : c_link_value) : c_link_value = i + 1
let site_name_of_int (a : int) : c_site_name = a
let int_of_site_name (a : c_site_name) : int = a
let string_of_site_name (a : c_site_name) : string = string_of_int a

let string_of_site_or_guard (a : c_site_or_guard_p) : string =
match a with
| Site s | Guard_p s -> string_of_int s

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 int_of_guard_parameter (a : c_guard_parameter) : int = a

let string_of_state_index_option_min parameters a =
match a with
Expand Down Expand Up @@ -812,6 +823,19 @@ type c_port = {
c_site_interval: c_state interval;
}

let pp_print_site_or_guard_p state site =
Format.pp_print_string state
(match site with
| Site s -> "Site " ^ Int.to_string s
| Guard_p g -> "Guard_p " ^ Int.to_string g)

module SiteOrGuard_map_and_set = Map_wrapper.Make (SetMap.Make (struct
type t = c_site_or_guard_p

let compare = compare
let print = pp_print_site_or_guard_p
end))

module Site_map_and_set = Map_wrapper.Make (SetMap.Make (struct
type t = c_site_name

Expand Down Expand Up @@ -945,6 +969,13 @@ let array_of_list_rule_id create set parameters error list =
in
aux list dummy_rule_id a

let to_site_list site_or_guard_list =
List.filter_map
(function
| Site s -> Some s
| Guard_p _ -> None)
site_or_guard_list

(***************************************************************************)
(*MODULE*)
(***************************************************************************)
Expand Down Expand Up @@ -1132,6 +1163,13 @@ module AgentSite_map_and_set = Map_wrapper.Make (SetMap.Make (struct
let print = Pp.pair Format.pp_print_int Format.pp_print_int
end))

module AgentSiteOrGuard_map_and_set = Map_wrapper.Make (SetMap.Make (struct
type t = c_agent_name * c_site_or_guard_p

let compare = compare
let print = Pp.pair Format.pp_print_int pp_print_site_or_guard_p
end))

module Agents_map_and_set = Map_wrapper.Make (SetMap.Make (struct
type t = c_agent_id * c_agent_name

Expand Down
15 changes: 15 additions & 0 deletions core/KaSa_rep/frontend/ckappa_sig.mli
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,8 @@ type c_rule_id
type c_agent_id
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

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

Expand All @@ -45,6 +47,8 @@ val string_of_c_link_value : c_link_value -> string
val dummy_agent_name : c_agent_name
val dummy_site_name : c_site_name
val dummy_state_index : c_state
val dummy_state_index_true : c_state
val dummy_state_index_false : c_state
val dummy_rule_id : c_rule_id
val dummy_agent_id : c_agent_id
val dummy_link_value : c_link_value
Expand All @@ -61,9 +65,12 @@ val string_of_agent_id : c_agent_id -> string
val site_name_of_int : int -> c_site_name
val int_of_site_name : c_site_name -> int
val string_of_site_name : c_site_name -> string
val string_of_site_or_guard : c_site_or_guard_p -> string
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 int_of_guard_parameter : c_guard_parameter -> int

val string_of_state_index_option_min :
Remanent_parameters_sig.parameters -> c_state option -> string
Expand Down Expand Up @@ -311,6 +318,8 @@ val add_free :
mixture ->
Exception.exceptions_caught_and_uncaught * mixture

val to_site_list : c_site_or_guard_p list -> c_site_name list

(*******************************************************)
(*C type*)
(*******************************************************)
Expand Down Expand Up @@ -361,6 +370,9 @@ type c_port = {
c_site_interval: c_state interval;
}

module SiteOrGuard_map_and_set :
Map_wrapper.S_with_logs with type elt = c_site_or_guard_p

module Site_map_and_set : Map_wrapper.S_with_logs with type elt = c_site_name

type c_interface = c_port Site_map_and_set.Map.t
Expand Down Expand Up @@ -553,6 +565,9 @@ module PairAgentSite_map_and_set :
module AgentSite_map_and_set :
Map_wrapper.S_with_logs with type elt = c_agent_name * c_site_name

module AgentSiteOrGuard_map_and_set :
Map_wrapper.S_with_logs with type elt = c_agent_name * c_site_or_guard_p

module Agents_map_and_set :
Map_wrapper.S_with_logs with type elt = c_agent_id * c_agent_name

Expand Down
2 changes: 1 addition & 1 deletion core/KaSa_rep/frontend/list_tokens.mli
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ val scan_compil :
Ckappa_sig.agent_sig,
Ckappa_sig.mixture,
Ckappa_sig.mixture,
'a,
string,
Ckappa_sig.mixture Ckappa_sig.rule )
Ast.compil ->
Exception_without_parameter.exceptions_caught_and_uncaught
Expand Down
25 changes: 14 additions & 11 deletions core/KaSa_rep/reachability_analysis/bdu_dynamic_views.ml
Original file line number Diff line number Diff line change
Expand Up @@ -79,17 +79,20 @@ let store_covering_classes_modification_update_aux parameters error
let store_covering_classes_modification_update parameters error
store_test_modification_map store_covering_classes_id =
let error, store_result =
Ckappa_sig.AgentSite_map_and_set.Map.fold
Ckappa_sig.AgentSiteOrGuard_map_and_set.Map.fold
(fun (agent_type_cv, site_type_cv) l2 store_result ->
List.fold_left
(fun (error, store_current_result) cv_id ->
let error, result =
store_covering_classes_modification_update_aux parameters error
agent_type_cv site_type_cv cv_id store_test_modification_map
store_current_result
in
error, result)
store_result l2
match site_type_cv with
| Ckappa_sig.Guard_p _ -> store_result
| Ckappa_sig.Site site_type_cv ->
List.fold_left
(fun (error, store_current_result) cv_id ->
let error, result =
store_covering_classes_modification_update_aux parameters error
agent_type_cv site_type_cv cv_id store_test_modification_map
store_current_result
in
error, result)
store_result l2
(*REMARK: when it is folding inside a list, start with empty result,
because the add_link function has already called the old result.*))
store_covering_classes_id
Expand Down Expand Up @@ -135,7 +138,7 @@ let store_covering_classes_modification_side_effects parameters error
(fun parameters error _agent_type_cv remanent store_result ->
let cv_dic = remanent.Covering_classes_type.store_dic in
let error, store_result =
Covering_classes_type.Dictionary_of_List_sites.fold
Covering_classes_type.Dictionary_of_List_sites_or_guard.fold
(fun _list_of_site_type ((), ()) cv_id
(error, store_result) ->
(*get a set of rule_id in update(c)*)
Expand Down
66 changes: 46 additions & 20 deletions core/KaSa_rep/reachability_analysis/bdu_static_views.ml
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,7 @@ let add_dependency_site parameters map_new_index_forward site state
(error, store_result) =
let error, site' =
match
Ckappa_sig.Site_map_and_set.Map.find_option parameters error site
Ckappa_sig.SiteOrGuard_map_and_set.Map.find_option parameters error site
map_new_index_forward
with
| error, None ->
Expand All @@ -132,17 +132,28 @@ let add_dependency_site parameters map_new_index_forward site state
in
Ckappa_sig.Site_map_and_set.Map.add parameters error site' state store_result

let to_site_or_guard_map parameters error site_map =
Ckappa_sig.Site_map_and_set.Map.fold
(fun site value (error, new_set) ->
Ckappa_sig.SiteOrGuard_map_and_set.Map.add parameters error
(Ckappa_sig.Site site) value new_set)
site_map
(error, Ckappa_sig.SiteOrGuard_map_and_set.Map.empty)

let get_pair_cv_map_with_missing_association_creation parameters error agent
triple_list =
List.fold_left
(fun (error, current_list) (cv_id, list, set) ->
let error, (map_new_index_forward, _) =
Common_map.new_index_pair_map parameters error list
in
let error, agent_interface =
to_site_or_guard_map parameters error agent.Cckappa_sig.agent_interface
in
(*----------------------------------------------------*)
let error', map_res =
try
Ckappa_sig.Site_map_and_set.Map
Ckappa_sig.SiteOrGuard_map_and_set.Map
.fold_restriction_with_missing_associations parameters error
(fun site port m ->
match
Expand All @@ -153,10 +164,15 @@ let get_pair_cv_map_with_missing_association_creation parameters error agent
add_dependency_site parameters map_new_index_forward site a m
| Some _, Some _ | None, _ | _, None -> raise Exit)
(fun site ->
add_dependency_site parameters map_new_index_forward site
Ckappa_sig.dummy_state_index)
set agent.Cckappa_sig.agent_interface
Ckappa_sig.Site_map_and_set.Map.empty
match site with
| Ckappa_sig.Site _ ->
add_dependency_site parameters map_new_index_forward site
Ckappa_sig.dummy_state_index
| Ckappa_sig.Guard_p _ ->
add_dependency_site parameters map_new_index_forward site
Ckappa_sig.dummy_state_index_true
(*rTODO does that mean that all parameters are true?*))
set agent_interface Ckappa_sig.Site_map_and_set.Map.empty
with Exit ->
Exception.warn parameters error __POS__ Exit
Ckappa_sig.Site_map_and_set.Map.empty
Expand Down Expand Up @@ -274,9 +290,12 @@ let get_pair_cv_map_with_restriction_modification parameters error agent
let error, (map_new_index_forward, _) =
Common_map.new_index_pair_map parameters error list
in
let error, agent_interface =
to_site_or_guard_map parameters error agent.Cckappa_sig.agent_interface
in
(*-----------------------------------------------------------*)
let error, map_res =
Ckappa_sig.Site_map_and_set.Map.fold_restriction parameters error
Ckappa_sig.SiteOrGuard_map_and_set.Map.fold_restriction parameters error
(fun site port (error, store_result) ->
let state = port.Cckappa_sig.site_state.Cckappa_sig.min in
let error, () =
Expand All @@ -286,7 +305,7 @@ let get_pair_cv_map_with_restriction_modification parameters error agent
Exception.warn parameters error __POS__ Exit ()
in
let error, site' =
Ckappa_sig.Site_map_and_set.Map.find_default_without_logs
Ckappa_sig.SiteOrGuard_map_and_set.Map.find_default_without_logs
parameters error Ckappa_sig.dummy_site_name site
map_new_index_forward
in
Expand All @@ -295,8 +314,7 @@ let get_pair_cv_map_with_restriction_modification parameters error agent
store_result
in
error, map_res)
set agent.Cckappa_sig.agent_interface
Ckappa_sig.Site_map_and_set.Map.empty
set agent_interface Ckappa_sig.Site_map_and_set.Map.empty
in
error, (cv_id, map_res) :: current_list)
(error, []) triple_list
Expand Down Expand Up @@ -398,11 +416,14 @@ let get_triple_map parameters error pair_list triple_list =
let error', map_res =
List.fold_left
(fun (error, map_res) (_, (site, state)) ->
if Ckappa_sig.Site_map_and_set.Set.mem site set then (
if
Ckappa_sig.SiteOrGuard_map_and_set.Set.mem (Ckappa_sig.Site site)
set
then (
let error, site' =
Ckappa_sig.Site_map_and_set.Map.find_default_without_logs
parameters error Ckappa_sig.dummy_site_name site
map_new_index_forward
Ckappa_sig.SiteOrGuard_map_and_set.Map.find_default_without_logs
parameters error Ckappa_sig.dummy_site_name
(Ckappa_sig.Site site) map_new_index_forward
in
let error, old =
Ckappa_sig.Site_map_and_set.Map.find_default_without_logs
Expand Down Expand Up @@ -530,7 +551,10 @@ let collect_site_to_renamed_site_list parameters error store_remanent_triple
let rec aux error site list output =
match list with
| [] -> error, output
| h :: t ->
| Ckappa_sig.Guard_p _ :: t ->
(*rTODO what is this for?*)
aux error site t output
| Ckappa_sig.Site h :: t ->
let key = agent_type', h in
let error, old =
match
Expand Down Expand Up @@ -604,22 +628,24 @@ let get_pair_cv_map_with_restriction_views parameters error agent triple_list =
let error, (map_new_index_forward, _) =
Common_map.new_index_pair_map parameters error list
in
let error, agent_interface =
to_site_or_guard_map parameters error agent.Cckappa_sig.agent_interface
in
(*----------------------------------------------------------*)
let error', map_res =
Ckappa_sig.Site_map_and_set.Map.fold_restriction parameters error
Ckappa_sig.SiteOrGuard_map_and_set.Map.fold_restriction parameters error
(fun site port (error, store_result) ->
let state = port.Cckappa_sig.site_state in
let error, site' =
Ckappa_sig.Site_map_and_set.Map.find_default parameters error
Ckappa_sig.dummy_site_name site map_new_index_forward
Ckappa_sig.SiteOrGuard_map_and_set.Map.find_default parameters
error Ckappa_sig.dummy_site_name site map_new_index_forward
in
let error, map_res =
Ckappa_sig.Site_map_and_set.Map.add parameters error site' state
store_result
in
error, map_res)
set agent.Cckappa_sig.agent_interface
Ckappa_sig.Site_map_and_set.Map.empty
set agent_interface Ckappa_sig.Site_map_and_set.Map.empty
in
let error =
Exception.check_point Exception.warn parameters error error' __POS__
Expand Down
17 changes: 9 additions & 8 deletions core/KaSa_rep/reachability_analysis/common_map.ml
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,8 @@ let get_list_from_agent_site parameters error (agent_type, site_type)
store_result =
let error, result =
match
Ckappa_sig.AgentSite_map_and_set.Map.find_option_without_logs parameters
error (agent_type, site_type) store_result
Ckappa_sig.AgentSiteOrGuard_map_and_set.Map.find_option_without_logs
parameters error (agent_type, site_type) store_result
with
| error, None -> error, []
| error, Some l -> error, l
Expand All @@ -36,8 +36,8 @@ let add_dependency_pair_sites_cv parameters error (agent_type, site_type) cv_id
store_result
in
let error, store_result =
Ckappa_sig.AgentSite_map_and_set.Map.add_or_overwrite parameters error
(agent_type, site_type) (cv_id :: old) store_result
Ckappa_sig.AgentSiteOrGuard_map_and_set.Map.add_or_overwrite parameters
error (agent_type, site_type) (cv_id :: old) store_result
in
error, store_result

Expand Down Expand Up @@ -196,8 +196,9 @@ let list2set parameters error list =
let error', set =
List.fold_left
(fun (error, current_set) elt ->
Ckappa_sig.Site_map_and_set.Set.add parameters error elt current_set)
(error, Ckappa_sig.Site_map_and_set.Set.empty)
Ckappa_sig.SiteOrGuard_map_and_set.Set.add parameters error elt
current_set)
(error, Ckappa_sig.SiteOrGuard_map_and_set.Set.empty)
list
in
let error =
Expand All @@ -213,7 +214,7 @@ let new_index_pair_map parameters error l =
| [] -> error, (map1, map2)
| h :: tl ->
let error, map1 =
Ckappa_sig.Site_map_and_set.Map.add parameters error h k map1
Ckappa_sig.SiteOrGuard_map_and_set.Map.add parameters error h k map1
in
let error, map2 =
Ckappa_sig.Site_map_and_set.Map.add parameters error k h map2
Expand All @@ -225,7 +226,7 @@ let new_index_pair_map parameters error l =
let error', (map1, map2) =
aux l
(Ckappa_sig.site_name_of_int 1)
Ckappa_sig.Site_map_and_set.Map.empty
Ckappa_sig.SiteOrGuard_map_and_set.Map.empty
Ckappa_sig.Site_map_and_set.Map.empty error
in
let error =
Expand Down
Loading

0 comments on commit 63e0d7e

Please sign in to comment.