From ef536f412d6fa51c6d60edbddc62bf9948f73bdb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= <gwenael.delaval@inria.fr>
Date: Fri, 23 Nov 2012 12:23:17 +0100
Subject: [PATCH] Added option -nosink (CS optimisation)

The -nosink option suppress the sink state of sigali equations.

This optimizes the controller synthesis, but work only
when the synthesis objective instantaneoulsy depends only
on the current state (and not on current inputs).
---
 compiler/main/heptc.ml                        |  1 +
 compiler/minils/sigali/sigalimain.ml          | 33 +++++++++++--------
 compiler/utilities/global/compiler_options.ml |  3 ++
 3 files changed, 24 insertions(+), 13 deletions(-)

diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml
index 13a58c9..71b8bee 100644
--- a/compiler/main/heptc.ml
+++ b/compiler/main/heptc.ml
@@ -148,6 +148,7 @@ let main () =
         "-fname", Arg.Set full_name, doc_full_name;
         "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion;
         "-strict_ssa", Arg.Unit set_strict_ssa, doc_strict_ssa;
+	"-nosink", Arg.Set nosink, doc_nosink;
         "-memalloc", Arg.Unit do_mem_alloc_and_typing, doc_memalloc;
         "-only-memalloc", Arg.Set do_mem_alloc, doc_memalloc_only;
         "-only-linear", Arg.Set do_linear_typing, doc_linear_only;
diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml
index 8fb77e1..f72adfc 100644
--- a/compiler/minils/sigali/sigalimain.ml
+++ b/compiler/minils/sigali/sigalimain.ml
@@ -402,19 +402,26 @@ let translate_node
       (fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
       (sig_inputs@sig_ctrl) in
   let constraints = constraints @ [Sequal (a_c,Sconst(Ctrue))] in
-  (* Sink state when the guarantee part of the contract becomes false *)
-  (* f_error_state state variable initialized to true; become false
-     the instant after the guarantee part is false *)
-  let error_state_name = f ^ "_error_state" in
-  let sig_states_full = sig_states @ [error_state_name] in
-  let body_sink =
-    [(extend
-        initialisations
-        (Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
-     (extend
-        evolutions
-        (Slist[g_c]))] in
-  let obj = Security(Svar(error_state_name)) in
+  let body_sink, sig_states_full, obj_exp =
+    if !Compiler_options.nosink then
+      ([], sig_states, g_c)
+    else
+      begin
+	(* Sink state when the guarantee part of the contract becomes false *)
+	(* f_error_state state variable initialized to true; become false
+	   the instant after the guarantee part is false *)
+	let error_state_name = f ^ "_error_state" in
+	let sig_states_full = sig_states @ [error_state_name] in
+	let body_sink =
+	  [(extend
+              initialisations
+              (Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
+	   (extend
+              evolutions
+              (Slist[g_c]))] in
+	(body_sink, sig_states_full, Svar(error_state_name))
+      end in
+  let obj = Security(obj_exp) in
   let p = { proc_dep = [];
             proc_name = f;
             proc_inputs = sig_inputs@sig_ctrl;
diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml
index 01fcc27..3109339 100644
--- a/compiler/utilities/global/compiler_options.ml
+++ b/compiler/utilities/global/compiler_options.ml
@@ -85,6 +85,8 @@ let create_object_file = ref false
 
 let boolean = ref false
 
+let nosink = ref false
+
 (* Target languages list for code generation *)
 let target_languages : string list ref = ref []
 
@@ -190,6 +192,7 @@ and doc_target_path =
   "<path>\tGenerated files will be placed in <path>\n\t\t\t(the directory is"
   ^ " cleaned)"
 and doc_boolean = "\t\tTranslate enumerated values towards boolean vectors"
+and doc_nosink = "\t\tSuppress the sink state in sigali equations"
 and doc_deadcode = "\t\tDeadcode removal"
 and doc_nocaus = "\t\tDisable causality analysis"
 and doc_noinit = "\t\tDisable initialization analysis"