genLutin.ml

(* 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
    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 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
        "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