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))
+ let hash ((a, b, c) : t) =
+ HASHINT4 (PRIME1, ((a) :> int), ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
end)
let print ppf t =
let q, l, f = t.node in
) ([], 0, 0) sorted_trs
in
let line = Pretty.line (max_all + max_pre + 6) in
- let prev_q = ref State.dummy in
+ let prev_q = ref State.dummy_state in
fprintf fmt "%s@\n" line;
List.iter (fun (q, s1, s2, s3) ->
- if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line;
+ if !prev_q != q && !prev_q != State.dummy_state then fprintf fmt "%s@\n" line;
prev_q := q;
fprintf fmt "%s, %s" s1 s2;
fprintf fmt "%s"
with
Not_found ->
(* create a new state and add it to the todo queue *)
- let nq = State.make () in
+ let nq = State.next () in
auto.states <- StateSet.add nq auto.states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
with
Not_found ->
let nq = if b then q else
- let nq = State.make () in
+ let nq = State.next () in
auto.states <- StateSet.add nq auto.states;
nq
in
edges
+let state_prerequisites dir auto q =
+ Hashtbl.fold (fun q' trans acc ->
+ List.fold_left (fun acc (_, phi) ->
+ let m_phi = Formula.get_states_by_move phi in
+ if StateSet.mem q (Move.get m_phi dir)
+ then StateSet.add q' acc else acc)
+ acc trans) auto.transitions StateSet.empty
let compute_rank auto =
let dependencies = compute_dependencies auto in
let copy a =
let mapper = Hashtbl.create MED_H_SIZE in
let () =
- StateSet.iter (fun q -> Hashtbl.add mapper q (State.make())) a.states
+ StateSet.iter (fun q -> Hashtbl.add mapper q (State.next())) a.states
in
rename_states mapper a
let union a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
- let q = State.make () in
+ let q = State.next () in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(or_ (stay q) phi))
let inter a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
- let q = State.make () in
+ let q = State.next () in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (stay q) phi))
let neg a =
let a = copy a in
- let q = State.make () in
+ let q = State.next () in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (not_(stay q)) phi))