Commit f8441922 authored by Ocan Sankur's avatar Ocan Sankur

Removed unnecessary Dbm.copy's

parent f1b3035d
......@@ -446,13 +446,13 @@ struct
let result_zone' = Fed.create (Fed.dimension result_zone) in
Fed.iter result_zone (fun z ->
ABS.extrapolate z (ta, target);
Fed.add_dbm result_zone' (Dbm.copy z)
Fed.add_dbm result_zone' z
);
let result_zone = result_zone' in
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));
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
......@@ -474,7 +474,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, (Dbm.copy z), arg, trans @ path))) (succs (statel, statez) [])
Fed.iter fed (fun z -> WO.add_to_waiting dbm_comp wot (loc, z, arg, trans @ path))) (succs (statel, statez) [])
);
walk_aux dbm_comp wot succs update_result new_res
)
......
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