Commit 33fc78d4 authored by Benoît Barbot's avatar Benoît Barbot
Browse files

progress

parent 79c4e79d
Pipeline #1641 passed with stages
in 41 seconds
......@@ -59,7 +59,7 @@ sig
val iterate_functionnal :
?update:(unit -> unit) ->
'a ZoneGraph.t -> int -> P.t array * P.t ZoneGraph.t
'a ZoneGraph.bt -> int -> P.t array * P.t ZoneGraph.bt
val find_root :
?factor:float ->
?max_iter:int ->
......@@ -71,31 +71,31 @@ sig
exception Deadlock of state
val eval_bound : state -> Common.bound -> float
val state_of_float : state -> int * P.F.t array
val init : int ZoneGraph.t -> state
val init : int ZoneGraph.bt -> state
val print_state : Format.formatter -> state -> unit
val eval_poly_state : state -> P.t -> P.t
val eval_poly_state_full : state -> P.t -> float
val elapse_time : state -> float -> state
val fire : state -> 'b ZoneGraph.transition -> state
val fire : state -> 'b ZoneGraph.bound_transition -> state
val sample_time :
?max_iter:int ->
int ->
state -> P.t ZoneGraph.transition -> float -> float
state -> P.t ZoneGraph.bound_transition -> float -> float
val available_trans :
'a ZoneGraph.t -> int * 'b -> 'a ZoneGraph.transition list
'a ZoneGraph.bt -> int * 'b -> 'a ZoneGraph.bound_transition list
val sample_trans :
P.t ZoneGraph.t ->
P.t ZoneGraph.bt ->
int ->
state ->
?tolerance:float ->
?filter:(float * float -> P.t ZoneGraph.transition -> bool) option ->
float -> P.t ZoneGraph.transition
?filter:(float * float -> P.t ZoneGraph.bound_transition -> bool) option ->
float -> P.t ZoneGraph.bound_transition
val sample_traj :
max_iter:int ->
update_callback:(unit -> 'a) * ((state -> int -> 'b) *
(state -> int -> 'c) *
(float -> P.t ZoneGraph.transition -> int -> 'd)) ->
P.t ZoneGraph.t ->
(float -> P.t ZoneGraph.bound_transition -> int -> 'd)) ->
P.t ZoneGraph.bt ->
(float transChoice * ZoneGraph.l transChoice) array ->
samplers:(int -> float) * (int -> float) -> unit
end
......@@ -105,7 +105,7 @@ module Make (P: WeightStructure) = struct
module P=P
open P
open ZoneGraph
type t = P.t ZoneGraph.t
type t = P.t ZoneGraph.bt
let t = var_of_int 0
......
......@@ -38,7 +38,7 @@ sig
val iterate_functionnal :
?update:(unit -> unit) ->
'a ZoneGraph.t -> int -> P.t array * P.t ZoneGraph.t
'a ZoneGraph.bt -> int -> P.t array * P.t ZoneGraph.bt
val find_root :
?factor:float ->
?max_iter:int ->
......@@ -50,31 +50,31 @@ sig
exception Deadlock of state
val eval_bound : state -> Common.bound -> float
val state_of_float : state -> int * P.F.t array
val init : int ZoneGraph.t -> state
val init : int ZoneGraph.bt -> state
val print_state : Format.formatter -> state -> unit
val eval_poly_state : state -> P.t -> P.t
val eval_poly_state_full : state -> P.t -> float
val elapse_time : state -> float -> state
val fire : state -> 'b ZoneGraph.transition -> state
val fire : state -> 'b ZoneGraph.bound_transition -> state
val sample_time :
?max_iter:int ->
int ->
state -> P.t ZoneGraph.transition -> float -> float
state -> P.t ZoneGraph.bound_transition -> float -> float
val available_trans :
'a ZoneGraph.t -> int * 'b -> 'a ZoneGraph.transition list
'a ZoneGraph.bt -> int * 'b -> 'a ZoneGraph.bound_transition list
val sample_trans :
P.t ZoneGraph.t ->
P.t ZoneGraph.bt ->
int ->
state ->
?tolerance:float ->
?filter:(float * float -> P.t ZoneGraph.transition -> bool) option ->
float -> P.t ZoneGraph.transition
?filter:(float * float -> P.t ZoneGraph.bound_transition -> bool) option ->
float -> P.t ZoneGraph.bound_transition
val sample_traj :
max_iter:int ->
update_callback:(unit -> 'a) * ((state -> int -> 'b) *
(state -> int -> 'c) *
(float -> P.t ZoneGraph.transition -> int -> 'd)) ->
P.t ZoneGraph.t ->
(float -> P.t ZoneGraph.bound_transition -> int -> 'd)) ->
P.t ZoneGraph.bt ->
(float transChoice * ZoneGraph.l transChoice) array ->
samplers:(int -> float) * (int -> float) -> unit
end
......
......@@ -29,33 +29,36 @@ type miniedge={
prob: float
}
type 'a transition ={
type ('a,'b) transition ={
action: l;
miniedge : miniedge list;
lower_bound : bound;
upper_bound : bound;
lower_bound : 'b;
upper_bound : 'b;
is_contained_in_zone : bool;
mutable weight: ('a * 'a * 'a) array;
}
type 'a loczone = {
type ('a,'b) loczone = {
name : string;
id : int;
redcoord: int list list;
transition : 'a transition list;
transition : ('a,'b) transition list;
clockmap : int array;
}
type 'a t = {
type ('a,'b) t = {
init: int;
nb_poly: int;
statelist: 'a loczone array;
statelist: ('a,'b) loczone array;
var_string : (string*bool) array;
cardclocks: int;
alphabet: l array;
printer: Format.formatter -> 'a -> unit
}
type 'a bound_transition = ('a,bound) transition
type 'a bt = ('a,bound) t
let print_reset vs f m =
let first = ref true in
Format.fprintf f "@[[%a]@]" (fun o a ->
......
......@@ -68,8 +68,8 @@ let save_precomputation file rg frequency npoly exact_rational =
close_out fd
(* Computing the reachability graph and then split it *)
let reachability_splitting ~verbose ~print_rg ~splitting_debug ta =
(* Computing the reachability graph *)
let reachability ~verbose ~print_rg ~splitting_debug ta =
(* Compute forward reachability zone graph *)
if verbose >0 then (printf "Computing forward reachability graph ... ";
print_flush (););
......@@ -92,13 +92,18 @@ let reachability_splitting ~verbose ~print_rg ~splitting_debug ta =
if verbose >0 then (
printf "%i states found. [%.2fs]@.Splitting reachability graph ... "
printf "%i states found. [%.2fs]@."
(Hashtbl.length reach) (check_time ());
print_flush ());
if print_rg then printf "Forward Reach : @.%a@." (Forward_reach.Bfs.print_reach_graph ta) reach;
Forward_reach.Bfs.print_split_graph ?debug:tex_out 0 reach;
tex_out,reach
(* Split the reachability graph *)
(* Split the reachability graph and export it to zone graphe *)
let splitting ~verbose ~print_rg ta (tex_out,reach) =
if verbose >0 then (
printf "Splitting reachability graph ... ";
print_flush ());
let split_reach = try
Forward_reach.Bfs.split ?debug:tex_out reach
with x -> eprintf "Fail to split the reachability graph. "; raise x in
......@@ -112,9 +117,25 @@ let reachability_splitting ~verbose ~print_rg ~splitting_debug ta =
if verbose >0 then printf "%i states found. [%.2fs]@." (Hashtbl.length split_reach) (check_time ());
if print_rg then printf "After split : @.%a@." (Forward_reach.Bfs.print_reach_graph ta) split_reach;
(*Transform into Zone graph suitable for volume computation *)
Forward_reach.Bfs.to_zone_graph ta split_reach
split_reach
let zone_graph_from_ta ?(verbose=1)
?(print_rg=false)
?(splitting_debug="")
?export_zone_graph ta =
if print_rg then TimedAutomaton.Uautomaton.print_timed_automaton stdout ta;
let reach = reachability ~verbose ~print_rg ~splitting_debug ta in
let split_reach = splitting ~verbose ~print_rg ta reach in
let rg =Forward_reach.Bfs.to_zone_graph ta split_reach in
if print_rg then Format.printf "%a@." ZoneGraph.print rg;
(match export_zone_graph with
None -> ()
| Some s -> let f = open_out s in
let ff = formatter_of_out_channel f in
Format.fprintf ff "ptavalue= %a@." ZoneGraph.print rg;
close_out f);
rg
let input_zone_graph ?verbose:(verbose=1)
?print_rg:(print_rg=false)
?splitting_debug:(splitting_debug="")
......@@ -146,25 +167,14 @@ let input_zone_graph ?verbose:(verbose=1)
with x -> eprintf "Fail to build automaton. "; raise x
in
if verbose>0 then printf " [%.2fs]@." (check_time ());
if print_rg then TimedAutomaton.Uautomaton.print_timed_automaton stdout ta;
let rg = reachability_splitting ~verbose ~print_rg ~splitting_debug ta in
if print_rg then Format.printf "%a@." ZoneGraph.print rg;
(match export_zone_graph with
None -> ()
| Some s -> let f = open_out s in
let ff = formatter_of_out_channel f in
Format.fprintf ff "ptavalue= %a@." ZoneGraph.print rg;
close_out f);
rg
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ?export_zone_graph ta
| _ -> failwith ("Unkown file extension "^e)
let input_from_string ?verbose:(verbose=1)
?print_rg:(print_rg=false)
?splitting_debug:(splitting_debug="")
let input_from_string ?(verbose=1)
?(print_rg=false)
?(splitting_debug="")
file_content =
ignore @@ check_time ();
(* Input is a time automaton in prism file format *)
let ta = try
let pmod = PrismTrans.read_from_string file_content in
......@@ -174,7 +184,4 @@ let input_from_string ?verbose:(verbose=1)
with x -> eprintf "Fail to build automaton. "; raise x
in
if verbose>0 then printf " [%.2fs]@." (check_time ());
if print_rg then TimedAutomaton.Uautomaton.print_timed_automaton stdout ta;
let rg = reachability_splitting ~verbose ~print_rg ~splitting_debug ta in
if print_rg then Format.printf "%a@." ZoneGraph.print rg;
rg
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ta
......@@ -451,7 +451,7 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON ) =
let to_zone_graph_trans ta edge =
let to_zone_graph_trans to_bound ta edge =
let open ZoneGraph in
let n = Dbm.dimension edge.guard in
(*Dbm.remove_useless edge.guard;*)
......@@ -460,7 +460,7 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON ) =
prob= 1.0
} in
(*Format.printf "%a@." (fun f -> Dbm.pretty_print f (Model.clocks ta)) edge.guard;*)
let lower_bound,upper_bound = Dbm.get_lower_upper edge.guard in
let lower_bound,upper_bound = to_bound edge.guard in
{
action=edge.action;
miniedge = [me];
......@@ -470,7 +470,7 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON ) =
weight = Array.make 0 ((),(),());
}
let to_zone_graph_loczone ta (lz:zg_node) =
let to_zone_graph_loczone to_bound ta (lz:zg_node) =
Format.fprintf Format.str_formatter "@[<h>%a@]" (fun o -> Model.print_extended_state o ta) (lz.disc_state,lz.entry_zone) ;
let trim_edge = List.filter (fun e -> e.target.edges <> []) lz.edges in
let open ZoneGraph in
......@@ -479,15 +479,15 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON ) =
id = lz.id;
redcoord = Dbm.get_reduced_coordinate lz.entry_zone;
clockmap = Array.make 0 0;
transition = List.map (to_zone_graph_trans ta) trim_edge
transition = List.map (to_zone_graph_trans to_bound ta) trim_edge
}
let to_zone_graph ta full_stateset =
let to_zone_graph_aux to_bound ta full_stateset =
let stateset = remove_empty full_stateset in
let size = Hashtbl.length stateset in
let init = Hashtbl.find stateset 0 in
let statelist = Array.make size (to_zone_graph_loczone ta init) in
Hashtbl.iter (fun _ loczone -> statelist.(loczone.id)<-to_zone_graph_loczone ta loczone) stateset;
let statelist = Array.make size (to_zone_graph_loczone to_bound ta init) in
Hashtbl.iter (fun _ loczone -> statelist.(loczone.id)<-to_zone_graph_loczone to_bound ta loczone) stateset;
let vcontext = Model.clocks ta in
let nclock = Uta.VarContext.size vcontext in
let var_string = Array.init (1+ nclock) (function
......@@ -508,6 +508,10 @@ module ExactReachability (Model : TimedAutomaton.TIMED_AUTOMATON ) =
printer = (fun _ _ -> ())
}
let to_zone_graph = to_zone_graph_aux Dbm.get_lower_upper
let to_zone_graph_no_split = to_zone_graph_aux Dbm.get_lower_upper_no_split
end
open TimedAutomaton
......
......@@ -70,6 +70,7 @@ sig
val minus : t -> t -> t list
val is_splitted : t -> bool
val get_lower_upper : t -> Common.bound * Common.bound
val get_lower_upper_no_split : t -> Common.bound list * Common.bound list
val remove_useless: t -> unit
val split_guard : t -> t list * int list
val get_reduced_coordinate: t -> int list list
......@@ -901,7 +902,29 @@ module SplitableDBM =
with Break b -> b end in
low,up
let get_lower_upper_no_split mdbm =
(* Not sure for close guard *)
close_guard mdbm;
remove_useless mdbm;
let dim = dimension mdbm in
let low = ref [] in
for i= 1 to dim-1 do
if not @@ Alg.is_infty mdbm.(0).(i) then
begin if Alg.is_zero mdbm.(0).(i) then
low := (Common.Const 0) :: !low
else
low := (Common.build_bound (abs (Alg.to_int mdbm.(0).(i))) i) :: !low
end
done;
let up = ref [] in
for i= 1 to dim-1 do
if not @@ Alg.is_infty mdbm.(i).(0) then begin
up := (Common.build_bound (abs (Alg.to_int mdbm.(i).(0))) i) :: !up
end
done;
!low, !up
end
end
module Guard = SplitableDBM
......@@ -99,9 +99,9 @@ struct
clocks : string VarContext.t;
vars : string VarContext.t;
init : discrete_state;
mutable query : query;
(* mutable query : query;
mutable lowerLU : int array array array;
mutable upperLU : int array array array;
mutable upperLU : int array array array;*)
guards_tbl : (_succinct_transition,Dbm.t) Hashtbl.t;
invars_tbl : (location array,Dbm.t) Hashtbl.t;
}
......@@ -350,7 +350,7 @@ struct
let is_committed state =
Array.exists (fun loc -> loc.locCommitted) state.stateLocs
let is_target ta state =
(* let is_target ta state =
let rec eval = function
| AtomicQuery(s) ->
Array.exists (fun loc -> loc.locName = s) state.stateLocs
......@@ -360,9 +360,9 @@ struct
in
match ta.query with
EmptyQuery -> true
| ReachQuery(pq) -> eval pq
| ReachQuery(pq) -> eval pq*)
let lu_bounds ta state lbounds ubounds =
(*let lu_bounds ta state lbounds ubounds =
Array.iteri (fun i _ ->
lbounds.(i) <- Pdbm.minfty_val;
ubounds.(i) <- Pdbm.minfty_val
......@@ -377,7 +377,7 @@ struct
lbounds.(cl) <- max lbounds.(cl) ta.lowerLU.(iproc).(iloc).(cl);
ubounds.(cl) <- max ubounds.(cl) ta.upperLU.(iproc).(iloc).(cl);
done;
done
done*)
let is_urgent_or_committed ta state =
Array.exists (fun loc -> loc.locCommitted || loc.locUrgent) state.stateLocs
......@@ -1023,9 +1023,9 @@ struct
clocks = clocks;
vars = vars;
init = {stateLocs = initLocs; stateVars = initVars};
query = EmptyQuery;
(*query = EmptyQuery;
lowerLU = [||];
upperLU = [||];
upperLU = [||];*)
guards_tbl = Hashtbl.create 1024;
invars_tbl = Hashtbl.create 1024
}
......
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