type t = {
id : Uid.t;
mutable states : StateSet.t;
+ mutable starting_states : StateSet.t;
mutable selecting_states: StateSet.t;
transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
}
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 =
fprintf fmt
"Internal UID: %i@\n\
States: %a@\n\
+ Starting states: %a@\n\
Selection states: %a@\n\
Alternating transitions:@\n"
(a.id :> int)
StateSet.print a.states
+ StateSet.print a.starting_states
StateSet.print a.selecting_states;
let trs =
Hashtbl.fold
let complete_transitions a =
StateSet.iter (fun q ->
- let qtrans = Hashtbl.find a.transitions q in
- let rem =
- List.fold_left (fun rem (labels, _) ->
- QNameSet.diff rem labels) QNameSet.any qtrans
- in
- let nqtrans =
- if QNameSet.is_empty rem then qtrans
- else
- (rem, Formula.false_) :: qtrans
- in
- Hashtbl.replace a.transitions q nqtrans
+ if StateSet.mem q a.starting_states then ()
+ else
+ let qtrans = Hashtbl.find a.transitions q in
+ let rem =
+ List.fold_left (fun rem (labels, _) ->
+ QNameSet.diff rem labels) QNameSet.any qtrans
+ in
+ let nqtrans =
+ if QNameSet.is_empty rem then qtrans
+ else
+ (rem, Formula.false_) :: qtrans
+ in
+ Hashtbl.replace a.transitions q nqtrans
) a.states
+(* [cleanup_states] remove states that do not lead to a
+ selecting states *)
+
let cleanup_states a =
let memo = ref StateSet.empty in
let rec loop q =
in
Hashtbl.add memo_state key nq; nq
in
- let trans = Hashtbl.find auto.transitions q in
+ let trans = try Hashtbl.find auto.transitions q with Not_found -> [] in
let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
Hashtbl.replace auto.transitions q' trans';
done;
cleanup_states auto
+
+
+
module Builder =
struct
type auto = t
{
id = next ();
states = StateSet.empty;
+ starting_states = StateSet.empty;
selecting_states = StateSet.empty;
transitions = Hashtbl.create MED_H_SIZE;
}
); *)
auto
- let add_state a ?(selecting=false) q =
+ let add_state a ?(starting=false) ?(selecting=false) q =
a.states <- StateSet.add q a.states;
+ if starting then a.starting_states <- StateSet.add q a.starting_states;
if selecting then a.selecting_states <- StateSet.add q a.selecting_states
let add_trans a q s f =
normalize_negations a;
a
end
+
+
+let map_set f s =
+ StateSet.fold (fun q a -> StateSet.add (f q) a) s StateSet.empty
+
+let map_hash fk fv h =
+ let h' = Hashtbl.create (Hashtbl.length h) in
+ let () = Hashtbl.iter (fun k v -> Hashtbl.add h' (fk k) (fv v)) h in
+ h'
+
+let rec map_form f phi =
+ match Formula.expr phi with
+ | Boolean.Or(phi1, phi2) -> Formula.or_ (map_form f phi1) (map_form f phi2)
+ | Boolean.And(phi1, phi2) -> Formula.and_ (map_form f phi1) (map_form f phi2)
+ | Boolean.Atom({ Atom.node = Move(m,q); _}, b) ->
+ let a = Formula.mk_atom (Move (m,f q)) in
+ if b then a else Formula.not_ a
+ | _ -> phi
+
+let rename_states mapper a =
+ let rename q = try Hashtbl.find mapper q with Not_found -> q in
+ { Builder.make () with
+ states = map_set rename a.states;
+ starting_states = map_set rename a.starting_states;
+ selecting_states = map_set rename a.selecting_states;
+ transitions =
+ map_hash
+ rename
+ (fun l ->
+ (List.map (fun (labels, form) -> (labels, map_form rename form)) l))
+ a.transitions;
+ }
+
+let copy a =
+ let mapper = Hashtbl.create MED_H_SIZE in
+ let () =
+ StateSet.iter (fun q -> Hashtbl.add mapper q (State.make())) a.states
+ in
+ rename_states mapper a
+
+
+let concat a1 a2 =
+ let a1 = copy a1 in
+ let a2 = copy a2 in
+ let link_phi =
+ StateSet.fold
+ (fun q phi -> Formula.(or_ (stay q) phi))
+ a1.selecting_states Formula.true_
+ in
+ StateSet.iter
+ (fun q ->
+ Hashtbl.add 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;
+ }