reachability.ml 18.8 KB
Newer Older
mcolange's avatar
mcolange committed
1 2
open Common
open TimedAutomaton
3
open Varcontext
mcolange's avatar
mcolange committed
4

5 6
let print_path = ref false

mcolange's avatar
mcolange committed
7 8 9 10 11
(** An abstract type for zone abstractions *)
module type ABSTRACTION =
sig
  (* the abstract type for a possible additional argument *)
  type arg_t
12
  type dbm_t
mcolange's avatar
mcolange committed
13

14
  val extrapolate : dbm_t -> arg_t -> unit
mcolange's avatar
mcolange committed
15 16 17 18 19
end

(** ID abstraction
 *)
module ID_abstraction (TA : TIMED_AUTOMATON) :
20
  ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
mcolange's avatar
mcolange committed
21
              and type dbm_t := TA.MDbm.Dbm.t =
mcolange's avatar
mcolange committed
22 23 24 25 26 27 28 29
struct
  type arg_t = TA.timed_automaton * TA.discrete_state

  let extrapolate _ _ = ()
end

(** LU abstraction
 *)
30
module Extra_LU (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t) :
31
  ABSTRACTION with type arg_t = TA.timed_automaton * TA.discrete_state
mcolange's avatar
mcolange committed
32
              and type dbm_t := TA.MDbm.Dbm.t =
mcolange's avatar
mcolange committed
33 34 35 36
struct
  type arg_t = TA.timed_automaton * TA.discrete_state

  let extrapolate zone (ta, loc) =
mcolange's avatar
mcolange committed
37
    let (lbounds, ubounds) = TA.lu_bounds ta loc in
38
    Udbml_unpriced.Dbm.extrapolate_lu_bounds zone lbounds ubounds
mcolange's avatar
mcolange committed
39 40 41 42 43 44 45 46 47 48 49 50

end

(** An abstract type for zone inclusion test *)
(** In fact the inclusion module should take responsibility of the storage of
 *  visited zones, as search for a stored zone that compares favorably to a
 *  newly encountered one is crucial performance-wise.
 *)
module type INCLUSION =
sig
  (* the abstract type for a possible additional argument *)
  type arg_t
51
  type dbm_t
52
  module TA : TIMED_AUTOMATON
mcolange's avatar
mcolange committed
53

54
  val inclusion : arg_t -> dbm_t -> dbm_t -> bool
55 56

  val get_arg : TA.timed_automaton -> TA.discrete_state -> arg_t
mcolange's avatar
mcolange committed
57 58 59 60
end

(** Vanilla inclusion *)
module Inclusion (TA : TIMED_AUTOMATON) :
61
  INCLUSION with type dbm_t := TA.MDbm.Dbm.t and module TA := TA =
mcolange's avatar
mcolange committed
62
struct
63
  type arg_t = unit
mcolange's avatar
mcolange committed
64

mcolange's avatar
mcolange committed
65
  let inclusion _ = TA.MDbm.Dbm.leq
66 67

  let get_arg _ _ = ()
mcolange's avatar
mcolange committed
68 69 70 71 72 73 74 75 76 77
end

(** Smart inclusion test, based on (insert reference here)
 *  According to Theorem 32, we have the following equivalence
 *  (L and U are global, not per location)
 *        not (Z \subseteq a_{LU}(Z'))
 *  iff   \exists x,y   such that   Z_{x,0} \geq (\leq, - U_x)
 *                            and   Z'_{x,y} < Z_{x,y}
 *                            and   Z'_{x,y} + (<, - L_y) < Z_{x,0}
 *)
78
module Sri (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t) :
79
  INCLUSION with type dbm_t := TA.MDbm.Dbm.t and module TA := TA =
mcolange's avatar
mcolange committed
80
struct
81
  type arg_t = Udbml.Carray.t * Udbml.Carray.t
mcolange's avatar
mcolange committed
82

83
  let inclusion (lbounds, ubounds) z1 z2 =
84
    Udbml_unpriced.Dbm.closure_leq lbounds ubounds z1 z2
85 86 87

  let get_arg ta loc = TA.lu_bounds ta loc

mcolange's avatar
mcolange committed
88 89
end

90 91 92 93 94
(** Smart inclusion test for priced zones (my original work)
 *  for every valuation z in the LHS, there exists a z' in the RHS which is
 *  equivalent, and whose cost is greater or arbitrarily close to equal
 *)
module PricedExp (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_priced.PDbm.t) :
95
  INCLUSION with type dbm_t := TA.MDbm.Dbm.t and module TA := TA =
96
struct
97
  type arg_t = Udbml.Carray.t
98

99
  let inclusion mbounds z1 z2 =
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
    let res = Udbml_priced.PDbm.square_inclusion_exp z1 z2 mbounds in
    (* control => res *)
    assert(
      let control = Udbml_priced.PDbm.leq z1 z2 in
      if (control && (not res)) then
        begin
          (* print the problematic zones *)
          Printf.printf "M = [%s]\n" (Udbml.Carray.to_string mbounds);
          Printf.printf "z1 =\n %s" (Udbml_priced.PDbm.to_string z1);
          Printf.printf "z2 =\n %s" (Udbml_priced.PDbm.to_string z2);
          flush stdout;
          false
        end
      else true);
    res
115 116

  let get_arg ta loc = TA.m_bounds ta loc
117 118
end

119 120 121
(* a helper type to avoid redundant verbosity in WALK_ORDER implementations *)
type 'a _path = ('a * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * 'a) list

mcolange's avatar
mcolange committed
122 123 124
(** An abstract type for the walk order of a graph *)
(** TODO  Operations returning unit are very imperative style...
 *        but efficiency should prevail
125 126
 *  TODO  Make a functor that takes a TA and returns a
 *        WALK_ORDER with type dbm_t := TA.Dbm.t
mcolange's avatar
mcolange committed
127 128 129
 *)
module type WALK_ORDER =
sig
130
  type key (* key to store dbm, i.e. discrete part of states *)
131
  type t
132
  type arg_t (* type of the additional argument to the comparison function *)
133

134 135 136 137 138 139 140 141 142
  type dbm_t (* type of dbm *)

  (* a path is a list of transitions
   * a transition is a quadruple of:
     * discrete state (i.e. key)
     * guard, as an unpriced dbm
     * clock updates list
     * discrete state (i.e. key)
   *)
143
  type path = key _path
144

145
  val create : unit -> t
Maximilien Colange's avatar
Maximilien Colange committed
146 147 148 149 150
  val add_to_waiting : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t * arg_t * path -> unit
  val is_in_passed : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t * arg_t -> bool
  val add_to_passed : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t * arg_t -> unit
  val get_next : t -> key * dbm_t * arg_t * path
  val is_done : t -> bool
151 152

  val clean : (dbm_t -> bool) -> t -> unit
Maximilien Colange's avatar
Maximilien Colange committed
153
  val waiting_length : t -> int
mcolange's avatar
mcolange committed
154 155
end

156 157 158 159 160 161
module type WaitOrderedType =
sig
  type t
  val compare : t -> t -> int
end

mcolange's avatar
mcolange committed
162 163
(** An abstract type for a container to store the nodes yet to explore.
 *  This implements the order in which nodes are explored.
164 165
 *  Takes an ordered type as argument, although the comparison does not really
 *  need to be a total order.
mcolange's avatar
mcolange committed
166 167
 *)
module type WAIT_CONTAINER =
168
  functor (Elem : WaitOrderedType) ->
mcolange's avatar
mcolange committed
169
sig
170
  type t
mcolange's avatar
mcolange committed
171

172 173 174 175 176
  val create : unit -> t
  val push : Elem.t -> t -> unit
  val pop : t -> Elem.t
  val is_empty : t -> bool
  val length : t -> int
mcolange's avatar
mcolange committed
177 178
end

179 180 181
module type BEST =
  functor (TA : TIMED_AUTOMATON) ->
    functor (COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t) ->
182 183
      WaitOrderedType
        with type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path
184 185 186 187 188 189 190 191 192 193 194 195

(** A module to compare two states in the waiting list by their infimum cost *)
module BestCost : BEST =
  functor (TA : TIMED_AUTOMATON) ->
    functor (COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t) ->
struct
  type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path

  let compare (_,z1,_,_) (_,z2,_,_) = TA.MDbm.Dbm.is_best z1 z2
end

(** A module to compare two states in the waiting list by their priority *)
196 197 198
module HighPrio : BEST =
  functor (TA : TIMED_AUTOMATON) ->
    functor (COMP : INCLUSION with type dbm_t := TA.MDbm.Dbm.t) ->
199 200 201 202 203 204 205
struct
  type t = TA.discrete_state * TA.MDbm.Dbm.t * COMP.arg_t * TA.discrete_state _path

  let compare (s1,_,_,_) (s2,_,_,_) = TA.priority_compare s1 s2
end


mcolange's avatar
mcolange committed
206 207
(** Builds an effective walk order, given a WAIT_CONTAINER and an INCLUSION.
 *)
208
module Walk_Order (ContFun : WAIT_CONTAINER)
209
                  (Key : Hashtbl.HashedType)
mcolange's avatar
mcolange committed
210
                  (BDbm : Dbm.BIG_IDBM)
211
                  (COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
212
                  (Best : WaitOrderedType with type t = Key.t * BDbm.Dbm.t * COMP.arg_t * Key.t _path)
213
  : WALK_ORDER with type key = Key.t and type dbm_t := BDbm.Dbm.t and type arg_t := COMP.arg_t =
mcolange's avatar
mcolange committed
214
struct
215 216 217

  module KeyHashtbl = Hashtbl.Make(Key)

mcolange's avatar
mcolange committed
218
  type dbm_list = BDbm.Dbm.t list ref
219
  type key = KeyHashtbl.key
220
  (* cf. WALK_ORDER signature *)
221
  type path = key _path
mcolange's avatar
mcolange committed
222

223 224
  module Cont = ContFun(Best)
  
225
  type t = dbm_list KeyHashtbl.t * Cont.t
226 227

  let create () = (KeyHashtbl.create 1024, Cont.create ())
mcolange's avatar
mcolange committed
228

229
  let find_or_add : dbm_list KeyHashtbl.t -> key -> dbm_list =
mcolange's avatar
mcolange committed
230
    fun h -> fun x ->
231
      try KeyHashtbl.find h x
mcolange's avatar
mcolange committed
232
      with Not_found ->
233
        incr Stats.number_of_discrete_states;
mcolange's avatar
mcolange committed
234
        let y = ref [] in
235
        KeyHashtbl.add h x y;
mcolange's avatar
mcolange committed
236 237
        y

Maximilien Colange's avatar
Maximilien Colange committed
238
  let add_to_waiting _ (_, waiting) s = Cont.push s waiting
239

Maximilien Colange's avatar
Maximilien Colange committed
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
  let is_in_passed comp (passed, _) (l, z, a) =
    let bucket = find_or_add passed l in
    List.exists (fun x -> comp a z x) !bucket

  let add_to_passed comp (passed, waiting) (l, z, a) =
      (* TODO it is the responsibility of the Stats module to print stat infos *)
      incr Stats.states_explored;
      if ((!Stats.states_explored mod Stats.modulo) = 0) then (
        Printf.printf "we have explored %d states, %d in the waiting list\r" !Stats.states_explored (Cont.length waiting);
        flush stdout
      );
      let bucket = find_or_add passed l in
      let old_size = List.length !bucket in
      let is_incomp x = not (comp a x z) in
      bucket := z :: (List.filter is_incomp !bucket);
      incr Stats.states_seen;
      if (old_size < List.length !bucket) then
        Stats.max_states := !Stats.max_states - old_size + List.length !bucket

  let get_next (_, waiting) = Cont.pop waiting

  let is_done (_, waiting) = Cont.is_empty waiting

  let waiting_length (_, waiting) = Cont.length waiting

  let clean pred (passed, waiting) =
    let size_before = ref 0 in
    let size_after = ref 0 in
    let predaux z =
      let res = pred z in
      incr size_before;
      if (res) then incr size_after;
      res
    in
    KeyHashtbl.iter (fun _ -> fun bucket -> bucket := List.filter predaux !bucket;) passed;
    Printf.printf "cleaning: shrink from %d states to %d states stored\n" !size_before !size_after;
    Printf.printf "still %d states waiting for treatment\n" (Cont.length waiting);
    flush stdout

end

281
module Walk_Order_Opt (ContFun : WAIT_CONTAINER)
Maximilien Colange's avatar
Maximilien Colange committed
282 283 284
                      (Key : Hashtbl.HashedType)
                      (BDbm : Dbm.BIG_IDBM)
                      (COMP : INCLUSION with type dbm_t := BDbm.Dbm.t)
285
                      (Best : WaitOrderedType with type t = Key.t * BDbm.Dbm.t * COMP.arg_t * Key.t _path)
Maximilien Colange's avatar
Maximilien Colange committed
286 287 288 289
  : WALK_ORDER with type key = Key.t and type dbm_t := BDbm.Dbm.t and type arg_t := COMP.arg_t =
struct

  module KeyHashtbl = Hashtbl.Make(Key)
290

Maximilien Colange's avatar
Maximilien Colange committed
291 292 293
  type dbm_list = BDbm.Dbm.t list ref
  type key = KeyHashtbl.key
  (* cf. WALK_ORDER signature *)
294 295 296
  type path = key _path
  
  module Cont = ContFun(Best)
297
  type t = dbm_list KeyHashtbl.t * Cont.t
Maximilien Colange's avatar
Maximilien Colange committed
298 299 300 301 302 303 304 305 306 307 308

  let create () = (KeyHashtbl.create 1024, Cont.create ())

  let find_or_add : dbm_list KeyHashtbl.t -> key -> dbm_list =
    fun h -> fun x ->
      try KeyHashtbl.find h x
      with Not_found ->
        incr Stats.number_of_discrete_states;
        let y = ref [] in
        KeyHashtbl.add h x y;
        y
309

Maximilien Colange's avatar
Maximilien Colange committed
310 311 312 313 314
  let add_to_waiting comp (passed, waiting) (l, z, a, p) =
    let bucket = find_or_add passed l in
    if (not (List.exists (fun x -> comp a z x) !bucket)) then
      begin
        Cont.push (l, z, a, p) waiting;
315
        let old_size = List.length !bucket in
316
        let is_incomp x = not (comp a x z) in
317 318 319 320
        bucket := z :: (List.filter is_incomp !bucket);
        incr Stats.states_seen;
        if (old_size < List.length !bucket) then
          Stats.max_states := !Stats.max_states - old_size + List.length !bucket
Maximilien Colange's avatar
Maximilien Colange committed
321
      end
mcolange's avatar
mcolange committed
322

Maximilien Colange's avatar
Maximilien Colange committed
323 324
  let is_in_passed _ (passed, _) (l, z, _) =
    let bucket = find_or_add passed l in
325
    not (List.memq z !bucket)
mcolange's avatar
mcolange committed
326

Maximilien Colange's avatar
Maximilien Colange committed
327 328 329 330 331 332 333
  let add_to_passed _ (_, waiting) _ =
    (* TODO it is the responsibility of the Stats module to print stat infos *)
    incr Stats.states_explored;
    if ((!Stats.states_explored mod Stats.modulo) = 0) then (
      Printf.printf "we have explored %d states, %d in the waiting list\r" !Stats.states_explored (Cont.length waiting);
      flush stdout
    )
mcolange's avatar
mcolange committed
334

Maximilien Colange's avatar
Maximilien Colange committed
335
  let get_next (_, waiting) = Cont.pop waiting
mcolange's avatar
mcolange committed
336

Maximilien Colange's avatar
Maximilien Colange committed
337
  let is_done (_, waiting) = Cont.is_empty waiting
mcolange's avatar
mcolange committed
338

Maximilien Colange's avatar
Maximilien Colange committed
339
  let waiting_length (_, waiting) = Cont.length waiting
Maximilien Colange's avatar
Maximilien Colange committed
340

Maximilien Colange's avatar
Maximilien Colange committed
341
  let clean pred (passed, waiting) =
342 343 344 345 346 347 348 349
    let size_before = ref 0 in
    let size_after = ref 0 in
    let predaux z =
      let res = pred z in
      incr size_before;
      if (res) then incr size_after;
      res
    in
Maximilien Colange's avatar
Maximilien Colange committed
350
    KeyHashtbl.iter (fun _ -> fun bucket -> bucket := List.filter predaux !bucket) passed;
351
    Printf.printf "cleaning: shrink from %d states to %d states stored\n" !size_before !size_after;
Maximilien Colange's avatar
Maximilien Colange committed
352
    Printf.printf "still %d states waiting for treatment\n" (Cont.length waiting);
353
    flush stdout
mcolange's avatar
mcolange committed
354 355 356 357 358 359 360
end


(** Other walk orders will probably require some knowledge about the states,
 *  and will thus be functors of TIMED_AUTOMATON *)
module TA_RG_WALK =
  functor (TA : TIMED_AUTOMATON) ->
361 362 363
    functor (ABS : ABSTRACTION
      with type arg_t = TA.timed_automaton * TA.discrete_state
      and type dbm_t := TA.MDbm.Dbm.t) ->
mcolange's avatar
mcolange committed
364
        functor (COMP : INCLUSION
365 366 367 368 369 370
          with type dbm_t := TA.MDbm.Dbm.t
          and module TA := TA) ->
            functor (WO : WALK_ORDER
              with type key = TA.discrete_state
              and type dbm_t := TA.MDbm.Dbm.t
              and type arg_t := COMP.arg_t) ->
mcolange's avatar
mcolange committed
371
struct
372

mcolange's avatar
mcolange committed
373 374
  module Dbm = TA.MDbm.Dbm
  module Fed = TA.MDbm.Fed
375

376 377 378 379 380 381 382 383 384
  module DSHashtbl = Hashtbl.Make(TA.DS)

  let transitions_cache = DSHashtbl.create 1024

  (** Auxiliary function that computes the list of successors of an
   *  extended state.
   *  Not intended to be called from the outside.
   *  TODO is returning succs in a list the most efficient way?
   *)
385
  let rec succ_zone ta (loc, zone) path = 
386 387 388 389 390
    let transition_list =
      try
        DSHashtbl.find transitions_cache loc
      with
      | Not_found ->
391 392
          let tlist0 = TA.transitions_from ta loc in
          let tlist = List.map (fun (s,g,u,t) -> (s,g,u,t,COMP.get_arg ta t)) tlist0
393 394 395 396 397
          in
          DSHashtbl.add transitions_cache loc tlist;
          tlist
    in
    List.fold_left
398
      (apply_single_transition ta (loc, zone) None path)
399
      [] transition_list
mcolange's avatar
mcolange committed
400

401 402 403
  and apply_single_transition =
    fun ta -> fun (sloc, szone) -> fun global_invariant -> fun path ->
      fun succs_list -> fun (source, guard, resets, target, target_arg) ->
404
    assert(TA.DS.equal sloc source);
405 406 407 408 409 410
    let result_zone = Dbm.to_fed (Dbm.copy szone) in
    Fed.intersect result_zone guard;
    if (Fed.is_empty result_zone) then
      succs_list
    else (
      List.iter (fun (c, v) -> Fed.update_value result_zone c v) resets;
Maximilien Colange's avatar
Maximilien Colange committed
411
      if (not (TA.is_urgent_or_committed ta target)) then (
412
        Fed.up result_zone (TA.rate_of_state ta target);
Maximilien Colange's avatar
Maximilien Colange committed
413
      );
414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432
      Fed.intersect result_zone (TA.invariant_of_discrete_state ta target);
      (match global_invariant with
      | None -> ()
      | Some inv -> Fed.intersect result_zone inv);
      if (Fed.is_empty result_zone) then
        succs_list
      else (
        Fed.iter result_zone (fun z -> ABS.extrapolate z (ta, target));
        let new_path = (source, guard, resets, target) :: path in
        if (TA.is_urgent_or_committed ta target) then
          let tmp = ref [] in
          Fed.iter result_zone (fun z -> tmp := !tmp @ (succ_zone ta (target, z) new_path));
          !tmp @ succs_list
        else
          (target, target_arg, result_zone, new_path) :: succs_list
      )
    )


mcolange's avatar
mcolange committed
433 434 435 436 437 438 439
  (* Auxiliary recursive function, not to call from the outside *)
  (* TODO   how can we early return?
   *        result should belong to an ordered set S,
   *        res0 should be inf S and update_result should be increasing.
   *        if S has a maximal element, we can compare result to it
   *)
  let rec walk_aux dbm_comp wot succs update_result result =
Maximilien Colange's avatar
Maximilien Colange committed
440
    if (WO.is_done wot) then
mcolange's avatar
mcolange committed
441 442
      result
    else (
Maximilien Colange's avatar
Maximilien Colange committed
443 444 445 446 447 448
      let (statel, statez, arg, path) = WO.get_next wot in
      let (worth, new_res) = update_result wot result (statel, statez) path in
      if (worth && (not (WO.is_in_passed dbm_comp wot (statel, statez, arg)))) then (
        WO.add_to_passed dbm_comp wot (statel, statez, arg);
        List.iter (fun (loc,arg,fed,trans) ->
          Fed.iter fed (fun z -> WO.add_to_waiting dbm_comp wot (loc, z, arg, trans @ path))) (succs (statel, statez) [])
mcolange's avatar
mcolange committed
449 450 451 452 453
      );
      walk_aux dbm_comp wot succs update_result new_res
    )

  (* The real function to call *)
454
  let walk ta succ_zone update_result res0 =
455
    let dbm_comp a x y =
mcolange's avatar
mcolange committed
456
      incr Stats.inclusion_tests;
457
      let r = COMP.inclusion a x y in
mcolange's avatar
mcolange committed
458 459 460
      if (r) then (incr Stats.positive_inclusion_tests);
      r
    in
mcolange's avatar
mcolange committed
461
    let wot = WO.create () in
462 463
    let (init, zinit) = TA.initial_extended_state ta in
    let initfed = Fed.from_dbm zinit in
464
    Fed.up initfed (TA.rate_of_state ta init);
465 466 467
    Fed.intersect initfed (TA.invariant_of_discrete_state ta init);
    List.iter (fun z ->
        ABS.extrapolate z (ta, init);
Maximilien Colange's avatar
Maximilien Colange committed
468
        WO.add_to_waiting dbm_comp wot (init, z, COMP.get_arg ta init, [])
469
      ) (Fed.to_dbm initfed);
mcolange's avatar
mcolange committed
470 471
    walk_aux dbm_comp wot (succ_zone ta) update_result res0

472 473

  (* a helper function to turn a path into a string *)
474 475 476 477 478 479 480
  let path_to_string ta path = 
    if (!print_path) then
      List.fold_right 
        (fun t -> fun s -> s ^ "\n" ^ (TA.transition_to_string ta t))
        path ""
    else
      ""
481

mcolange's avatar
mcolange committed
482 483 484
end

module Reachability =
485
  functor (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_unpriced.Dbm.t) ->
486 487 488
    functor (ABS : ABSTRACTION
      with type arg_t = TA.timed_automaton * TA.discrete_state
      and type dbm_t := TA.MDbm.Dbm.t) ->
mcolange's avatar
mcolange committed
489
        functor (COMP : INCLUSION
490 491 492 493 494 495
          with type dbm_t := TA.MDbm.Dbm.t
          and module TA := TA) ->
            functor (WO : WALK_ORDER
              with type key = TA.discrete_state
              and type dbm_t := TA.MDbm.Dbm.t
              and type arg_t := COMP.arg_t) ->
mcolange's avatar
mcolange committed
496
struct
497
  type res_t = bool
498

499
  module Walker = TA_RG_WALK(TA)(ABS)(COMP)(WO)
mcolange's avatar
mcolange committed
500

501
  exception Found of WO.path
mcolange's avatar
mcolange committed
502

503
  let reach ta _ : res_t * WO.path =
504 505 506 507 508
    let update_result _ (current_result, _) (l, _) p =
      if (current_result || (TA.is_target ta l)) then
        raise (Found p)
      else
        (true, (false, []))
mcolange's avatar
mcolange committed
509 510 511
    in
    let result =
      try
512 513
        Walker.walk ta Walker.succ_zone update_result (false, [])
      with Found(path) -> (true, path)
mcolange's avatar
mcolange committed
514
    in
mcolange's avatar
mcolange committed
515
    Stats.print_stats ();
mcolange's avatar
mcolange committed
516
    result
517

518 519 520
  let to_string ta = function
    | (true,p) -> "Reachable!\nPath is\n" ^ (Walker.path_to_string ta p)
    | (false,_) -> "Not reachable..."
mcolange's avatar
mcolange committed
521 522
end

523 524
let pruning = ref false

mcolange's avatar
mcolange committed
525
module OptReachability =
526
  functor (TA : TIMED_AUTOMATON with type MDbm.dbm_t = Udbml_priced.PDbm.t) ->
527 528 529
    functor (ABS : ABSTRACTION
      with type arg_t = TA.timed_automaton * TA.discrete_state
      and type dbm_t := TA.MDbm.Dbm.t) ->
530
        functor (COMP : INCLUSION
531 532 533 534 535 536
          with type dbm_t := TA.MDbm.Dbm.t
          and module TA := TA) ->
            functor (WO : WALK_ORDER
              with type key = TA.discrete_state
              and type dbm_t := TA.MDbm.Dbm.t
              and type arg_t := COMP.arg_t) ->
mcolange's avatar
mcolange committed
537
struct
538

539
  module Walker = TA_RG_WALK(TA)(ABS)(COMP)(WO)
540

541
  type res_t = int
542

543
  let reach ta v0 : res_t * WO.path =
544
    let update_result wo (current_opt, current_path) = fun (l,z) -> fun p ->
545
      let inf = Udbml_priced.PDbm.infimum z in
546
      let worth = if (!pruning) then inf < current_opt else true in
547
      let res =
548
        if (TA.is_target ta l && inf < current_opt) then (
549
          Printf.printf "new optimal value %d replaces %d, found after seeing %d states\n" inf current_opt !Stats.states_explored;
550
          Printf.printf "corresponding path has length %d\n" (List.length p);
551 552 553 554 555
          if (!pruning) then begin
            WO.clean (fun x -> Udbml_priced.PDbm.infimum x < inf) wo;
            (* trigger the GC after cleaning the WO, to reclaim memory *)
            Gc.full_major ()
          end;
556 557
          inf, p
        ) else current_opt, current_path
558
      in (worth, res)
559
    in
560
    let result = Walker.walk ta Walker.succ_zone update_result (v0, []) in
561 562 563
    Stats.print_stats ();
    result

564 565
  let to_string ta (res,path) =
    if (res = Dbm.PDbm.Dbm.infty) then
566
      "Not reachable..."
567
    else
568
      Printf.sprintf "%d\nPath is\n%s" res (Walker.path_to_string ta path)
mcolange's avatar
mcolange committed
569 570 571

end