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