Commit f559f2fc authored by Benoit Barbot's avatar Benoit Barbot
Browse files

add interactive option

parent cb7689f5
Pipeline #2092 failed with stages
in 31 seconds
......@@ -102,6 +102,8 @@ let splitting_debug = ref ""
let out_style = ref Wordgen_lib.OutFormat.Timeword
let is_interactive = ref false
let store_traj = ref false
let print_rg = ref false
......@@ -185,6 +187,8 @@ let spec_short =
let to_string = Wordgen_lib.OutFormat.string_of_style
end ),
" choose the format of the output" );
("--interactive", Bool is_interactive, "Interactive mode");
("-i", Bool is_interactive, "Interactive mode");
("--apericube", Bool store_traj, "Compute apericube");
("-v", Int (verbose, 1), "Verbose level");
( "--exact-rational",
......
......@@ -9,7 +9,6 @@ type output_style =
| StateListFull
| TimeAndLabels
| Debug
| Interactive
let style_list =
[
......@@ -22,7 +21,6 @@ let style_list =
"state_list_full";
"time_and_label";
"debug";
"interactive";
"void";
]
......@@ -37,7 +35,6 @@ let style_of_string = function
| "state_list_full" -> StateListFull
| "debug" -> Debug
| "time_and_label" -> TimeAndLabels
| "interactive" -> Interactive
| _ -> Void
let string_of_style = function
......@@ -51,7 +48,6 @@ let string_of_style = function
| StateListFull -> "state_list_full"
| TimeAndLabels -> "time_and_label"
| Debug -> "debug"
| Interactive -> "interactive"
open Format
......@@ -62,7 +58,7 @@ module Make
struct
open State
type style = output_style
type style = output_style * bool
type bound = Bt.t
......@@ -86,29 +82,21 @@ struct
let mon_state = ref (0, 0.0) in
((outfile, rg, ost, mon_state, parse_action) : t)
let end_traj (outfile, _, ost, mon_state, _) store_traj =
let end_traj (outfile, _, (ost, _), mon_state, _) store_traj =
if store_traj then
fprintf outfile "%i\t%g" (fst !mon_state) (snd !mon_state);
if ost <> Void || store_traj then fprintf outfile "@."
let end_sampling _ = ()
let up_state ((outfile, rgpoly, ost, _, parse_action) : t) ?smp (st : State.t)
i =
match ost with
| TimewordState ->
fprintf outfile "(%a)@." print_state st;
None
| StateList ->
fprintf outfile "%a@." print_state st;
None
| StateListFull ->
fprintf outfile "%a\t%i@." print_state st 1;
None
| StateListDelay ->
fprintf outfile "%a\t%i@." print_state st 1;
None
| Debug | Interactive ->
let up_state ((outfile, rgpoly, (ost, is_interactive), _, parse_action) : t)
?smp (st : State.t) i =
( match ost with
| TimewordState -> fprintf outfile "(%a)@." print_state st
| StateList -> fprintf outfile "%a@." print_state st
| StateListFull -> fprintf outfile "%a\t%i@." print_state st 1
| StateListDelay -> fprintf outfile "%a\t%i@." print_state st 1
| Debug ->
fprintf outfile "@[<h 0>%a@. @[<v 2>@[<v 0>%a@]@]@]@."
(print_state_long rgpoly) st
(fun f l ->
......@@ -131,44 +119,45 @@ struct
fprintf f "[%s]-[%g;%g]--(%a)->%g->\"%s\"@,"
tr.ZoneGraph.action low up W.print weight w target.name
else fprintf f "[%s]-[%g;%g]@," tr.ZoneGraph.action low up))
rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition;
if ost <> Interactive then None
else
let rec aux () =
try
fprintf outfile ">@?";
match read_line () with
| "step" | "s" -> Some (List.hd @@ parse_action "_[_]")
| "exit" -> exit 0
| "reset" -> raise Exit
| "help" ->
fprintf outfile
"available command : help, step, reset, exit, \"t[a]\" \
with t a time and a an action@.";
aux ()
| instr ->
let l = parse_action instr in
Some (List.hd l)
with
| Exit -> raise Exit
| End_of_file -> exit 1
| _ -> aux ()
in
aux ()
| Void | Word | Timestamp | Timeword | TimeAndLabels -> None
let up_state_elapsed (outfile, _, ost, _, _) st _ =
rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition
| Void | Word | Timestamp | Timeword | TimeAndLabels -> () );
if is_interactive then
let rec aux () =
try
fprintf outfile ">@?";
match read_line () with
| "step" | "s" -> Some (List.hd @@ parse_action "_[_]")
| "exit" -> exit 0
| "reset" -> raise Exit
| "help" ->
fprintf outfile
"available command : help, step, reset, exit, \"t[a]\" with t \
a time and a an action@.";
aux ()
| instr ->
let l = parse_action instr in
Some (List.hd l)
with
| Exit -> raise Exit
| End_of_file -> exit 1
| _ -> aux ()
in
aux ()
else None
let up_state_elapsed (outfile, _, (ost, _), _, _) st _ =
match ost with
| StateListFull | StateListDelay -> fprintf outfile "%a" print_state st
| _ -> ()
let up_trans (outfile, _, ost, mon_state, _) time tr i =
let up_trans (outfile, _, (ost, _), mon_state, _) time tr i =
let t2 = int_of_float time in
(mon_state :=
let ap, tt = !mon_state in
((2 * ap) + t2, tt +. time));
match ost with
| (Interactive | Debug) when Array.length tr.ZoneGraph.weight > 0 ->
| Debug when Array.length tr.ZoneGraph.weight > 0 ->
let weight, cdf, _ = tr.ZoneGraph.weight.(i) in
fprintf outfile "((%a)/(%a))->%f[%s]\n" W.print cdf W.print weight time
tr.ZoneGraph.action
......@@ -184,7 +173,7 @@ struct
| TimeAndLabels ->
fprintf outfile "%f\t%i@." (snd !mon_state)
(int_of_char tr.ZoneGraph.action.[0])
| Interactive | StateList | Void -> ()
| StateList | Void -> ()
end
let plot_of_style style store_traj ntraj data =
......
......@@ -30,7 +30,7 @@ module type COMPUTE = sig
?outfile:Format.formatter ->
?boltz:float ->
?seed:int ->
out_style:OutFormat.output_style ->
out_style:OutFormat.output_style * bool ->
max_iter:int ->
sampler:(int -> int -> float) ->
?store_traj:bool ->
......
......@@ -122,7 +122,8 @@ let _ =
in
Weight.sample smp ~outfile ?seed:!Arguments.random_seed ?boltz
~out_style:!out_style ~max_iter:!max_iteration
~out_style:(!out_style, !is_interactive)
~max_iter:!max_iteration
~sampler:(Low_disc_sampler.get_sampler !sampler)
~store_traj:!store_traj rgpoly !template !nbtraj
......
......@@ -343,7 +343,7 @@ Test with s<>0
Computing Distribution[floating point; ExpPoly; s=1 inlined; clocks:{x4; x3; x2; x1; x; }; vars:{t; z; s; }] -> 3: [|||]
Sampling: []
$ echo "s\nhelp\nreset\ns\ns" | wordgen twoears.prism --seed 42 --output-format interactive
$ echo "s\nhelp\nreset\ns\ns" | wordgen twoears.prism --seed 42 --output-format debug -i
Precomputation file found ! [0.00]
Reading Distribution[floating point; Poly; no s; clocks:{y; x; }; vars:{t; z; s; }] -> 3
"m.UID x=0" y:0.000000 x:0.000000
......@@ -686,7 +686,7 @@ Test Template
Test Monitor
$ wordgen test2mod.prism --frequency 1 --seed 42 --apericube | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
$ wordgen test2mod.prism --frequency 1 --seed 42 --apericube --traj 10 | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
Reading Prism automaton file.
Computing forward reachability graph ... 13 states found.
Splitting reachability graph ... 41 states found.
......@@ -704,23 +704,113 @@ Test Monitor
Test time duration
$ wordgen test2mod.prism --time-duration 9 --exact-rational --seed 42 | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
$ wordgen test2mod.prism --time-duration 9 --exact-rational --seed 42 --output-format state_list_delay | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
Precomputation file found but file have change discard !
Reading Prism automaton file.
Computing forward reachability graph ... 13 states found.
Splitting reachability graph ... 41 states found.
Computing Distribution[exact rational; ExpPoly; s formal; clocks:{y; x; }; vars:{t; z; s; }] -> 3: [|||]
Computing laplace parameter s for E[T]=9 range:[0; inf; inf] -> s=0.416001;E[T]=9
0.293253[a] 0.360785[a] 3.698914[c]
0.884738[a] 7.736354[c] 7.599024[c]
0.157617[a] 6.523910[c] 0.271320[b]
0.625960[a] 0.112452[a] 0.446482[a]
0.545104[a] 0.271327[a] 0.989546[a]
0.309396[a] 7.997563[c] 0.841300[c]
7.817728[c] 4.497768[c] 0.082973[a]
8.153777[c] 0.205900[c] 6.554909[c]
5.742706[c] 1.229928[c] 4.491650[c]
7.270902[c] 1.958720[c] 2.902132[c]
0 0.000000 0.000000 1
0 0.293253 0.293253 97
35 0.000000 0.293253 1
35 0.360785 0.654038 97
28 0.000000 0.654038 1
28 3.698914 4.352952 99
0 0.000000 0.000000 1
0 0.884738 0.884738 97
35 0.000000 0.884738 1
35 7.736354 8.621092 99
30 7.736354 0.000000 1
30 15.335378 7.599024 99
0 0.000000 0.000000 1
0 0.157617 0.157617 97
35 0.000000 0.157617 1
35 6.523910 6.681527 99
30 6.523910 0.000000 1
30 6.795230 0.271320 98
0 0.000000 0.000000 1
0 0.625960 0.625960 97
35 0.000000 0.625960 1
35 0.112452 0.738412 97
28 0.000000 0.738412 1
28 0.446482 1.184894 97
0 0.000000 0.000000 1
0 0.545104 0.545104 97
35 0.000000 0.545104 1
35 0.271327 0.816431 97
28 0.000000 0.816431 1
28 0.989546 1.805977 97
0 0.000000 0.000000 1
0 0.309396 0.309396 97
35 0.000000 0.309396 1
35 7.997563 8.306959 99
30 7.997563 0.000000 1
30 8.838863 0.841300 99
0 0.000000 0.000000 1
0 7.817728 7.817728 99
2 7.817728 0.000000 1
2 12.315497 4.497768 99
1 0.000000 4.497768 1
1 0.082973 4.580741 97
0 0.000000 0.000000 1
0 8.153777 8.153777 99
2 8.153777 0.000000 1
2 8.359678 0.205900 99
29 0.000000 0.205900 1
29 6.554909 6.760809 99
0 0.000000 0.000000 1
0 5.742706 5.742706 99
2 5.742706 0.000000 1
2 6.972634 1.229928 99
6 0.000000 1.229928 1
6 4.491650 5.721578 99
0 0.000000 0.000000 1
0 7.270902 7.270902 99
2 7.270902 0.000000 1
2 9.229622 1.958720 99
6 0.000000 1.958720 1
6 2.902132 4.860852 99
$ wordgen bimodal.prism --time-duration 4.4 --seed 42 | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
Reading Prism automaton file.
......
Supports Markdown
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