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

cosim add time

parent 513bde38
Pipeline #2205 passed with stages
in 2 minutes and 32 seconds
......@@ -95,7 +95,7 @@ struct
let end_sampling _ = ()
let up_state ((outfile, rgpoly, (ost, is_interactive), _, parse_action) : t)
?smp (st : State.t) i =
?smp (st : State.t) i (_, u2) =
( match ost with
| TimewordState -> fprintf outfile "(%a)@." print_state st
| StateList -> fprintf outfile "%a@." print_state st
......@@ -116,13 +116,30 @@ struct
else compare low1 low2)
|> List.iter (fun (tr, low, up) ->
if Array.length tr.ZoneGraph.weight > 0 then
let weight, _, _ = tr.ZoneGraph.weight.(i) in
let weight, cdf, pdf = tr.ZoneGraph.weight.(i) in
let w = eval_poly_state_full ?smp st weight in
let cdfap = eval_poly_state ?smp st cdf
and pdfap = eval_poly_state ?smp st pdf in
let t = Common.VarSet.find_var W.var_string "t" in
let invweight =
1.0 /. W.fully_apply_float ?smp cdfap t up
in
let open W in
let pb =
(F.of_float invweight **. cdfap)
-.. (const @@ F.of_float u2)
in
let diffcdf = F.of_float invweight **. pdfap in
let time =
find_root ?smp pb ~diffp:diffcdf ~bound:(low, up) t
(0.5 *. (low +. up))
in
let target =
rgpoly.statelist.((List.hd tr.ZoneGraph.miniedge).target)
in
fprintf f "[%s]-[%g;%g]-->%g->\"%s\"@," tr.ZoneGraph.action
low up w target.name
fprintf f "[%s]-[%g;%g]-%g-%g->\"%s\"@,"
tr.ZoneGraph.action low up w time target.name
else fprintf f "[%s]-[%g;%g]@," tr.ZoneGraph.action low up))
rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition
| Debug ->
......
......@@ -118,6 +118,7 @@ module type MONITOR = sig
?smp:float ->
state ->
int ->
float * float ->
(float transChoice * string transChoice) option
val up_state_elapsed : t -> state -> int -> unit
......@@ -290,10 +291,13 @@ struct
try
while !i < lengthword && !continue do
let j = !i in
let u1 = samp1 j and u2 = samp2 j in
up0 ();
(* Index of polynome depending of sampling method*)
let polyindex = max 0 (j - lengthword + rgpoly.nb_poly) in
let override = OF.up_state monitor_state ?smp !state polyindex in
let override =
OF.up_state monitor_state ?smp !state polyindex (u1, u2)
in
let taction = Option.value override ~default:template_word.(j) in
(* Filter transition according to template *)
let filter =
......@@ -311,7 +315,7 @@ struct
match snd taction with
| Rand u -> sample_trans ?smp ?boltz rgpoly polyindex !state ~filter u
| Fixed | Label _ ->
sample_trans ?smp ?boltz rgpoly polyindex !state ~filter (samp1 j)
sample_trans ?smp ?boltz rgpoly polyindex !state ~filter u1
in
(* Sample time *)
......@@ -319,7 +323,7 @@ struct
match fst taction with
| Label t -> t
| Rand u -> sample_time ?smp ~max_iter polyindex !state tr u
| Fixed -> sample_time ?smp ~max_iter polyindex !state tr (samp2 j)
| Fixed -> sample_time ?smp ~max_iter polyindex !state tr u2
in
(* Update state *)
state := elapse_time !state time;
......@@ -414,7 +418,7 @@ struct
if size > 10000 then raise SMC_Not_terminating;
mon_state := ((size + 1, duration +. time), glob)
let up_state _ ?smp:_ _ _ = None
let up_state _ ?smp:_ _ _ _ = None
let up_state_elapsed _ _ _ = ()
......
......@@ -14,7 +14,7 @@ Simple interaction
--expected-size time word size parameter
--template specify a template for time words; template look like '0.2[a]_[b]'
--max-iteration Number of iteration for Newton method (default:20)
--output-format {timeword|timestamp|word|timeword_state|state_list|state_list_delay|state_list_full|time_and_label|debug|void} choose the format of the output (default:timeword)
--output-format {timeword|timestamp|word|timeword_state|state_list|state_list_delay|state_list_full|time_and_label|debug|void|cosim} choose the format of the output (default:timeword)
--apericube Compute apericube
-v Verbose level (default:1)
--exact-rational Use exact arithmetic for computation
......@@ -43,7 +43,7 @@ Simple interaction
--expected-size time word size parameter
--template specify a template for time words; template look like '0.2[a]_[b]'
--max-iteration Number of iteration for Newton method (default:20)
--output-format {timeword|timestamp|word|timeword_state|state_list|state_list_delay|state_list_full|time_and_label|debug|void} choose the format of the output (default:timeword)
--output-format {timeword|timestamp|word|timeword_state|state_list|state_list_delay|state_list_full|time_and_label|debug|void|cosim} choose the format of the output (default:timeword)
--apericube Compute apericube
-v Verbose level (default:1)
--exact-rational Use exact arithmetic for computation
......@@ -368,17 +368,17 @@ Test with s<>0
[a]-[1;2]--(5.66666666667)->5.66667->"m.UID y=0"
[b]-[0;2]--(16.3333333333)->16.3333->"m.UID x=0"
>((11.5t-2t²+0.166666666667t³)/(16.3333333333))->0.879989[b]
"m.UID x=0" y:0.879989 x:0.000000
[a]-[0;1]--(3.5)->3.5->"m.UID y=0"
[a]-[1;2]--(2)->2->"m.UID y=0"
[b]-[0;1.12001]--(6-4y+½y²)->2.86724->"m.UID x=0"
>((11.5t-2t²+0.166666666667t³)/(9.66666666667))->0.528281[a]
"m.UID y=0" y:0.000000 x:0.528281
[a]-[0;0.471719]--(3.5-4x+½x²)->1.52642->"m.UID y=0"
[a]-[0.471719;1.47172]--(2)->2->"m.UID y=0"
[b]-[0;2]--(6)->6->"m.UID x=0"
>((4t-½t²)/(3.5))->0.537763[a]
"m.UID y=0" y:0.000000 x:0.537763
[a]-[0;0.462237]--(1-x)->0.462237->"m.UID y=0"
[a]-[0.462237;1.46224]--(1)->1->"m.UID y=0"
[b]-[0;2]--(2)->2->"m.UID x=0"
>((4t-½t²)/(6))->1.696314[b]
"m.UID x=0" y:1.696314 x:0.000000
[a]-[0;1]--(1)->1->"m.UID y=0"
[a]-[1;2]--(1)->1->"m.UID y=0"
[b]-[0;0.303686]--(2-y)->0.303686->"m.UID x=0"
>
[1]
......@@ -594,8 +594,8 @@ Test Template
Computing forward reachability graph ... 3 states found.
Splitting reachability graph ... 4 states found.
Computing Distribution[floating point; Poly; no s; clocks:{y; x; }; vars:{t; z; s; }] -> 3: [|||]
1.403733[a] 1.084316[b] 0.500000[a] 0.608733[b]
0.454917[a] 1.694403[b] 0.500000[a] 1.577337[b]
1.403733[a] 0.731974[b] 0.500000[a] 1.782172[b]
1.403733[a] 1.148209[b] 0.500000[a] 1.150045[a]
$ wordgen twoears.prism --template "0.5[a]_[b]@0.5[0.5]_[_]" out.dat --traj 10 --seed 42 --gnuplot-cmd '' --gnuplot-driver 'png size 10,10' | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
Precomputation file found ! [0.00]
......@@ -619,43 +619,43 @@ Test Template
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
1.592912[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
1.458619[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
0.616674[d]
1.620995[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
1.620995[d]
0.250899[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
1.164899[d]
0.223932[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
0.250899[d]
0.791379[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
0.774095[d]
0.973542[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (10 1.000000 1.000000 1.000000 0.000000 0.000000 )
1.200000[c] (12 2.200000 2.200000 0.000000 1.200000 0.000000 )
1.223932[d]
0.079755[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
0.961825[d]
1.000000[b] (10 1.000000 1.000000 1.000000 0.000000 0.000000 )
1.200000[c] (12 2.200000 2.200000 0.000000 1.200000 0.000000 )
0.523623[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (39 1.000000 1.000000 1.000000 0.000000 0.000000 )
0.200000[c] (27 1.200000 1.200000 0.000000 0.200000 0.000000 )
0.791379[d]
0.147974[d]
(0 0.000000 0.000000 0.000000 0.000000 0.000000 )
1.000000[b] (10 1.000000 1.000000 1.000000 0.000000 0.000000 )
1.200000[c] (12 2.200000 2.200000 0.000000 1.200000 0.000000 )
0.732169[d]
$ wordgen nfm19.prism --seed 42 --template "@1[b]0.2[0.3]_[_]" --poly -1 --output-format debug --traj 2 | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
Precomputation file found but file have change discard !
......@@ -673,7 +673,7 @@ Test Template
"m.UID m.s = 2, x4 in [0,4); x3 in [0,4); x2=0; x1 in [0,2); x=0; x4=x3; 0<= x4-x1 <2; 0<= x3-x1 <2" x4:1.400000 x3:1.400000 x2:0.000000 x1:0.400000 x:0.000000
[d]-[0;2]
->1.482281[d]
->1.146547[d]
"m.UID m.s = 0, x4=0; x3=0; x2=0; x1=0; x=0" x4:0.000000 x3:0.000000 x2:0.000000 x1:0.000000 x:0.000000
[b]-[0;2]
......@@ -686,7 +686,7 @@ Test Template
"m.UID m.s = 2, x4 in [0,4); x3 in [0,4); x2=0; x1 in [0,2); x=0; x4=x3; 0<= x4-x1 <2; 0<= x3-x1 <2" x4:1.400000 x3:1.400000 x2:0.000000 x1:0.400000 x:0.000000
[d]-[0;2]
->1.146547[d]
->1.552488[d]
Test Monitor
......
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