- let rec comp_acc_self set flag = function
- | [] -> set,flag
- | (q,form) :: tl ->
- if Formula.infer_form set qf qn form
- then if StateSet.mem q set
- then comp_acc_self set 0 tl
- else comp_acc_self (StateSet.add q set) 1 tl
- else comp_acc_self set 0 tl
- and rec fix_point selfq_i =
- let setq,flag = comp_acc_self selfq_i 0 list_tr in
- if flag = 1 then set
- else fix_point setq qf qn 0 in
- NodeHash.replace run node (fix_point set_node, set_nr);
+ let rec comp_acc_self set flag =
+ () (* given a current set of states we add
+ states from self transitions which satisfy the two conditions *)
+ (* With result (below) we have all valid transitions at step 0
+ we compute the self states which occur in it and which are not in cthe current state.
+ For each of these states we compute the transitions with the correct label and state
+ we infer each of these transitions: true -> add self states occuring in it
+ to the acc and to the current set + add left and right states as result do *)
+ (* ----> With a FIFO *)
+ and fix_point selfq_i =
+ () in
+ NodeHash.replace run node (set_node, set_nr);