(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-13 18:54:08 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-13 19:02:13 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 redo = ref false in