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-02-06 14:24:24 CET by Kim Nguyen>
  18 *)
  19
  20 open Format
  21 type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ]
  22 type state_ctx = { left : StateSet.t;
  23                    right : StateSet.t;
  24                    up1 : StateSet.t;
  25                    up2 : StateSet.t;
  26                    epsilon : StateSet.t}
  27 type ctx_ = { mutable positive : state_ctx;
  28              mutable negative : state_ctx }
  29 type pred_ = move * bool * State.t
  30
  31 module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) =
  32 struct
  33
  34   module Node =
  35   struct
  36     type t = move * bool * State.t
  37     let equal n1 n2 = n1 = n2
  38     let hash n = Hashtbl.hash n
  39   end
  40
  41   type ctx = ctx_
  42   let make_ctx a b c d e =
  43     { left = a; right = b; up1 = c; up2 = d; epsilon = e }
  44
  45   include Hcons.Make(Node)
  46
  47   let print ppf a =
  48     let _ = flush_str_formatter() in
  49     let fmt = str_formatter in
  50
  51     let m, b, s = a.node in
  52     let dir,num =
  53       match  m with
  54       | `Left ->  Pretty.down_arrow, Pretty.subscript 1
  55       | `Right -> Pretty.down_arrow, Pretty.subscript 2
  56       | `Epsilon -> Pretty.epsilon, ""
  57       | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
  58       | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
  59     in
  60     fprintf fmt "%s%s" dir num;
  61     State.print fmt s;
  62     let str = flush_str_formatter() in
  63     if b then fprintf ppf "%s" str
  64     else Pretty.pp_overline ppf str
  65
  66   let neg p =
  67     let l, b, s = p.node in
  68     make (l, not b, s)
  69
  70   let eval ctx p =
  71     let l, b, s = p.node in
  72     let nctx = if b then ctx.positive else ctx.negative in
  73     StateSet.mem s begin
  74       match l with
  75         `Left -> nctx.left
  76       | `Right -> nctx.right
  77       | `Up1 -> nctx.up1
  78       | `Up2 -> nctx.up2
  79       | `Epsilon -> nctx.epsilon
  80     end
  81 end
  82
  83 module SFormula = Formula.Make(Move)
  84 type t = {
  85   id : Uid.t;
  86   mutable states : StateSet.t;
  87   mutable top_states : StateSet.t;
  88   mutable bottom_states: StateSet.t;
  89   mutable selection_states: StateSet.t;
  90   transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
  91 }
  92
  93
  94
  95 let next = Uid.make_maker ()
  96
  97 let create () = { id = next ();
  98                   states = StateSet.empty;
  99                   top_states = StateSet.empty;
 100                   bottom_states = StateSet.empty;
 101                   selection_states = StateSet.empty;
 102                   transitions = Hashtbl.create 17;
 103  }
 104
 105 let add_trans a q s f =
 106   let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
 107   let rem, ntrs =
 108     List.fold_left (fun (rem, atrs) ((labs, phi) as tr) ->
 109       let nlabs = QNameSet.inter labs rem in
 110       if QNameSet.is_empty nlabs then
 111         (rem, tr :: atrs)
 112       else
 113         let nrem = QNameSet.diff rem labs in
 114         nrem, (nlabs, SFormula.or_ phi f)::atrs
 115     ) (s, []) trs
 116   in
 117   let ntrs = if QNameSet.is_empty rem then ntrs
 118     else (rem, f) :: ntrs
 119   in
 120   Hashtbl.replace a.transitions q ntrs
 121
 122
 123 let print fmt a =
 124   fprintf fmt
 125     "Unique ID: %i@\n\
 126      States %a@\n\
 127      Top states: %a@\n\
 128      Bottom states: %a@\n\
 129      Selection states: %a@\n\
 130      Alternating transitions:@\n"
 131     (a.id :> int)
 132     StateSet.print a.states
 133     StateSet.print a.top_states
 134     StateSet.print a.bottom_states
 135     StateSet.print a.selection_states;
 136   let trs =
 137     Hashtbl.fold
 138       (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
 139       a.transitions
 140       []
 141   in
 142   let sorted_trs = List.stable_sort (fun (q1, s1, phi1) (q2, s2, phi2) ->
 143     let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
 144     trs
 145   in
 146   let sfmt = str_formatter in
 147   let _ = flush_str_formatter () in
 148   let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
 149     let s1 = State.print sfmt q; flush_str_formatter () in
 150     let s2 = QNameSet.print sfmt s; flush_str_formatter () in
 151     let s3 = SFormula.print sfmt f; flush_str_formatter () in
 152     ( (s1, s2, s3) :: accl,
 153       max
 154         accm (2 + String.length s1 + String.length s2))
 155   ) ([], 0) sorted_trs
 156   in
 157   List.iter (fun (s1, s2, s3) ->
 158     fprintf fmt "%s, %s" s1 s2;
 159     fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2));
 160     fprintf fmt "%s  %s@\n" Pretty.right_arrow s3) strs_strings