Commit a6c0ea42 authored by erwan's avatar erwan
Browse files

Fix: force generated lutin demon to activate at least one action

parent 7105bae2
(* Time-stamp: <modified the 20/03/2019 (at 15:13) by Erwan Jahier> *)
(* Time-stamp: <modified the 21/03/2019 (at 17:40) by Erwan Jahier> *)
open Process
......@@ -7,7 +7,10 @@ let (gen_atmost_macro : int -> string) =
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
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
......@@ -52,14 +55,16 @@ let (f: Process.t list -> string) =
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 nl = List.map (fun al -> List.length al) all in
let nl = List.sort_uniq compare nl in
let nl = List.filter (fun n -> n>1) nl in
let atmost_macro_l = List.map gen_atmost_macro nl in
let atmost_macro = String.concat "\n" atmost_macro_l in
let atleastone = "("^(String.concat " or " al)^") and " 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
let demon_prop(%s,\n\t%s:bool):bool =\n\t\t%s\n\t\t%s%s"
atmost_macro (ins "\n\t") (outs "\n\t") atleastone acti_if_enab one_per_process
in
let distributed = Printf.sprintf
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment