Commit 5d1c687c authored by Benoît Barbot's avatar Benoît Barbot
Browse files

progress

parent e3ef678a
Pipeline #1645 failed with stages
in 34 seconds
......@@ -29,12 +29,15 @@ module Make(Sem:Semantic.S) = struct
| StateListFull -> fprintf outfile "%a\t%i@." print_state st 1
| Debug ->
fprintf outfile "%a@.\t[%a]@." print_state st (fun f l ->
List.iter (fun tr ->
let weight,_,_ = tr.ZoneGraph.weight.(i) in
let w = eval_poly_state_full st weight in
let low = Sem.Bt.eval_max_bound st tr.ZoneGraph.lower_bound
and up = Sem.Bt.eval_min_bound st tr.ZoneGraph.upper_bound in
fprintf f " [%c]-[%g;%g]--(%a)->%g " tr.ZoneGraph.action low up P.print weight w
List.iter (fun tr ->
let low = Sem.Bt.eval_max_bound st tr.ZoneGraph.lower_bound
and up = Sem.Bt.eval_min_bound st tr.ZoneGraph.upper_bound in
if Array.length tr.ZoneGraph.weight >0 then
let weight,_,_ = tr.ZoneGraph.weight.(i) in
let w = eval_poly_state_full st weight in
fprintf f " [%c]-[%g;%g]--(%a)->%g " tr.ZoneGraph.action low up P.print weight w
else
fprintf f " [%c]-[%g;%g] " tr.ZoneGraph.action low up;
) l) rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition
| Void | Timestamp | Timeword -> () in
let up_state_elapsed st i = match ost with
......@@ -44,9 +47,10 @@ module Make(Sem:Semantic.S) = struct
let t2= int_of_float time in
trajectory := (let ap,tt = !trajectory in 2* ap + t2, tt+.time);
match ost with
| Debug ->
let weight,cdf,_ = tr.ZoneGraph.weight.(i) in
fprintf outfile "((%a)/(%a))->%f[%c]\n" P.print cdf P.print weight time tr.ZoneGraph.action
| Debug when Array.length tr.ZoneGraph.weight >0 ->
let weight,cdf,_ = tr.ZoneGraph.weight.(i) in
fprintf outfile "((%a)/(%a))->%f[%c]\n" P.print cdf P.print weight time tr.ZoneGraph.action
| Debug -> fprintf outfile "->%f[%c]\n" time tr.ZoneGraph.action
| Timestamp -> fprintf outfile "%f\t" time
| Timeword | TimewordState -> fprintf outfile "%f[%c] " time tr.ZoneGraph.action
| StateListFull -> fprintf outfile "\t%i@." (int_of_char tr.ZoneGraph.action)
......
......@@ -55,7 +55,7 @@ type 'a transChoice = Label of 'a | Rand of float | Fixed
module type S =
sig
module P:WeightStructure
module Bt:BoundType
module Bt:ZoneGraphInput.BoundType
val t : P.var
......@@ -102,7 +102,7 @@ sig
end
exception Zero_derivative
module Make (Bt: BoundType) (P: WeightStructure) = struct
module Make (Bt: ZoneGraphInput.BoundType) (P: WeightStructure) = struct
module P=P
module Bt=Bt
open P
......
......@@ -221,3 +221,32 @@ module Make (Bt:BoundType) =
if verbose>0 then printf " [%.2fs]@." (check_time ());
zone_graph_from_ta ~verbose ~print_rg ~splitting_debug ta
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
let split_to_zg ta split taz =
let split_reach = split taz in
Forward_reach.Bfs.to_zone_graph ta split_reach
end
module GeneralBound = struct
type t = Common.bound list
type state = int * float array
let get_bound x = assert false
let zero = [Const 0]
let map v = List.map (Common.SBound.map v)
let print vx f l = List.iter (Common.SBound.print vx f) l
let eval_min_bound st = List.fold_left (fun m b -> min m (Common.SBound.eval st b)) infinity
let eval_max_bound st = List.fold_left (fun m b -> min m (Common.SBound.eval st b)) 0.0
let split_to_zg ta _ taz =
Forward_reach.Bfs.to_zone_graph_no_split ta taz
end
......@@ -39,17 +39,7 @@ let halton base index =
!r
module PX = Polynome.Make (Fl.Float) (struct let var_string=[|"x",false|] end)
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
let split_to_zg _ _ _ = {ZoneGraph.init=0; nb_poly=0; statelist =[||]; var_string=[||]; cardclocks=0; alphabet=[||]; printer = (fun _ _ -> ()) }
end) (PX)
module SX = Semantic.Make (ZoneGraphInput.LinearBound) (PX)
let phi =1.61803398874989484820458683436563
let phi2=1.32471795724474602596090885447809
......
......@@ -22,9 +22,9 @@ with this program; if not, write to the Free Software Foundation, Inc.,
open Common
module ZGI = ZoneGraphInput.Make (ZoneGraphInput.LinearBound)
(*Building the zone graph *)
let rg = ZoneGraphInput.input_zone_graph ~verbose:0 Sys.argv.(1)
let rg = ZGI.input_zone_graph ~verbose:0 Sys.argv.(1)
let poly = if Array.length Sys.argv >2 then int_of_string Sys.argv.(2) else 4
......@@ -38,19 +38,7 @@ module Weight = ExpPoly.Make(P)(struct
end)
(* Build the functionnal iterator module based on the polynomial ring *)
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)
module FunIt = Semantic.Make (ZoneGraphInput.LinearBound) (Weight)
let compute_weight rg =
let svar = P.var_of_int (P.nb_var-1) in
......
......@@ -46,37 +46,12 @@ let precomp_exists =
then printf "Precomputation file found ! [%.2f]@." (check_time ())
else printf "Precomputation file found but file have change discard !@.")
!infile !frequency !npoly !rational_impl
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
let split_to_zg ta split taz =
let split_reach = split taz in
Forward_reach.Bfs.to_zone_graph ta split_reach
end
module GeneralBound = struct
type t = Common.bound list
type state = int * float array
let get_bound x = assert false
let zero = [Const 0]
let map v = List.map (Common.SBound.map v)
let print vx f l = List.iter (Common.SBound.print vx f) l
let eval_min_bound st = List.fold_left (fun m b -> min m (Common.SBound.eval st b)) infinity
let eval_max_bound st = List.fold_left (fun m b -> min m (Common.SBound.eval st b)) 0.0
let split_to_zg ta _ taz =
Forward_reach.Bfs.to_zone_graph_no_split ta taz
end
module ZGI = (val if !npoly<0 then (module (ZoneGraphInput.Make (GeneralBound)):ZoneGraphInput.S )
else (module (ZoneGraphInput.Make(LinearBound)):ZoneGraphInput.S ))
module Bound = (val if !npoly<0 then (module ZoneGraphInput.GeneralBound:ZoneGraphInput.BoundType )
else (module ZoneGraphInput.LinearBound ))
module ZGI = ZoneGraphInput.Make (Bound)
(*Building the zone graph *)
let rgopt =
......@@ -101,13 +76,13 @@ module Weight = (val if !frequency =0.0 then (module P:Semantic.WeightStructure)
end)))
(* Build the functionnal iterator module based on the polynomial ring *)
module FunIt = Semantic.Make (GeneralBound) (Weight)
module FunIt = Semantic.Make (Bound) (Weight)
(* Compute Weight and distribution as polynomials *)
let rgpoly =
match precomp_exists,rgopt with
| Some rg,_ -> rg
| _,Some rg ->
match precomp_exists, rgopt, !npoly>=0 with
| Some rg,_,_ -> rg
| _, Some rg, true ->
if !verbose>0 then (
printf "Computing Distribution -> %i: [" !npoly; flush stdout;
print_flush ()
......@@ -116,14 +91,15 @@ let rgpoly =
rg !npoly in
if !verbose>0 then printf "] [%.2fs]@." (check_time ());
rgp
| None,None -> assert false
| _, Some rg, false -> snd @@ FunIt.iterate_functionnal rg 0
| None,None,_ -> assert false
let _ =
ZoneGraphInput.save_precomputation !infile rgpoly !frequency !npoly !rational_impl;
if !print_rg then begin
printf "%a@." (ZoneGraph.print SBound.print) rgpoly;
printf "%a@." (ZoneGraph.print Bound.print) rgpoly;
let fdot = open_out ((Filename.chop_extension !infile)^".dot") in
ZoneGraph.print_dot rgpoly SBound.print (Format.formatter_of_out_channel fdot);
ZoneGraph.print_dot rgpoly Bound.print (Format.formatter_of_out_channel fdot);
close_out fdot
end
......@@ -134,7 +110,8 @@ module M = MainLoop.Make(FunIt)
let _ =
(* Compute template if not provided *)
let template_word = match !sampling_meth with
Exact -> Array.make !npoly (Semantic.Fixed,Semantic.Fixed)
Exact when !npoly>=0 -> Array.make !npoly (Semantic.Fixed,Semantic.Fixed)
| Exact (*receding 3*)-> Array.make 3 (Semantic.Fixed,Semantic.Fixed)
| Receding x -> Array.make x (Semantic.Fixed,Semantic.Fixed)
| Driven l -> Array.of_list l 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