package KaSim

  1. Overview
  2. Docs
type agent_name = int
type site_name = int
type internal_state = int
type binding_type = agent_name * site_name
type abstract = Matching.Agent.t
type concrete = Agent.t
type !'a site = 'a * site_name
type !'a test =
  1. | Is_Here of 'a
  2. | Has_Internal of 'a site * internal_state
  3. | Is_Free of 'a site
  4. | Is_Bound of 'a site
  5. | Has_Binding_type of 'a site * binding_type
  6. | Is_Bound_to of 'a site * 'a site
type !'a action =
  1. | Create of 'a * (site_name * internal_state option) list
  2. | Mod_internal of 'a site * internal_state
  3. | Bind of 'a site * 'a site
  4. | Bind_to of 'a site * 'a site
  5. | Free of 'a site
  6. | Remove of 'a
type !'a binding_state =
  1. | ANY
  2. | FREE
  3. | BOUND
  4. | BOUND_TYPE of binding_type
  5. | BOUND_to of 'a site
type !'a event = {
  1. tests : 'a test list list;
  2. actions : 'a action list;
  3. side_effects_src : ('a site * 'a binding_state) list;
  4. side_effects_dst : 'a site list;
  5. connectivity_tests : 'a test list;
}
val empty_event : 'a event
val rename_abstract_test : int -> Renaming.t -> abstract test -> abstract test
val rename_abstract_action : int -> Renaming.t -> abstract action -> abstract action
val rename_abstract_event : int -> Renaming.t -> abstract event -> abstract event
val rename_abstract_side_effect : int -> Renaming.t -> ((Matching.Agent.t * 'a) * Matching.Agent.t binding_state) -> (Matching.Agent.t * 'a) * Matching.Agent.t binding_state
val concretize_test : (Matching.t * int Mods.IntMap.t) -> abstract test -> concrete test
val concretize_action : (Matching.t * int Mods.IntMap.t) -> abstract action -> concrete action
val try_concretize_action : (Matching.t * int Mods.IntMap.t) -> abstract action -> concrete action option
val concretize_event : (Matching.t * int Mods.IntMap.t) -> abstract event -> concrete event
val matching_abstract_concrete : abstract event -> concrete event -> Renaming.t option
val subst_map_agent_in_concrete_test : (int -> int) -> concrete test -> concrete test
val subst_agent_in_concrete_test : int -> int -> concrete test -> concrete test
val subst_map_agent_in_concrete_action : (int -> int) -> concrete action -> concrete action
val subst_agent_in_concrete_action : int -> int -> concrete action -> concrete action
val subst_map_agent_in_concrete_side_effect : (int -> int) -> (concrete site * concrete binding_state) -> concrete site * concrete binding_state
val subst_agent_in_concrete_side_effect : int -> int -> (concrete site * concrete binding_state) -> concrete site * concrete binding_state
val subst_map_agent_in_concrete_event : (int -> int) -> concrete event -> concrete event
val subst_map2_agent_in_concrete_event : (int -> int) -> (int -> int) -> concrete event -> concrete event
val subst_agent_in_concrete_event : int -> int -> concrete event -> concrete event
val print_concrete_test : ?sigs:Signature.s -> Format.formatter -> concrete test -> unit
val print_concrete_action : ?sigs:Signature.s -> Format.formatter -> concrete action -> unit
val print_concrete_binding_state : ?sigs:Signature.s -> Format.formatter -> concrete binding_state -> unit
val test_to_json : ('a -> Yojson.Basic.json) -> 'a test -> Yojson.Basic.json
val test_of_json : (Yojson.Basic.json -> 'a) -> Yojson.Basic.json -> 'a test
val action_to_json : ('a -> Yojson.Basic.json) -> 'a action -> Yojson.Basic.json
val action_of_json : (Yojson.Basic.json -> 'a) -> Yojson.Basic.json -> 'a action
val event_to_json : ('a -> Yojson.Basic.json) -> 'a event -> Yojson.Basic.json
val event_of_json : (Yojson.Basic.json -> 'a) -> Yojson.Basic.json -> 'a event
OCaml

Innovation. Community. Security.