Commit 46b83a77 authored by Benoît Barbot's avatar Benoît Barbot
Browse files

some progress

parent c1b265fa
Pipeline #1648 passed with stages
in 42 seconds
...@@ -314,18 +314,24 @@ module Make (Bt: ZoneGraphInput.BoundType) (P: WeightStructure) = struct ...@@ -314,18 +314,24 @@ module Make (Bt: ZoneGraphInput.BoundType) (P: WeightStructure) = struct
(* All transitions *) (* All transitions *)
state.transition state.transition
(* filter them *) (* filter them *)
|> (fun l -> match filter with |> (fun l ->
None -> l let l2 = if rg.nb_poly <= 0 then
| Some ff -> List.filter (fun tr ->
List.filter (fun tr -> let low = Bt.eval_max_bound (id,tab) tr.lower_bound
let low = Bt.eval_max_bound (id,tab) tr.lower_bound and up = Bt.eval_min_bound (id,tab) tr.upper_bound in low <= up) l
and up = Bt.eval_min_bound (id,tab) tr.upper_bound in else l in
ff (low,up) tr) l match filter with
) None -> l2
| Some ff ->
List.filter (fun tr ->
let low = Bt.eval_max_bound (id,tab) tr.lower_bound
and up = Bt.eval_min_bound (id,tab) tr.upper_bound in
ff (low,up) tr) l2
)
(* compute weight *) (* compute weight *)
|> List.map (fun trans -> |> List.map (fun trans ->
if Array.length trans.weight =0 then if Array.length trans.weight <= 0 then
(*Isotropic sampling constant weight*) (*Isotropic sampling constant weight*)
1.0, trans 1.0, trans
else else
......
...@@ -245,7 +245,7 @@ module GeneralBound = struct ...@@ -245,7 +245,7 @@ module GeneralBound = struct
let map v = List.map (Common.SBound.map v) let map v = List.map (Common.SBound.map v)
let print vx f l = List.iter (Common.SBound.print vx f) l 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_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 eval_max_bound st = List.fold_left (fun m b -> max m (Common.SBound.eval st b)) 0.0
let split_to_zg ta _ taz = let split_to_zg ta _ taz =
Forward_reach.Bfs.to_zone_graph_no_split ta taz Forward_reach.Bfs.to_zone_graph_no_split ta taz
end end
......
...@@ -24,6 +24,8 @@ open Common ...@@ -24,6 +24,8 @@ open Common
open Format open Format
open Arguments open Arguments
(* Parsing Arguments *)
let _ = let _ =
Format.set_margin 190 Format.set_margin 190
...@@ -39,75 +41,73 @@ let _ = ...@@ -39,75 +41,73 @@ let _ =
Arg.usage spec_list_full usage_str; Arg.usage spec_list_full usage_str;
exit 1) exit 1)
(* Main *)
let precomp_exists =
if !print_rg then None else ZoneGraphInput.precomputation_exists
~debug:(fun b -> if !verbose>0 then if b
then printf "Precomputation file found ! [%.2f]@." (check_time ())
else printf "Precomputation file found but file have change discard !@.")
!infile !frequency !npoly !rational_impl
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 =
if precomp_exists = None then
Some (ZGI.input_zone_graph
~verbose:!verbose ~print_rg:!print_rg ~splitting_debug:!splitting_debug
?export_zone_graph:!export_zone_graph !infile)
else None
(* Build the polynomial ring *)
module R = (val if !rational_impl then (module Flq.Q :Fl.FSIG) else (module Fl.Float:Fl.FSIG))
module P = Polynome.Make (R) (struct let var_string= match rgopt,precomp_exists with
Some a,_ -> a.ZoneGraph.var_string
| _,Some b -> b.ZoneGraph.var_string
| None,None -> assert false end)
module Weight = (val if !frequency =0.0 then (module P:Semantic.WeightStructure)
else (module ExpPoly.Make(P)(struct
let smp = if P.F.is_exact then None else Some !frequency
let tvar = P.var_of_int 0
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 (Bound) (Weight)
(* Compute Weight and distribution as polynomials *)
let rgpoly =
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 ()
);
let _,rgp = FunIt.iterate_functionnal ~update:(fun () ->printf "|"; print_flush ())
rg !npoly in
if !verbose>0 then printf "] [%.2fs]@." (check_time ());
rgp
| _, Some rg, false -> snd @@ FunIt.iterate_functionnal rg 0
| None,None,_ -> assert false
let _ = let _ =
let precomp_exists =
if !print_rg then None else ZoneGraphInput.precomputation_exists
~debug:(fun b -> if !verbose>0 then
if b
then printf "Precomputation file found ! [%.2f]@." (check_time ())
else printf "Precomputation file found but file have change discard !@.")
!infile !frequency !npoly !rational_impl in
(* Use splitted or general bound general only for isotropic sampling *)
let module Bound = (val if !npoly<0 then (module ZoneGraphInput.GeneralBound:ZoneGraphInput.BoundType )
else (module ZoneGraphInput.LinearBound )) in
let module ZGI = ZoneGraphInput.Make (Bound) in
(*Building the zone graph *)
let rgopt =
if precomp_exists = None then
Some (ZGI.input_zone_graph
~verbose:!verbose ~print_rg:!print_rg ~splitting_debug:!splitting_debug
?export_zone_graph:!export_zone_graph !infile)
else None in
(* Build the polynomial ring with exact or approximated rationnal and with or without Exppolynomials *)
let module R = (val if !rational_impl then (module Flq.Q :Fl.FSIG) else (module Fl.Float:Fl.FSIG)) in
let module P = Polynome.Make (R) (struct let var_string= match rgopt,precomp_exists with
Some a,_ -> a.ZoneGraph.var_string
| _,Some b -> b.ZoneGraph.var_string
| None,None -> assert false end) in
let module Weight = (val if !frequency =0.0 then (module P:Semantic.WeightStructure)
else (module ExpPoly.Make(P)(struct
let smp = if P.F.is_exact then None else Some !frequency
let tvar = P.var_of_int 0
let svar= P.var_of_int (P.nb_var-1)
end))) in
(* Build the functionnal iterator module based on the bound type and the polynomial ring *)
let module FunIt = Semantic.Make (Bound) (Weight) in
(* Compute Weight and distribution as polynomials *)
let rgpoly =
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 ()
);
let _,rgp = FunIt.iterate_functionnal ~update:(fun () ->printf "|"; print_flush ())
rg !npoly in
if !verbose>0 then printf "] [%.2fs]@." (check_time ());
rgp
| _, Some rg, false -> snd @@ FunIt.iterate_functionnal rg 0
| None,None,_ -> assert false in
ZoneGraphInput.save_precomputation !infile rgpoly !frequency !npoly !rational_impl; ZoneGraphInput.save_precomputation !infile rgpoly !frequency !npoly !rational_impl;
if !print_rg then begin if !print_rg then
printf "%a@." (ZoneGraph.print Bound.print) rgpoly; begin
let fdot = open_out ((Filename.chop_extension !infile)^".dot") in printf "%a@." (ZoneGraph.print Bound.print) rgpoly;
ZoneGraph.print_dot rgpoly Bound.print (Format.formatter_of_out_channel fdot); let fdot = open_out ((Filename.chop_extension !infile)^".dot") in
close_out fdot ZoneGraph.print_dot rgpoly Bound.print (Format.formatter_of_out_channel fdot);
end close_out fdot
end;
module M = MainLoop.Make(FunIt) let module M = MainLoop.Make(FunIt) in
(* Sampling *) (* Sampling *)
(* Most of the code handle printing, Most of the work done by FunIt.sample_traj*)
let _ =
(* Compute template if not provided *) (* Compute template if not provided *)
let template_word = match !sampling_meth with let template_word = match !sampling_meth with
Exact when !npoly>=0 -> Array.make !npoly (Semantic.Fixed,Semantic.Fixed) Exact when !npoly>=0 -> Array.make !npoly (Semantic.Fixed,Semantic.Fixed)
...@@ -153,7 +153,7 @@ let _ = ...@@ -153,7 +153,7 @@ let _ =
!npoly !frequency driver; !npoly !frequency driver;
fprintf gnuplot "set xrange [-0.5 :*]\nbinwidth = 0.1\nbinstart= -0.5\nset boxwidth 0.9*binwidth\nset style fill solid 0.5\n"; fprintf gnuplot "set xrange [-0.5 :*]\nbinwidth = 0.1\nbinstart= -0.5\nset boxwidth 0.9*binwidth\nset style fill solid 0.5\n";
fprintf gnuplot "plot '%s' i 0 u (binwidth*(floor(($2-binstart)/binwidth)+0.5)+binstart):(1.0) smooth freq w boxes\n" data fprintf gnuplot "plot '%s' i 0 u (binwidth*(floor(($2-binstart)/binwidth)+0.5)+binstart):(1.0) smooth freq w boxes\n" data
) else if !out_style = StateListFull then fprintf gnuplot "plot '%s' u 2:3:5 w points pt 7 lc variable" data ) else if !out_style = StateListFull then fprintf gnuplot "plot '%s' u 2:3:4 w points pt 7 lc variable" data
else fprintf gnuplot "plot '%s' u 1:2 w dots" data; else fprintf gnuplot "plot '%s' u 1:2 w dots" data;
ignore @@ Unix.close_process_out gnuplot ignore @@ Unix.close_process_out gnuplot
| _ -> eprintf "No output file specified, cannot use gnuplot\n" | _ -> eprintf "No output file specified, cannot use gnuplot\n"
B _build/web-view B _build/web-view
B _build/
S ./ S ./
S web-view S web-view
S ../src/ S ../src/
B ../_build
B ../_build/src B ../_build/src
B ../_build/web-wiew/ B ../_build/web-wiew/
PKG yojson xml-light js_of_ocaml js_of_ocaml-camlp4 js_of_ocaml-camlp4 PKG yojson xml-light js_of_ocaml js_of_ocaml-camlp4 js_of_ocaml-camlp4
...@@ -66,6 +66,13 @@ let a ?(class_ = "") ?(href = "") ?(title="") ?(on_click = fun () -> ()) items = ...@@ -66,6 +66,13 @@ let a ?(class_ = "") ?(href = "") ?(title="") ?(on_click = fun () -> ()) items =
a##.onclick := Dom.handler on_click; a##.onclick := Dom.handler on_click;
(a :> t) (a :> t)
let kbd' value =
let kbd = Dom_html.document##createElement(Js.string "kbd") in
let textv,textup = text' value in
ignore @@ kbd##appendChild(textv);
( kbd :> t),textup
let button ?(class_ = "") ?(on_click = fun () -> ()) items = let button ?(class_ = "") ?(on_click = fun () -> ()) items =
let button = Dom_html.(createButton document) in let button = Dom_html.(createButton document) in
let append_node node = let append_node node =
......
...@@ -34,6 +34,7 @@ val text': string -> t * (string -> unit) ...@@ -34,6 +34,7 @@ val text': string -> t * (string -> unit)
val img: ?class_: string -> ?alt: string -> ?title: string -> string -> t val img: ?class_: string -> ?alt: string -> ?title: string -> string -> t
val a: val a:
?class_: string -> ?href: string -> ?title: string -> ?on_click: (unit -> unit) -> t list -> t ?class_: string -> ?href: string -> ?title: string -> ?on_click: (unit -> unit) -> t list -> t
val kbd' : string -> t * (string -> unit)
val button: ?class_: string -> ?on_click: (unit -> unit) -> t list -> t val button: ?class_: string -> ?on_click: (unit -> unit) -> t list -> t
val p: ?class_: string -> t list -> t val p: ?class_: string -> t list -> t
val p_text: ?class_: string -> string -> t val p_text: ?class_: string -> string -> t
......
...@@ -20,16 +20,32 @@ let build_interface_elem up (opt,x,help) = ...@@ -20,16 +20,32 @@ let build_interface_elem up (opt,x,help) =
in in
div ~class_:"cmdelem" ~title:help [text opt; text " : "; input ] div ~class_:"cmdelem" ~title:help [text opt; text " : "; input ]
let build_cmd_elem (opt,x,help) =
let open Arg in
match x with
Set a when !a -> " "^opt
| Clear a when not !a -> " "^opt
| Set_string a -> Printf.sprintf " %s %s" opt !a
| Set_float a -> Printf.sprintf " %s %g" opt !a
| Set_int a -> Printf.sprintf " %s %i" opt !a
| _ -> ""
let build_interface ?(class_="") up l = let build_cmd l =
let str = List.fold_left (fun acc elem -> acc ^ (build_cmd_elem elem)) "wordgen" l in
str ^" automata.prism"
let build_interface ?(class_="") ?(stop=(fun () -> ())) up l =
let cmd,cmdup = kbd' (build_cmd l) in
let autocompute = ref true in let autocompute = ref true in
let up2 () = if !autocompute then up true else up false in let up2 () =
cmdup (build_cmd l);
if !autocompute then up true else up false in
let elemlist = List.map (build_interface_elem up2) l in let elemlist = List.map (build_interface_elem up2) l in
let bottom = [button ~on_click:(fun _ -> up true) [text "Compute"] ; let bottom = [button ~on_click:(fun _ -> up true) [text "Compute"] ; (*button ~on_click:(fun _ -> stop ()) [text "Stop"];*)
text " autocompute: " ; text " autocompute: " ;
checkbox_input ~on_change:(fun x -> autocompute:=x;up2 ()) !autocompute ] in checkbox_input ~on_change:(fun x -> autocompute:=x;up2 ()) !autocompute ] in
div ~class_ (text "arguments : " :: elemlist @ ( br () :: bottom ) ) div ~class_ (text "arguments : " :: elemlist @ ( br () :: cmd :: br () :: bottom ) )
let file_content = ref let file_content = ref
...@@ -98,7 +114,7 @@ let _ = run @@ fun () -> ...@@ -98,7 +114,7 @@ let _ = run @@ fun () ->
container_up []; container_up [];
Buffer.clear buffstd; Buffer.clear buffstd;
Buffer.clear buffdata; Buffer.clear buffdata;
worker##postMessage({Worker_sync.ta = !file_content; worker##postMessage(Worker_sync.Task {Worker_sync.ta = !file_content;
rational_impl = !rational_impl; rational_impl = !rational_impl;
frequency = !frequency; frequency = !frequency;
verbose = !verbose; verbose = !verbose;
...@@ -117,7 +133,7 @@ let _ = run @@ fun () -> ...@@ -117,7 +133,7 @@ let _ = run @@ fun () ->
div ~class_:"main container-fluid"[ div ~class_:"main container-fluid"[
div ~class_:"jumbotron cmdline" [hi 1 "Wordgen"; div ~class_:"jumbotron cmdline" [hi 1 "Wordgen";
build_interface ~class_:"" launch_compt spec_short;]; build_interface ~class_:"" ~stop:(fun () -> worker##postMessage (Worker_sync.Stop)) launch_compt spec_short;];
div ~class_:"" [div ~class_:"output" [ txin; container]]; div ~class_:"" [div ~class_:"output" [ txin; container]];
br (); br ();
alert; sigt; alert; sigt;
......
open Worker_sync open Worker_sync
let is_stopped =ref true
exception Interrupted
let computation outfile task = let computation outfile task =
let module ZGI = ZoneGraphInput.Make (ZoneGraphInput.LinearBound) in let module Bound = (val if task.npoly<0 then (module ZoneGraphInput.GeneralBound:ZoneGraphInput.BoundType )
else (module ZoneGraphInput.LinearBound )) in
let module ZGI = ZoneGraphInput.Make (Bound) in
let rg = ZGI.input_from_string task.ta in let rg = ZGI.input_from_string task.ta in
Js_of_ocaml.Worker.post_message ParseOK; Js_of_ocaml.Worker.post_message ParseOK;
if not task.only_parse then ( if not task.only_parse then (
...@@ -9,36 +14,40 @@ let computation outfile task = ...@@ -9,36 +14,40 @@ let computation outfile task =
let module P = Polynome.Make (R) (struct let var_string= rg.ZoneGraph.var_string end) in let module P = Polynome.Make (R) (struct let var_string= rg.ZoneGraph.var_string end) in
let module Weight = ( let module Weight = (
val if task.frequency =0.0 then (module P:Semantic.WeightStructure) val if task.frequency =0.0 then (module P:Semantic.WeightStructure)
else (module ExpPoly.Make(P)(struct else (module ExpPoly.Make(P)(struct
let smp = if P.F.is_exact then None else Some task.frequency let smp = if P.F.is_exact then None else Some task.frequency
let tvar = P.var_of_int 0 let tvar = P.var_of_int 0
let svar= P.var_of_int (P.nb_var-1) let svar= P.var_of_int (P.nb_var-1)
end))) in end))) in
let module FunIt = Semantic.Make (ZoneGraphInput.LinearBound) (Weight) in let module FunIt = Semantic.Make (Bound) (Weight) in
let module M = MainLoop.Make(FunIt) in let module M = MainLoop.Make(FunIt) in
let rgpoly = let rgpoly =
if task.verbose>0 then ( if task.npoly > 0 then (
Format.printf "Computing Distribution -> %i: [" task.npoly; flush stdout; if task.verbose>0 then (
Format.print_flush () Format.printf "Computing Distribution -> %i: [" task.npoly; flush stdout;
); Format.print_flush ()
let _,rgp = FunIt.iterate_functionnal ~update:(fun () ->Format.printf "|"; Format.print_flush ()) );
rg task.npoly in let _,rgp = FunIt.iterate_functionnal ~update:(fun () ->
if task.verbose>0 then Format.printf "] [%.2fs]@." (Common.check_time ()); if !is_stopped then raise Interrupted;
rgp in Format.printf "|"; Format.print_flush ())
rg task.npoly in
if task.verbose>0 then Format.printf "] [%.2fs]@." (Common.check_time ());
rgp
) else
snd @@ FunIt.iterate_functionnal rg 0
in
if task.print_rg then ( if task.print_rg then (
let buff = Buffer.create 100 in let buff = Buffer.create 100 in
let form = Format.formatter_of_buffer buff in let form = Format.formatter_of_buffer buff in
ZoneGraph.print_dot rgpoly ZoneGraphInput.LinearBound.print form; ZoneGraph.print_dot rgpoly Bound.print form;
Format.fprintf form "@."; Format.fprintf form "@.";
Format.printf "%a@." (ZoneGraph.print ZoneGraphInput.LinearBound.print) rgpoly; Format.printf "%a@." (ZoneGraph.print Bound.print) rgpoly;
Js_of_ocaml.Worker.post_message (Graph (String.escaped (Buffer.contents buff))) Js_of_ocaml.Worker.post_message (Graph (String.escaped (Buffer.contents buff)))
); );
let module OutFormatter = OutFormat.Make(FunIt) in
let template_word = match task.sampling_meth with let template_word = match task.sampling_meth with
Exact -> Array.make task.npoly (Semantic.Fixed,Semantic.Fixed) Exact -> Array.make task.npoly (Semantic.Fixed,Semantic.Fixed)
| Receding x -> Array.make x (Semantic.Fixed,Semantic.Fixed) | Receding x -> Array.make x (Semantic.Fixed,Semantic.Fixed)
...@@ -58,23 +67,30 @@ else (module ExpPoly.Make(P)(struct ...@@ -58,23 +67,30 @@ else (module ExpPoly.Make(P)(struct
) )
let _ = let _ =
Js_of_ocaml.Worker.set_onmessage (fun x -> Js_of_ocaml.Worker.set_onmessage (function
print_endline ("New Job"); | Stop ->
let buff_std = Buffer.create 10 in is_stopped := true;
Format.set_formatter_output_functions (Buffer.add_substring buff_std) print_endline "Stop"
| Task x ->
is_stopped := false;
print_endline ("New Job");
let buff_std = Buffer.create 10 in
Format.set_formatter_output_functions (Buffer.add_substring buff_std)
(fun () -> (fun () ->
let m = Buffer.contents buff_std in let m = Buffer.contents buff_std in
Buffer.clear buff_std; Buffer.clear buff_std;
Js_of_ocaml.Worker.post_message (StdOut(m))); Js_of_ocaml.Worker.post_message (StdOut(m)));
let buff_out = Buffer.create 100 in let buff_out = Buffer.create 100 in
let out_formatter = Format.make_formatter (Buffer.add_substring buff_out) let out_formatter = Format.make_formatter (Buffer.add_substring buff_out)
(fun () -> (fun () ->
let m = Buffer.contents buff_out in let m = Buffer.contents buff_out in
Buffer.clear buff_out; Buffer.clear buff_out;
Js_of_ocaml.Worker.post_message (Data m)) in Js_of_ocaml.Worker.post_message (Data m)) in
try try
computation out_formatter x; computation out_formatter x;
Js_of_ocaml.Worker.post_message (Finish) Js_of_ocaml.Worker.post_message (Finish)
with with
x -> Js_of_ocaml.Worker.post_message (Error x) Interrupted -> ()
) | x -> Js_of_ocaml.Worker.post_message (Error x)
)
...@@ -13,7 +13,8 @@ type task = { ...@@ -13,7 +13,8 @@ type task = {
nbtraj : int; nbtraj : int;
only_parse : bool; only_parse : bool;
} }
type order = Task of task | Stop
type result_type = type result_type =
| StdOut of string | StdOut of string
......
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