src/ata.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 (*
  17   Time-stamp: <Last modified on 2013-01-30 19:09:27 CET by Kim Nguyen>
  18 *)
  19
  20 open Format
  21
  22 type t = {
  23   id : Uid.t;
  24   mutable states : StateSet.t;
  25   mutable top_states : StateSet.t;
  26   mutable bottom_states: StateSet.t;
  27   mutable selection_states: StateSet.t;
  28   transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
  29 }
  30
  31 let next = Uid.make_maker ()
  32
  33 let create () = { id = next ();
  34                   states = StateSet.empty;
  35                   top_states = StateSet.empty;
  36                   bottom_states = StateSet.empty;
  37                   selection_states = StateSet.empty;
  38                   transitions = Hashtbl.create 17;
  39  }
  40
  41 let add_trans a q s f =
  42   let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
  43   let rem, ntrs =
  44     List.fold_left (fun (rem, atrs) ((labs, phi) as tr) ->
  45       let nlabs = QNameSet.inter labs rem in
  46       if QNameSet.is_empty nlabs then
  47         (rem, tr :: atrs)
  48       else
  49         let nrem = QNameSet.diff rem labs in
  50         nrem, (nlabs, Formula.or_ phi f)::atrs
  51     ) (s, []) trs
  52   in
  53   let ntrs = if QNameSet.is_empty rem then ntrs
  54     else (rem, f) :: ntrs
  55   in
  56   Hashtbl.replace a.transitions q ntrs
  57
  58
  59 let print fmt a =
  60   fprintf fmt
  61     "Unique ID: %i@\n\
  62      States %a@\n\
  63      Top states: %a@\n\
  64      Bottom states: %a@\n\
  65      Selection states: %a@\n\
  66      Alternating transitions:@\n"
  67     (a.id :> int)
  68     StateSet.print a.states
  69     StateSet.print a.top_states
  70     StateSet.print a.bottom_states
  71     StateSet.print a.selection_states;
  72   let trs =
  73     Hashtbl.fold
  74       (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
  75       a.transitions
  76       []
  77   in
  78   let sorted_trs = List.stable_sort (fun (q1, s1, phi1) (q2, s2, phi2) ->
  79     let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
  80     trs
  81   in
  82   let sfmt = str_formatter in
  83   let _ = flush_str_formatter () in
  84   let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
  85     let s1 = State.print sfmt q; flush_str_formatter () in
  86     let s2 = QNameSet.print sfmt s; flush_str_formatter () in
  87     let s3 = Formula.print sfmt f; flush_str_formatter () in
  88     ( (s1, s2, s3) :: accl,
  89       max
  90         accm (2 + String.length s1 + String.length s2))
  91   ) ([], 0) sorted_trs
  92   in
  93   List.iter (fun (s1, s2, s3) ->
  94     fprintf fmt "%s, %s" s1 s2;
  95     fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2));
  96     fprintf fmt "%s  %s@\n" Pretty.right_arrow s3) strs_strings