automata.ml 18.8 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) 2001 - 2003 - Verimag.
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: automata.ml
** Author: jahier@imag.fr
**
*)

open Formula 
open List
open Util

(****************************************************************************)
(** Set of integers *)
module IntSet = struct
  include Set.Make(struct type t = int let compare = compare end)
end

let (intset_to_string : IntSet.t -> string) =
  fun set -> 
    let elt = IntSet.max_elt set in
    let set1 = IntSet.remove elt set in
    IntSet.fold 
      (fun i acc -> ((string_of_int i) ^ ", " ^ acc)) 
      set1 
      (string_of_int elt)


(****************************************************************************)
33
type arc_info_static =  int * formula_eps * Control.state option
34 35 36 37
(* We call it static in the sense that weights are no more dynamic. *)

let (arc_info_static_to_string : arc_info_static -> string) =
  fun (w, formula_eps, pcl) -> 
38
    let pc_str = 
39
      " XXX arc_info_static_to_string "
40 41
(*       fold_left (fun acc str -> (acc^":"^str)) "" pcl  *)
    in
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
    ( (string_of_int w) ^ " "  ^ 
      (formula_eps_to_string formula_eps) ^ " " ^ pc_str)


type lnode = IntSet.t
(* We need node to be set of [int]s so that the product of an
automata is still an automata. *)


type transition = lnode * arc_info_static * lnode

type dyn_trans_list = (node, arc_info) Graph.t
type stat_trans_list = (lnode, arc_info_static) Graph.t

type t = lnode * stat_trans_list

(****************************************************************************)
let (get_origin_nodes_from_trans_list : transition list -> lnode list) =
  fun tl ->
    (* collect all the starting nodes of the transitions in [tl] *)
    fold_left (fun nl (n,_,_) -> if mem n nl then nl else n::nl) [] tl
   
let (is_epsilon : formula_eps -> bool) =
  fun f -> 
    match f with 
	Eps -> true
      | Form(_) -> false

(* exported *)
let rec (remove_formula : t -> formula -> t) =
  fun (n, g) f ->
    let all_trans = Graph.get_all_trans g in
    let trans_to_rm =
      fst (partition (fun (_,(_,fe,_),_) -> fe = Form(f)) all_trans)
    in
    let nodes_to_rm = get_origin_nodes_from_trans_list  trans_to_rm in
      iter (Graph.remove_trans g) trans_to_rm;
      iter (rm_useless_eps_trans g) nodes_to_rm;
      (n, g)
and 
  (rm_useless_eps_trans : stat_trans_list -> lnode -> unit) =
  fun g node -> 
    (* recursively remove epsilon transitions that comes to [node] if it
       has no successor. *)
    if (Graph.get_list_of_target_nodes g node) = [] then
      let (l, _) = partition 
		     (fun (nf, (_,fe,_), nt) -> nt = node && is_epsilon fe) 
		     (Graph.get_all_trans g) 
      in
	iter (Graph.remove_trans g) l;
	iter (rm_useless_eps_trans g) (get_origin_nodes_from_trans_list  l)

		  
(****************************************************************************)
(* 
   When I build sub-automata, I must remove loop bodies from the
   automata iff its weight is 0 *AND* it has been obtained from the draw
   (loop_between v min max) and [v] in bound to [max] (1) (ie, we can
   not loop once more without violating te user spec). We say that [v]
   is not recoverable.

   Indeed, if I do that, then whenever no non-O-weighted branches exist,
   then they can safely be taken; if it is a loop body branch, then it
   corresponds to the recovery case; if it is a loop end one, then it
   corresponds to the case where the formula in the loop is
   unsatisfiable, which means that the end branch should be tried then.
   
   (1) Maybe we could also remove branches where [v] comes from the draw
   [(loop_gauss v m std)] where [v > m + 100*std] (for which the probability
   is very small ...) and print a warning.
   
   If they are several of 0-weighted transitions, then we simply perform
   a fair toss. But Lutin should not generate such automata.
*)
let rec (get_automaton: node -> t) =
  fun n ->
    let g = Env_state.graph ()
    and st = Env_state.ctrl_state ()
    and t = Graph.create ()
    in
122
      get_automaton_acc g (IntSet.singleton n) n t st;
123 124 125 126
(*       Show_env.graph_to_dot [] []  "toto" (intset_to_string)  *)
(* 	(arc_info_static_to_string) t; *)
      (IntSet.singleton n, t)
and 
127
  (get_automaton_acc: dyn_trans_list -> IntSet.t -> node -> stat_trans_list 
128
     -> Control.state -> unit) =
129 130 131 132 133 134 135
  fun g handled_nodes n t st0 ->

    (* 
       handled_nodes is the set of nodes get_automaton was  called with. This 
       set is used to detect loop of eps transitions. 
       
    *)
136 137 138 139 140 141 142 143 144 145 146 147 148
    let tnl = Graph.get_list_of_target_nodes g n in
      (* Add the current transitions and draw weights *)
      List.iter
	(fun (nt, (w, f, pc)) ->
	   let st1 = (Env_state.ctrl_expr pc) st0 in
	     if 
	       is_pos_or_recoverable_var w st1
	     then
	       (* if [w] is dynamic and bound to 0, we keep the
		  transition iff [w] is recoverable. *)
	       (
		 match f with
		     Eps -> 
149
		       if not (IntSet.mem nt handled_nodes) then
150 151 152 153 154
			 (* In order to cut epsilon loops *)
			 (
			   Graph.add_trans 
			    t 
			    (IntSet.singleton n) 
155
			    (get_weight w st1, f, None)
156
			    (IntSet.singleton nt) ;
157
			   get_automaton_acc g (IntSet.add nt handled_nodes) nt t st1
158 159 160 161 162 163 164 165 166 167 168 169
			 )
		   | Form(f2) ->
		       if 
			 (Solver.is_satisfiable (Env_state.input ()) f2)
			 (* check formula boolean satisfiability and
			    replaces inputs and pre (in the bdd that is
			    build (and stored) to check the satisfiability).
			 *)
		       then
			 Graph.add_trans 
			   t 
			   (IntSet.singleton n)
170
			   (get_weight w st1, f, Some st1)
171 172 173 174 175
			   (IntSet.singleton nt)
	       )
	)
	tnl 
and 
176 177
  (* We only keep transitions which weigth is positive and one that
     <<could have been>> positive. *)
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
  (is_pos_or_recoverable_var : weight -> Control.state -> bool) =
  fun w st ->
    match w with
	Wint(i) -> i > 0
      | Wident(id) -> 
	  (Control.return id st > 0) || Control.is_recoverable id st
      | Wident_not_sig(id) -> 
	  (Control.return id st <= 0)  || Control.is_recoverable id st
	  
	  
and
  (get_weight : weight -> Control.state -> int) =
  fun w st -> 
    match w with
	Wint(i) -> i
      | Wident(id) -> Control.return id st
      | Wident_not_sig(id) -> if (Control.return id st) > 0 then 0 else 1


197 198 199 200 201 202 203 204 205
let (compose_state_option : Control.state option -> Control.state option -> 
       Control.state option) =
  fun st1 st2 -> 
    match (st1, st2) with
	None, None -> None
      | None, Some s -> Some s
      | Some s, None -> Some s
      | Some s1, Some s2 -> Some (Control.compose_state s1 s2)

206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232

let rec (automata_x_automata : t -> t -> t) =
  fun (n1, g1) (n2, g2) -> 
    let g = Graph.create ()
    and n = IntSet.union n1 n2
    in
      automata_x_automata_acc (n1, g1) (n2, g2) g ;
      (n, g)
and
  (automata_x_automata_acc : t -> t -> stat_trans_list -> unit) =
  fun (n1, g1) (n2, g2) g -> 
    let nl1 = Graph.get_list_of_target_nodes g1 n1 
    and nl2 = Graph.get_list_of_target_nodes g2 n2 
    in
      List.iter 
	(fun (nt2, arc2) -> 
	   List.iter 
	      (fun (nt1, arc1) ->

		   trans_x_trans g g1 g2 (n1, arc1, nt1) (n2, arc2, nt2)
	      )
	      nl1
	)
	nl2
and
  (trans_x_trans : stat_trans_list ->  stat_trans_list ->  stat_trans_list -> 
     transition -> transition -> unit) =
233
  fun g g1 g2 (n1, (w1, f1, st1), n2) (n3, (w2, f2, st2), n4) ->
234 235 236 237 238
    let n13 = IntSet.union n1 n3 in
      match (f1, f2) with
	  Form(ff1), Form(ff2) -> 
	    let n24 = IntSet.union n2 n4
	    and f = Form(And(ff1, ff2)) in
239
	    let arc = (w1*w2, f, compose_state_option st1 st2) in
240 241 242 243 244 245 246 247 248 249 250 251 252
	      if 
		not (Graph.contain_trans g n13 arc n24)
		&& Solver.is_satisfiable (Env_state.input ()) (And(ff1, ff2))
	      then
		let n24_done = Graph.contain_node g n24 in
		  (
		    Graph.add_trans g n13 arc n24 ;
		    if not n24_done then
		      automata_x_automata_acc (n2, g1) (n4, g2) g
		  );
	      
	| Eps, Eps -> 
	    let n24 = IntSet.union n2 n4
253
	    and arc = (w1*w2, Eps, (compose_state_option st1 st2)) in
254 255 256 257 258 259 260 261 262 263 264 265
	      if 
		not (Graph.contain_trans g n13 arc n24)
	      then
		let n24_done = Graph.contain_node g n24 in
		  (
		    Graph.add_trans g n13 arc n24 ;
		    if not n24_done then
		      automata_x_automata_acc (n2, g1) (n4, g2) g
		  )

	| Eps, Form(ff2) -> 
	    let n23 = IntSet.union n2 n3
266
	    and arc = (w1, Eps, st1) in
267 268 269 270 271 272 273 274 275 276 277 278
	      if 
		not (Graph.contain_trans g n13 arc n23)
	      then
		let n23_done = Graph.contain_node g n23 in
		  (
		    Graph.add_trans g n13 arc n23 ;
		    if not n23_done then
		      automata_x_automata_acc (n2, g1) (n3, g2) g
		  )

	| Form(ff1), Eps ->
	    let n14 = IntSet.union n1 n4
279
	      and arc = (w2, Eps, st2) in
280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
	      if 
		not (Graph.contain_trans g n13 arc n14)
	      then
		let n14_done = Graph.contain_node g n14 in
		  (
		    Graph.add_trans g n13 arc n14 ;
		    if not n14_done then
		      automata_x_automata_acc (n1, g1) (n4, g2) g
		  )

let rec (automata_product : t list -> t) = 
  fun al -> 
    match al with
	[] -> assert false
      | [a] -> a 
      | a1::tail -> automata_x_automata a1 (automata_product tail)


let show_automata str a =
  Show_env.graph_to_dot [fst a] [fst a]  
    str 
    (fun n -> ("\"" ^ (intset_to_string n) ^ "\"")) 
    (arc_info_static_to_string) (snd a) ;
  Util.gv (str ^ ".ps")


let _ = assert (
  let g1 = Graph.create ()    and g2 = Graph.create () and g12 = Graph.create ()
  and n1 = IntSet.singleton 1 and n2 = IntSet.singleton 2
  and n3 = IntSet.singleton 3 and n4 = IntSet.singleton 4 
  and n10 = IntSet.singleton 10 and n11 = IntSet.singleton 11
  in
  let n1_10 = IntSet.union n1 n10 and n2_10 = IntSet.union n2 n10 
  and n3_11 = IntSet.union n3 n11 and n4_11 = IntSet.union n4 n11 
  in 
  let _ =
316 317 318
    Graph.add_trans g1 n1 (2, Eps, None) n2 ;
    Graph.add_trans g1 n2 (1, Form(Bvar("a")), None) n3 ;
    Graph.add_trans g1 n1 (4, Form(Bvar("b")), None) n4 ;
319

320
    Graph.add_trans g2 n10 (3, Form(Bvar("o")), None) n11 ;
321 322

    Graph.add_trans g12 n1_10
323 324
      (12, (Form(And(Bvar("b"), (Bvar("o"))))), None)  n4_11;
    Graph.add_trans g12 n1_10 (2, Eps, None) n2_10;
325
    Graph.add_trans g12 n2_10
326
      (3, (Form(And(Bvar("a"), (Bvar("o"))))), None)  n3_11 ;
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
  in
  let a12 = automata_product [(n1, g1); (n10,g2)] 
  in    
    a12 = (n1_10, g12)
)




let _ = assert (
  let g1 = Graph.create ()  and g2 = Graph.create ()
  and g12 = Graph.create () and g13 = Graph.create ()
  and n1 = IntSet.singleton 1 and n2 = IntSet.singleton 2
  and n3 = IntSet.singleton 3 and n4 = IntSet.singleton 4 

  and n5 = IntSet.singleton 5   and n6 = IntSet.singleton 6 
  and n7 = IntSet.singleton 7 and n11 = IntSet.singleton 11
  in
  let n1_7 = IntSet.union n1 n7 and n2_7 = IntSet.union n2 n7
  and n1_5 = IntSet.union n1 n5   and n2_5 = IntSet.union n2 n5
  and n3_5 = IntSet.union n3 n5   and n4_5 = IntSet.union n4 n5 
  and n1_6 = IntSet.union n1 n6    and n2_6 = IntSet.union n2 n6 
  in 
  let _ =
351 352 353 354 355
    Graph.add_trans g1 n1 (1, Eps, None) n2 ;
    Graph.add_trans g1 n2 (1, Eps, None) n3 ;
    Graph.add_trans g1 n3 (1, Form(Bvar("a")), None) n2 ;
    Graph.add_trans g1 n2 (0, Eps, None) n4 ;
    Graph.add_trans g1 n4 (1, Form(Bvar("b")), None) n1 ;
356

357 358
    Graph.add_trans g2 n5 (1, Form(Bvar("o")), None) n6 ;
    Graph.add_trans g2 n5 (3, Form(Bvar("p")), None) n7 ;
359

360 361
    Graph.add_trans g12 n1_5 (1, Eps, None) n2_5;
    Graph.add_trans g12 n2_5 (0, Eps, None) n4_5;
362
    Graph.add_trans g12 n4_5 
363
      (3, (Form(And(Bvar("b"), (Bvar("p"))))), None) n1_7;
364
    Graph.add_trans g12 n4_5 
365
      (1, (Form(And(Bvar("b"), (Bvar("o"))))), None) n1_6;
366
    Graph.add_trans g12 n2_5 
367
      (1, Eps, None) n3_5;
368
    Graph.add_trans g12 n3_5 
369
      (3, (Form(And(Bvar("a"), (Bvar("p"))))), None) n2_7;
370
    Graph.add_trans g12 n3_5 
371
      (1, (Form(And(Bvar("a"), (Bvar("o"))))), None) n2_6;
372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425
  in
  let a12 = automata_product [(n1, g1); (n5,g2)] in
    
(*     show_automata "g1" (n1, g1); *)
(*     show_automata "g2" (n2, g2); *)
(*     show_automata "g12" (n1_5, g12); *)
(*     show_automata "a12" a12; *)
    (snd a12) = g12
)

	      
(****************************************************************************)
(* exported *)
let (get : node list list -> t list) =
  fun nll ->
    let al =
      List.map 
	(fun nl -> 
	   let a = (automata_product (List.map (get_automaton) nl)) in
	   let g = snd a in
	   let eps_trans_to_rm = 
	     fold_left
	       (fun acc (nf,(_,fe,_),nt) -> 
		  if 
		    is_epsilon fe 
		    && (Graph.get_list_of_target_nodes g nt) = []
		  then
		    Util.merge [nt] acc
		  else 
		    acc
	       )
	       []
	       (Graph.get_all_trans g)     
	   in
	     iter (rm_useless_eps_trans g) eps_trans_to_rm;
	     a
	)
	nll
    in
    let rec show_automata_list_with_dot al n =
      match al with
	  [] -> ()
	| a::tail -> 
	    Show_env.graph_to_dot [fst a] [fst a]  
	      ("automata" ^ (string_of_int n)) 
	      (fun n -> ("\"" ^ (intset_to_string n) ^ "\"")) 
	      (arc_info_static_to_string) (snd a);
	    show_automata_list_with_dot tail (n+1)
    in
(*       show_automata_list_with_dot al 1; *)
      al
    

(****************************************************************************)
426 427 428 429 430 431 432 433 434 435 436 437

let (is_node_set_transient: IntSet.t -> bool) =
  fun ns -> 
    (* A set of nodes is transient if one of the nodes in set is transient *)
    (IntSet.fold
       (fun e acc -> 
	  acc || (Env_state.is_node_transient e)
       )
       ns
       false
    )

438 439
let rec (choose_a_formula: t -> node list * formula * Control.state) =
  fun (node, trans) -> 
440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455
    (** Draws a formula in an automata (according to node weights);
      also returns the list of their corresponding target nodes, and
      control expression.  *)
    let nt_arc_l0 = Graph.get_list_of_target_nodes trans node in
    let (nt_arc_l, null_weigth_trans) = 
      List.partition (fun (_, (w,_,_)) -> w <> 0) nt_arc_l0
    in  
      if
	(List.length nt_arc_l) = 0
      then
	(* If all transitions have a weigth of 0, then we perform a
	   fair toss among them. *)
	let s2 = List.length null_weigth_trans in
	  if s2 = 0 then raise Not_found
	  else
	    let (nt, (_,f,ce)) = List.nth null_weigth_trans (Random.int s2) in
456 457 458 459 460
	      match f,ce with
		  Form(ff), Some st -> (IntSet.elements nt, ff, st)
		| Eps, None -> choose_a_formula (nt, trans)
		| Form(_), None -> assert false
		| Eps, Some _   -> assert false
461 462
      else
	let w_sum = List.fold_left (fun acc (_,(w,_,_)) -> acc+w) 0 nt_arc_l in
463 464 465
	let j =
	  try Random.int (w_sum + 1)
	    with _ ->
466 467 468 469 470 471 472 473 474 475 476
	      Control.print_state (Env_state.ctrl_state ());
	      (List.iter 
		 (fun (nt,(w,f,st_opt)) -> 
		    output_string stderr ("\n" ^ (string_of_int w) );
		       match st_opt with
			   None -> output_string stderr "None"
			 | Some st -> Control.print_state st
		 )
		 nt_arc_l );
	      assert false
	in
477 478 479 480 481 482 483 484 485 486 487 488 489
	let rec get_jth_trans j list =
	  match list with
	      [] -> assert false 
	    | (nt, (w,f,ce))::tail -> 
		let newj = j - w in
		  if 
		    (newj < 1) 
		  then 
		    (nt, (w,f,ce))
 		  else 
		    get_jth_trans newj tail	  
	in
	  match get_jth_trans j nt_arc_l with
490 491 492 493
	      (nt, (w,Eps,None)) -> choose_a_formula (nt, trans) 
	    | (nt, (w,Form(ff), Some st)) -> (IntSet.elements nt, ff, st)
	    | (nt, (w,Form(_), None)) -> assert false
	    | (nt, (w,Eps, Some _))   -> assert false
494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576


(* XXX Version with transient/recurrent nodes *)
(* let rec (choose_a_formula: formula -> t -> node list * formula * Control.state) = *)
(*   fun f_acc (node, trans) ->  *)
(*     (** Draws a formula in an automata (according to node weights); *)
(*       also returns the list of their corresponding target nodes, and *)
(*       control expression.  *) *)
(*     let nt_arc_l0 = Graph.get_list_of_target_nodes trans node in *)
(*     let (nt_arc_l, null_weigth_trans) =  *)
(*       List.partition (fun (_, (w,_,_)) -> w <> 0) nt_arc_l0 *)
(*     in   *)
(*       if *)
(* 	(List.length nt_arc_l) = 0 *)
(*       then *)
(* 	(* If all transitions have a weigth of 0, then we perform a *)
(* 	   fair toss among them. *) *)
(* 	let s2 = List.length null_weigth_trans in *)
(* 	  if s2 = 0 then raise Not_found *)
(* 	  else *)
(* 	    let (nt, (_,f,ce)) = List.nth null_weigth_trans (Random.int s2) in *)
(* 	      match f,ce with *)
(* 		  Form(ff), Some st -> *)
(* 		    let new_f = And(f_acc, ff) in  *)
(* 		      if  *)
(* 			Solver.is_satisfiable (Env_state.input ()) new_f *)
(* 		      then *)
(* 			if *)
(* 			  is_node_set_transient nt *)
(* 			then *)
(* 			  choose_a_formula new_f (nt, trans) *)
(* 			else *)
(* 			  (IntSet.elements nt, new_f, st) *)
(* 		      else *)
(* 			raise Not_found *)
(* 		| Eps, None -> choose_a_formula f_acc (nt, trans) *)
(* 		| Form(_), None -> assert false *)
(* 		| Eps, Some _   -> assert false *)
(*       else *)
(* 	let w_sum = List.fold_left (fun acc (_,(w,_,_)) -> acc+w) 0 nt_arc_l in *)
(* 	let j = *)
(* 	  try Random.int (w_sum + 1) *)
(* 	    with _ -> *)
(* 	      Control.print_state (Env_state.ctrl_state ()); *)
(* 	      (List.iter  *)
(* 		 (fun (nt,(w,f,st_opt)) ->  *)
(* 		    output_string stderr ("\n" ^ (string_of_int w) ); *)
(* 		       match st_opt with *)
(* 			   None -> output_string stderr "None" *)
(* 			 | Some st -> Control.print_state st *)
(* 		 ) *)
(* 		 nt_arc_l ); *)
(* 	      assert false *)
(* 	in *)
(* 	let rec get_jth_trans j list = *)
(* 	  match list with *)
(* 	      [] -> assert false  *)
(* 	    | (nt, (w,f,ce))::tail ->  *)
(* 		let newj = j - w in *)
(* 		  if  *)
(* 		    (newj < 1)  *)
(* 		  then  *)
(* 		    (nt, (w,f,ce)) *)
(*  		  else  *)
(* 		    get_jth_trans newj tail	   *)
(* 	in *)
(* 	  match get_jth_trans j nt_arc_l with *)
(* 	      (nt, (w,Eps,None)) -> choose_a_formula f_acc (nt, trans)  *)
(* 	    | (nt, (w,Form(ff), Some st)) ->  *)
(* 		let new_f = And(f_acc, ff) in  *)
(* 		  if  *)
(* 		    Solver.is_satisfiable (Env_state.input ()) new_f *)
(* 		  then *)
(* 		    if  *)
(* 		      is_node_set_transient nt *)
(* 		    then *)
(* 		      choose_a_formula new_f (nt, trans) *)
(* 		    else *)
(* 		      (IntSet.elements nt, new_f, st) *)
(* 		  else  *)
(* 		    raise Not_found *)
(* 	    | (nt, (w,Form(_), None)) -> assert false *)
(* 	    | (nt, (w,Eps, Some _))   -> assert false *)
577 578
	  

579
type accT = (node list * formula * Control.state) list
580 581

let rec (choose_n_formula_acc: int -> t -> accT -> accT) =
582
  fun n a nt_f_st_l0 -> 
583 584 585
    if 
      n = 0
    then 
586
      nt_f_st_l0
587 588
    else 
      try
589
	let (ntl, f, st) = choose_a_formula a in
590
(* 	let (ntl, f, st) = choose_a_formula True a in *)
591
	  choose_n_formula_acc (n-1) a ((ntl, f, st)::nt_f_st_l0)
592 593 594 595 596 597 598 599 600 601
      with Not_found -> 	 
	let nodes_str = intset_to_string (fst a) in
	  if (IntSet.cardinal (fst a)) = 1 
	  then failwith ("*** No (more) transition(s) can be made from node " 
			 ^ nodes_str ^ ". \n")
	  else failwith ("*** No (more) transition(s) can be made from one " 
			 ^ "of the nodes: " ^ nodes_str ^ ".\n") 


(* exported *)
602
let (choose_n_formula: int -> t -> (node list * formula * Control.state) list) =
603 604 605 606 607 608 609 610 611
  fun n a -> 
    let l = choose_n_formula_acc n a [] in
      assert ((List.length l) = n);
      l