end
-module Transition = Hcons.Make (struct
+module Transition =
+ struct
+ include Hcons.Make (struct
type t = State.t * QNameSet.t * Formula.t
let equal (a, b, c) (d, e, f) =
a == d && b == e && c == f
let hash (a, b, c) =
HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
end)
+ let print ppf t =
+ let q, l, f = t.node in
+ fprintf ppf "%a, %a %s %a"
+ State.print q
+ QNameSet.print l
+ Pretty.double_right_arrow
+ Formula.print f
+ end
module TransList : sig
transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
}
-
+let uid t = t.id
let get_states a = a.states
let get_starting_states a = a.starting_states
let get_selecting_states a = a.selecting_states
-let get_trans a tag states =
- StateSet.fold (fun q acc0 ->
- try
- let trs = Hashtbl.find a.transitions q in
- List.fold_left (fun acc1 (labs, phi) ->
- if QNameSet.mem tag labs then
- TransList.cons (Transition.make (q, labs, phi)) acc1
- else acc1) acc0 trs
- with Not_found -> acc0
- ) states TransList.nil
-
-
let _pr_buff = Buffer.create 50
let _str_fmt = formatter_of_buffer _pr_buff
Buffer.clear _pr_buff; s
let print fmt a =
+ let _ = _flush_str_fmt() in
fprintf fmt
"Internal UID: %i@\n\
States: %a@\n\
) strs_strings;
fprintf fmt "%s@\n" line
+
+let get_trans a tag states =
+ StateSet.fold (fun q acc0 ->
+ try
+ let trs = Hashtbl.find a.transitions q in
+ List.fold_left (fun acc1 (labs, phi) ->
+ if QNameSet.mem tag labs then
+ TransList.cons (Transition.make (q, labs, phi)) acc1
+ else acc1) acc0 trs
+ with Not_found -> acc0
+ ) states TransList.nil
+
+
+
+
(*
[complete transitions a] ensures that for each state q
and each symbols s in the alphabet, a transition q, s exists.
let link_phi =
StateSet.fold
(fun q phi -> Formula.(or_ (stay q) phi))
- a1.selecting_states Formula.true_
+ a1.selecting_states Formula.false_
in
+ Hashtbl.iter (fun q trs -> Hashtbl.add a1.transitions q trs)
+ a2.transitions;
StateSet.iter
(fun q ->
- Hashtbl.add a1.transitions q [(QNameSet.any, link_phi)])
+ Hashtbl.replace a1.transitions q [(QNameSet.any, link_phi)])
a2.starting_states;
- Hashtbl.iter (fun q trs -> Hashtbl.add a1.transitions q trs)
- a2.transitions;
{ a1 with
states = StateSet.union a1.states a2.states;
selecting_states = a2.selecting_states;
transitions = a1.transitions;
}
+
+let merge a1 a2 =
+ let a1 = copy a1 in
+ let a2 = copy a2 in
+ { a1 with
+ states = StateSet.union a1.states a2.states;
+ selecting_states = StateSet.union a1.selecting_states a2.selecting_states;
+ starting_states = StateSet.union a1.starting_states a2.starting_states;
+ transitions =
+ let () =
+ Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions
+ in
+ a1.transitions
+ }