diff --git a/bin/genLutin.ml b/bin/genLutin.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8cda553497dbfd69e671f56f5d8422b11bec5682
--- /dev/null
+++ b/bin/genLutin.ml
@@ -0,0 +1,72 @@
+(* Time-stamp: <modified the 14/03/2019 (at 16:01) by Erwan Jahier> *)
+
+open Process
+
+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 "(not (%s))" (String.concat " and " 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
+ 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
+
diff --git a/bin/genLutin.mli b/bin/genLutin.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ac5c2f0221836230d87452521d694162c9bbae11
--- /dev/null
+++ b/bin/genLutin.mli
@@ -0,0 +1,4 @@
+(* Time-stamp: <modified the 14/03/2019 (at 13:21) by Erwan Jahier> *)
+
+
+val f: Process.t list -> string
diff --git a/bin/sasArg.ml b/bin/sasArg.ml
index 5dca76ec1aa8b3288e426f54bfa30fab3e02ff53..eb4723710c6273d5fa7382e546abb4acf23abee6 100644
--- a/bin/sasArg.ml
+++ b/bin/sasArg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 13/03/2019 (at 16:59) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/03/2019 (at 13:36) by Erwan Jahier> *)
type t = {
@@ -8,6 +8,7 @@ type t = {
mutable demon: Demon.t;
mutable rif: bool;
mutable ifi: bool;
+ mutable gen_lutin: bool;
mutable _args : (string * Arg.spec * string) list;
mutable _user_man : (string * string list) list;
@@ -32,7 +33,8 @@ let (make_args : unit -> t) =
demon = Demon.Distributed;
rif = false;
ifi = false;
- _args = [];
+ gen_lutin = false;
+ _args = [];
_user_man = [];
_hidden_man = [];
_others = [];
@@ -107,6 +109,10 @@ let (mkoptab : t -> unit) =
(Arg.Unit(fun () -> args.rif <- true))
["Follows RIF conventions"];
+ mkopt opt ["--gen-lutin-demon";"-gld"]
+ (Arg.Unit(fun () -> args.gen_lutin <- true))
+ ["Generate Lutin demons and exit"];
+
mkopt opt ["--ignore-first-inputs"; "-ifi"]
(Arg.Unit(fun () -> args.ifi <- true))
["Ignore first inputs (necessary to use luciole via lurette/rdbg/luciole-rif)"];
diff --git a/bin/sasa.ml b/bin/sasa.ml
index 392cb5c142d60380df8f0b7a8b5381ad5330752e..ca38f9c5bd99061fa58a925a9c71471ad4ccee9c 100644
--- a/bin/sasa.ml
+++ b/bin/sasa.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 13/03/2019 (at 18:04) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/03/2019 (at 16:06) by Erwan Jahier> *)
(* XXX Je pourrais utiliser Lwt pour rendre step non-bloquant, ce qui
permettrait d'accelerer la simu sur les machines qui ont plusieurs
@@ -143,14 +143,14 @@ let rec (simu: int -> int -> Process.t list -> string ->
let () =
( try SasArg.parse Sys.argv;
with
- Failure(e) ->
- output_string stdout e;
- flush stdout ;
- exit 2
- | e ->
- output_string stdout (Printexc.to_string e);
- flush stdout;
- exit 2
+ Failure(e) ->
+ output_string stdout e;
+ flush stdout ;
+ exit 2
+ | e ->
+ output_string stdout (Printexc.to_string e);
+ flush stdout;
+ exit 2
);
let dot_file = SasArg.args.topo in
let nl = Topology.read dot_file in
@@ -167,6 +167,16 @@ let () =
let e = update_env_with_init e pl algo_neighors in
let pl_n = List.combine pl neighors in
if !Algo.verbose_level > 0 then List.iter dump_process pl_n;
+ if SasArg.args.gen_lutin then (
+ let fn = (Filename.remove_extension SasArg.args.topo) ^ ".lut" in
+ if Sys.file_exists fn then (
+ Printf.eprintf "%s already exists.\n" fn; flush stderr
+ ) else
+ let oc = open_out fn in
+ Printf.fprintf oc "%s" (GenLutin.f pl);
+ flush oc;
+ close_out oc;
+ exit 0);
let n = SasArg.args.length in
if SasArg.args.rif then (
Printf.printf "#inputs %s\n"
@@ -176,7 +186,7 @@ let () =
p.actions
in
String.concat " " (List.flatten (List.map f pl))
- ) else "");
+ ) else "");
Printf.printf "#outputs %s\n" (StringOf.env_rif_decl pl);
flush stdout
);
@@ -193,7 +203,7 @@ let () =
| Failure msg -> Printf.printf "Error: %s\n" msg
| Silent i ->
let str = if SasArg.args.rif then "#" else "" in
- Printf.printf "%sThis algo is silent after %i steps\n" str i ;
+ Printf.printf "%sThis algo is silent after %i steps\n" str i ;
flush stdout;
if SasArg.args.rif && args.demon = Custom then (
print_string "q\n"; flush stdout
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index 5e8f5b9d1fd8fdb6c91896e42e073a70fa799346..a16bbf9faa0ec50d20db4ff34d3e187380d4547a 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 13/03/2019 (at 18:01) by Erwan Jahier>
+# Time-stamp: <modified the 14/03/2019 (at 13:40) by Erwan Jahier>
test: test0 lurette0
test0: cmxs
@@ -6,6 +6,9 @@ test0: cmxs
cmxs:root.cmxs p.cmxs
+lutin:
+ $(sasa) -gld fig5.1-noinit.dot
+
test2: cmxs
$(sasa) -l 200 fig5.1.dot -sd
@@ -15,6 +18,9 @@ sim2chrogtk: fig5.1-noinit.rif
gnuplot: fig5.1-noinit.rif
gnuplot-rif $<
+gnuplot2: fig5.2.rif
+ gnuplot-rif $<
+
lurette0:cmxs
lurette -o lurette.rif \
-env "$(sasa) fig5.1-noinit.dot -custd -rif" \
diff --git a/test/bfs-spanning-tree/demon.lut b/test/bfs-spanning-tree/demon.lut
index fc881c28430d081b77d0043c5404d419a3b7d88d..a1d905deea1ad9d83898d18f4955c3092289def3 100644
--- a/test/bfs-spanning-tree/demon.lut
+++ b/test/bfs-spanning-tree/demon.lut
@@ -19,7 +19,14 @@ let demon_prop(
((not Enab_p6_CP) => (not p6_CP)) and
((not Enab_p7_CD) => (not p7_CD)) and
((not Enab_p7_CP) => (not p7_CP)) and
- ((not Enab_p8_CD) => (not p8_CD))
+ ((not Enab_p8_CD) => (not p8_CD)) and
+ (not (p2_CD and p2_CP)) and
+ (not (p3_CD and p3_CP)) and
+ (not (p4_CD and p4_CP)) and
+ (not (p5_CD and p5_CP)) and
+ (not (p6_CD and p6_CP)) and
+ (not (p7_CD and p7_CP)) and
+ (not (p8_CD and p8_CP))
node distributed (Enab_p1_CD,Enab_p2_CD,Enab_p2_CP,Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,