Fix: in the generated lutin demon, the constraint to prevent several actions...

Fix: in the generated lutin demon, the constraint to prevent several actions to be activated in the same process was wrong

lib/sasacore/genLutin.ml

-(* Time-stamp: <modified the 14/03/2019 (at 16:01) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/03/2019 (at 15:13) by Erwan Jahier> *)
 
 open Process
 
+let (gen_atmost_macro : int -> string) =
+  fun n ->
+    let xs = List.init n (fun i -> Printf.sprintf "x%d" (i+1))  in
+    let notxs = List.map (fun x -> Printf.sprintf "not(%s)" x) xs in
+    let x = String.concat "," xs in 
+    let str = ref (Printf.sprintf "let at_most_1_of_%d(%s:bool):bool = \n\t\t(" n x) in
+    str := !str ^(String.concat " and " notxs) ^ ") or\n\t\t(";
+    for i=1 to n do
+      for j=1 to n do
+        let istr = string_of_int j in
+        str := !str ^ (if i=j then "x"^istr else ("not(x"^istr^")")); 
+        str := !str ^ (if j<n then " and " else
+                         if i =n then "" else ") or\n\t\t(");
+      done;
+    done;
+    !str^")\n"
+
 let (f: Process.t list -> string) =
   fun pl ->
     let all = List.map (fun p -> List.map (fun a -> p.pid^"_"^a) p.actions) pl in
@@ -27,13 +44,22 @@ let (f: Process.t list -> string) =
     let one_per_process =  
       (String.concat " and\n\t\t"
          (List.map
-            (fun al -> Printf.sprintf "(not (%s))" (String.concat " and " al))
+            (fun al -> Printf.sprintf "(at_most_1_of_%d(%s))" (List.length al)
+                (String.concat "," al))
             all1
          ))
     in
-
-    let macro = Printf.sprintf "let demon_prop(%s,\n\t%s:bool):bool =\n\t\t%s and\n\t\t%s"
-        (ins "\n\t") (outs "\n\t") acti_if_enab one_per_process 
+    let one_per_process = if one_per_process="" then "" else
+        " and\n\t\t"^one_per_process
+    in
+    let atmost_macro =
+      let n = List.length (List.hd all) in
+      if n < 1 then "" else gen_atmost_macro n
+    in
+    let macro = Printf.sprintf " (* Genarated by sasa *)
+%s
+let demon_prop(%s,\n\t%s:bool):bool =\n\t\t%s%s"
+      atmost_macro (ins "\n\t") (outs "\n\t") acti_if_enab one_per_process 
     in
 
     let distributed = Printf.sprintf