src/ata.ml

   1 open Format
   2
   3 type t = {
   4   id : Uid.t;
   5   mutable states : StateSet.t;
   6   mutable top_states : StateSet.t;
   7   mutable bottom_states: StateSet.t;
   8   mutable selection_states: StateSet.t;
   9   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
  10 }
  11
  12 let next = Uid.make_maker ()
  13
  14 let create () = { id = next ();
  15                   states = StateSet.empty;
  16                   top_states = StateSet.empty;
  17                   bottom_states = StateSet.empty;
  18                   selection_states = StateSet.empty;
  19                   transitions = Hashtbl.create 17;
  20  }
  21
  22 let add_trans a q s f =
  23   let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
  24   let rem, ntrs =
  25     List.fold_left (fun (rem, atrs) ((labs, phi) as tr) ->
  26       let nlabs = QNameSet.inter labs rem in
  27       if QNameSet.is_empty nlabs then
  28         (rem, tr :: atrs)
  29       else
  30         let nrem = QNameSet.diff rem labs in
  31         nrem, (nlabs, Formula.or_ phi f)::atrs
  32     ) (s, []) trs
  33   in
  34   let ntrs = if QNameSet.is_empty rem then ntrs
  35     else (rem, f) :: ntrs
  36   in
  37   Hashtbl.replace a.transitions q ntrs
  38
  39
  40 let print fmt a =
  41   fprintf fmt
  42     "Unique ID: %i@\n\
  43      States %a@\n\
  44      Top states: %a@\n\
  45      Bottom states: %a@\n\
  46      Selection states: %a@\n\
  47      Alternating transitions:@\n"
  48     (a.id :> int)
  49     StateSet.print a.states
  50     StateSet.print a.top_states
  51     StateSet.print a.bottom_states
  52     StateSet.print a.selection_states;
  53   let trs =
  54     Hashtbl.fold
  55       (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
  56       a.transitions
  57       []
  58   in
  59   let sorted_trs = List.stable_sort (fun (q1, s1, phi1) (q2, s2, phi2) ->
  60     let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
  61     trs
  62   in
  63   let sfmt = str_formatter in
  64   let _ = flush_str_formatter () in
  65   let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
  66     let s1 = State.print sfmt q; flush_str_formatter () in
  67     let s2 = QNameSet.print sfmt s; flush_str_formatter () in
  68     let s3 = Formula.print sfmt f; flush_str_formatter () in
  69     ( (s1, s2, s3) :: accl,
  70       max
  71         accm (2 + String.length s1 + String.length s2))
  72   ) ([], 0) sorted_trs
  73   in
  74   List.iter (fun (s1, s2, s3) ->
  75     fprintf fmt "%s, %s" s1 s2;
  76     fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2));
  77     fprintf fmt "%s  %s@\n" Pretty.right_arrow s3) strs_strings