Compute and print the path leading to the result.

src/dbm.ml

@@ -14,6 +14,7 @@ sig
   val infty : int
   val is_empty : t -> bool
   val leq : t -> t -> bool
+  val equal : t -> t -> bool
 
   val to_fed : t -> fed_t
 

src/reachability.ml

@@ -108,17 +108,26 @@ end
  *)
 module type WALK_ORDER =
 sig
-  type key
+  type key (* key to store dbm, i.e. discrete part of states *)
   type t
-  type arg_t
+  type arg_t (* type of the additional argument to the comparison function *)
 
-  type dbm_t
+  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)
+   *)
+  type path = (key * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * key) list
 
   val create : unit -> t
   val mark : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t -> unit
   val is_marked : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * dbm_t -> bool
-  val add : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * arg_t * dbm_t -> unit
-  val get_next : t -> key * dbm_t
+  val add : (arg_t -> dbm_t -> dbm_t -> bool) -> t -> key * arg_t * dbm_t * path -> unit
+  val get_next : t -> (key * dbm_t) * path
   val finished : t -> bool
 
   val clean : (dbm_t -> bool) -> t -> unit
@@ -152,9 +161,12 @@ struct
 
   type dbm_list = BDbm.Dbm.t list ref
   type key = KeyHashtbl.key
-  type t = dbm_list KeyHashtbl.t * (key * BDbm.Dbm.t) Cont.t
+  (* cf. WALK_ORDER signature *)
+  type path = (key * Dbm.UDbm.Dbm.t * ((clock_t * int) list) * key) list
 
-  let create () = (KeyHashtbl.create 1000, Cont.create ())
+  type t = dbm_list KeyHashtbl.t * (key * BDbm.Dbm.t * path) Cont.t
+
+  let create () = (KeyHashtbl.create 1024, Cont.create ())
 
   let find_or_add : dbm_list KeyHashtbl.t -> key -> dbm_list =
     fun h -> fun x ->
@@ -171,10 +183,10 @@ struct
     let bucket = KeyHashtbl.find v l in
     not (List.mem z !bucket)
 
-  let add comp (v, t) (l, a, z) =
+  let add comp (v, t) (l, a, z, p) =
       let bucket = find_or_add v l in
       if (not (List.exists (fun x -> comp a z x) !bucket)) then (
-        Cont.push (l, z) t;
+        Cont.push (l, z, p) t;
         let old_size = List.length !bucket in
         let is_incomp x = not (comp a x z) in
         bucket := z :: (List.filter is_incomp !bucket);
@@ -183,7 +195,7 @@ struct
           Stats.max_states := !Stats.max_states - old_size + List.length !bucket
       )
 
-  let get_next (_, t) = Cont.pop t
+  let get_next (_, t) = let a,b,c = Cont.pop t in (a,b),c
 
   let finished (_, t) = 
 (*    Printf.printf "%d waiting\n" (Cont.length t); *)
@@ -250,7 +262,7 @@ struct
         succs_list
       else (
         Fed.iter result_zone (fun z -> ABS.extrapolate z (ta, target));
-        (target, target_arg, result_zone) :: succs_list
+        (target, target_arg, result_zone, (source, guard, resets, target)) :: succs_list
       )
     )
 
@@ -289,8 +301,8 @@ struct
     if (WO.finished wot) then
       result
     else (
-      let state = WO.get_next wot in
-      let (worth,new_res) = update_result wot result state in
+      let (state, path) = WO.get_next wot in
+      let (worth,new_res) = update_result wot result state path in
       if (worth && (not (WO.is_marked dbm_comp wot state))) then (
         WO.mark dbm_comp wot state;
         incr Stats.states_explored;
@@ -298,7 +310,7 @@ struct
           Printf.printf "we have explored %d states, %d in the waiting list\r" !Stats.states_explored (WO.waiting_length wot);
           flush stdout
         );
-        let add (loc,arg,fed) = Fed.iter fed (fun z -> WO.add dbm_comp wot (loc, arg, z))
+        let add (loc,arg,fed,trans) = Fed.iter fed (fun z -> WO.add dbm_comp wot (loc, arg, z, trans::path))
         in
         List.iter add (succs state)
       );
@@ -320,7 +332,7 @@ struct
     Fed.intersect initfed (TA.invariant_of_discrete_state ta init);
     List.iter (fun z ->
         ABS.extrapolate z (ta, init);
-        WO.add dbm_comp wot (init, COMP.get_arg ta init, z)
+        WO.add dbm_comp wot (init, COMP.get_arg ta init, z, [])
       ) (Fed.to_dbm initfed);
     walk_aux dbm_comp wot (succ_zone ta) update_result res0
 
@@ -348,7 +360,7 @@ struct
   let reach ta : res_t =
     let update_result _ = function
       | true -> raise Found
-      | false -> fun (l, _) ->
+      | false -> fun (l, _) -> fun _ ->
           if (TA.is_target ta l) then
             raise Found
           else
@@ -380,37 +392,47 @@ module OptReachability =
               and type dbm_t := TA.MDbm.Dbm.t
               and type arg_t := COMP.arg_t) ->
 struct
-  type res_t = int option
 
   module Walker = TA_RG_WALK(TA)(ABS)(COMP)(WO)
 
+  type res_t = (int * string) option
+
   let reach ta : res_t =
-    let update_result wo current_opt = fun (l,z) ->
+    let update_result wo (current_opt, current_path) = fun (l,z) -> fun p ->
       let inf = Udbml_priced.PDbm.infimum z in
       let worth = inf < current_opt in
       let res =
         if (TA.is_target ta l && inf < current_opt) then (
           Printf.printf "new optimal value %d replaces %d, found after seeing %d states\n" inf current_opt !Stats.states_explored;
+          Printf.printf "corresponding path has length %d\n" (List.length p);
           WO.clean (fun x -> Udbml_priced.PDbm.infimum x < inf) wo;
           (* trigger the GC after cleaning the WO, to reclaim memory *)
           Gc.full_major ();
-          inf
-        ) else current_opt
+          inf, p
+        ) else current_opt, current_path
       in (worth, res)
     in
-    let res = Walker.walk ta Walker.succ_zone update_result Dbm.PDbm.Dbm.infty in
+    let (res, path) = Walker.walk ta Walker.succ_zone update_result (Dbm.PDbm.Dbm.infty, []) in
     let result = 
       if (res = Dbm.PDbm.Dbm.infty) then
         None
-      else
-        Some res
+      else begin
+        let path_string =
+          List.fold_right
+            (fun t -> fun s ->
+              let ss = TA.transition_to_string ta t in
+              s ^ "\n" ^ ss)
+            path ""
+        in
+        Some (res, path_string)
+      end
     in
     Stats.print_stats ();
     result
 
   let to_string = function
     | None -> "not reachable..."
-    | Some x -> Printf.sprintf "%d" x
+    | Some (x,s) -> Printf.sprintf "%d with path\n%s" x s
 
 end
 

src/timedAutomaton.ml

@@ -36,6 +36,8 @@ sig
   val print_transition : 'b BatIO.output -> timed_automaton -> transition -> unit
   val print_timed_automaton : 'b BatIO.output -> timed_automaton -> unit
   val print_extended_state : 'b BatIO.output -> 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
 
@@ -698,6 +700,16 @@ struct
   let transitions_from ta state =
     List.map (fun tr -> transition_fields ta tr) (_transitions_from ta state)
 
+  let transition_to_string ta (source, dbm, ulist, target) =
+    let res = List.find
+      (fun trans ->
+        let (_, d, u, t) = transition_fields ta trans in
+        is_state_equal target t && ulist = u && UDbm.Dbm.equal dbm d)
+      (_transitions_from ta source)
+    in
+    string_of_transition ta res
+
+
   let is_urgent_or_committed ta state =
     let rec aux ar n =
       if (ar.(n).locCommitted || ar.(n).locUrgent) then true