let table = get_states_by_move phi in
Move.fold (fun _ s acc -> StateSet.union s acc) table StateSet.empty
+ let rec rename_state phi qfrom qto =
+ let open Boolean in
+ match expr phi with
+ False | True -> phi
+ | Or (phi1, phi2) -> or_ (rename_state phi1 qfrom qto) (rename_state phi2 qfrom qto)
+ | And (phi1, phi2) -> and_ (rename_state phi1 qfrom qto) (rename_state phi2 qfrom qto)
+ | Atom ({ Atom.node = Move(m, q); }, b) when q == qfrom ->
+ let atm = mk_move m qto in if b then atm else not_ atm
+ | Atom _ -> phi
end
module Transition =
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
fprintf ppf "%a, %a %s %a"
State.print q
QNameSet.print l
- Pretty.double_right_arrow
+ Pretty.left_arrow
Formula.print f
end
module TransList : sig
include Hlist.S with type elt = Transition.t
- val print : Format.formatter -> ?sep:string -> t -> unit
+ val print : ?sep:string -> Format.formatter -> t -> unit
end =
struct
include Hlist.Make(Transition)
- let print ppf ?(sep="\n") l =
+ let print ?(sep="\n") ppf l =
iter (fun t ->
- let q, lab, f = Transition.node t in
- fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab Formula.print f sep) l
+ fprintf ppf "%a%s" Transition.print t sep) l
end
[]
in
let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
- let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
+ let c = State.compare q2 q1 in if c == 0 then QNameSet.compare s2 s1 else c)
trs
in
let _ = _flush_str_fmt () in
- let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
- let s1 = State.print _str_fmt q; _flush_str_fmt () in
- let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
- let s3 = Formula.print _str_fmt f; _flush_str_fmt () in
- let pre = Pretty.length s1 + Pretty.length s2 in
- let all = Pretty.length s3 in
- ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
- ) ([], 0, 0) sorted_trs
+ let strs_strings, max_pre, max_all =
+ List.fold_left (fun (accl, accp, acca) (q, s, f) ->
+ let s1 = State.print _str_fmt q; _flush_str_fmt () in
+ let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
+ let s3 = Formula.print _str_fmt f; _flush_str_fmt () in
+ let pre = Pretty.length s1 + Pretty.length s2 in
+ let all = Pretty.length s3 in
+ ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
+ ) ([], 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" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
- fprintf fmt " %s %s@\n" Pretty.right_arrow s3;
+ fprintf fmt "%s"
+ (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
+ fprintf fmt " %s %s@\n" Pretty.left_arrow s3;
) strs_strings;
fprintf fmt "%s@\n" line
let rec flip b f =
match Formula.expr f with
Boolean.True | Boolean.False -> if b then f else Formula.not_ f
- | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
- | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
+ | Boolean.Or(f1, f2) ->
+ (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
+ | Boolean.And(f1, f2) ->
+ (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
| Boolean.Atom(a, b') -> begin
match a.Atom.node with
| Move (m, q) ->
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
done;
cleanup_states auto
+exception Found of State.t * State.t
+
+let simplify_epsilon auto =
+ let rec loop old_states =
+ if old_states != auto.states then begin
+ let old_states = auto.states in
+ try
+ Hashtbl.iter
+ (fun qfrom v -> match v with
+ [ (labels, phi) ] ->
+ if labels == QNameSet.any then begin
+ match (Formula.expr phi) with
+ Boolean.Atom ( {Atom.node = Move(`Stay, qto); _ }, true) -> raise (Found (qfrom, qto))
+ | _ -> ()
+ end
+ | _ -> ()
+ ) auto.transitions
+ with Found (qfrom, qto) ->
+ Hashtbl.remove auto.transitions qfrom;
+ let new_trans = Hashtbl.fold (fun q tr_lst acc ->
+ let new_tr_lst =
+ List.map (fun (lab, phi) ->
+ (lab, Formula.rename_state phi qfrom qto))
+ tr_lst
+ in
+ (q, new_tr_lst) :: acc) auto.transitions []
+ in
+ Hashtbl.reset auto.transitions;
+ List.iter (fun (q, l) -> Hashtbl.add auto.transitions q l) new_trans;
+ auto.states <- StateSet.remove qfrom auto.states;
+ if (StateSet.mem qfrom auto.starting_states) then
+ auto.starting_states <- StateSet.add qto (StateSet.remove qfrom auto.starting_states);
+ if (StateSet.mem qfrom auto.selecting_states) then
+ auto.selecting_states <- StateSet.add qto (StateSet.remove qfrom auto.selecting_states);
+ loop old_states
+ end
+ in
+ loop StateSet.empty
+
+
+
(* [compute_dependencies auto] returns a hash table storing for each
states [q] a Move.table containing the set of states on which [q]
depends (loosely). [q] depends on [q'] if there is a transition
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 upward = [ `Stay ; `Parent ; `Previous_sibling ] in
let downward = [ `Stay; `First_child; `Next_sibling ] in
let swap dir = if dir == upward then downward else upward in
- let is_satisfied q t =
- Move.for_all (fun _ set -> StateSet.(is_empty (remove q set))) t
+ let is_satisfied dir q t =
+ Move.for_all (fun d set ->
+ if List.mem d dir then
+ StateSet.(is_empty (remove q set))
+ else StateSet.is_empty set) t
in
let update_dependencies dir initacc =
let rec loop acc =
Move.set deps m (StateSet.diff (Move.get deps m) to_remove)
)
dir;
- if is_satisfied q deps then StateSet.add q acc else acc
+ if is_satisfied dir q deps then StateSet.add q acc else acc
) dependencies acc
in
if acc == new_acc then new_acc else loop new_acc
done;
let by_rank = Hashtbl.create 17 in
List.iter (fun (r,s) ->
- let r = r/2 in
- let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
- Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
+ let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
+ Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
auto.ranked_states <-
Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i)
in
Hashtbl.replace a.transitions q ntrs
+
+
let finalize a =
complete_transitions a;
normalize_negations a;
+ simplify_epsilon a;
compute_rank a;
a
end
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))