From 2d00f0a91cfcaae1dde0781fc11b140e9666ea43 Mon Sep 17 00:00:00 2001
From: Nicolas Berthier <nicolas.berthier@inria.fr>
Date: Fri, 31 Oct 2014 14:41:42 +0100
Subject: [PATCH] Fix sink state variable generation in Controllable-Nbac
 export.

---
 compiler/minils/ctrln/ctrlNbacGen.ml    | 29 +++++++++++++++----------
 compiler/utilities/ctrln/ctrln_utils.ml |  1 -
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml
index b9e6aa3..6e8c8bd 100644
--- a/compiler/minils/ctrln/ctrlNbacGen.ml
+++ b/compiler/minils/ctrln/ctrlNbacGen.ml
@@ -374,18 +374,18 @@ let declare_contr (decls, contrs, vds)
   SMap.add v (id, ty) contrs,
   vd :: vds
 
+let declare_contrs acc cl =
+  fst & List.fold_left
+    (fun (acc, rank) c -> (declare_contr acc c rank, AST.succ rank))
+    (acc, one) cl
+
 (** Contract translation *)
 let translate_contract ~pref gd
     ({ c_local;           c_eq = equs;
        c_assume = a;      c_enforce = g;
        c_assume_loc = a'; c_enforce_loc = g';
-       c_controllables = cl } as contract) =
-  let declare_contrs acc cl =
-    fst & List.fold_left
-      (fun (acc, rank) c -> (declare_contr acc c rank, AST.succ rank))
-      (acc, one) cl
-  in
-
+       c_controllables = cl } as contract)
+    =
   let pref = prefix_vars ~pref c_local in
   let decls, contrs, locals = declare_contrs (gd.decls, SMap.empty, []) cl in
   let c = SMap.fold (fun v _ -> SSet.add v) contrs SSet.empty in
@@ -394,14 +394,16 @@ let translate_contract ~pref gd
   let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a')
   and ok = as_bexp & mk_and (translate_ext ~pref g) (translate_ext ~pref g') in
 
-  let gd, ok =
+  let gd, ok, locals =                  (* Generate error variable if needed: *)
     if !Compiler_options.nosink
-    then (gd, ok)
-    else let sink = gen_var "" sink_state_str in
+    then (gd, ok, locals)
+    else let sink = gen_var "cn" "error_state" in
          let sink_expr = mk_bref' & pref & mk_symb & name sink in
-         let ok = `Bexp ((* mk_bcond' gd.init_cond tt *) ok) in
-         (add_state_var ~pref gd sink Initial.tbool ok None, sink_expr)
+         let ok = `Bexp (mk_bcond' gd.init_cond tt ok) in
+         (add_state_var ~pref gd sink Initial.tbool ok None, sink_expr,
+          mk_var_dec sink Initial.tbool Linearity.Ltop Clocks.Cbase :: locals)
   in
+
   let assertion = mk_and' gd.assertion ak
   and invariant = mk_and' gd.invariant ok in
   ({ gd with assertion; invariant; }, { contract with c_eq = equs'; }, locals)
@@ -517,6 +519,9 @@ let translate_node ~requal_types typdefs = function
   | ({ n_contract = None } as node) -> node, None
   | ({ n_name; n_input; n_output; n_local; n_equs;
        n_contract = Some contr } as node) ->
+
+      enter_node n_name;              (* for optional sink symbol generation. *)
+
       let pref p = p in
       let local = List.fold_left register_var_typ SMap.empty n_local in
       let input = List.fold_left register_var_typ SMap.empty n_input in
diff --git a/compiler/utilities/ctrln/ctrln_utils.ml b/compiler/utilities/ctrln/ctrln_utils.ml
index b8912d1..b6aa5ae 100644
--- a/compiler/utilities/ctrln/ctrln_utils.ml
+++ b/compiler/utilities/ctrln/ctrln_utils.ml
@@ -67,4 +67,3 @@ let save_controller_modul_for modul =
   Modules.select om
 
 let init_cond_str = "__init__"                             (* XXX uniqueness? *)
-and sink_state_str = "__sink__"