Commit 4445daee authored by Ocan Sankur's avatar Ocan Sankur

Always copying the iterated dbm inside Fed.iter

parent 53b01430
......@@ -55,7 +55,7 @@ module WSTS_WO (Key : Hashtbl.HashedType)
(Best : WaitOrderedType with type t = Key.t * BDbm.Dbm.t * COMP.arg_t * Key.t _path)
: 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)
type dbm_list = BDbm.Dbm.t list ref
......
......@@ -39,6 +39,7 @@ sig
val is_empty : t -> bool
val set_empty : t -> unit
val add_dbm : t -> dbm_t -> unit
(* TODO replace this with an iterator *)
val to_dbm : t -> dbm_t list
......@@ -95,7 +96,7 @@ struct
let to_dbm t =
let res = ref [] in
iter t (fun z -> res := z :: !res);
iter t (fun z -> res := (Dbm.copy z) :: !res);
!res
let intersect t z = intersect_dbm t z
......@@ -127,6 +128,7 @@ struct
f
let is_best z1 z2 = compare (infimum z1) (infimum z2)
end
and Fed : FED =
struct
......
......@@ -75,7 +75,8 @@ let main() =
let res = Options.verify (module MC) in
Printf.printf "Result of verification is %s\n" res;
if (!show_gc_stats) then
Gc.print_stat stdout
Gc.print_stat stdout;;
let _ = main ()
open Common
open TimedAutomaton
open Varcontext
open Printf
open Dbm
let print_path = ref false
......@@ -256,6 +258,7 @@ struct
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
......@@ -324,7 +327,7 @@ struct
let bucket = find_or_add passed l in
not (List.memq z !bucket)
let add_to_passed _ (_, waiting) _ =
let add_to_passed _ (_, waiting) (_,z,_) =
(* 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 (
......@@ -382,7 +385,8 @@ struct
* Not intended to be called from the outside.
* TODO is returning succs in a list the most efficient way?
*)
let rec succ_zone ta (loc, zone) path =
let rec succ_zone ta (loc, zone) path =
let transition_list =
try
DSHashtbl.find transitions_cache loc
......@@ -397,38 +401,37 @@ struct
List.fold_left
(apply_single_transition ta (loc, zone) None path)
[] transition_list
and apply_single_transition =
fun ta -> fun (sloc, szone) -> fun global_invariant -> fun path ->
fun succs_list -> fun (source, guard, resets, target, target_arg) ->
assert(TA.DS.equal sloc source);
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;
if (not (TA.is_urgent_or_committed ta target)) then (
Fed.up result_zone (TA.rate_of_state ta target);
);
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
)
)
assert(TA.DS.equal sloc source);
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;
if (not (TA.is_urgent_or_committed ta target)) then (
Fed.up result_zone (TA.rate_of_state ta target);
);
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, Dbm.copy z) new_path));
!tmp @ succs_list
else
(target, target_arg, result_zone, new_path) :: succs_list
)
)
(* Auxiliary recursive function, not to call from the outside *)
(* TODO how can we early return?
......@@ -445,7 +448,7 @@ struct
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) [])
Fed.iter fed (fun z -> WO.add_to_waiting dbm_comp wot (loc, (Dbm.copy z), arg, trans @ path))) (succs (statel, statez) [])
);
walk_aux dbm_comp wot succs update_result new_res
)
......
open Printf
open Common
open Dbm
open Varcontext
......@@ -181,29 +182,29 @@ struct
let print_extended_state chan ta (s,z) =
print_discrete_state chan ta s;
Printf.fprintf chan "%s " (MDbm.Dbm.to_string z)
Printf.fprintf chan "\n%s " (MDbm.Dbm.to_string z)
(* indirection *)
let print_timed_automaton chan ta =
BareTA.print_timed_automaton chan ta.t
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)
in
let buf = Buffer.create 128 in
let out = Buffer.add_string buf in
out "(";
out (BareTA.string_of_state ta.t source);
out ",";
out (Ita.print_guard (BareTA.string_of_clock ta.t) guard);
out ",";
out (Ita.print_resets (BareTA.string_of_clock ta.t) ulist);
out ",";
out (BareTA.string_of_state ta.t target);
out ")";
Buffer.contents buf
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)
in
let buf = Buffer.create 128 in
let out = Buffer.add_string buf in
out "(";
out (BareTA.string_of_state ta.t source);
out ",";
out (Ita.print_guard (BareTA.string_of_clock ta.t) guard);
out ",";
out (Ita.print_resets (BareTA.string_of_clock ta.t) ulist);
out ",";
out (BareTA.string_of_state ta.t target);
out ")";
Buffer.contents buf
let model =
let ta = BareTA.model in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment