then ()
else NodeHash.add run node (map_leaf asta)
else
- let tfnode = Tree.first_child tree tnode
+ let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
let fnode,nnode = (* their preorders *)
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
then
()
else
- let tfnode = Tree.first_child tree tnode
+ let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
begin
bu_over_max asta run tree tfnode;
()
else
let node = Tree.preorder tree tnode
- and tfnode = Tree.first_child tree tnode
+ and tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
let (fnode,nnode) =
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
(* compute states occuring in transition candidates *)
let rec add_st (ql,qr) = function
| [] -> ql,qr
- | f :: tl -> let sql,sqr = Formula.st f in
+ | f :: tl -> let sqs,sql,sqr = Formula.st f in
let ql' = StateSet.union sql ql
and qr' = StateSet.union sqr qr in
add_st (ql',qr') tl in
and qnq,qnr = try NodeHash.find run nnode
with | _ -> map_leaf asta in
begin
- if tfnode == Tree.nil
+ if tfnode == Tree.nil || Tree.is_attribute tree tnode
then ()
else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
- if tnnode == Tree.nil
+ if tnnode == Tree.nil || Tree.is_attribute tree tnode
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
(* indeed we delete all states from self transitions! *)
NodeHash.fold
(fun key set acc ->
if not(StateSet.is_empty
- (StateSet.inter (fst set) (Asta.selec_states asta)))
+ (StateSet.inter (fst set) (Asta.selec_states asta)))
then key :: acc
else acc)
run []