Commit 8ac65af4 authored by Benoit Barbot's avatar Benoit Barbot
Browse files

progress

parent f3a4e3fd
Pipeline #2122 passed with stages
in 2 minutes and 54 seconds
......@@ -254,15 +254,17 @@ struct
let module SMCMonitor = Sampling.MakeSMCMonitor (Bt) (P) (State) in
let module SMCSampler = Sampling.Make (Bt) (P) (State) (SMCMonitor) in
let make_estimate n boltz =
let module Samp = SMCSampler (struct
let smp = None
end) in
let rgp2 =
ZoneGraph.copy_map_weight rgp (fun p ->
P.apply_const p P.z (P.F.of_float boltz))
in
let smp = if P.is_exp_poly then compute_s 4.0 rgp2 else None in
let module Samp = SMCSampler (struct
let smp = smp
end) in
if
P.to_float @@ rgp2.statelist.(rgp2.init).loc_weight
P.to_float ?smp @@ rgp2.statelist.(rgp2.init).loc_weight
|>>> (fun x -> x < 0.0)
|>>| true
then (0, -.target -. 1.0, 0.0)
......
......@@ -49,6 +49,8 @@ struct
let var_string = P.var_string
let is_exp_poly = true
let z = P.z
let s = P.s
......@@ -352,30 +354,38 @@ struct
| None, None -> failwith "No value for s parameter"
let apply_const ?smp ep var c =
let s = smpv ?smp () in
if var = Param.svar then assert (F.to_float c = s);
Poly.fold
(fun k v acc ->
let v2 = P.apply_const ?smp v var c in
match (k, var = Param.svar) with
| Infinite, _ -> assert false
| Const _, false -> add_mon k v2 acc
| Finite (_, var2), false when var2 <> var -> add_mon k v2 acc
| Finite (a, _), false ->
let isvart = if var = Param.tvar then -1.0 else 1.0 in
let v3 =
P.( **. )
(F.of_float @@ exp (s *. (float a +. (isvart *. F.to_float c))))
v2
in
add_mon (Const 0) v3 acc
| Const a, true ->
let v3 = P.( **. ) (F.of_float @@ exp (s *. float a)) v2 in
add_mon (Const 0) v3 acc
| Finite (a, v), true ->
let v3 = P.( **. ) (F.of_float @@ exp (s *. float a)) v2 in
add_mon (Finite (0, v)) v3 acc)
ep Poly.empty
if var = z then
Poly.fold
(fun k v acc ->
let v2 = P.apply_const ?smp v var c in
add_mon k v2 acc)
ep Poly.empty
else
let s = smpv ?smp () in
if var = Param.svar then assert (F.to_float c = s);
Poly.fold
(fun k v acc ->
let v2 = P.apply_const ?smp v var c in
match (k, var = Param.svar) with
| Infinite, _ -> assert false
| Const _, false -> add_mon k v2 acc
| Finite (_, var2), false when var2 <> var -> add_mon k v2 acc
| Finite (a, _), false ->
let isvart = if var = Param.tvar then -1.0 else 1.0 in
let v3 =
P.( **. )
( F.of_float
@@ exp (s *. (float a +. (isvart *. F.to_float c))) )
v2
in
add_mon (Const 0) v3 acc
| Const a, true ->
let v3 = P.( **. ) (F.of_float @@ exp (s *. float a)) v2 in
add_mon (Const 0) v3 acc
| Finite (a, v), true ->
let v3 = P.( **. ) (F.of_float @@ exp (s *. float a)) v2 in
add_mon (Finite (0, v)) v3 acc)
ep Poly.empty
let to_float ?smp p =
let smpv2 = smpv ?smp () in
......
......@@ -12,6 +12,8 @@ module Make : functor
-> sig
include Polynomial.WeightStructure
val is_exp_poly : bool
val print_dumb : Format.formatter -> t -> unit
val term : P.t -> Common.bound -> t
......
......@@ -35,6 +35,8 @@ module type WeightStructure = sig
val desc : string
val is_exp_poly : bool
val var_string : VarSet.varset
val nb_var : int
......@@ -161,6 +163,8 @@ struct
type ftp = float Poly.t
let is_exp_poly = false
(*let var_string = [|"t"; "x"; "y"; "z"; "x_1"; "x_2";"x_3";"x_4";"x_5";"x_6";"x_7"|]*)
let z = VarSet.find_var var_string "z"
......
......@@ -35,6 +35,8 @@ module type WeightStructure = sig
val desc : string
val is_exp_poly : bool
val var_string : Common.VarSet.varset
val nb_var : int
......
......@@ -17,6 +17,8 @@ module Make (P : Polynomial.S) = struct
(if P.F.is_exact then "exact rational" else "floating point")
("RationalFraction; " ^ VarSet.to_string var_string)
let is_exp_poly = false
let nb_var = P.nb_var
let zero = (P.zero, P.one)
......
......@@ -83,6 +83,8 @@ module Notdet = struct
type t = { init : int list; trans : TrSet.t array; final : bool array }
let epsilon = { init = [ 0 ]; trans = [| TrSet.empty |]; final = [| true |] }
let of_char c =
{
init = [ 0 ];
......@@ -293,6 +295,13 @@ module Notdet = struct
let minimize a = determinize @@ reverse @@ determinize @@ reverse a
let rec of_regexp = function
| Regexp_type.Empty -> epsilon
| Char c -> of_char c
| Or (r1, r2) -> merge (of_regexp r1) (of_regexp r2)
| Cat (r1, r2) -> cat (of_regexp r1) (of_regexp r2)
| Star r -> star (of_regexp r)
let to_det a =
let a2 = determinize @@ reverse @@ determinize @@ reverse a in
{
......
......@@ -3,22 +3,33 @@ open Regexp_type
%}
%token <char> CHAR
%token LSQBRK, RSQBRK
%token <string> CHAR
%token LSQBRK, RSQBRK
%token LPAR, RPAR
%token STAR
%token PLUS
%token PIPE
%token EOF
%type <Regexp_type.t> regexp
%start regexp
%left PIPE
%type <Regexp_type.t> main
%start main
%%
regexp:
| EOF {Empty}
| LPAR regexp RPAR { $2 }
| LPAR regexp RPAR regexp { Cat($2,$4) }
| LPAR regexp RPAR PIPE regexp { Or($2,$5) }
| CHAR PIPE regexp { Or(Char $1,$3) }
| CHAR regexp { Cat(Char $1,$2) }
| CHAR {
let s = $1 in
let l = ref (Char (s.[0])) in
for i=1 to String.length s -1 do
l := Cat( !l , Char s.[i]);
done;
!l }
| regexp regexp { Cat($1,$2) }
| LPAR regexp RPAR { $2 }
| regexp PIPE regexp { Or( $1,$3) }
| regexp STAR { Star( $1) }
main:
regexp EOF {$1}
......@@ -7,14 +7,13 @@ let letter = ['a'-'z' 'A'-'Z']
rule tok = parse
'(' {LPAR}
| ')' {RPAR}
'(' {LPAR}
| ')' {RPAR}
| ']' {RSQBRK}
| '[' {LSQBRK}
| '*' {STAR}
| '+' {PLUS}
| '|' {PIPE}
| ')' {RPAR}
| letter {CHAR ((Lexing.lexeme lexbuf).[0]) }
| letter+ {CHAR ((Lexing.lexeme lexbuf)) }
| "\n" { EOF }
| eof { EOF }
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