genLutin.ml

(* Time-stamp: <modified the 28/03/2019 (at 18:16) 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
    let al = List.flatten all in
    let ins str = String.concat (","^str)
        (List.map (fun al -> String.concat "," (List.map (fun a -> "Enab_"^a) al)) all)
    in
    let outs str = String.concat  (","^str) (List.map (fun al -> String.concat "," al) all) in
    let acti_if_enab = 
      (String.concat " and\n\t\t"
         (List.map
            (fun al ->
               Printf.sprintf "%s"
                 (String.concat " and\n\t\t"
                    (List.map (fun a ->
                         Printf.sprintf "((not Enab_%s) => (not %s))" a a) al)
                 )
            )
            all
         ))
    in
    let all1 = List.filter (fun al -> List.length al > 1) all in
    let one_per_process =  
      (String.concat " and\n\t\t"
         (List.map
            (fun al -> Printf.sprintf "(at_most_1_of_%d(%s))" (List.length al)
                (String.concat "," al))
            all1
         ))
    in
    let one_per_process = if one_per_process="" then "" else
        " and\n\t\t"^one_per_process
    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 "%s
%s

-- useful for using built-in demons with rdbg (add --dummy-input option to sasa)
node dummy()
returns(_dummy:bool) = loop true

let demon_prop(%s,\n\t%s:bool):bool =\n\t\t%s%s"
        (Mypervasives.entete "--"  SasaVersion.str SasaVersion.sha)
        atmost_macro (ins "\n\t") (outs "\n\t") acti_if_enab one_per_process 
    in

    let distributed = Printf.sprintf
        "node distributed(%s:bool)\nreturns(%s:bool) =
  assert\n\t\tdemon_prop(%s,%s)\n  in
  loop\n\t{ %s\n\t|> true -- silent!\n  }\n"
        (ins "\n\t") (outs "\n\t") (ins "\n\t\t\t") (outs "\n\t\t\t")
        (String.concat " or " al)
    in
    let synchronous = Printf.sprintf
        "node synchronous(%s:bool)\nreturns(%s:bool) =
  assert\n\t\tdemon_prop(%s,%s)\n  in
  loop\n\t%s\n"  (ins "\n\t") (outs "\n\t") (ins "\n\t\t\t") (outs "\n\t\t\t")
        (String.concat " and\n\t"
         (List.map
            (fun al ->
               Printf.sprintf "%s"
                 (String.concat " and\n\t"
                    (List.map (fun a ->
                         Printf.sprintf "(Enab_%s = %s)" a a) al)
                 )
            )
            all
         ))
    in
    let central = Printf.sprintf
        "(* 
n-ary xor not yet implemented in lutin
node central(%s:bool)\nreturns(\n\t %s:bool) =
  assert\n\t\tdemon_prop(%s,%s)\n  in
  loop \n\txor(%s)\n *)"
        (ins "\n\t\t") (outs "\n\t\t") (ins "\n\t\t\t") (outs "\n\t\t\t")
        (String.concat "," al)
    in
    Printf.sprintf "%s\n\n%s\n%s\n%s\n" macro distributed synchronous central