Commit 3c8b9b5b authored by Benoit Barbot's avatar Benoit Barbot
Browse files

fix length

parent f54303ae
Pipeline #2153 passed with stages
in 2 minutes and 12 seconds
......@@ -83,10 +83,10 @@ struct
((outfile, rg, ost, mon_state, parse_action) : t)
let end_traj (outfile, _, (ost, _), mon_state, _) store_traj =
if store_traj then (
let aper, _, duration = !mon_state in
fprintf outfile "%i\t%g" aper duration;
if ost <> Void || store_traj then fprintf outfile "@." )
( if store_traj then
let aper, size, duration = !mon_state in
Format.fprintf outfile "%i\t%i\t%g" aper size duration );
if ost <> Void || store_traj then fprintf outfile "@."
let end_sampling _ = ()
......
......@@ -45,6 +45,7 @@ module type S = sig
?verbose:int ->
?seed:int ->
float option * float option ->
(float Sampling.transChoice * string Sampling.transChoice) array ->
(t, Bt.t) ZoneGraph.t ->
(float * float * float) option
* (float * (float * float * float) * float) option
......@@ -243,7 +244,7 @@ struct
Format.printf "Target outside range, aborting@.";
exit 1 )
let compute_params ?(verbose = 1) ?seed targets rgp =
let compute_params ?(verbose = 1) ?seed targets template rgp =
match targets with
| Some t_length, t_duration ->
let module State = Sampling.State (P) in
......@@ -270,9 +271,7 @@ struct
else
let n, size, duration =
Samp.sample ~out_style:t_length ~max_iter:100 ~boltz ?seed
~sampler:Low_disc_sampler.random rgp2
[| (Fixed, Fixed); (Fixed, Fixed) |]
n
~sampler:Low_disc_sampler.random rgp2 template n
in
(n, size, duration, smp_full)
in
......
......@@ -22,6 +22,7 @@ module type S = sig
?verbose:int ->
?seed:int ->
float option * float option ->
(float Sampling.transChoice * string Sampling.transChoice) array ->
(t, Bt.t) ZoneGraph.t ->
(float * float * float) option
* (float * (float * float * float) * float) option
......
......@@ -52,7 +52,10 @@ module type COMPUTE = sig
bool -> string -> ('a, Bt.t) ZoneGraph.t -> (t, Bt.t) ZoneGraph.t
val compute_params :
?seed:int -> (t, Bt.t) ZoneGraph.t -> float option * float option
?seed:int ->
(float Sampling.transChoice * string Sampling.transChoice) array ->
(t, Bt.t) ZoneGraph.t ->
float option * float option
val sample :
float option ->
......@@ -130,7 +133,7 @@ module Instantiate
rg Param.npoly (Param.z_param <> No)
(* Compute parameters z and s *)
let compute_params ?seed rgpoly =
let compute_params ?seed template rgpoly =
let z_target =
match Param.z_param with
| No -> None
......@@ -152,9 +155,9 @@ module Instantiate
in
let boltz_full, smp_full =
compute_params ~verbose:Param.verbose
Weight.compute_params ~verbose:Param.verbose
?seed:(match seed with None -> None | Some s -> Some ((s * 11) + 7))
(z_target, smp_target) rgpoly
(z_target, smp_target) template rgpoly
in
let boltz =
......@@ -278,7 +281,7 @@ let main print_rg infile frequency npoly expected_duration boltzmann_param
(frequency = None && expected_duration <> None)
rational_impl;
let boltz, smp = Weight.compute_params ?seed rgpoly in
let boltz, smp = Weight.compute_params ?seed template rgpoly in
(* tidying up memory after the distribution computation*)
Gc.compact ();
......
......@@ -272,7 +272,7 @@ module Compute (Bt : ZoneGraphInput.BoundType) (P : Polynomial.S) = struct
(*let compute_s ?verbose:_ ?finish:_ _ _ = None*)
let compute_params ?(verbose = 1) ?seed (t_length, _) rg =
let compute_params ?(verbose = 1) ?seed (t_length, _) _ rg =
match t_length with
| Some t -> (compute_z ~verbose ?seed t rg, None)
| _ -> (None, None)
......
......@@ -695,16 +695,16 @@ Test Monitor
Computing forward reachability graph ... 13 states found.
Splitting reachability graph ... 41 states found.
Computing Distribution[floating point; ExpPoly; s=1 inlined; clocks:{y; x; }; vars:{t; z; s; }] -> 3: [|||]
0.225325[a] 0.341408[a] 0.225108[a] 0 0.791841
0.839894[a] 5.554328[c] 0.674678[c] 10 7.0689
0.116431[a] 0.484975[a] 0.551448[a] 0 1.15285
0.536562[a] 0.123248[a] 0.485461[a] 0 1.14527
0.454113[a] 0.298229[a] 0.987982[a] 0 1.74032
0.238888[a] 0.568487[a] 0.847873[a] 0 1.65525
5.588180[c] 0.125826[b] 0.065092[c] 20 5.7791
0.748744[a] 0.382126[a] 0.478156[a] 0 1.60903
0.410433[a] 0.678157[a] 0.117229[a] 0 1.20582
0.652080[a] 0.967316[a] 0.342085[a] 0 1.96148
0.225325[a] 0.341408[a] 0.225108[a] 0 3 0.791841
0.839894[a] 5.554328[c] 0.674678[c] 10 3 7.0689
0.116431[a] 0.484975[a] 0.551448[a] 0 3 1.15285
0.536562[a] 0.123248[a] 0.485461[a] 0 3 1.14527
0.454113[a] 0.298229[a] 0.987982[a] 0 3 1.74032
0.238888[a] 0.568487[a] 0.847873[a] 0 3 1.65525
5.588180[c] 0.125826[b] 0.065092[c] 20 3 5.7791
0.748744[a] 0.382126[a] 0.478156[a] 0 3 1.60903
0.410433[a] 0.678157[a] 0.117229[a] 0 3 1.20582
0.652080[a] 0.967316[a] 0.342085[a] 0 3 1.96148
Test time duration
......@@ -971,32 +971,32 @@ Test expected size
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: [|||]
Computing boltzmann parameter z for E[N]=10 |101->11.44 samples with z:1 s:? -> size:11.4356 duration:9.04949
|101->4.11 samples with z:0.5 s:? -> size:4.10891 duration:3.37354
|101->7.01 samples with z:0.75 s:? -> size:7.0099 duration:5.69477
|217->9.66 samples with z:0.925 s:? -> size:9.65899 duration:7.57826
|101->12.26 samples with z:1.0475 s:? -> size:12.2574 duration:9.7432
|102->11.19 samples with z:0.96175 s:? -> size:11.1863 duration:8.86401
|206->9.64 samples with z:0.901725 s:? -> size:9.63592 duration:7.59757
|345->9.84 samples with z:0.943743 s:? -> size:9.83768 duration:7.75404
|101->11.39 samples with z:0.973155 s:? -> size:11.3861 duration:9.00026
|185->10.61 samples with z:0.952566 s:? -> size:10.6108 duration:8.3074
|323->9.81 samples with z:0.938154 s:? -> size:9.81115 duration:7.73567
|452->9.90 samples with z:0.948243 s:? -> size:9.89602 duration:7.75556
|185->10.61 samples with z:0.955304 s:? -> size:10.6108 duration:8.31263
|185->10.61 samples with z:0.950361 s:? -> size:10.6108 duration:8.30764
|415->9.88 samples with z:0.946901 s:? -> size:9.88434 duration:7.7909
|186->10.55 samples with z:0.949323 s:? -> size:10.5484 duration:8.26633
|449->9.89 samples with z:0.947627 s:? -> size:9.89087 duration:7.74958
|452->9.90 samples with z:0.948814 s:? -> size:9.89602 duration:7.7555
|186->10.55 samples with z:0.949645 s:? -> size:10.5484 duration:8.26629
|186->10.55 samples with z:0.949064 s:? -> size:10.5484 duration:8.26635
|452->9.90 samples with z:0.948657 s:? -> size:9.89602 duration:7.75552
-> z=0.948543;E[N]=9.89602
1.468118[b] 0.386887[b] 1.859121[a] 0.144908[b] 1.574526[b] 1.541086[a] 0.115433[a] 0.294879[b] 0.632177[a] 0.955383[b] 0.193531[a] 0.701896[b] 0.328159[b] 0.242664[a] 0.331117[a] 0.087880[a] 0.455452[a] 0.652435[a] 0.116353[b] 0.346468[a] 1.337000[a] 1.028421[b] 0.491065[a] 0.440621[b] 1.000067[a] 0.611301[b] 0.764688[a] 1.167837[a] 0.517032[b] 0.245160[b] 0.368711[b] 0.647165[b] 0.917491[a] 0.775553[a] 0.118633[a] 0.886841[b] 0.142061[a] 1.651595[b] 0.007530[a] 0.965707[a] 0.247496[b] 1.190209[b] 1.042339[a] 0.486350[a] 0.757760[b] 0.332317[b] 0.799340[a] 1.572124[b] 0.959692[a] 1.250248[b]
1.237450[b] 1.278443[a] 0.099013[b] 0.058665[b] 0.254618[b] 0.415417[b] 0.225496[b] 0.847689[b] 0.312058[a] 0.803576[b] 0.447121[a] 1.783964[b] 0.189639[a] 0.736130[a] 0.943429[b] 1.856337[a] 0.276649[b] 0.020802[a] 1.978183[a]
0.251862[a] 1.733855[a] 0.865520[b] 0.631276[b] 0.101328[a] 0.807807[b] 0.694637[b] 0.531304[a] 0.914295[a] 1.137561[b] 0.592208[a] 1.566198[b] 0.803846[a] 0.343933[a] 0.353415[b]
1.516524[b] 0.499012[a] 0.539092[b] 0.520296[b] 0.807138[a] 1.148349[b] 1.092205[a] 0.792806[b] 0.142281[b]
Computing boltzmann parameter z for E[N]=10 |101->35.26 samples with z:1 s:? -> size:35.2574 duration:27.0266
|101->6.72 samples with z:0.5 s:? -> size:6.72277 duration:5.3703
|101->18.51 samples with z:0.75 s:? -> size:18.5149 duration:14.2747
|126->9.35 samples with z:0.575 s:? -> size:9.34921 duration:7.40538
|101->15.51 samples with z:0.6975 s:? -> size:15.5149 duration:12.004
|415->9.88 samples with z:0.61175 s:? -> size:9.88434 duration:7.70053
|101->13.10 samples with z:0.671775 s:? -> size:13.099 duration:10.2245
|101->11.41 samples with z:0.629757 s:? -> size:11.4059 duration:8.94531
|217->9.66 samples with z:0.600345 s:? -> size:9.65899 duration:7.52021
|102->11.19 samples with z:0.620934 s:? -> size:11.1863 duration:8.79425
|280->9.74 samples with z:0.606522 s:? -> size:9.74286 duration:7.56378
|185->10.61 samples with z:0.61661 s:? -> size:10.6108 duration:8.24379
|322->9.82 samples with z:0.609548 s:? -> size:9.81988 duration:7.66433
|384->10.24 samples with z:0.614492 s:? -> size:10.2448 duration:7.97712
|415->9.88 samples with z:0.611031 s:? -> size:9.88434 duration:7.69941
|449->9.89 samples with z:0.613454 s:? -> size:9.89087 duration:7.65957
|185->10.61 samples with z:0.615149 s:? -> size:10.6108 duration:8.24411
|452->9.90 samples with z:0.613962 s:? -> size:9.89602 duration:7.66184
|185->10.61 samples with z:0.614793 s:? -> size:10.6108 duration:8.24418
|452->9.90 samples with z:0.614211 s:? -> size:9.89602 duration:7.66178
|384->10.24 samples with z:0.614619 s:? -> size:10.2448 duration:7.97709
-> z=0.613935;E[N]=9.89602
1.481135[b] 0.378541[b] 1.864734[a] 0.146367[b] 0.870034[a] 1.122585[b] 1.230249[a] 0.162378[a] 0.986370[b] 0.527478[b] 0.195797[a] 0.715771[b] 0.330115[b] 0.245349[a] 0.332168[a] 0.087605[a] 0.455150[a] 0.657011[a] 0.117586[b] 0.349823[a] 0.484708[a] 1.530152[b] 0.494842[a] 0.450753[b] 1.000068[a] 0.624084[b]
0.948685[a] 0.905922[b] 0.192523[b] 0.281513[b] 0.745860[a] 1.810471[b] 0.744752[a] 0.704589[b] 0.755338[a] 0.369273[a] 0.724206[a]
0.973425[a] 0.253740[b] 1.197395[b] 1.043538[a] 0.494530[a] 0.761820[b] 0.336180[b] 0.801867[a] 1.583467[b] 0.960314[a] 1.265492[b]
1.252772[b] 1.285070[a] 0.100997[b] 0.060157[b] 0.260177[b] 0.420936[b] 0.226412[b] 0.835463[b]
$ wordgen noclock.prism --seed 42 -v 5 --output-format word --debug --boltzmann 0.48 --receding 10 | sed 's/[[][0-9]*[.][0-9]*s[]]//g'
......
......@@ -27,7 +27,9 @@ let computation ta outfile =
let module Weight = Compute.Instantiate (Fl.Num) (Bound) (Param) () in
let rgpoly = Weight.compute_weight !print_rg !infile rg in
let boltz, smp = Weight.compute_params ?seed:!random_seed rgpoly in
let boltz, smp =
Weight.compute_params ?seed:!random_seed !template rgpoly
in
if !print_rg then printf "%a@." (ZoneGraph.print Bound.print) rgpoly;
......
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