+++ /dev/null
-(***********************************************************************)
-(* *)
-(* TAToo *)
-(* *)
-(* Kim Nguyen, LRI UMR8623 *)
-(* Université Paris-Sud & CNRS *)
-(* *)
-(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(* Recherche Scientifique. All rights reserved. This file is *)
-(* distributed under the terms of the GNU Lesser General Public *)
-(* License, with the special exception on linking described in file *)
-(* ../LICENSE. *)
-(* *)
-(***********************************************************************)
-
-(*
- Time-stamp: <Last modified on 2013-02-06 14:24:24 CET by Kim Nguyen>
-*)
-
-open Format
-type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ]
-type state_ctx = { left : StateSet.t;
- right : StateSet.t;
- up1 : StateSet.t;
- up2 : StateSet.t;
- epsilon : StateSet.t}
-type ctx_ = { mutable positive : state_ctx;
- mutable negative : state_ctx }
-type pred_ = move * bool * State.t
-
-module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) =
-struct
-
- module Node =
- struct
- type t = move * bool * State.t
- let equal n1 n2 = n1 = n2
- let hash n = Hashtbl.hash n
- end
-
- type ctx = ctx_
- let make_ctx a b c d e =
- { left = a; right = b; up1 = c; up2 = d; epsilon = e }
-
- include Hcons.Make(Node)
-
- let print ppf a =
- let _ = flush_str_formatter() in
- let fmt = str_formatter in
-
- let m, b, s = a.node in
- let dir,num =
- match m with
- | `Left -> Pretty.down_arrow, Pretty.subscript 1
- | `Right -> Pretty.down_arrow, Pretty.subscript 2
- | `Epsilon -> Pretty.epsilon, ""
- | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
- | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
- in
- fprintf fmt "%s%s" dir num;
- State.print fmt s;
- let str = flush_str_formatter() in
- if b then fprintf ppf "%s" str
- else Pretty.pp_overline ppf str
-
- let neg p =
- let l, b, s = p.node in
- make (l, not b, s)
-
- let eval ctx p =
- let l, b, s = p.node in
- let nctx = if b then ctx.positive else ctx.negative in
- StateSet.mem s begin
- match l with
- `Left -> nctx.left
- | `Right -> nctx.right
- | `Up1 -> nctx.up1
- | `Up2 -> nctx.up2
- | `Epsilon -> nctx.epsilon
- end
-end
-
-module SFormula = Formula.Make(Move)
-type t = {
- id : Uid.t;
- mutable states : StateSet.t;
- mutable top_states : StateSet.t;
- mutable bottom_states: StateSet.t;
- mutable selection_states: StateSet.t;
- transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
-}
-
-
-
-let next = Uid.make_maker ()
-
-let create () = { id = next ();
- states = StateSet.empty;
- top_states = StateSet.empty;
- bottom_states = StateSet.empty;
- selection_states = StateSet.empty;
- transitions = Hashtbl.create 17;
- }
-
-let add_trans a q s f =
- let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
- let rem, ntrs =
- List.fold_left (fun (rem, atrs) ((labs, phi) as tr) ->
- let nlabs = QNameSet.inter labs rem in
- if QNameSet.is_empty nlabs then
- (rem, tr :: atrs)
- else
- let nrem = QNameSet.diff rem labs in
- nrem, (nlabs, SFormula.or_ phi f)::atrs
- ) (s, []) trs
- in
- let ntrs = if QNameSet.is_empty rem then ntrs
- else (rem, f) :: ntrs
- in
- Hashtbl.replace a.transitions q ntrs
-
-
-let print fmt a =
- fprintf fmt
- "Unique ID: %i@\n\
- States %a@\n\
- Top states: %a@\n\
- Bottom states: %a@\n\
- Selection states: %a@\n\
- Alternating transitions:@\n"
- (a.id :> int)
- StateSet.print a.states
- StateSet.print a.top_states
- StateSet.print a.bottom_states
- StateSet.print a.selection_states;
- let trs =
- Hashtbl.fold
- (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
- a.transitions
- []
- in
- let sorted_trs = List.stable_sort (fun (q1, s1, phi1) (q2, s2, phi2) ->
- let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
- trs
- in
- let sfmt = str_formatter in
- let _ = flush_str_formatter () in
- let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) ->
- let s1 = State.print sfmt q; flush_str_formatter () in
- let s2 = QNameSet.print sfmt s; flush_str_formatter () in
- let s3 = SFormula.print sfmt f; flush_str_formatter () in
- ( (s1, s2, s3) :: accl,
- max
- accm (2 + String.length s1 + String.length s2))
- ) ([], 0) sorted_trs
- in
- List.iter (fun (s1, s2, s3) ->
- fprintf fmt "%s, %s" s1 s2;
- fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2));
- fprintf fmt "%s %s@\n" Pretty.right_arrow s3) strs_strings