+ bu_oracle asta run tree tfnode hashOracle hashEval;
+ bu_oracle asta run tree tnnode hashOracle hashEval;
+ (* add states which satisfy a transition *)
+ let rec result set qfr qnr flag = function
+ | [] -> set,flag
+ | (q,form) :: tl ->
+ if Formula.eval_form (set,qfr,qnr) form hashEval
+ then
+ if StateSet.mem q set
+ then result set qfr qnr 0 tl
+ else result (StateSet.add q set) qfr qnr 1 tl
+ else result set qfr qnr 0 tl in
+ (* compute the fixed point of states of node *)
+ let rec fix_point set_i qfr qnr list_tr t =
+ try HashOracle.find hashOracle (set_i, qfr, qnr, list_tr, t)
+ with _ ->
+ let set,flag = result set_i qfr qnr 0 list_tr in
+ HashOracle.add hashOracle (set_i,qfr,qnr,list_tr,t) (set); (* todo: Think about this position *)
+ if flag = 0
+ then set
+ else fix_point set qfr qnr list_tr t in