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

implement cosim

parent c48b8708
Pipeline #2209 passed with stages
in 2 minutes and 45 seconds
......@@ -94,8 +94,10 @@ struct
let end_sampling _ = ()
module StringMap = Map.Make (String)
let up_state ((outfile, rgpoly, (ost, is_interactive), _, parse_action) : t)
?smp (st : State.t) i (_, u2) =
?smp (st : State.t) i (u1, u2) =
( match ost with
| TimewordState -> fprintf outfile "(%a)@." print_state st
| StateList -> fprintf outfile "%a@." print_state st
......@@ -114,33 +116,68 @@ struct
if tr1.ZoneGraph.action <> tr2.ZoneGraph.action then
compare tr1.ZoneGraph.action tr2.ZoneGraph.action
else compare low1 low2)
|> List.iter (fun (tr, low, up) ->
if Array.length tr.ZoneGraph.weight > 0 then
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-%g->\"%s\"@,"
tr.ZoneGraph.action low up w time target.name
else fprintf f "[%s]-[%g;%g]@," tr.ZoneGraph.action low up))
|> List.filter (fun (tr, _, _) ->
Array.length tr.ZoneGraph.weight > 0)
|> List.map (fun (tr, low, up) ->
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
(tr, (low, up, w, time)))
|> List.fold_left
(fun acc (tr, inst) ->
StringMap.update tr.ZoneGraph.action
(function
| Some l -> Some ((tr, inst) :: l)
| None -> Some [ (tr, inst) ])
acc)
StringMap.empty
|> StringMap.map (fun l ->
let totalw, accl =
List.fold_left
(fun (acc, l) ((_, (_, _, w, _)) as inst) ->
(acc +. w, ((acc, acc +. w), inst) :: l))
(0.0, []) l
in
let skip = u1 *. totalw in
let n = List.length accl in
match accl with
| [] -> None
| [ (_, tr) ] -> Some tr
| _ when u1 = 1.0 -> Some (snd @@ List.nth accl (n - 1))
| _ when skip > 0.0 ->
Some
( snd
@@ List.find
(fun ((x, y), _) -> x <= skip && skip < y)
accl )
| _ ->
Some
( snd
@@ List.nth accl
(min (int_of_float (u1 *. float n)) (n - 1)) ))
|> StringMap.iter (fun _ v ->
match v with
| Some (tr, (low, up, _, time)) ->
let target =
rgpoly.statelist.((List.hd tr.ZoneGraph.miniedge)
.target)
in
fprintf f "[%s]-[%g;%g]-%g->\"%s\"@," tr.ZoneGraph.action
low up time target.name
| None -> ()))
rgpoly.ZoneGraph.statelist.(get_loc st).ZoneGraph.transition
| Debug ->
fprintf outfile "@[<h 0>%a@. @[<v 2>@[<v 0>%a@]@]@]@."
......
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