(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-08 18:43:08 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-04 16:36:40 CET by Kim Nguyen>
*)
INCLUDE "utils.ml"
end
module SFormula = Formula.Make(Move)
-type 'a t = {
+type t = {
id : Uid.t;
mutable states : StateSet.t;
- mutable top_states : StateSet.t;
- mutable bottom_states: StateSet.t;
+(* mutable top_states : StateSet.t;
+ mutable bottom_states: StateSet.t; *)
mutable selection_states: StateSet.t;
transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
}
let create () = { id = next ();
states = StateSet.empty;
- top_states = StateSet.empty;
- bottom_states = StateSet.empty;
+(* top_states = StateSet.empty;
+ bottom_states = StateSet.empty; *)
selection_states = StateSet.empty;
transitions = Hashtbl.create 17;
}
fprintf fmt
"Unique ID: %i@\n\
States %a@\n\
- Top states: %a@\n\
- Bottom states: %a@\n\
Selection states: %a@\n\
Alternating transitions:@\n"
(a.id :> int)
StateSet.print a.states
- StateSet.print a.top_states
- StateSet.print a.bottom_states
+(* StateSet.print a.top_states
+ StateSet.print a.bottom_states *)
StateSet.print a.selection_states;
let trs =
Hashtbl.fold
end
end
in
- StateSet.iter (fun q -> Queue.add (q, true) todo) a.top_states;
+ StateSet.iter (fun q -> Queue.add (q, true) todo) a.selection_states;
while not (Queue.is_empty todo) do
let (q, b) as key = Queue.pop todo in
let q' =
let trans = Hashtbl.find a.transitions q in
let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
Hashtbl.replace a.transitions q' trans'
- done;
- Hashtbl.iter (fun (q, b) q' ->
- if not (b || StateSet.mem q a.bottom_states) then
- a.bottom_states <- StateSet.add q' a.bottom_states
- ) memo_state
-
+ done