timedAutomaton.ml

open Common
open Dbm
open Varcontext

module type TIMED_AUTOMATON =
sig
  module MDbm : BIG_IDBM

  type timed_automaton
  type discrete_state
  type edge

  module DS : Hashtbl.HashedType with type t = discrete_state

  val clocks : timed_automaton -> VarContext.t
  val priority_compare : discrete_state -> discrete_state -> int
  val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
  val transitions_from : timed_automaton -> discrete_state ->
    (discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state) list
  val invariant_of_discrete_state : timed_automaton -> discrete_state -> UDbm.Dbm.t
  val is_urgent_or_committed : timed_automaton -> discrete_state -> bool
  val is_target : timed_automaton -> discrete_state -> bool
  val rate_of_state : timed_automaton -> discrete_state -> int
  val lu_bounds : timed_automaton -> discrete_state -> Udbml.Carray.t * Udbml.Carray.t
  val m_bounds : timed_automaton -> discrete_state -> Udbml.Carray.t
  val global_m_bounds : timed_automaton -> int array
  (** print functions *)
  val print_discrete_state  : out_channel -> timed_automaton -> discrete_state -> unit
  val print_timed_automaton : out_channel -> timed_automaton -> unit
  val print_extended_state : out_channel -> timed_automaton -> (discrete_state * MDbm.Dbm.t) -> unit
  val transition_to_string : timed_automaton ->
    (discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state) -> string
  val from_file : string -> string -> ?scale:int -> ?enlarge:int -> unit -> timed_automaton
end

module MBoundedAutomaton (TA : TIMED_AUTOMATON) =
struct
  include TA

  let bounding_transitions ta state=
    let n = VarContext.size (TA.clocks ta) in
    let m = TA.global_m_bounds ta in
    let rec build_list cl accu =
      if (cl = n) then accu
      else
        let guard = Dbm.UDbm.Dbm.create n in
        Dbm.UDbm.Dbm.set_init guard;
        Dbm.UDbm.Dbm.constrain guard (0, cl, (-m.(cl)-2, Udbml.Basic_types.DBM_WEAK));
        Dbm.UDbm.Dbm.constrain guard (cl, 0, (m.(cl)+2, Udbml.Basic_types.DBM_WEAK));
        assert(not(Dbm.UDbm.Dbm.is_empty guard));
        build_list (cl+1) ((state, guard, [(cl, m.(cl)+1)], state)::accu)
    in 
    build_list 1 []

  let transitions_from ta state =
    List.rev_append (TA.transitions_from ta state) (bounding_transitions ta state)

  let invariant_of_discrete_state ta state =
    let inv = TA.invariant_of_discrete_state ta state in
    let n = VarContext.size (TA.clocks ta) in
    let m = TA.global_m_bounds ta in
    for cl = 0 to n-1 do
      Dbm.UDbm.Dbm.constrain inv (cl, 0, (m.(cl) + 2, Udbml.Basic_types.DBM_WEAK))
    done;
    assert(not(Dbm.UDbm.Dbm.is_empty inv));
    inv
    
end

module type TIMED_GAME = 
sig
  include TIMED_AUTOMATON
  
  (* I am not convinced it is the better interface *)
  val is_controllable : timed_automaton -> edge -> bool
end

module MakeTimedAutomaton (BareTA : Ita.TA) (MDbm : Dbm.BIG_IDBM)
  : TIMED_AUTOMATON with type MDbm.dbm_t = MDbm.dbm_t and type discrete_state = BareTA.state =
struct
  module DS =
    struct
      type t = BareTA.state

      let hash = BareTA.hash_state
      let equal = BareTA.equal_state
    end

  module MDbm = MDbm
  
  module DSHashtbl = Hashtbl.Make(DS)

  type timed_automaton =
    {
      t : BareTA.ta;
      lu_tbl : (Udbml.Carray.t * Udbml.Carray.t) DSHashtbl.t;
      m_tbl : Udbml.Carray.t DSHashtbl.t;
    }
  type discrete_state = BareTA.state
  type edge (* TODO *)
  
  (* indirection *)
  let clocks ta = BareTA.clocks ta.t
  (* indirection *)
  let priority_compare = BareTA.priority_compare
  (* indirection *)
  let is_urgent_or_committed ta = BareTA.is_urgent_or_committed ta.t
  (* indirection *)
  let is_target ta = BareTA.is_target ta.t
  (* indirection *)
  let rate_of_state ta = BareTA.rate_of_state ta.t
  (* indirection *)
  let global_m_bounds ta = BareTA.global_mbounds ta.t

  let initial_extended_state ta =
    let dim = (VarContext.size (clocks ta)) in
    let z = MDbm.Dbm.create dim in
    MDbm.Dbm.set_zero z;
    (BareTA.initial_state ta.t, z)

  (* a helper function to turn a guard into a Dbm *)
  let guard_to_dbm ta s g =
    let z = Dbm.UDbm.Dbm.create (VarContext.size (clocks ta)) in
    Dbm.UDbm.Dbm.set_init z;
    List.iter (function
      | Ita.LT (c,k) ->
          Dbm.UDbm.Dbm.constrain z (c, 0, (k, Udbml.Basic_types.DBM_STRICT))
      | Ita.LEQ (c,k) ->
          Dbm.UDbm.Dbm.constrain z (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
      | Ita.GT (c,k) ->
          Dbm.UDbm.Dbm.constrain z (0, c, (-k, Udbml.Basic_types.DBM_STRICT))
      | Ita.GEQ (c,k) -> 
          Dbm.UDbm.Dbm.constrain z (0, c, (-k, Udbml.Basic_types.DBM_WEAK))
      | Ita.EQ (c,k) ->
          Dbm.UDbm.Dbm.constrain z (0, c, (-k, Udbml.Basic_types.DBM_WEAK));
          Dbm.UDbm.Dbm.constrain z (c, 0, (k, Udbml.Basic_types.DBM_WEAK))
    ) g;
    z     
    
  let transitions_from ta state =
    List.map (fun (s,g,r,s') -> (s,guard_to_dbm ta s g,r,s')) (BareTA.transitions_from ta.t state)
  
  let invariant_of_discrete_state ta s =
    guard_to_dbm ta s (BareTA.invariant ta.t s)

  (* store LU bounds in their C form, to avoid repeated translations *)
  let lu_bounds ta s =
    try
      DSHashtbl.find ta.lu_tbl s
    with
    | Not_found ->
        let larr, uarr = BareTA.lubounds ta.t s in
        let n = Array.length larr in
        let ltmp, utmp = Udbml.Carray.to_c larr n, Udbml.Carray.to_c uarr n in
        DSHashtbl.add ta.lu_tbl s (ltmp, utmp);
        (ltmp, utmp)

  (* store M bounds in their C form, to avoid repeated translations *)
  let m_bounds ta s =
    try
      DSHashtbl.find ta.m_tbl s
    with
    | Not_found ->
        let larr, uarr = BareTA.lubounds ta.t s in
        let n = Array.length larr in
        let marr = Array.make n 0 in
        for i=0 to n-1 do
          marr.(i) <- max larr.(i) uarr.(i)
        done;
        let mtmp = Udbml.Carray.to_c marr n in
        DSHashtbl.add ta.m_tbl s mtmp;
        mtmp

  (* PRINT functions *)
  (* indirection *)
  let print_discrete_state chan ta s =
    Printf.fprintf chan "%s" (BareTA.state_to_string ta.t s)
  
  let print_extended_state chan ta (s,z) =
    print_discrete_state chan ta s;
    Printf.fprintf chan "%s " (MDbm.Dbm.to_string z)
  
  (* indirection *)
  let print_timed_automaton chan ta =
    BareTA.print_timed_automaton chan ta.t

  let transition_to_string ta (source, dbm, ulist, target) =
    let (_,guard,_,_) = List.find (fun (_, g, u, t) ->
      DS.equal target t && ulist = u && Dbm.UDbm.Dbm.equal dbm (guard_to_dbm ta source g))
    (BareTA.transitions_from ta.t source)
    in
    let buf = Buffer.create 128 in
    let out = Buffer.add_string buf in
    out "(";
    out (BareTA.state_to_string ta.t source);
    out ",";
    out (Ita.print_guard (clocks ta) guard);
    out ",";
    out (Ita.print_resets (clocks ta) ulist);
    out ",";
    out (BareTA.state_to_string ta.t target);
    out ")";
    Buffer.contents buf

  let from_file filename _ ?scale:(scale=1) ?enlarge:(enlarge=0) () =
    {
      t = BareTA.from_file filename;
      lu_tbl = DSHashtbl.create 1024;
      m_tbl = DSHashtbl.create 1024;
    }
end