timedAutomaton.ml 7.04 KB
Newer Older
mcolange's avatar
mcolange committed
1
open Common
mcolange's avatar
mcolange committed
2
open Dbm
3
open Varcontext
mcolange's avatar
mcolange committed
4 5 6

module type TIMED_AUTOMATON =
sig
mcolange's avatar
mcolange committed
7
  module MDbm : BIG_IDBM
8

mcolange's avatar
mcolange committed
9 10
  type timed_automaton
  type discrete_state
11
  type edge
mcolange's avatar
mcolange committed
12

13 14
  module DS : Hashtbl.HashedType with type t = discrete_state

15
  val clocks : timed_automaton -> VarContext.t
16
  val priority_compare : discrete_state -> discrete_state -> int
mcolange's avatar
mcolange committed
17
  val initial_extended_state : timed_automaton -> discrete_state * MDbm.Dbm.t
18 19
  val transitions_from : timed_automaton -> discrete_state ->
    (discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state) list
20
  val invariant_of_discrete_state : timed_automaton -> discrete_state -> UDbm.Dbm.t
mcolange's avatar
mcolange committed
21 22
  val is_urgent_or_committed : timed_automaton -> discrete_state -> bool
  val is_target : timed_automaton -> discrete_state -> bool
Maximilien Colange's avatar
Maximilien Colange committed
23
  val rate_of_state : timed_automaton -> discrete_state -> int
mcolange's avatar
mcolange committed
24
  val lu_bounds : timed_automaton -> discrete_state -> Udbml.Carray.t * Udbml.Carray.t
25
  val m_bounds : timed_automaton -> discrete_state -> Udbml.Carray.t
mcolange's avatar
mcolange committed
26
  val global_m_bounds : timed_automaton -> int array
mcolange's avatar
mcolange committed
27
  (** print functions *)
28 29 30
  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
31 32
  val transition_to_string : timed_automaton ->
    (discrete_state * UDbm.Dbm.t * ((clock_t * int) list) * discrete_state) -> string
mcolange's avatar
mcolange committed
33
  val from_file : string -> string -> ?scale:int -> ?enlarge:int -> unit -> timed_automaton
mcolange's avatar
mcolange committed
34 35
end

36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
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

mcolange's avatar
mcolange committed
70 71 72 73 74 75 76 77
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

78 79
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 =
mcolange's avatar
mcolange committed
80
struct
81
  module DS =
82
    struct
83
      type t = BareTA.state
84

85 86
      let hash = BareTA.hash_state
      let equal = BareTA.equal_state
87
    end
mcolange's avatar
mcolange committed
88

89
  module MDbm = MDbm
mcolange's avatar
mcolange committed
90
  
91
  module DSHashtbl = Hashtbl.Make(DS)
mcolange's avatar
mcolange committed
92

93 94 95 96 97 98 99 100
  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 *)
mcolange's avatar
mcolange committed
101
  
102 103 104 105 106 107 108 109 110 111 112 113
  (* 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
Maximilien Colange's avatar
Maximilien Colange committed
114

mcolange's avatar
mcolange committed
115 116
  let initial_extended_state ta =
    let dim = (VarContext.size (clocks ta)) in
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
    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     
    
140
  let transitions_from ta state =
141 142 143 144
    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)
mcolange's avatar
mcolange committed
145

146 147
  (* store LU bounds in their C form, to avoid repeated translations *)
  let lu_bounds ta s =
mcolange's avatar
mcolange committed
148
    try
149 150 151 152 153 154 155 156 157 158 159
      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 =
160
    try
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
      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 =
Maximilien Colange's avatar
Maximilien Colange committed
177
    Printf.fprintf chan "%s" (BareTA.string_of_state ta.t s)
mcolange's avatar
mcolange committed
178
  
179 180 181 182 183
  let print_extended_state chan ta (s,z) =
    print_discrete_state chan ta s;
    Printf.fprintf chan "%s " (MDbm.Dbm.to_string z)
  
  (* indirection *)
mcolange's avatar
mcolange committed
184
  let print_timed_automaton chan ta =
185
    BareTA.print_timed_automaton chan ta.t
186

187 188 189 190
  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)
191
    in
192 193 194
    let buf = Buffer.create 128 in
    let out = Buffer.add_string buf in
    out "(";
Maximilien Colange's avatar
Maximilien Colange committed
195
    out (BareTA.string_of_state ta.t source);
196 197 198 199 200
    out ",";
    out (Ita.print_guard (clocks ta) guard);
    out ",";
    out (Ita.print_resets (clocks ta) ulist);
    out ",";
Maximilien Colange's avatar
Maximilien Colange committed
201
    out (BareTA.string_of_state ta.t target);
202 203 204
    out ")";
    Buffer.contents buf

205
  let from_file filename queryname ?scale:(scale=1) ?enlarge:(enlarge=0) () =
206
    {
207
      t = BareTA.from_file filename queryname ~scale:scale ~enlarge:enlarge ();
208 209 210
      lu_tbl = DSHashtbl.create 1024;
      m_tbl = DSHashtbl.create 1024;
    }
mcolange's avatar
mcolange committed
211 212
end