timedAutomaton.ml 7.34 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
  type timed_automaton =
    {
      t : BareTA.ta;
98
      clocks : VarContext.t;
99 100 101 102 103
      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
104
  
105
  (* indirection *)
106
  let clocks ta = ta.clocks
107 108 109 110 111 112 113 114 115 116
  (* 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
117

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

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

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

208
  let model =
209 210 211 212 213 214
    let ta = BareTA.model in
    let clocks = VarContext.create () in
    for i = 1 to BareTA.nb_clocks ta do
      let j = VarContext.add clocks (BareTA.string_of_clock ta i) in
      assert(i = j)
    done;
215 216 217 218 219 220
    (* the reference clock *)
    let _ =
      try
        VarContext.add clocks "t(0)"
      with Var_already_defined -> -1 (* OK, uppaalta already defines t(0) *)
    in
221
    {
222
      t = BareTA.model;
223
      clocks = clocks;
224 225 226
      lu_tbl = DSHashtbl.create 1024;
      m_tbl = DSHashtbl.create 1024;
    }
227

mcolange's avatar
mcolange committed
228 229
end