timedAutomaton.ml 6.89 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
33 34 35

  (* the loaded model *)
  val model : timed_automaton
mcolange's avatar
mcolange committed
36 37
end

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 70 71
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
72 73 74 75 76 77 78 79
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

80 81
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
82
struct
83
  module DS =
84
    struct
85
      type t = BareTA.state
86

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

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

95 96 97 98 99 100 101 102
  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
103
  
104 105 106 107 108 109 110 111 112 113 114 115
  (* 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
116

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

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

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

207
  let model =
208
    {
209
      t = BareTA.model;
210 211 212
      lu_tbl = DSHashtbl.create 1024;
      m_tbl = DSHashtbl.create 1024;
    }
213

mcolange's avatar
mcolange committed
214 215
end