(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-13 18:54:08 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-14 11:12:24 CET by Kim Nguyen>
*)
INCLUDE "utils.ml"
loop phi
let eval_trans cache ltrs node_info fcs nss ps ss =
- let i = (ltrs.Ata.TransList.id :> int)
- and j = (node_info.NodeInfo.id :> int)
+ let j = (node_info.NodeInfo.id :> int)
and k = (fcs.StateSet.id :> int)
and l = (nss.StateSet.id :> int)
- and m = (ps.StateSet.id :> int)
+ and m = (ps.StateSet.id :> int) in
+ let rec loop ltrs ss =
+ let i = (ltrs.Ata.TransList.id :> int)
and n = (ss.StateSet.id :> int) in
- let res = Cache.N6.find cache i j k l m n in
- if res == Cache.N6.dummy cache then
- let res =
- Ata.TransList.fold (fun trs (acct, accs) ->
- let q, _, phi = Ata.Transition.node trs in
- if StateSet.mem q accs then (acct, accs) else
- if eval_form phi node_info fcs nss ps accs then
- (acct, StateSet.add q accs)
- else
- (Ata.TransList.cons trs acct, accs)
- ) ltrs (Ata.TransList.nil, ss)
- in
- Cache.N6.add cache i j k l m n res; res
- else
- res
+ let (new_ltrs, new_ss) as res =
+ let res = Cache.N6.find cache i j k l m n in
+ if res == Cache.N6.dummy cache then
+ let res =
+ Ata.TransList.fold (fun trs (acct, accs) ->
+ let q, _, phi = Ata.Transition.node trs in
+ if StateSet.mem q accs then (acct, accs) else
+ if eval_form phi node_info fcs nss ps accs then
+ (acct, StateSet.add q accs)
+ else
+ (Ata.TransList.cons trs acct, accs)
+ ) ltrs (Ata.TransList.nil, ss)
+ in
+ Cache.N6.add cache i j k l m n res; res
+ else
+ res
+ in
+ if new_ss == ss then res else
+ loop new_ltrs new_ss
+ in
+ loop ltrs ss
- let top_down_run auto tree node cache _i =
+ let top_down_run auto tree node cache trans_cache2 trans_cache6 _i =
let redo = ref false in
- let dummy2 = Ata.TransList.cons
- (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_))
- Ata.TransList.nil
- in
- let dummy6 = (dummy2, StateSet.empty) in
- let trans_cache6 = Cache.N6.create 17 dummy6 in
- let trans_cache2 = Cache.N2.create 17 dummy2 in
let rec loop node =
if node != T.nil then begin
let parent = T.parent tree node in
Cache.N2.find trans_cache2
(tag.QName.id :> int) (auto.Ata.states.StateSet.id :> int)
in
- if trs == dummy2 then
+ if trs == Cache.N2.dummy trans_cache2 then
let trs = Ata.get_trans auto auto.Ata.states tag in
(Cache.N2.add
trans_cache2
let cache = Cache.N1.create (T.size tree) StateSet.empty in
let redo = ref true in
let iter = ref 0 in
+ let dummy2 = Ata.TransList.cons
+ (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_))
+ Ata.TransList.nil
+ in
+ let dummy6 = (dummy2, StateSet.empty) in
+ let trans_cache6 = Cache.N6.create 17 dummy6 in
+ let trans_cache2 = Cache.N2.create 17 dummy2 in
+ let () = at_exit (fun () ->
+ let num_phi = ref 0 in
+ let num_trans = ref 0 in
+ Cache.N6.iteri (fun _ _ _ _ _ _ _ b -> if not b then incr num_phi) trans_cache6;
+ Cache.N2.iteri (fun _ _ _ b -> if not b then incr num_trans) trans_cache2;
+ Format.eprintf "PROFILE:materialized %i transitions and %i configurations\n@." !num_trans !num_phi
+ )
+ in
while !redo do
- redo := top_down_run auto tree node cache !iter;
+ redo := top_down_run auto tree node cache trans_cache2 trans_cache6 !iter;
incr iter;
done;
get_results auto tree node cache