Commit 72565b58 authored by Benoit Barbot's avatar Benoit Barbot
Browse files

improve expected-duration

parent df1d8c30
Pipeline #1693 passed with stages
in 32 seconds
pta
module m
x : clock;
s : [0..2] init 0;
invariant
(x<=3)
endinvariant
[a] (s=0) -> (s'=1)&(x'=0);
[b] (s=0) -> (s'=2) & (x'=0);
[c] (x<=1)&(s=1) -> (x'=0);
[c] (x>=2)&(s=2) -> (x'=0);
endmodule
......@@ -7,7 +7,7 @@ module type SYM = sig
val to_string : t -> string
end
type 'a arg_t =
type arg_t =
Bool of bool ref
| Set_string of string option ref
| Set_int of int option ref
......@@ -19,18 +19,45 @@ type 'a arg_t =
(*string list * 'a ref * 'a * ('a -> string) * (string -> 'a)*)
let to_caml_arg = function
Bool b -> Arg.Set b
| Set_string sr -> Arg.String (fun s -> sr := Some s)
| Set_int ir -> Arg.Int (fun i -> ir := Some i)
| Set_float fr -> Arg.Float (fun f -> fr := Some f)
| Int (ir,_) -> Arg.Set_int ir
| Float (fr,_) -> Arg.Set_float fr
| String (sr,_) -> Arg.Set_string sr
let to_caml_arg (opt,x,help) = match x with
Bool b -> opt,Arg.Set b,help
| Set_string sr -> opt,Arg.String (fun s -> sr := Some s),help
| Set_int ir -> opt,Arg.Int (fun i -> ir := Some i),help
| Set_float fr -> opt,Arg.Float (fun f -> fr := Some f),help
| Int (ir,d) -> opt,Arg.Set_int ir, Printf.sprintf "%s (default:%i)" help d
| Float (fr,d) -> opt,Arg.Set_float fr, Printf.sprintf "%s (default:%g)" help d
| String (sr,d) -> opt,Arg.Set_string sr, Printf.sprintf "%s (default:%s)" help d
| Symbol s ->
let module S = (val s : SYM) in
Arg.Symbol (S.list, fun s -> S.content := S.of_string s)
opt, Arg.Symbol (S.list, fun s -> S.content := S.of_string s), Printf.sprintf "%s (default:%s)" help (S.to_string S.def)
let build_cmd_elem (opt,x,help) =
match x with
Bool a when !a -> " "^opt
| Bool _ -> ""
| Set_string a -> (match !a with
Some v -> Printf.sprintf " %s %s" opt v
| None -> "")
| String (s,ds) -> if !s = ds then ""
else Printf.sprintf " %s %s" opt !s
| Set_float a -> (match !a with
Some v -> Printf.sprintf " %s %g" opt v
| None -> "")
| Float (s,ds) -> if !s = ds then ""
else Printf.sprintf " %s %g" opt !s
| Set_int a -> (match !a with
Some v -> Printf.sprintf " %s %i" opt v
| None -> "")
| Int (s,ds) -> if !s = ds then ""
else Printf.sprintf " %s %i" opt !s
| Symbol s ->
let module S = (val s:SYM) in
if !(S.content) = S.def then ""
else Printf.sprintf " %s %s" opt (S.to_string !(S.content))
let build_cmd l =
let str = List.fold_left (fun acc elem -> acc ^ (build_cmd_elem elem)) "wordgen" l in
str
type samplingMeth =
Exact
......@@ -72,7 +99,7 @@ let splitting_debug = ref ""
let out_style = ref OutFormat.Timeword
let store_traj = ref false
let print_rg = ref false
let sampler = ref Low_disc_sampler.random
let sampler = ref Low_disc_sampler.Random
let gnuplot_driver = ref None
let export_zone_graph = ref None
let frequency = ref None
......@@ -90,6 +117,11 @@ let spec_short = [
"--poly", Int (npoly,3), "Number of polynome Iteration";
"--traj", Int (nbtraj,10), "Number of trajectories";
"--receding", Set_int receding, "trajectory length";
"--sampler", Symbol (module struct
include Low_disc_sampler
let list = ["random"; "halton";"kronecker"]
let content = sampler
end), " choose sampler";
"--seed", Set_int random_seed, "seed of the random sampler";
"--frequency", Set_float frequency, "frequency parameter s";
"--time-duration", Set_float expected_duration, "time word duration parameter";
......@@ -107,7 +139,7 @@ let spec_short = [
"--apericube", Bool store_traj, "Compute apericube";
"-v", Int (verbose,1), "Verbose level";
"--exact-rational", Bool rational_impl, "Use exact arithmetic for computation";
"--exact-rational", Bool rational_impl, "Use exact arithmetic for computation";
]
let spec_full =
......@@ -115,38 +147,29 @@ let spec_full =
"--gnuplot-driver", Set_string gnuplot_driver, "launch gnuplot";
"--export-splitreach", Set_string export_zone_graph, "Export the splitted zone graph";
"--splitting-debug", String (splitting_debug,"") , "Export debug information on the splitting in tex format";
"--sampler", Symbol (module struct
type t = int -> int -> float
let list = ["random"; "halton";"kronecker"]
let content = sampler
let def = Low_disc_sampler.random
let to_string = function
f when f=Low_disc_sampler.halton -> "halton"
| f when f=Low_disc_sampler.kronecker_phi -> "kronecker"
| _ -> "random"
let of_string = function
"halton" -> Low_disc_sampler.halton
| "kronecker" -> Low_disc_sampler.kronecker_phi
| _ -> Low_disc_sampler.random
end), " choose sampler (default random)"
]
let post_parse () =
(match !frequency, !expected_duration with
Some _ ,Some _ -> failwith "Set frequency or expected duration not both"
| _ -> ());
match !receding,!template with
(match !receding,!template with
None, None -> sampling_meth := Exact
| Some r, None -> sampling_meth := Receding r
| None, Some t -> (try
sampling_meth := Driven (timeword_parser t);
with
| x -> failwith "Fail to parse driving command")
| Some _, Some _ -> failwith "Set receding horizon or a template not both"
| Some _, Some _ -> failwith "Set receding horizon or a template not both");
(match !sampling_meth, !expected_duration with
| Receding r, Some t -> expected_duration := Some (t *. (float !npoly) /. (float r))
| Driven l, Some t -> expected_duration := Some (t *. (float !npoly) /. (float (List.length l)))
| _ -> ()
)
let spec_caml_arg = List.map (fun (n,spec,def) -> (n, to_caml_arg spec,def)) spec_full
let spec_caml_arg = List.map to_caml_arg spec_full
let usage_str = "wordgen automaton.prism [outputfile]"
......
......@@ -57,3 +57,18 @@ let init ?seed n =
let kronecker_phi base index =
let b = base +1 in
mod_float ((float_of_int index) *. (1.0 /. (!kronecker_state ** (float b) ))) 1.0
type t = Random | Halton | Kronecker
let def = Random
let to_string = function
Halton -> "halton"
| Kronecker -> "kronecker"
| Random -> "random"
let of_string = function
"halton" -> Halton
| "kronecker" -> Kronecker
| _ -> Random
let get_sampler = function
Random -> random
| Halton -> halton
| Kronecker -> kronecker_phi
......@@ -163,7 +163,7 @@ let _ =
~verbose:!verbose
~out_style: !out_style
~max_iter: !max_iteration
~sampler: !sampler
~sampler: (Low_disc_sampler.get_sampler !sampler)
~store_traj: !store_traj
rgpoly
template_word
......
......@@ -31,4 +31,4 @@ deploy: web
server: web
#cd website; python -m SimpleHTTPServer 8080
cd website; ocsigenserver -c simpleserve.conf
cd website; ocsigenserver -c simpleserve.conf -v
......@@ -177,15 +177,16 @@ let text_input' ?(class_ = "") ?(on_change = fun _ -> ()) ?(_type = "text") valu
let set_value value = input##.value := Js.string value in
(input :> t), set_value
let option value =
let option ?(def=false) value =
let opt = Dom_html.(createOption document) in
opt##.value := Js.string value;
append_node opt (text value);
if def then opt##.defaultSelected := Js._true;
(opt :> t)
let select ?(class_ = "") ?(on_change = fun _ -> ()) sl =
let select ?(class_ = "") ?def ?(on_change = fun _ -> ()) sl =
let sel = Dom_html.(createSelect document) in
List.iter (fun s -> append_node sel (option s)) sl;
List.iter (fun s -> append_node sel (option ~def:(match def with None -> false | Some x -> x=s) s)) sl;
let on_input _ = on_change (Js.to_string sel##.value); Js._true in
sel##.oninput := Dom.handler on_input;
sel##.className := Js.string class_;
......
......@@ -58,7 +58,7 @@ val text_input':
t * (string -> unit)
val select:
?class_: string -> ?on_change: (string -> unit) -> string list ->
?class_: string -> ?def:string -> ?on_change: (string -> unit) -> string list ->
t
......
......@@ -56,8 +56,8 @@
from the directory 'dir' (in alphabetical order): -->
<!--<extconf dir="/home/ben/.opam/4.10.0/lib/ocsigenserver/etc/ocsigenserver/conf.d" />-->
<host charset="utf-8" hostfilter="*">
<host defaulthostname="wordgen" charset="utf-8" hostfilter="*">
<!--<site path="ocsigenstuff" charset="utf-8">
<static dir="/home/ben/.opam/4.10.0/lib/ocsigenserver/var/www/ocsigenstuff" />
</site>-->
......
......@@ -19,39 +19,12 @@ let build_interface_elem up (opt,x,help) =
| String (a,ds) -> [text_input ~_type:"text" ~on_change:(fun x -> a:= x;up ()) ds]
| Symbol s ->
let module S = (val s : SYM) in
[select S.list ~on_change:(fun x -> S.content := S.of_string x;up ())]
[select S.list ~def:(S.to_string S.def) ~on_change:(fun x -> S.content := S.of_string x;up ())]
in
div ~class_:"cmdelem" ~title:help ([text opt; text " : " ] @ input )
let build_cmd_elem (opt,x,help) =
let open Arguments in
match x with
Bool a when !a -> " "^opt
| Bool _ -> ""
| Set_string a -> (match !a with
Some v -> Printf.sprintf " %s %s" opt v
| None -> "")
| String (s,ds) -> if !s = ds then ""
else Printf.sprintf " %s %s" opt !s
| Set_float a -> (match !a with
Some v -> Printf.sprintf " %s %g" opt v
| None -> "")
| Float (s,ds) -> if !s = ds then ""
else Printf.sprintf " %s %g" opt !s
| Set_int a -> (match !a with
Some v -> Printf.sprintf " %s %i" opt v
| None -> "")
| Int (s,ds) -> if !s = ds then ""
else Printf.sprintf " %s %i" opt !s
| Symbol s ->
let module S = (val s:SYM) in
if !(S.content) = S.def then ""
else Printf.sprintf " %s %s" opt (S.to_string !(S.content))
let build_cmd l =
let str = List.fold_left (fun acc elem -> acc ^ (build_cmd_elem elem)) "wordgen" l in
str ^" automata.prism"
(Arguments.build_cmd l)^" automata.prism"
let build_interface ?(class_="") ?(stop=(fun () -> ())) up l =
let cmd,cmdup = kbd' (build_cmd l) in
......@@ -143,19 +116,21 @@ let _ = run @@ fun () ->
container_up [];
Buffer.clear buffstd;
Buffer.clear buffdata;
worker##postMessage(Worker_sync.Task {Worker_sync.ta = !file_content;
rational_impl = !rational_impl;
frequency = !frequency;
expected_duration = !expected_duration;
verbose = !verbose;
npoly = !npoly;
print_rg = !print_rg;
sampling_meth = !sampling_meth;
out_style = !out_style;
max_iteration = !max_iteration;
store_traj = !store_traj;
nbtraj = !nbtraj;
only_parse = not b;
worker##postMessage(Worker_sync.Task {
Worker_sync.ta = !file_content;
rational_impl = !rational_impl;
frequency = !frequency;
expected_duration = !expected_duration;
verbose = !verbose;
npoly = !npoly;
print_rg = !print_rg;
sampling_meth = !sampling_meth;
sampler = !sampler;
out_style = !out_style;
max_iteration = !max_iteration;
store_traj = !store_traj;
nbtraj = !nbtraj;
only_parse = not b;
}) in
let txin = text_area ~class_:"input_file col-sm-6" ~on_change:(fun x->
......@@ -163,9 +138,14 @@ let _ = run @@ fun () ->
launch_compt false) !file_content in
dirup !file_content;
launch_compt true;
div ~class_:"main container-fluid"[
div ~class_:"jumbotron cmdline" [hi 1 "Wordgen"; p [text "Time word generator. Read more on "; a ~href:"https://git.lacl.fr/barbot/wordgen" [text "the source repository page."] ];
div ~class_:"jumbotron cmdline" [
hi 1 "Wordgen";
p [
text "Time word generator. Read more on ";
a ~href:"https://git.lacl.fr/barbot/wordgen" [text "the source repository page"];
text ". Be aware the tool Wordgen is a native commandline tool, this website if limited in speed and functionalities.";
];
build_interface ~class_:"" ~stop:(fun () -> worker##postMessage (Worker_sync.Stop)) launch_compt spec_short;];
div ~class_:"" [div ~class_:"output" [ txin; container]];
dirlink;
......
......@@ -86,7 +86,7 @@ let computation outfile task =
~out_style: task.out_style
~max_iter: task.max_iteration
~verbose: task.verbose
~sampler: Low_disc_sampler.random
~sampler: (Low_disc_sampler.get_sampler task.sampler)
~store_traj: task.store_traj
rgpoly
template_word
......
......@@ -9,6 +9,7 @@ type task = {
print_rg : bool;
sampling_meth : Arguments.samplingMeth;
out_style : OutFormat.output_style;
sampler : Low_disc_sampler.t;
max_iteration : int;
store_traj :bool;
nbtraj : int;
......
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