jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Bug fix with controllable-less contracts in ControllableNbac exporter.

Browse source
This commit is contained in:
Nicolas Berthier 2014-12-02 10:13:09 +01:00
parent 2a0927bd98
commit 045e624f94
1 changed files with 18 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
compiler/minils/ctrln/ctrlNbacGen.ml
View file

@ -435,19 +435,24 @@ let finalize_uc_groups gd =
let assign_uc_groups gd =
let gd = finalize_uc_groups gd in
let uc_groups = List.rev gd.uc_groups in (* start from the first group *)
let decls, _ = List.fold_left begin fun (decls, group) (u, c) ->
let decls = SSet.fold (fun u decls -> match SMap.find u decls with
| (t, `Input _, l) ->
SMap.add u (t, `Input group, l) decls
| _ -> decls) u decls
in
let decls = SSet.fold (fun c decls -> match SMap.find c decls with
| (t, `Contr (_, r, l'), l) ->
SMap.add c (t, `Contr (group, r, l'), l) decls
| _ -> decls) c decls
in
decls, AST.succ group
end (gd.decls, AST.succ one) (List.tl uc_groups) in
let decls, _ =
if uc_groups = [] then
gd.decls, one (* no group to change *)
else
List.fold_left begin fun (decls, group) (u, c) ->
let decls = SSet.fold (fun u decls -> match SMap.find u decls with
| (t, `Input _, l) ->
SMap.add u (t, `Input group, l) decls
| _ -> decls) u decls
in
let decls = SSet.fold (fun c decls -> match SMap.find c decls with
| (t, `Contr (_, r, l'), l) ->
SMap.add c (t, `Contr (group, r, l'), l) decls
| _ -> decls) c decls
in
decls, AST.succ group
end (gd.decls, AST.succ one) (List.tl uc_groups)
in
{ gd with decls; uc_groups }
(* --- *)