From 045e624f94fd36e7c9ef94514a1921eb046659bd Mon Sep 17 00:00:00 2001
From: Nicolas Berthier <nicolas.berthier@inria.fr>
Date: Tue, 2 Dec 2014 10:13:09 +0100
Subject: [PATCH] Bug fix with controllable-less contracts in ControllableNbac
 exporter.

---
 compiler/minils/ctrln/ctrlNbacGen.ml | 31 ++++++++++++++++------------
 1 file changed, 18 insertions(+), 13 deletions(-)

diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml
index bf48cf3..47003b1 100644
--- a/compiler/minils/ctrln/ctrlNbacGen.ml
+++ b/compiler/minils/ctrln/ctrlNbacGen.ml
@@ -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 }
 
 (* --- *)