Commit 0b13eafe authored by Benoît Barbot's avatar Benoît Barbot
Browse files

generalize

parent 633e350e
Pipeline #1643 failed with stages
in 34 seconds
......@@ -32,8 +32,8 @@ module Make(Sem:Semantic.S) = struct
List.iter (fun tr ->
let weight,_,_ = tr.ZoneGraph.weight.(i) in
let w = eval_poly_state_full st weight in
let low = eval_bound st tr.ZoneGraph.lower_bound
and up = eval_bound st tr.ZoneGraph.upper_bound in
let low = Sem.Bt.eval_min_bound st tr.ZoneGraph.lower_bound
and up = Sem.Bt.eval_max_bound st tr.ZoneGraph.upper_bound in
fprintf f " [%c]-[%g;%g]--(%a)->%g " tr.ZoneGraph.action low up P.print weight w
) l) rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition
| Void | Timestamp | Timeword -> () in
......
......@@ -52,60 +52,74 @@ end
type 'a transChoice = Label of 'a | Rand of float | Fixed
module type BoundType = sig
type t
val zero : t
val print : VarSet.varset -> Format.formatter -> t -> unit
val map : int array -> t -> t
val get_bound : t -> Common.bound
type state = int *float array
val eval_min_bound : state -> t -> float
val eval_max_bound : state -> t -> float
end
module type S =
sig
module P:WeightStructure
module Bt:BoundType
val t : P.var
val iterate_functionnal :
?update:(unit -> unit) ->
'a ZoneGraph.bt -> int -> P.t array * P.t ZoneGraph.bt
('a,Bt.t) ZoneGraph.t -> int -> P.t array * (P.t,Bt.t) ZoneGraph.t
val find_root :
?factor:float ->
?max_iter:int ->
?bound:float * float -> P.t -> ?diffp:P.t -> P.var -> float -> float
type state (*= int * float array*)
type state = Bt.state (*= int * float array*)
val get_loc : state -> int
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.bt -> state
val init : (int,Bt.t) ZoneGraph.t -> 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.bound_transition -> state
val fire : state -> ('b,Bt.t) ZoneGraph.transition -> state
val sample_time :
?max_iter:int ->
int ->
state -> P.t ZoneGraph.bound_transition -> float -> float
state -> (P.t,Bt.t) ZoneGraph.transition -> float -> float
val available_trans :
'a ZoneGraph.bt -> int * 'b -> 'a ZoneGraph.bound_transition list
('a,Bt.t) ZoneGraph.t -> int * 'b -> ('a,Bt.t) ZoneGraph.transition list
val sample_trans :
P.t ZoneGraph.bt ->
(P.t,Bt.t) ZoneGraph.t ->
int ->
state ->
?tolerance:float ->
?filter:(float * float -> P.t ZoneGraph.bound_transition -> bool) option ->
float -> P.t ZoneGraph.bound_transition
?filter:(float * float -> (P.t,Bt.t) ZoneGraph.transition -> bool) option ->
float -> (P.t,Bt.t) ZoneGraph.transition
val sample_traj :
max_iter:int ->
update_callback:(unit -> 'a) * ((state -> int -> 'b) *
(state -> int -> 'c) *
(float -> P.t ZoneGraph.bound_transition -> int -> 'd)) ->
P.t ZoneGraph.bt ->
(float -> (P.t,Bt.t) ZoneGraph.transition -> int -> 'd)) ->
(P.t,Bt.t) ZoneGraph.t ->
(float transChoice * ZoneGraph.l transChoice) array ->
samplers:(int -> float) * (int -> float) -> unit
end
exception Zero_derivative
module Make (P: WeightStructure) = struct
module Make (Bt: BoundType) (P: WeightStructure) = struct
module P=P
module Bt=Bt
open P
open ZoneGraph
type t = P.t ZoneGraph.bt
type bt = Bt.t
type t = (P.t,bt) ZoneGraph.t
let t = var_of_int 0
......@@ -130,9 +144,9 @@ module Make (P: WeightStructure) = struct
(* Compute a primitive of the pdf *)
let primitive = primitive te_weight_reset t in
(* The cdf is the integral of the pdf between the lower bound and t *)
let cdf = primitive -.. (apply_bound primitive t trans.lower_bound) in
let cdf = primitive -.. (apply_bound primitive t (Bt.get_bound trans.lower_bound)) in
(* The weight is the cdf apply on the upper bound *)
let weight = apply_bound cdf t trans.upper_bound in
let weight = apply_bound cdf t (Bt.get_bound trans.upper_bound) in
(*Format.printf "[%i -> %i] weight = %a, " state.id edge.target P.print weighttarget;
Format.printf "pdf_med =%a, pdf = %a, " P.print weight_reset P.print te_weight_reset;
Format.printf "primitive = %a, cdf = %a, weight = %a @." P.print primitive P.print cdf P.print weight;*)
......@@ -143,7 +157,7 @@ module Make (P: WeightStructure) = struct
ZoneGraph.apply_functionnal rg i P.vector_space weight_operator stateweight
let iterate_functionnal ?update rg n =
let rgp =ZoneGraph.copy n P.zero P.print rg in
let rgp =ZoneGraph.copy n (Bt.zero,Bt.map) P.zero P.print rg in
let stateweight = ref @@ Array.map (fun _ -> P.const F.one) rgp.ZoneGraph.statelist in
for i=1 to n do
stateweight := weightsPdfCdf rgp (n-i) !stateweight;
......@@ -236,11 +250,6 @@ module Make (P: WeightStructure) = struct
let get_loc = fst
let eval_bound (_,clocks) =function
Infinite -> infinity
| Const a -> float a
| Finite (a,b) -> (float a) -. clocks.(VarSet.int_of_var b-1)
let init rg = rg.init,(Array.make rg.cardclocks 0.0)
let print_state f (id,tab) =
Format.fprintf f "@[%i @ @[%a@]@]" id
......@@ -272,8 +281,8 @@ module Make (P: WeightStructure) = struct
(* Sample firing time of transition trans using random number u*)
let sample_time ?max_iter:(max_iter=20) i state trans u =
let low = eval_bound state trans.lower_bound
and up = eval_bound state trans.upper_bound in
let low = Bt.eval_min_bound state trans.lower_bound
and up = Bt.eval_max_bound state trans.upper_bound in
assert (low <= up);
assert (0.0 <= low);
if Array.length trans.weight =0 then
......@@ -320,8 +329,8 @@ module Make (P: WeightStructure) = struct
None -> l
| Some ff ->
List.filter (fun tr ->
let low = eval_bound (id,tab) tr.lower_bound
and up = eval_bound (id,tab) tr.upper_bound in
let low = Bt.eval_min_bound (id,tab) tr.lower_bound
and up = Bt.eval_max_bound (id,tab) tr.upper_bound in
ff (low,up) tr) l
)
......
......@@ -31,52 +31,63 @@ type 'a transChoice = Label of 'a | Rand of float | Fixed
exception Zero_derivative
module type BoundType = sig
type t
val zero : t
val print : Common.VarSet.varset -> Format.formatter -> t -> unit
val map : int array -> t -> t
type state = int * float array
val get_bound : t -> Common.bound
val eval_min_bound : state -> t -> float
val eval_max_bound : state -> t -> float
end
module type S =
sig
module P:WeightStructure
val t : P.var
module Bt:BoundType
val t : P.var
val iterate_functionnal :
?update:(unit -> unit) ->
'a ZoneGraph.bt -> int -> P.t array * P.t ZoneGraph.bt
('a,Bt.t) ZoneGraph.t -> int -> P.t array * (P.t,Bt.t) ZoneGraph.t
val find_root :
?factor:float ->
?max_iter:int ->
?bound:float * float -> P.t -> ?diffp:P.t -> P.var -> float -> float
type state (*= int * float array*)
type state = int * float array
val get_loc : state -> int
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.bt -> state
val init : (int,Bt.t) ZoneGraph.t -> 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.bound_transition -> state
val fire : state -> ('b,Bt.t) ZoneGraph.transition -> state
val sample_time :
?max_iter:int ->
int ->
state -> P.t ZoneGraph.bound_transition -> float -> float
state -> (P.t,Bt.t) ZoneGraph.transition -> float -> float
val available_trans :
'a ZoneGraph.bt -> int * 'b -> 'a ZoneGraph.bound_transition list
('a,Bt.t) ZoneGraph.t -> int * 'b -> ('a,Bt.t) ZoneGraph.transition list
val sample_trans :
P.t ZoneGraph.bt ->
(P.t,Bt.t) ZoneGraph.t ->
int ->
state ->
?tolerance:float ->
?filter:(float * float -> P.t ZoneGraph.bound_transition -> bool) option ->
float -> P.t ZoneGraph.bound_transition
?filter:(float * float -> (P.t,Bt.t) ZoneGraph.transition -> bool) option ->
float -> (P.t,Bt.t) ZoneGraph.transition
val sample_traj :
max_iter:int ->
update_callback:(unit -> 'a) * ((state -> int -> 'b) *
(state -> int -> 'c) *
(float -> P.t ZoneGraph.bound_transition -> int -> 'd)) ->
P.t ZoneGraph.bt ->
(float -> (P.t,Bt.t) ZoneGraph.transition -> int -> 'd)) ->
(P.t,Bt.t) ZoneGraph.t ->
(float transChoice * ZoneGraph.l transChoice) array ->
samplers:(int -> float) * (int -> float) -> unit
end
module Make (P : WeightStructure) : S with type P.t = P.t and type P.var=P.var
module Make (Bt : BoundType) (P : WeightStructure) : S with type P.t = P.t and type P.var=P.var and type Bt.t=Bt.t and type Bt.state=Bt.state
......@@ -56,8 +56,8 @@ type ('a,'b) t = {
printer: Format.formatter -> 'a -> unit
}
type 'a bound_transition = ('a,bound) transition
type 'a bt = ('a,bound) t
(*type 'a bound_transition = ('a,bound) transition*)
(*type 'a bt = ('a,bound) t*)
let print_reset vs f m =
let first = ref true in
......@@ -81,9 +81,9 @@ let print_poly rg f t =
Format.fprintf f ", \"weight\":%a,@ \"cdf\":%a,@ \"pdf\":%a,@ " pl weight pl cdf pl pdf
let print_transition rg f t =
let print_transition rg pb f t =
let vs = rg.var_string in
Format.fprintf f "{@[<hov 2>@,\"action\":\"%c\",@ \"zone\":[%a ; %a], @ \"is_contained_in_zone\": %b,@ %a@ %a@ @]}" t.action (print_bound vs) t.lower_bound (print_bound vs) t.upper_bound t.is_contained_in_zone (print_miniedge_list vs) t.miniedge (print_poly rg) t
Format.fprintf f "{@[<hov 2>@,\"action\":\"%c\",@ \"zone\":[%a ; %a], @ \"is_contained_in_zone\": %b,@ %a@ %a@ @]}" t.action (pb vs) t.lower_bound (pb vs) t.upper_bound t.is_contained_in_zone (print_miniedge_list vs) t.miniedge (print_poly rg) t
let print_redcoord f rc =
Format.pp_print_list ~pp_sep:(fun o () -> Format.fprintf o ", ") (fun o l ->
......@@ -91,30 +91,30 @@ let print_redcoord f rc =
)) l
) f rc
let print_loczone rg f r =
Format.fprintf f "{@[<v 2>@ \"id\":%i,@ \"name\":@[<hov>\"%s\"@],@ \"redcoord\":[%a],@ \"clockmap\":[@[%a@]],@ \"transitions\":[@[<v 2>@ %a]@]@]@,}@ " r.id r.name print_redcoord r.redcoord (fun f -> Array.iter (fun x-> Format.fprintf f "%s; " (if x=0 then "0" else fst rg.var_string.(x)))) r.clockmap (Format.pp_print_list ~pp_sep:(fun f () -> Format.fprintf f ",@ ") (fun f g -> print_transition rg f g)) r.transition
let print_loczone rg pb f r =
Format.fprintf f "{@[<v 2>@ \"id\":%i,@ \"name\":@[<hov>\"%s\"@],@ \"redcoord\":[%a],@ \"clockmap\":[@[%a@]],@ \"transitions\":[@[<v 2>@ %a]@]@]@,}@ " r.id r.name print_redcoord r.redcoord (fun f -> Array.iter (fun x-> Format.fprintf f "%s; " (if x=0 then "0" else fst rg.var_string.(x)))) r.clockmap (Format.pp_print_list ~pp_sep:(fun f () -> Format.fprintf f ",@ ") (fun f g -> print_transition rg pb f g)) r.transition
let print f rg =
let print pb f rg =
Format.fprintf f "{@[<v 2>@ \"init\":%i,@ \"cardclocks\":%i,@ \"statelist\":[@ @[<v 2>%a@]@ ]@]}" rg.init rg.cardclocks
(fun f a -> Array.iteri (fun i state ->
if i>0 then Format.fprintf f ","; print_loczone rg f state) a) rg.statelist
if i>0 then Format.fprintf f ","; print_loczone rg pb f state) a) rg.statelist
let print_transition_dot rg f source t =
let print_transition_dot rg pb f source t =
match t.miniedge with
[m] ->
Format.fprintf f "l_%i -> l_%i [label=\"%c; [%a;%a];%a\"]@." source m.target t.action (print_bound rg) t.lower_bound (print_bound rg) t.upper_bound (print_reset rg) m
Format.fprintf f "l_%i -> l_%i [label=\"%c; [%a;%a];%a\"]@." source m.target t.action (pb rg) t.lower_bound (pb rg) t.upper_bound (print_reset rg) m
| _ -> ()
let print_loczone_dot rg f r =
Format.fprintf f "l_%i [shape=box, label=\"[%i] %s\"]@." r.id r.id r.name
let print_dot rg f =
let print_dot rg pb f =
Format.fprintf f "digraph D{@[<hov 2>@.";
Array.iter (fun lz -> print_loczone_dot rg f lz) rg.statelist;
Array.iter (fun lz ->
List.iter (fun tr ->
print_transition_dot rg.var_string f lz.id tr) lz.transition) rg.statelist;
print_transition_dot rg.var_string pb f lz.id tr) lz.transition) rg.statelist;
Format.fprintf f "@]}@."
......@@ -193,26 +193,26 @@ let toDisjointSet li m =
li
(* Build a new zone graph augmented with volumetric data*)
let copy_trans nbpoly clockmap zero tr =
let copy_trans nbpoly (z,f_map_bound) clockmap zero tr =
{ tr with
lower_bound= if tr.is_contained_in_zone then Const 0
else map_bound clockmap tr.lower_bound;
upper_bound= map_bound clockmap tr.upper_bound;
lower_bound= if tr.is_contained_in_zone then z
else f_map_bound clockmap tr.lower_bound;
upper_bound= f_map_bound clockmap tr.upper_bound;
weight=(Array.make nbpoly (zero,zero,zero));
}
let copy_loczone nbpoly cardclocks zero loczone =
let copy_loczone nbpoly fbt cardclocks zero loczone =
(* The var at index 0 is either the 'zero' clock or 't' -1 +1 to remember that*)
let disSet = toDisjointSet loczone.redcoord (cardclocks +1) in
let clockmap = Array.init (cardclocks+1) (fun i ->
if i =0 then 0
else Puf.find disSet i
) in
{ loczone with transition=List.map (copy_trans nbpoly clockmap zero) loczone.transition;
{ loczone with transition=List.map (copy_trans nbpoly fbt clockmap zero) loczone.transition;
clockmap=clockmap }
let copy nbpoly zero printer rg =
let copy nbpoly fbt zero printer rg =
{ rg with
nb_poly=nbpoly;
statelist=Array.map (copy_loczone nbpoly rg.cardclocks zero) rg.statelist;
statelist=Array.map (copy_loczone nbpoly fbt rg.cardclocks zero) rg.statelist;
printer }
let add_triplet (_,(+..),( **.)) (a,b,c) p (d,e,f) =
......
......@@ -127,12 +127,12 @@ let zone_graph_from_ta ?(verbose=1)
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;
if print_rg then Format.printf "%a@." (ZoneGraph.print Common.SBound.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;
Format.fprintf ff "ptavalue= %a@." (ZoneGraph.print Common.SBound.print) rg;
close_out f);
rg
......
......@@ -68,14 +68,21 @@ let is_time = function
let build_bound a b =
if b=0 then Const ( a) else Finite ( a,b)
let map_bound clockmap = function
module SBound = struct
let map clockmap = function
Infinite -> Infinite
| Const a -> Const a
| Finite (a,b) -> let c = clockmap.(b) in
if c <> 0 then Finite (a,c) else Const a
let print_bound vs f= function
let print vs f= function
Infinite -> Format.fprintf f "inf"
| Const (a) -> Format.fprintf f "%i" a
| Finite (0,b) -> Format.fprintf f "-%s" (fst vs.(b))
| Finite (a,b) -> Format.fprintf f "%i-%s" a (fst vs.(b))
let eval (_,clocks) = function
Infinite -> infinity
| Const a -> float a
| Finite (a,b) -> (float a) -. clocks.(VarSet.int_of_var b-1)
end
......@@ -38,5 +38,8 @@ module VarSet :
type bound = Finite of int * VarSet.var | Const of int | Infinite
val is_time : bound -> bool
val build_bound : int -> int -> bound
val map_bound : int array -> bound -> bound
val print_bound : VarSet.varset -> Format.formatter -> bound -> unit
module SBound : sig
val map : int array -> bound -> bound
val print : VarSet.varset -> Format.formatter -> bound -> unit
val eval: 'a * float array -> bound -> float
end
......@@ -39,7 +39,16 @@ let halton base index =
!r
module PX = Polynome.Make (Fl.Float) (struct let var_string=[|"x",false|] end)
module SX = Semantic.Make (PX)
module SX = Semantic.Make (struct
type t = Common.bound
let zero= Common.Const 0
let print _ _ _ = ()
let map _ a =a
type state = int * float array
let get_bound x = x
let eval_max_bound _ _ = 0.0
let eval_min_bound _ _ = 0.0
end) (PX)
let phi =1.61803398874989484820458683436563
let phi2=1.32471795724474602596090885447809
......
......@@ -37,7 +37,20 @@ module Weight = ExpPoly.Make(P)(struct
let svar= P.var_of_int (P.nb_var-1)
end)
(* Build the functionnal iterator module based on the polynomial ring *)
module FunIt = Semantic.Make (Weight)
module LinearBound = struct
type t = Common.bound
type state = int * float array
let get_bound x = x
let zero = Const 0
let map = Common.SBound.map
let print = Common.SBound.print
let eval_min_bound = Common.SBound.eval
let eval_max_bound = Common.SBound.eval
end
module FunIt = Semantic.Make (LinearBound) (Weight)
let compute_weight rg =
let svar = P.var_of_int (P.nb_var-1) in
......
......@@ -68,8 +68,20 @@ module Weight = (val if !frequency =0.0 then (module P:Semantic.WeightStructure)
let tvar = P.var_of_int 0
let svar= P.var_of_int (P.nb_var-1)
end)))
module LinearBound = struct
type t = Common.bound
type state = int * float array
let get_bound x = x
let zero = Const 0
let map = Common.SBound.map
let print = Common.SBound.print
let eval_min_bound = Common.SBound.eval
let eval_max_bound = Common.SBound.eval
end
(* Build the functionnal iterator module based on the polynomial ring *)
module FunIt = Semantic.Make (Weight)
module FunIt = Semantic.Make (LinearBound) (Weight)
(* Compute Weight and distribution as polynomials *)
let rgpoly =
......@@ -89,9 +101,9 @@ let rgpoly =
let _ =
ZoneGraphInput.save_precomputation !infile rgpoly !frequency !npoly !rational_impl;
if !print_rg then begin
printf "%a@." ZoneGraph.print rgpoly;
printf "%a@." (ZoneGraph.print SBound.print) rgpoly;
let fdot = open_out ((Filename.chop_extension !infile)^".dot") in
ZoneGraph.print_dot rgpoly (Format.formatter_of_out_channel fdot);
ZoneGraph.print_dot rgpoly SBound.print (Format.formatter_of_out_channel fdot);
close_out fdot
end
......
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