diff --git a/lib/sasa/sasaRun.ml b/lib/sasa/sasaRun.ml
index 299227c4363bdb9dbcf9725e73db3c5f38e77e3e..3b051f81941af6b6387698e45223cf9025076342 100644
--- a/lib/sasa/sasaRun.ml
+++ b/lib/sasa/sasaRun.ml
@@ -21,7 +21,7 @@ let (from_sasa_env : 'v Main.layout -> 'v Env.t -> RdbgPlugin.sl) =
List.fold_left
(fun acc (p,_) ->
let state = Env.get e p.pid in
- let sl = State.to_rdbg_subst p.pid state in
+ let sl = SasaState.to_rdbg_subst p.pid state in
acc@sl
)
[]
diff --git a/lib/sasacore/genRegister.ml b/lib/sasacore/genRegister.ml
new file mode 100644
index 0000000000000000000000000000000000000000..241461dccfdbb2d3e283761fdca214e18d784618
--- /dev/null
+++ b/lib/sasacore/genRegister.ml
@@ -0,0 +1,75 @@
+(*
+takes as input some ocaml files, and generates an ocaml file
+that (Algo.)register(s) the corresponding algorithms.
+
+More precisely, the input files ougth to define a module inplementing
+the following interface:
+
+ val name: string
+ val actions : string list option;
+ type state
+ val init_state: int -> state
+ val enable_f: state Algo.neighbor list -> state -> Algo.action list
+ val step_f : state Algo.neighbor list -> state -> Algo.action -> state
+ val state_to_string: state -> string
+ val state_copy : state -> dfs_value
+
+ *)
+
+let ml_filename_to_module fn =
+ let str = Filename.chop_extension fn in
+ String.capitalize_ascii str
+
+let from_ml ml =
+ let m = ml_filename_to_module ml in
+ Printf.sprintf "
+ {
+ algo_id = \"%s\";
+ init_state = %s.init_state;
+ actions = %s.actions;
+ enab = %s.enable_f;
+ step = %s.step_f;
+ }" (String.uncapitalize_ascii m) m m m m
+
+
+let (f: string list -> string * string -> unit) =
+ fun ml_ins (state_file, register_file) ->
+ let state_module = ml_filename_to_module state_file in
+ if Sys.file_exists register_file then (
+ Printf.printf "Warning: %s already exist.\n" register_file
+ ) else (
+ let oc = open_out register_file in
+ let entete = Mypervasives.entete2 "(*" "*)" SasaVersion.str SasaVersion.sha in
+ let l = List.map from_ml ml_ins in
+ Printf.fprintf oc "%s" entete ;
+ Printf.fprintf oc "let () =
+ Algo.register {
+ algo = [ %s ];
+ state_to_string = %s.to_string;
+ state_of_string = %s.of_string;
+ copy_state = %s.copy;
+ }
+"
+ (String.concat ";" l)
+ state_module state_module state_module ;
+ flush oc;
+ close_out oc;
+ Printf.printf "The file %s has been generated\n" register_file;
+ flush stdout
+ );
+ if Sys.file_exists state_file then (
+ Printf.printf "Warning: %s already exist.\n" state_file
+ ) else (
+ let oc = open_out state_file in
+ let entete = Mypervasives.entete2 "(*" "*)" SasaVersion.str SasaVersion.sha in
+ Printf.fprintf oc "%s" entete ;
+ Printf.fprintf oc "type t = define_me
+let to_string _ = \"define_me\"
+let of_string = None
+let copy x = x
+";
+ flush oc;
+ close_out oc;
+ Printf.printf "The file %s has been generated\n" state_file;
+ flush stdout
+ )
diff --git a/lib/sasacore/genRegister.mli b/lib/sasacore/genRegister.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2a1d00b9cc1f74918d33ca2a6ce7d6bb7535c316
--- /dev/null
+++ b/lib/sasacore/genRegister.mli
@@ -0,0 +1,27 @@
+
+(** Takes as input some ocaml files and the output file name, and
+ generates 2 ocaml files
+ - 1 that defines a skeleton ocaml program for dealing with algo states
+ - 1 that (Algo.)register(s) the (input) algorithms.
+
+ Existing output file won't be overrided (a warning is printed).
+
+ The input files ougth to define a module implementing the following interface:
+
+ val name: string
+ val actions : string list option;
+ val init_state: int -> state
+ val enable_f: state Algo.neighbor list -> state -> Algo.action list
+ val step_f : state Algo.neighbor list -> state -> Algo.action -> state
+ val state_to_string: state -> string
+
+ The algo state definition file implements the following interface:
+
+ type state
+ val state_copy : state -> state
+ val state_of_string: (string -> state) option
+ val copy_state: state -> state
+
+ *)
+
+val f: string list -> string * string -> unit
diff --git a/lib/sasacore/main.ml b/lib/sasacore/main.ml
index 3af7e1279aa8790660f5b18701b3c52f582ceb05..1d1a0ecd2cc110dce68cc9f7fdb82bc35d2ff8e1 100644
--- a/lib/sasacore/main.ml
+++ b/lib/sasacore/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/09/2019 (at 16:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:32) by Erwan Jahier> *)
open Register
@@ -42,7 +42,7 @@ let (get_neighors: Topology.t -> Topology.node_id -> 'v -> 'v Register.neighbor
let (dump_process: 'v Process.t * 'v Register.neighbor list -> unit) =
fun (p,nl) ->
- let pvars = String.concat "," (State.to_var_names p.pid p.init) in
+ let pvars = String.concat "," (SasaState.to_var_names p.pid p.init) in
let neighbors = List.map StringOf.algo_neighbor nl in
Printf.printf "process %s\n\tvars:%s\n\tneighors: \n\t\t%s\n" p.pid pvars
(String.concat "\n\t\t" neighbors)
@@ -119,7 +119,7 @@ let (get_outputs_rif_decl: SasArg.t -> 'v Process.t list -> (string * string) li
fun args pl ->
let ll = List.map
(fun p ->
- let l = State.to_rif_decl p.pid p.init in
+ let l = SasaState.to_rif_decl p.pid p.init in
List.map (fun (n,t) -> n, Data.type_to_string t) l
)
pl
@@ -230,9 +230,35 @@ let (make : bool -> string array -> 'v t) =
exit 2
in
try
+ let dynlink = if args.output_algos then false else dynlink in
let dot_file = args.topo in
let g = Topology.read dot_file in
let nl = g.nodes in
+ if args.output_algos then (
+ let fl = List.map (fun n -> n.Topology.file) nl in
+ let fl = List.sort_uniq compare fl in
+ Printf.printf "%s\n" (String.concat " " fl);
+ flush stdout;
+ exit 0
+ );
+ let cmxs = (Filename.chop_extension dot_file) ^ ".cmxs" in
+ if args.gen_register then (
+ let base = Filename.chop_extension dot_file in
+ let base = Str.global_replace (Str.regexp "\\.") "" base in
+ let ml_register_file = base ^ ".ml" in
+ let ml_state_file = "state.ml" in
+ let algo_files = List.map (fun n -> n.Topology.file) nl in
+ let algo_files = List.sort_uniq compare algo_files in
+ let ml_inputs = String.concat " " algo_files in
+ GenRegister.f algo_files (ml_state_file, ml_register_file);
+ Printf.printf "Hint: you may wish to generate %s out of %s with:\n"
+ cmxs ml_register_file;
+ Printf.printf " ocamlfind ocamlopt -package algo -shared %s %s %s -o %s\n"
+ ml_state_file ml_inputs ml_register_file cmxs;
+ flush stdout;
+ exit 0
+ );
+
let nidl = List.map (fun n -> n.Topology.id) nl in
let nstr = String.concat "," nidl in
Register.set_card (fun () -> List.length nl);
@@ -247,9 +273,12 @@ let (make : bool -> string array -> 'v t) =
Random.init args.seed;
if !Register.verbose_level > 0 then Printf.eprintf "nodes: %s\nedges:\n" nstr;
- let algo_files = List.map (fun n -> n.Topology.file) nl in
- if dynlink then List.iter Process.dynlink_nodes (List.sort_uniq compare algo_files);
-
+ if dynlink then (
+ (* Dynamically link the cmxs file (not possible from rdbg) *)
+ if !Register.verbose_level > 0 then Printf.printf "Loading %s...\n" cmxs;
+ Dynlink.loadfile (Dynlink.adapt_filename cmxs);
+ );
+
let initl = List.map (fun n ->
let algo_id = Filename.chop_suffix n.Topology.file ".ml" in
let value_of_string_opt = Register.get_value_of_string () in
@@ -269,13 +298,6 @@ let (make : bool -> string array -> 'v t) =
let e = update_env_with_init e pl in
let pl_n = List.combine pl algo_neighors in
if !Register.verbose_level > 0 then List.iter dump_process pl_n;
- if args.output_algos then (
- let fl = List.map (fun n -> Filename.chop_extension n.Topology.file) nl in
- let fl = List.sort_uniq compare fl in
- Printf.printf "%s\n" (String.concat "\n" fl);
- flush stdout;
- exit 0
- );
if args.gen_lutin then (
let fn = (Filename.remove_extension args.topo) ^ ".lut" in
if Sys.file_exists fn then (
diff --git a/lib/sasacore/process.ml b/lib/sasacore/process.ml
index e8ab45aad7fe4035f5a85234e97735bf5a2d8e4a..8971c7632da5f3d8ff495f5ebd323af0abb3615b 100644
--- a/lib/sasacore/process.ml
+++ b/lib/sasacore/process.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 03/07/2019 (at 15:53) by Erwan Jahier> *)
+(* Time-stamp: <modified the 06/09/2019 (at 15:51) by Erwan Jahier> *)
type 'v t = {
pid : string;
@@ -8,14 +8,6 @@ type 'v t = {
step : 'v Register.step_fun ;
}
-
-let (dynlink_nodes: string -> unit) =
- fun ml ->
- let id = Filename.chop_suffix ml ".ml" in
- let cmxs = id^".cmxs" in
- if !Register.verbose_level > 0 then Printf.printf "Loading %s...\n" cmxs;
- Dynlink.loadfile (Dynlink.adapt_filename cmxs)
-
let (make: bool -> Topology.node -> 'v -> 'v t) =
fun custom_mode n init ->
let pid = n.Topology.id in
diff --git a/lib/sasacore/process.mli b/lib/sasacore/process.mli
index e24cc396dadf22db8085dfc7074c8b71ab4eaa41..0fbc4d3ad61ba2981d146dbe3e7635fcba29db1f 100644
--- a/lib/sasacore/process.mli
+++ b/lib/sasacore/process.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/06/2019 (at 10:47) by Erwan Jahier> *)
+(* Time-stamp: <modified the 06/09/2019 (at 15:51) by Erwan Jahier> *)
(** There is such a Process.t per node in the dot file. *)
type 'v t = {
@@ -9,10 +9,6 @@ type 'v t = {
step : 'v Register.step_fun;
}
-
-(* Dynamically link the algo_nodes.cmxs files (not possible from rdbg) *)
-val dynlink_nodes: string -> unit
-
(** [make custom_mode_flag node init_state] builds a process out of a dot
node. To do that, it retreives the registered functions by Dynamic
linking of the cmxs file specified in the "algo" field of the dot
diff --git a/lib/sasacore/sasArg.ml b/lib/sasacore/sasArg.ml
index 425b46237df8cfe774535a90066f9a7eda2ff296..1cfac9f8cbf08c7940fe9a64de1faddc4253c8cc 100644
--- a/lib/sasacore/sasArg.ml
+++ b/lib/sasacore/sasArg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 25/06/2019 (at 11:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 12/09/2019 (at 08:54) by Erwan Jahier> *)
type t = {
@@ -13,6 +13,7 @@ type t = {
mutable gen_oracle: bool;
mutable dummy_input: bool;
mutable output_algos: bool;
+ mutable gen_register: bool;
mutable _args : (string * Arg.spec * string) list;
mutable _user_man : (string * string list) list;
@@ -42,6 +43,7 @@ let (make_args : unit -> t) =
gen_oracle = false;
dummy_input = false;
output_algos = false;
+ gen_register = false;
_args = [];
_user_man = [];
_hidden_man = [];
@@ -129,7 +131,14 @@ let (mkoptab : string array -> t -> unit) =
mkopt args ~hide:true ["--list-algos";"-algo"]
(Arg.Unit(fun () -> args.output_algos <- true))
- ["Output the algo names used in the dot file and exit. "];
+ ["Output the algo files used in the dot file and exit. "];
+
+ mkopt args ~hide:false ["--gen-register";"-reg"]
+ (Arg.Unit(fun () -> args.gen_register <- true))
+ ["Generates the registering file and exit.
+
+
+ "];
mkopt args ~hide:true ["--dummy-input"]
(Arg.Unit(fun () -> args.dummy_input <- true))
diff --git a/lib/sasacore/sasArg.mli b/lib/sasacore/sasArg.mli
index 0858798814b8e4e022bbc153b0d3c1dce5604edb..25d56e192fd5ce2f9277abf3c0a358786fe8292a 100644
--- a/lib/sasacore/sasArg.mli
+++ b/lib/sasacore/sasArg.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 25/06/2019 (at 11:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 06/09/2019 (at 17:17) by Erwan Jahier> *)
type t = {
mutable topo: string;
@@ -12,6 +12,7 @@ type t = {
mutable gen_oracle: bool;
mutable dummy_input: bool;
mutable output_algos: bool;
+ mutable gen_register: bool;
mutable _args : (string * Arg.spec * string) list;
mutable _user_man : (string * string list) list;
diff --git a/lib/sasacore/state.ml b/lib/sasacore/sasaState.ml
similarity index 100%
rename from lib/sasacore/state.ml
rename to lib/sasacore/sasaState.ml
diff --git a/lib/sasacore/state.mli b/lib/sasacore/sasaState.mli
similarity index 100%
rename from lib/sasacore/state.mli
rename to lib/sasacore/sasaState.mli
diff --git a/lib/sasacore/stringOf.ml b/lib/sasacore/stringOf.ml
index af1d8ff159dbb1ea4a955088e68b98c67822fa92..7db502ab2be315135ea6edadf57dddac120c7aac 100644
--- a/lib/sasacore/stringOf.ml
+++ b/lib/sasacore/stringOf.ml
@@ -21,7 +21,7 @@ let (env_rif: 'v Env.t -> 'v Process.t list -> string) =
fun env pl ->
let l = List.map
(fun p ->
- Printf.sprintf "%s" (State.to_rif_data (Env.get env p.pid)))
+ Printf.sprintf "%s" (SasaState.to_rif_data (Env.get env p.pid)))
pl
in
String.concat " " l
diff --git a/src/dune b/src/dune
index 9adadbd58b8e4495957f53f5e8b795fee81c31c1..2d043061ae631ba5b629d9c386cb6d94889a771a 100644
--- a/src/dune
+++ b/src/dune
@@ -1,4 +1,4 @@
-;; Time-stamp: <modified the 05/09/2019 (at 15:26) by Erwan Jahier>
+;; Time-stamp: <modified the 18/09/2019 (at 15:07) by Erwan Jahier>
(executable
(name sasaMain)
diff --git a/test/Makefile b/test/Makefile
index c5839e6d26d8843a2186696e1b2e8d2bfe2d9164..a6d7b232c5a1cafc00f7f51328a21bf3889c3f10 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -4,9 +4,11 @@ test:
cd dijkstra-ring/ && make
cd unison/ && make
cd coloring/ && make
+ cd alea-coloring/ && make
cd bfs-spanning-tree/ && make
cd dfs/ && make
cd dfs-list/ && make
+
echo "Every test went fine!"
clean:
@@ -14,6 +16,7 @@ clean:
cd dijkstra-ring/ && make clean
cd unison/ && make clean
cd coloring/ && make clean
+ cd alea-coloring/ && make clean
cd bfs-spanning-tree/ && make clean
cd dfs/ && make clean
cd dfs-list/ && make clean
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 8565eefabe2cde93289fcc8c78da5b47042664ff..27bad78fa5b2391e8cd8f8e44c147ab6d087ce15 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 05/09/2019 (at 14:47) by Erwan Jahier>
+# Time-stamp: <modified the 13/09/2019 (at 11:09) by Erwan Jahier>
DIR=../../_build/install/default
@@ -6,20 +6,18 @@ sasa=$(DIR)/bin/sasa -l 100
LIB=-package algo
-%.cmxs: %.ml
- ocamlfind ocamlopt -shared $(LIB) $^ -o $@
-
-%.cmx: %.ml
- ocamlfind ocamlopt $(LIB) $^ -o $@
+.PRECIOUS: .ml
+%.ml: %.dot
+ sasa -reg $<
-%.cma: %.ml
- ocamlfind ocamlc $(LIB) $^ -a -o $@
+%.cmxs: %.ml
+ ocamlfind ocamlopt $(LIB) -shared state.ml $(shell sasa -algo $*.dot) $< -o $@
-%.lut: %.dot
- $(sasa) -gld $^
+%.lut: %.dot %.cmxs
+ $(sasa) -gld $< || echo "==> ok, I'll use the existing $@ file"
-%_oracle.lus: %.dot
- $(sasa) -glos $^
+%_oracle.lus: %.dot %.cmxs
+ $(sasa) -glos $< || echo "==> ok, I'll use the existing $@ file"
%.rif: cmxs %.dot
$(sasa) $(sasaopt) $*.dot -rif > $*.rif
diff --git a/test/alea-coloring/Makefile b/test/alea-coloring/Makefile
index 15f9b40ffd6f24eefeab479841c2ca70204f3a98..be5efc6bc29305b623e803ba4ea25585ba50619f 100644
--- a/test/alea-coloring/Makefile
+++ b/test/alea-coloring/Makefile
@@ -1,10 +1,9 @@
-# Time-stamp: <modified the 05/09/2019 (at 14:47) by Erwan Jahier>
+# Time-stamp: <modified the 12/09/2019 (at 10:44) by Erwan Jahier>
-test: p.cmxs ring.lut
+test: ring.cmxs
$(sasa) -l 200 ring.dot -cd
-cmxs: p.cmxs p.cma
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
@@ -14,18 +13,18 @@ gnuplot: ring.rif
###################################################################
# Interactive session with lutin
-rdbg: p.cma p.cmxs ring.lut
+rdbg: ring.lut ring.ml
rdbg -o ring.rif \
-env "$(sasa) ring.dot -custd -rif" \
-sut-nd "lutin ring.lut -n distributed"
# Interactive session with internal deamons
-rdbg2: p.cma p.cmxs ring.lut
+rdbg2: ring.lut ring.ml
rdbg -o ring.rif \
-env "$(sasa) ring.dot -dd --dummy-input" \
-sut-nd "lutin ring.lut -n dummy"
-rdbg3: p.cma p.cmxs
+rdbg3: ring.ml
rdbg -o ring.rif \
-sut "$(sasa) ring.dot -cd -rif"
@@ -34,4 +33,4 @@ rdbg3: p.cma p.cmxs
-include ../Makefile.inc
clean: genclean
- rm -f rdbg-session*.ml ring.lut load-ring.dot.ml *~
+ rm -f ring.lut *~ ring.ml
diff --git a/test/alea-coloring/p.ml b/test/alea-coloring/p.ml
index 7ec431a28d07b6cc2715f2f73e138c8c0b0e85c4..923347151f4b3b413d68d76194a35a9876a4ff66 100644
--- a/test/alea-coloring/p.ml
+++ b/test/alea-coloring/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/06/2019 (at 17:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 12/09/2019 (at 10:39) by Erwan Jahier> *)
open Algo
@@ -32,22 +32,6 @@ let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
function | _ ->
if (Random.bool ()) then e else (List.hd (free nl))
-let (state_to_string: ('v -> string)) = string_of_int
-let (copy_state : ('v -> 'v)) = fun x -> x
-
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "p";
- init_state = init_state;
- actions = Some ["conflict"];
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = state_to_string;
- state_of_string = None;
- copy_state = copy_state;
- }
+let actions = Some ["conflict"];
+
diff --git a/test/alea-coloring/state.ml b/test/alea-coloring/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..bf935f06d5e0cb5274a946f690648112f7745bcf
--- /dev/null
+++ b/test/alea-coloring/state.ml
@@ -0,0 +1,9 @@
+(* Automatically generated by /home/jahier/sasa/_build/default/src/sasaMain.exe version "2.10.4-1-g9a7f112" ("9a7f112")*)
+(* on crevetete the 12/9/2019 at 10:36:45*)
+(*../../_build/install/default/bin/sasa -l 100 -reg ring.dot*)
+
+type t = int (* fixme *)
+let to_string = string_of_int
+let of_string = Some int_of_string
+let copy = fun x -> x
+
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index de9270b4c7ea7812aceb3e3c284ceca7794ffd18..45b2ebd29c3581f129b2f756e673e9cbf09c8a08 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,65 +1,61 @@
-# Time-stamp: <modified the 05/09/2019 (at 21:32) by Erwan Jahier>
+# Time-stamp: <modified the 18/09/2019 (at 21:34) by Erwan Jahier>
-test: test0 test2 lurette0 lurette1
-test0: cmxs
- $(sasa) -rif -l 200 fig5.1-noinit.dot -sd
+test: test0 test2 lurette0
+test0: fig51_noinit.cmxs
+ $(sasa) -rif -l 200 fig51_noinit.dot -sd
-cmxs:root.cmxs p.cmxs root.cma p.cma
+lutin: fig51_noinit.cmxs
+ $(sasa) -gld fig51_noinit.dot
-root.cmxs:root.ml
- ocamlfind ocamlopt -shared -package algo p.mli root.ml -o root.cmxs
+test2: fig51.cmxs
+ $(sasa) -l 200 fig51.dot -sd
-lutin:
- $(sasa) -gld fig5.1-noinit.dot
-
-test2: cmxs
- $(sasa) -l 200 fig5.1.dot -sd
-
-sim2chrogtk: fig5.1-noinit.rif
+sim2chrogtk: fig51_noinit.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: fig5.1-noinit.rif
+gnuplot: fig51_noinit.rif
gnuplot-rif $<
-gnuplot2: fig5.2.rif
+gnuplot2: fig52.rif
gnuplot-rif $<
-lurette0:cmxs fig5.1-noinit.lut fig5.1-noinit_oracle.lus
+lurette0: fig51_noinit.cmxs fig51_noinit.lut
lurette -o lurette.rif \
- -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
- -sut "lutin fig5.1-noinit.lut -n distributed"
+ -env "sasa fig51_noinit.dot -custd -rif" \
+ -sut "lutin fig51_noinit.lut -n distributed"
+# rdbg -lurette is broken from ocaml 4.08; but lurette works fine
lurette1:lurette1.rif
-lurette1.rif:cmxs fig5.1.lut fig5.1_oracle.lus
+lurette1.rif: fig51.cmxs fig51.lut fig51_oracle.lus
rdbg -lurette -o lurette1.rif \
- -env "$(sasa) fig5.1.dot -dd -rif" \
- -oracle "lv6 fig5.1_oracle.lus -n oracle"
+ -env "$(sasa) fig51.dot -dd -rif" \
+ -oracle "lv6 fig51_oracle.lus -n oracle"
lurette: lurette0
sim2chrogtk -ecran -in lurette.rif > /dev/null
gnuplot-rif lurette.rif
-rdbg: cmxs fig5.1-noinit.lut
+rdbg: fig51_noinit.ml fig51_noinit.lut
rdbg -o lurette.rif \
- -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
- -sut-nd "lutin fig5.1-noinit.lut -n distributed"
+ -env "$(sasa) fig51_noinit.dot -custd -rif" \
+ -sut-nd "lutin fig51_noinit.lut -n distributed"
-rdbg2: cmxs fig5.1.lut
+rdbg2: fig51.ml fig51.lut
rdbg -o lurette.rif \
- -env "$(sasa) fig5.1.dot -custd -rif" \
- -sut-nd "lutin fig5.1.lut -n distributed"
+ -env "$(sasa) fig51.dot -custd -rif" \
+ -sut-nd "lutin fig51.lut -n distributed"
-manual:cmxs fig5.1-noinit.lut
+manual: fig51_noinit.cmxs fig51_noinit.lut
lurette -o lurette.rif --sim2chro \
- -sut "$(sasa) fig5.1-noinit.dot -custd -rif -ifi" \
- -env "lutin fig5.1-noinit.lut -n manual" &&\
+ -sut "$(sasa) fig51_noinit.dot -custd -rif -ifi" \
+ -env "lutin fig51_noinit.lut -n manual" &&\
gnuplot-rif lurette.rif
-include ../Makefile.inc
clean: genclean
- rm -f fig*oracle.lus
+ rm -f fig*oracle.lus fig5*.ml
diff --git a/test/bfs-spanning-tree/fig5.1_oracle.lus b/test/bfs-spanning-tree/fig5.1_oracle.lus
deleted file mode 100644
index ef5c53b9dbc3db38d2b4c95cbe962322af31e509..0000000000000000000000000000000000000000
--- a/test/bfs-spanning-tree/fig5.1_oracle.lus
+++ /dev/null
@@ -1,37 +0,0 @@
--- Automatically generated by /home/jahier/sasa/_build/default/src/sasaMain.exe version "2.10.3" ("42ccc7f")
--- on crevetete the 6/9/2019 at 14:12:45
---../../_build/install/default/bin/sasa -l 100 -glos fig5.1.dot
-
-include "bfs_spanning_tree_oracle.lus"
-const an=2; -- actions number
-const pn=8; -- processes number
-const degree=3;
-const min_degree=2;
-const mean_degree=2.250000;
-const diameter=4;
-const card=8;
-const links_number=9;
-const is_cyclic=true;
-const is_connected=true;
-const is_a_tree=false;
-const adjency=[
- [f,t,f,f,f,f,f,t],
- [t,f,t,f,f,f,f,f],
- [f,t,f,t,f,f,t,f],
- [f,f,t,f,t,f,f,f],
- [f,f,f,t,f,t,f,f],
- [f,f,f,f,t,f,t,f],
- [f,f,t,f,f,t,f,t],
- [t,f,f,f,f,f,t,f]];
-const k=42;
-
-node oracle(p1_CD,p1_CP,p2_CD,p2_CP,p3_CD,p3_CP,p4_CD,p4_CP,p5_CD,p5_CP,p6_CD,p6_CP,p7_CD,p7_CP,p8_CD,p8_CP,Enab_p1_CD,Enab_p1_CP,Enab_p2_CD,Enab_p2_CP,Enab_p3_CD,Enab_p3_CP,Enab_p4_CD,Enab_p4_CP,Enab_p5_CD,Enab_p5_CP,Enab_p6_CD,Enab_p6_CP,Enab_p7_CD,Enab_p7_CP,Enab_p8_CD,Enab_p8_CP:bool) returns (ok:bool);
-var
- Acti:bool^2^8;
- Enab:bool^2^8;
-let
- Acti = [[p1_CD,p1_CP],[p2_CD,p2_CP],[p3_CD,p3_CP],[p4_CD,p4_CP],[p5_CD,p5_CP],[p6_CD,p6_CP],[p7_CD,p7_CP],[p8_CD,p8_CP]];
- Enab = [[Enab_p1_CD,Enab_p1_CP],[Enab_p2_CD,Enab_p2_CP],[Enab_p3_CD,Enab_p3_CP],[Enab_p4_CD,Enab_p4_CP],[Enab_p5_CD,Enab_p5_CP],[Enab_p6_CD,Enab_p6_CP],[Enab_p7_CD,Enab_p7_CP],[Enab_p8_CD,Enab_p8_CP]];
-
- ok = bfs_spanning_tree_oracle<<an,pn>>(Enab,Acti);
-tel
diff --git a/test/bfs-spanning-tree/fig5.1.dot b/test/bfs-spanning-tree/fig51.dot
similarity index 100%
rename from test/bfs-spanning-tree/fig5.1.dot
rename to test/bfs-spanning-tree/fig51.dot
diff --git a/test/bfs-spanning-tree/fig5.1-noinit.dot b/test/bfs-spanning-tree/fig51_noinit.dot
similarity index 100%
rename from test/bfs-spanning-tree/fig5.1-noinit.dot
rename to test/bfs-spanning-tree/fig51_noinit.dot
diff --git a/test/bfs-spanning-tree/fig5.2.dot b/test/bfs-spanning-tree/fig52.dot
similarity index 100%
rename from test/bfs-spanning-tree/fig5.2.dot
rename to test/bfs-spanning-tree/fig52.dot
diff --git a/test/bfs-spanning-tree/p.ml b/test/bfs-spanning-tree/p.ml
index 3fa2b956df8cf4260b5dbabfc5f14d1f81d82157..11951dadcc2afa101bf46d7420575369cda2dd9b 100644
--- a/test/bfs-spanning-tree/p.ml
+++ b/test/bfs-spanning-tree/p.ml
@@ -1,26 +1,11 @@
-(* Time-stamp: <modified the 26/06/2019 (at 11:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:36) by Erwan Jahier> *)
(* This is algo 5.4 in the book *)
open Algo
-
-let d=10 (* degree() *)
-let actions = ["CD";"CP"]
-
-type state = {
- d:int;
- par:int;
-}
-let (state_to_string: ('v -> string)) =
- fun s ->
- Printf.sprintf "d=%d par=%d" s.d s.par
-
-let (parse_state: string -> state) =
- fun s ->
- Scanf.sscanf s "{d=%d;par=%d}" (fun d par -> {d = d; par = par})
-
-let (copy_state : ('v -> 'v)) = fun x -> x
-
+open State
+
+let actions = Some ["CD";"CP"]
let (init_state: int -> 'v) =
fun i ->
@@ -49,7 +34,7 @@ let (get_parent: 'v neighbor list -> 'v -> 'v neighbor) =
canal ((List.length nl)-1))
let (enable_f:'v neighbor list -> 'v -> action list) =
- fun nl e ->
+ fun nl e ->
let par = get_parent nl e in
let par_st = par.state in
(if (e.d) <> dist nl then ["CD"] else []) @
diff --git a/test/bfs-spanning-tree/p.mli b/test/bfs-spanning-tree/p.mli
deleted file mode 100644
index b2fb93882dcaf5855ec2ac6dff27c7db58716c33..0000000000000000000000000000000000000000
--- a/test/bfs-spanning-tree/p.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-open Algo
-
-type state = {
- d:int;
- par:int;
-}
-
-val d:int
-val actions: string list
-val init_state: int -> state
-val enable_f:state neighbor list -> state -> action list
-val step_f : state neighbor list -> state -> action -> state
-val state_to_string: state -> string
-val parse_state: string -> state
-val copy_state : state -> state
diff --git a/test/bfs-spanning-tree/root.ml b/test/bfs-spanning-tree/root.ml
index 7fd669f6badc19a05bd1dc5589c85cca9be8cb1c..9ea5b402b38c97bc4a3dd37fb436848bcbcfe795 100644
--- a/test/bfs-spanning-tree/root.ml
+++ b/test/bfs-spanning-tree/root.ml
@@ -1,46 +1,23 @@
-(* Time-stamp: <modified the 26/06/2019 (at 12:08) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:35) by Erwan Jahier> *)
(* This is algo 5.3 in the book *)
open Algo
-open P
+open State
-let (init_state: int -> 'v) =
+let (init_state: int -> State.t) =
fun i ->
{
- P.d = Random.int P.d;
- P.par = -1;
+ d = Random.int d;
+ par = -1;
}
-let (enable_f:'v neighbor list -> 'v -> action list) =
+let (enable_f: State.t neighbor list -> State.t -> action list) =
fun nl st ->
if st.d <> 0 then ["CD"] else []
-let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
+let (step_f : State.t neighbor list -> State.t -> action -> State.t) =
fun _nl st ->
- function | _ -> { st with P.d = 0 }
+ function | _ -> { st with d = 0 }
-
-
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "root";
- init_state = init_state;
- actions = Some ["CD";"CP"];
- enab = enable_f;
- step = step_f;
- };
- {
- algo_id = "p";
- init_state = P.init_state;
- actions = Some P.actions;
- enab = P.enable_f;
- step = P.step_f;
- }
- ];
- state_to_string = P.state_to_string;
- state_of_string = (Some P.parse_state);
- copy_state = P.copy_state;
- }
+let actions = Some ["CD";"CP"]
diff --git a/test/bfs-spanning-tree/state.ml b/test/bfs-spanning-tree/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1d4dcb22925974f5316a7f3a5c6c4ca21f4084e9
--- /dev/null
+++ b/test/bfs-spanning-tree/state.ml
@@ -0,0 +1,18 @@
+
+let d=10 (* degree() *)
+
+type t = {
+ d:int;
+ par:int;
+}
+
+let (to_string: (t -> string)) =
+ fun s ->
+ Printf.sprintf "d=%d par=%d" s.d s.par
+
+let (of_string: (string -> t) option) =
+ Some (fun s ->
+ Scanf.sscanf s "{d=%d;par=%d}" (fun d par -> {d = d; par = par}))
+
+let (copy : ('v -> 'v)) = fun x -> x
+
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index dfde4c50910de78c5a2b5ddd32064d5d6d48b947..9f376e4b6bf616e238133e6d40f3a6e1fe9825e4 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,38 +1,43 @@
-# Time-stamp: <modified the 05/09/2019 (at 21:20) by Erwan Jahier>
+# Time-stamp: <modified the 17/09/2019 (at 16:54) by Erwan Jahier>
sasa=$(DIR)/bin/sasa -l 100
-test: p.cmxs ring.lut lurette
- $(sasa) -l 200 ring.dot && make clean
+test: ring.cmxs coloring.rif lurette
+coloring.rif: ring.cmxs
+ $(sasa) -l 200 ring.dot -rif > $@
-cmxs: p.cmxs p.cma
-sim2chrogtk: ring.rif
+sim2chrogtk: coloring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
+gnuplot: coloring.rif
gnuplot-rif $<
-lurette:cmxs ring_oracle.lus
- lurette \
+lurette: ring.cmxs ring_oracle.lus
+ lurette -o lurette-ring.rif \
-sut "sasa ring.dot -rif -lcd " \
- -oracle "lv6 ring_oracle.lus -n oracle "
+ -oracle "lv6 ring_oracle.lus -n oracle -exec"
test100:
for i in $$(seq 100); do make lurette && make clean; done
-rdbg: p.cma p.cmxs ring.lut
+rdbg: ring.ml
rdbg -o ring.rif \
- -env "$(sasa) g.dot -lcd"
+ -env "$(sasa) ring.dot -lcd"
+rdbg1: ring.cmxs ring_oracle.lus
+ rdbg -o rdbg-ring.rif \
+ -sut "sasa ring.dot -rif -lcd " \
+ -oracle "lv6 ring_oracle.lus -n oracle -exec"
-rdbg2: p.cma ring.lut
+rdbg2: ring.cmxs ring.lut
rdbg -o ring.rif \
-env "$(sasa) ring.dot -custd -rif" \
- -sut-nd "lutin ring.lut -n distributed"
+ -sut-nd "lutin ring.lut -n distributed"
clean: genclean
+ rm -f ring.lut ring.ml ring_oracle.ml
-include ../Makefile.inc
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
index 458fca7d5678d172c8dd826344ce9c092e6579ea..31621fcf46939a6072d3a7615520ebf91ed055e2 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/test/coloring/coloring_oracle.lus
@@ -18,10 +18,10 @@ tel
-- Theorem 3.17 The stabilization time of Color is at most one round
-- (under a Locally Central demon).
node theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
-returns (res:bool);
+returns (res:bool; RoundNb:int);
var
Round:bool;
- RoundNb:int;
+-- RoundNb:int;
let
Round = round <<an,pn>>(Enab,Acti);
RoundNb = count(Round);
@@ -30,8 +30,11 @@ tel
node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
-returns (res:bool);
+returns (res:bool; RoundNb:int);
let
- res = lemma_3_14<<an,pn>>(Enab,Acti) and theorem_3_17<<an,pn>>(Enab,Acti);
+ res, RoundNb = -- lemma_3_14<<an,pn>>(Enab,Acti) and
+ theorem_3_17<<an,pn>>(Enab,Acti);
tel
+
+node test=coloring_oracle<< 5,2 >>
diff --git a/test/coloring/p.ml b/test/coloring/p.ml
index c36cbd700ce7c27f6c71f293038ebab8185a73fd..6ebe9ce9be95602a25e4212cf59bbf5342039d00 100644
--- a/test/coloring/p.ml
+++ b/test/coloring/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/06/2019 (at 17:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 12/09/2019 (at 10:46) by Erwan Jahier> *)
(* This is algo 3.1 in the book *)
@@ -53,19 +53,5 @@ let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
match a with
| _ -> List.hd f
+let actions = Some ["conflict"]
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "p";
- init_state = init_state;
- actions = Some ["conflict"];
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = state_to_string;
- state_of_string = None;
- copy_state = copy_state;
- }
diff --git a/test/coloring/ring_oracle.lus b/test/coloring/ring_oracle.lus
index c05483b07eb67dd7c1fb410f8f071f2f0d8100fd..e6c9cab9ac7fd515c9d91244da3e4f3025947073 100644
--- a/test/coloring/ring_oracle.lus
+++ b/test/coloring/ring_oracle.lus
@@ -23,7 +23,7 @@ const adjency=[
[f,f,f,f,t,f,t],
[t,f,f,f,f,t,f]];
-node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok:bool);
+node oracle(p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool) returns (ok:bool; r:int);
var
Acti:bool^1^7;
Enab:bool^1^7;
@@ -31,6 +31,6 @@ let
Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
- ok = coloring_oracle<<an,pn>>(Enab,Acti);
+ ok, r = coloring_oracle<<an,pn>>(Enab,Acti);
tel
diff --git a/test/coloring/round.lus b/test/coloring/round.lus
deleted file mode 100644
index 1979ad73e7bbbfd1bcd8ca6a474e1758ea988b3a..0000000000000000000000000000000000000000
--- a/test/coloring/round.lus
+++ /dev/null
@@ -1,132 +0,0 @@
--- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
---
--- Computing rounds in Lustre
--- The inputs are 2 arrays Enab and Acti, where:
--- - Enab[i][j] is true iff action i of process j is enabled
--- - Acti[i][j] is true iff action i of process j is active
-
--- n holds the number of processes
--- m holds the number of actions per process
-node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
-var
- mask: bool^n;
- pres: bool;
-let
- pres = true -> pre res;
- mask = merge pres (true -> mask_init<<m, n>> (Enab, Acti) when pres)
- (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);
-
- res = boolred<<0,0,n>>(mask); -- when all are false,
-tel
-
-node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
-var
- enab:bool^n; -- at least one action is enabled
- acti:bool^n; -- at least one action is active
-let
- enab = map<< red<<or, m>>, n >>(false^n, E);
- acti = map<< red<<or, m>>, n >>(false^n, A);
- res = map<<not_implies, n>>(enab,acti);
-tel
-
-function not_implies(a,b:bool) returns (res:bool);
-let
- res = not(a=>b);
-tel
-
-node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
-var
- acti:bool^n; -- at least one action is active
-let
- acti = map<< red<<or, m>>, n >>(false^n, A);
- res = map<<not_implies, n>>(pmask,acti);
-tel
-
-
-node test53=round<< 5,3 >>
-node test52=round<< 5,2 >>
-
------------------------------------------------------------------------------
-node count(x:bool) returns(cpt:int);
-let
- cpt = 0 -> if x then pre cpt + 1 else pre cpt;
-tel
------------------------------------------------------------------------------
-
-node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
-var
- enab:bool^n; -- at least one action is enabled
-let
- enab = map<< red<<or, m>>, n >>(false^n, Enab);
- ok = not(red<<or, n>>(false, enab));
-tel
-
------------------------------------------------------------------------------
-node after_n(n:int; x:bool) returns (res:bool);
-var cpt:int;
-let
- cpt = 0 -> pre cpt + 1;
- res = cpt <= n or x;
-tel
-
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-node bool_to_int(X:int; Y:bool) returns (Z:int);
-let
- Z = if(Y) then X+1 else X;
-tel
-
------------------------------------------------------------------------------
-node map_and (X,Y:bool^m) returns (Z:bool^m);
-let
- Z = map<<and,m>>(X,Y) ;
-tel
-
------------------------------------------------------------------------------
-node implies_list(A,B:bool^m) returns (res:bool^m);
-let
- res = map<<=>,m>>(A,B) ;
-tel
-
------------------------------------------------------------------------------
-node count_true_acc(X:int; Y:bool^m) returns (Z:int);
-let
- Z = red<<bool_to_int,m>>(X,Y);
-tel
-
------------------------------------------------------------------------------
-node one_true (tab:bool^m^n) returns (res:bool);
-let
- res = (((red<<count_true_acc,n>>(0,tab)))=1);
-tel
-
------------------------------------------------------------------------------
-node all_true (tab_acti:bool^m^n) returns (res:bool);
-let
- res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
-tel
-
------------------------------------------------------------------------------
-node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
-let
- nb_act = 0 -> pre(nb_act) + (red<<count_true_acc,n>>(0,tab_acti));
-tel
-
------------------------------------------------------------------------------
-node is_distributed(acti,enab:bool^m^n) returns (res:bool);
-let
- res = true -> (((red<<count_true_acc,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_central(acti:bool^m^n) returns (res:bool);
-let
- res = true -> (one_true(acti)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
-let
- res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
-tel
-
diff --git a/test/coloring/round.lus b/test/coloring/round.lus
new file mode 120000
index 0000000000000000000000000000000000000000..453c4f026c4ca356655dad74ae2d22c1c243aef5
--- /dev/null
+++ b/test/coloring/round.lus
@@ -0,0 +1 @@
+../lustre/round.lus
\ No newline at end of file
diff --git a/test/coloring/state.ml b/test/coloring/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3aba8f23a03e29804f045124fb8f2fda56067cc0
--- /dev/null
+++ b/test/coloring/state.ml
@@ -0,0 +1,6 @@
+
+type t = int
+let to_string = string_of_int
+let of_string = Some int_of_string
+let copy = fun x -> x
+
diff --git a/test/dfs-list/Makefile b/test/dfs-list/Makefile
index b4993c414c1ca37ac79acdabaf93bfd0e6786d1d..b3a3bd163ca23be00b60c793c5e051b5ea202441 100644
--- a/test/dfs-list/Makefile
+++ b/test/dfs-list/Makefile
@@ -1,14 +1,11 @@
-# Time-stamp: <modified the 05/09/2019 (at 22:34) by Erwan Jahier>
+# Time-stamp: <modified the 13/09/2019 (at 10:55) by Erwan Jahier>
test: test0 lurette0
-test0: cmxs
+test0: g.cmxs
$(sasa) -rif -l 200 g.dot -sd
-
-cmxs: root.cmxs p.cmxs g.lut p.cma root.cma
-
sim2chrogtk: g.rif
sim2chrogtk -ecran -in $< > /dev/null
@@ -16,7 +13,7 @@ gnuplot: g.rif
gnuplot-rif $<
-lurette0:cmxs
+lurette0: g.cmxs g.lut
lurette -o lurette.rif \
-env "$(sasa) g.dot -custd -rif" \
-sut "lutin g.lut -n distributed"
@@ -26,7 +23,7 @@ lurette: lurette0
gnuplot-rif lurette.rif
-rdbg: cmxs g.lut
+rdbg: g.ml g.lut
rdbg -o lurette.rif \
-env "$(sasa) g.dot -rif" \
-sut-nd "lutin g.lut -n dummy"
@@ -39,6 +36,7 @@ root.cmxs: root.ml
ocamlfind ocamlopt -shared $(LIB) p.mli $^ -o $@
clean: genclean
+ rm -f g.ml
-include ../Makefile.inc
diff --git a/test/dfs-list/p.ml b/test/dfs-list/p.ml
index 133e21762ebcdc966950b0e980371a1680b6d0c0..ed585a5e11f52581afe287a58943fa7baf2ddb23 100644
--- a/test/dfs-list/p.ml
+++ b/test/dfs-list/p.ml
@@ -1,31 +1,13 @@
-(* Time-stamp: <modified the 20/06/2019 (at 17:24) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:59) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
open Algo
+open State
-let delta=10 (* diameter() *)
-let actions = ["update_path";"compute_parent"]
-type dfs_value = {
- path: int list;
- par: int
-}
+let actions = Some ["update_path";"compute_parent"]
-let string_of_int_list l =
- let n = List.length l in
- let rec f i acc =
- if i = delta then acc else
- (* for RIF tools, we need to always output the same number of values *)
- f (i+1) (Printf.sprintf "%s path%d=%d" acc i (if i<n then List.nth l i else -1))
- in
- f 0 ""
-let (dfs_value_to_string: dfs_value -> string) =
- fun v ->
- Printf.sprintf "%s par=%i" (string_of_int_list v.path) v.par
-
-let (dfs_value_copy : dfs_value -> dfs_value) =
- fun x -> x
let (init_state: int -> 'v) =
fun i ->
@@ -51,7 +33,7 @@ let (concat_path : int list -> int -> int list) =
let is_sub_list l1 l2 = (List.rev (List.tl (List.rev l2))) = l1
-let (compute_parent : dfs_value neighbor list -> int list -> int) =
+let (compute_parent : State.t neighbor list -> int list -> int) =
fun nl p ->
(* The parent of a process p is the neighbor which path is a
subpath of p *)
diff --git a/test/dfs-list/p.mli b/test/dfs-list/p.mli
deleted file mode 100644
index bda29cd4ba0b3670df528294032c1902b3ac37cd..0000000000000000000000000000000000000000
--- a/test/dfs-list/p.mli
+++ /dev/null
@@ -1,16 +0,0 @@
-open Algo
-
-type dfs_value = {
- path: int list;
- par: int
-}
-
-
-
-val actions: string list
-val init_state: int -> dfs_value
-val enable_f:dfs_value neighbor list -> dfs_value -> action list
-val step_f : dfs_value neighbor list -> dfs_value -> action -> dfs_value
-val dfs_value_to_string: dfs_value -> string
-
-val dfs_value_copy : dfs_value -> dfs_value
diff --git a/test/dfs-list/root.ml b/test/dfs-list/root.ml
index 93cd6c85d77c6e27bc43e8e3d0b45992b6560aca..a0a0b0b53b3030f7820a58666b0816ae421edace 100644
--- a/test/dfs-list/root.ml
+++ b/test/dfs-list/root.ml
@@ -1,12 +1,11 @@
-(* Time-stamp: <modified the 21/06/2019 (at 17:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:58) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
open Algo
-open P
+open State
-let delta=10
-let actions = ["a"]
+let actions = Some ["a"]
let (init_state: int -> 'v) =
fun i ->
@@ -25,25 +24,3 @@ let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
function
| "a" -> { v with path = [] }
| _ -> assert false
-
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "p";
- init_state = P.init_state;
- actions = Some P.actions;
- enab = P.enable_f;
- step = P.step_f;
- };{
- algo_id = "root";
- init_state = init_state;
- actions = Some actions;
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = P.dfs_value_to_string;
- state_of_string = None;
- copy_state = P.dfs_value_copy;
- }
diff --git a/test/dfs-list/state.ml b/test/dfs-list/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3121712116170e1d90f45546af1860ced8410377
--- /dev/null
+++ b/test/dfs-list/state.ml
@@ -0,0 +1,19 @@
+
+let delta=10 (* diameter() *)
+type t = {
+ path: int list;
+ par: int
+}
+
+let string_of_int_list l =
+ let n = List.length l in
+ let rec f i acc =
+ if i = delta then acc else
+ (* for RIF tools, we need to always output the same number of values *)
+ f (i+1) (Printf.sprintf "%s path%d=%d" acc i (if i<n then List.nth l i else -1))
+ in
+ f 0 ""
+
+let to_string v = Printf.sprintf "%s par=%i" (string_of_int_list v.path) v.par
+let of_string = None
+let copy x = x
diff --git a/test/dfs/Makefile b/test/dfs/Makefile
index 69c023dd475e6ebb7ff0b8e212c12da9d6b43aec..0367b1fe08a56ec58ab741ee914460c7822b00f0 100644
--- a/test/dfs/Makefile
+++ b/test/dfs/Makefile
@@ -1,22 +1,17 @@
-# Time-stamp: <modified the 05/09/2019 (at 22:30) by Erwan Jahier>
+# Time-stamp: <modified the 12/09/2019 (at 10:29) by Erwan Jahier>
test: test0 lurette0
-test0: cmxs
+test0: g.cmxs g.lut
$(sasa) -rif -l 200 g.dot -sd
-
-
-cmxs: root.cmxs p.cmxs g.lut p.cma root.cma
-
sim2chrogtk: g.rif
sim2chrogtk -ecran -in $< > /dev/null
gnuplot: g.rif
gnuplot-rif $<
-
-lurette0:cmxs
+lurette0: g.cmxs g.lut
lurette -o lurette.rif \
-env "$(sasa) g.dot -custd -rif" \
-sut "lutin g.lut -n distributed"
@@ -26,20 +21,14 @@ lurette: lurette0
gnuplot-rif lurette.rif
-rdbg: cmxs g.lut
+rdbg: g.lut g.ml
rdbg -o lurette.rif \
-env "$(sasa) g.dot -rif" \
-sut-nd "lutin g.lut -n dummy"
-%.cmxs: %.ml
- ocamlfind ocamlopt -shared $(LIB) $^ -o $@
-
-root.cmxs: root.ml
- ocamlfind ocamlopt -shared $(LIB) p.mli $^ -o $@
-
clean: genclean
- rm -f g_oracle.lus
+ rm -f g_oracle.lus g.ml
-include ../Makefile.inc
diff --git a/test/dfs/p.ml b/test/dfs/p.ml
index c26ed4efa92d72f2968cade97d9ca6844784df92..18495b6b968adbd0f5cbe616ee24b92bb2841e4c 100644
--- a/test/dfs/p.ml
+++ b/test/dfs/p.ml
@@ -1,27 +1,15 @@
-(* Time-stamp: <modified the 20/06/2019 (at 17:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:54) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
open Algo
+open State
let delta=10 (* diameter() *)
-let actions = ["update_path";"compute_parent"]
-type dfs_value = {
- path: int array;
- par: int
-}
-
-let (dfs_value_to_string: dfs_value -> string) =
- fun v ->
- Printf.sprintf "%s par=%i"
- (snd (Array.fold_left
- (fun (i,acc) x -> i+1,Printf.sprintf "%s path%d=%d" acc i x) (0,"") v.path))
- v.par
-
-let (dfs_value_copy : dfs_value -> dfs_value) =
- fun x -> { x with path = Array.copy x.path }
-
-let (init_state: int -> 'v) =
+let actions = Some ["update_path";"compute_parent"]
+
+
+let (init_state: int -> State.t ) =
fun i ->
{
path = Array.make delta (-1);
@@ -29,7 +17,7 @@ let (init_state: int -> 'v) =
}
let str_of_array a =
- let l = List.map dfs_value_to_string (Array.to_list a) in
+ let l = List.map State.to_string (Array.to_list a) in
"["^(String.concat "," l)^"]"
let min_path al =
@@ -76,7 +64,7 @@ let equals_up_to p1 p2 i =
done;
!res
-let (compute_parent : dfs_value neighbor list -> int array -> int) =
+let (compute_parent : t neighbor list -> int array -> int) =
fun nl p ->
(* The parent of a process p is the neighbor which path is a
subpath of p *)
@@ -102,14 +90,14 @@ let compute_path nl e =
let path = min_path paths in
path
-let (enable_f:'v neighbor list -> 'v -> action list) =
+let (enable_f:t neighbor list -> t -> action list) =
fun nl v ->
let path = compute_path nl v in
if path <> v.path then ["update_path"] else
if compute_parent nl path <> v.par then ["compute_parent"]
else []
-let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
+let (step_f : t neighbor list -> t -> action -> t) =
fun nl v ->
function
| "update_path" ->
@@ -120,5 +108,4 @@ let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
{ v with par = compute_parent nl path }
| _ -> assert false
-
diff --git a/test/dfs/p.mli b/test/dfs/p.mli
deleted file mode 100644
index d3e635d3363ad00299276e49524b06e8c2e78db4..0000000000000000000000000000000000000000
--- a/test/dfs/p.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-open Algo
-
-type dfs_value = {
- path: int array;
- par: int
-}
-
-
-val actions: string list
-val init_state: int -> dfs_value
-val enable_f:dfs_value neighbor list -> dfs_value -> action list
-val step_f : dfs_value neighbor list -> dfs_value -> action -> dfs_value
-val dfs_value_to_string: dfs_value -> string
-
-val dfs_value_copy : dfs_value -> dfs_value
diff --git a/test/dfs/root.ml b/test/dfs/root.ml
index 1ae6a0ff140c77ca1c24d291187e2350150f483b..3c6abc2437b9594ee9ccb9f2d0f39b65b062c5a5 100644
--- a/test/dfs/root.ml
+++ b/test/dfs/root.ml
@@ -1,49 +1,28 @@
-(* Time-stamp: <modified the 06/09/2019 (at 14:12) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 10:54) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
open Algo
-open P
+open State
let delta=10
-let actions = ["a"]
+let actions = Some ["a"]
-let (init_state: int -> 'v) =
+let (init_state: int -> State.t ) =
fun i ->
{
path = Array.make delta (-1);
par = -10
}
-let (enable_f:'v neighbor list -> 'v -> action list) =
+let (enable_f: t neighbor list -> t -> action list) =
fun _nl v ->
if v.path = (Array.make delta (-1)) then [] else ["a"]
-let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
+let (step_f : t neighbor list -> t -> action -> t) =
fun nl v ->
function
| "a" -> { v with path = Array.make delta (-1) }
| _ -> assert false
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "p";
- init_state = P.init_state;
- actions = Some P.actions;
- enab = P.enable_f;
- step = P.step_f;
- };{
- algo_id = "root";
- init_state = init_state;
- actions = Some actions;
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = P.dfs_value_to_string;
- state_of_string = None;
- copy_state = P.dfs_value_copy;
- }
diff --git a/test/dfs/state.ml b/test/dfs/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..00541d86dd873be27c60365237f978d6c4a003dc
--- /dev/null
+++ b/test/dfs/state.ml
@@ -0,0 +1,18 @@
+
+type t = {
+ path: int array;
+ par: int
+}
+
+let (to_string: t -> string) =
+ fun v ->
+ Printf.sprintf "%s par=%i"
+ (snd (Array.fold_left
+ (fun (i,acc) x -> i+1,Printf.sprintf "%s path%d=%d" acc i x) (0,"") v.path))
+ v.par
+
+let (copy : t -> t) =
+ fun x -> { x with path = Array.copy x.path }
+
+let of_string = None
+
diff --git a/test/dijkstra-ring/Makefile b/test/dijkstra-ring/Makefile
index 376ffe4ffd6742925a569972216438d429d501c2..4e6eb131177526049e6077ede958f7d9962a0a46 100644
--- a/test/dijkstra-ring/Makefile
+++ b/test/dijkstra-ring/Makefile
@@ -1,26 +1,24 @@
-# Time-stamp: <modified the 05/09/2019 (at 14:48) by Erwan Jahier>
+# Time-stamp: <modified the 18/09/2019 (at 21:10) by Erwan>
-test: cmxs lurette1
+test: ring.cmxs lurette1
$(sasa) ring.dot
-cmxs: ring.cmxs ringroot.cmxs ring.cma ringroot.cma
-
-sim2chrogtk: ring.rif
+sim2chrogtk: dijkstra-ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
+gnuplot: dijkstra-ring.rif
gnuplot-rif $<
-rdbg: cmxs ring.lut
+rdbg: ring.ml ring.lut
rdbg -o ring.rif \
-env "$(sasa) ring.dot -custd -rif" \
-sut-nd "lutin ring.lut -n distributed"\
-lurette1:cmxs ring.lut ring_oracle.lus
+lurette1: ring.lut ring_oracle.lus
lurette \
-env "$(sasa) ring.dot -custd " \
-sut "lutin ring.lut -n distributed" \
@@ -29,4 +27,4 @@ lurette1:cmxs ring.lut ring_oracle.lus
-include ../Makefile.inc
clean: genclean
- rm -f ring_oracle.lus
+ rm -f ring_oracle.lus ring.ml
diff --git a/test/dijkstra-ring/ring.ml b/test/dijkstra-ring/p.ml
similarity index 73%
rename from test/dijkstra-ring/ring.ml
rename to test/dijkstra-ring/p.ml
index 80ef35ca72ded194efa07b1b7771474d6cadfba1..f72bae298c14be7d6314a5d2995173ac0248ac45 100644
--- a/test/dijkstra-ring/ring.ml
+++ b/test/dijkstra-ring/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/06/2019 (at 14:49) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 09:50) by Erwan Jahier> *)
open Algo
@@ -22,8 +22,6 @@ let (step_f : 's neighbor list -> 's -> action -> 's) =
match a with
| _ -> pred.state
-let (state_to_string: ('s -> string)) = string_of_int
-let (copy_state : ('s -> 's)) = fun x -> x
-
+let actions = Some ["a"]
diff --git a/test/dijkstra-ring/ring.dot b/test/dijkstra-ring/ring.dot
index 8466e481aa26607b534dce4f85bb79471916f51b..b34e38951ffb6106fd3c101f80284044a4633739 100644
--- a/test/dijkstra-ring/ring.dot
+++ b/test/dijkstra-ring/ring.dot
@@ -1,14 +1,14 @@
digraph ring7 {
graph [k=3]
- p1 [algo="ringroot.ml" init="v=1" ]
- p2 [algo="ring.ml" init="v=3" ]
- p3 [algo="ring.ml" init="v=3" ]
- p4 [algo="ring.ml" init="v=2" ]
- p5 [algo="ring.ml" init="v=2" ]
- p6 [algo="ring.ml" init="v=1" ]
- p7 [algo="ring.ml" init="v=1" ]
- p8 [algo="ring.ml" init="v=0" ]
+ p1 [algo="root.ml" init="v=1" ]
+ p2 [algo="p.ml" init="v=3" ]
+ p3 [algo="p.ml" init="v=3" ]
+ p4 [algo="p.ml" init="v=2" ]
+ p5 [algo="p.ml" init="v=2" ]
+ p6 [algo="p.ml" init="v=1" ]
+ p7 [algo="p.ml" init="v=1" ]
+ p8 [algo="p.ml" init="v=0" ]
p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p1
diff --git a/test/dijkstra-ring/ringroot.ml b/test/dijkstra-ring/ringroot.ml
deleted file mode 100644
index e1864a438aa204e88f7a620474f651995e103191..0000000000000000000000000000000000000000
--- a/test/dijkstra-ring/ringroot.ml
+++ /dev/null
@@ -1,49 +0,0 @@
-(* Time-stamp: <modified the 21/06/2019 (at 17:29) by Erwan Jahier> *)
-
-open Algo
-
-let k = 42
-
-let (init_state: int -> 's) =
- fun _n ->
- (* let k = (card() - 1) in *)
- (* let _ = assert (k > 0) in *)
- Random.int k
-
-let (enable_f: 's neighbor list -> 's -> action list) =
- fun nl e ->
- let pred = List.hd nl in
- if e = pred.state then ["a"] else []
-
-let (step_f : 's neighbor list -> 's -> action -> 's) =
- fun nl e a ->
- (* let k = (card() - 1) in *)
- match a with
- | _ -> (e + 1) mod k
-
-
-open Ring
-
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "ring";
- init_state = Ring.init_state;
- actions = Some ["a"];
- enab = Ring.enable_f;
- step = Ring.step_f;
- };
- {
- algo_id = "ringroot";
- init_state = init_state;
- actions = Some ["a"];
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = Ring.state_to_string;
- state_of_string = None;
- copy_state = Ring.copy_state;
- }
-
diff --git a/test/dijkstra-ring/root.ml b/test/dijkstra-ring/root.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c5b56d464dd537bbddab8f41ac8759088bd8bd55
--- /dev/null
+++ b/test/dijkstra-ring/root.ml
@@ -0,0 +1,26 @@
+(* Time-stamp: <modified the 13/09/2019 (at 09:50) by Erwan Jahier> *)
+
+open Algo
+
+let k = 42
+
+let (init_state: int -> 's) =
+ fun _n ->
+ (* let k = (card() - 1) in *)
+ (* let _ = assert (k > 0) in *)
+ Random.int k
+
+let (enable_f: 's neighbor list -> 's -> action list) =
+ fun nl e ->
+ let pred = List.hd nl in
+ if e = pred.state then ["a"] else []
+
+let (step_f : 's neighbor list -> 's -> action -> 's) =
+ fun nl e a ->
+ (* let k = (card() - 1) in *)
+ match a with
+ | _ -> (e + 1) mod k
+
+let actions = Some ["a"]
+
+
diff --git a/test/dijkstra-ring/round.lus b/test/dijkstra-ring/round.lus
deleted file mode 100644
index 94dfbc6bf42973a7e7027e594bffb55ee7368285..0000000000000000000000000000000000000000
--- a/test/dijkstra-ring/round.lus
+++ /dev/null
@@ -1,132 +0,0 @@
--- -- Time-stamp: <modified the 26/06/2019 (at 15:13) by Erwan Jahier>
---
--- Computing rounds in Lustre
--- The inputs are 2 arrays Enab and Acti, where:
--- - Enab[i][j] is true iff action i of process j is enabled
--- - Acti[i][j] is true iff action i of process j is active
-
--- n holds the number of processes
--- m holds the number of actions per process
-node round<<const m : int; const n: int>> (Enab, Acti: bool^m^n) returns (res:bool);
-var
- mask: bool^n;
- pres: bool;
-let
- pres = true -> pre res;
- mask = merge pres (true -> mask_init<<m, n>> (Enab, Acti) when pres)
- (false -> mask_update<<m, n>>(Enab, Acti, pre mask) when not pres);
-
- res = boolred<<0,0,n>>(mask); -- when all are false,
-tel
-
-node mask_init <<const m:int; const n:int>> (E,A: bool^m^n) returns (res : bool^n);
-var
- enab:bool^n; -- at least one action is enabled
- acti:bool^n; -- at least one action is active
-let
- enab = map<< red<<or, m>>, n >>(false^n, E);
- acti = map<< red<<or, m>>, n >>(false^n, A);
- res = map<<not_implies, n>>(enab,acti);
-tel
-
-function not_implies(a,b:bool) returns (res:bool);
-let
- res = not(a=>b);
-tel
-
-node mask_update<<const m: int; const n: int>> (E,A: bool^m^n; pmask:bool^n) returns (res : bool^n);
-var
- acti:bool^n; -- at least one action is active
-let
- acti = map<< red<<or, m>>, n >>(false^n, A);
- res = map<<not_implies, n>>(pmask,acti);
-tel
-
-
-node test53=round<< 5,3 >>
-node test52=round<< 5,2 >>
-
------------------------------------------------------------------------------
-node count(x:bool) returns(cpt:int);
-let
- cpt = 0 -> if x then pre cpt + 1 else pre cpt;
-tel
------------------------------------------------------------------------------
-
-node silent<<const m: int; const n: int>> (Enab: bool^m^n) returns (ok:bool);
-var
- enab:bool^n; -- at least one action is enabled
-let
- enab = map<< red<<or, m>>, n >>(false^n, Enab);
- ok = not(red<<or, n>>(false, enab));
-tel
-
------------------------------------------------------------------------------
-node after_n(n:int; x:bool) returns (res:bool);
-var cpt:int;
-let
- cpt = 0 -> pre cpt + 1;
- res = cpt <= n or x;
-tel
-
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-node bool_to_int(X:int; Y:bool) returns (Z:int);
-let
- Z = if(Y) then X+1 else X;
-tel
-
------------------------------------------------------------------------------
-node map_and (X,Y:bool^m) returns (Z:bool^m);
-let
- Z = map<<and,m>>(X,Y) ;
-tel
-
------------------------------------------------------------------------------
-node implies_list(A,B:bool^m) returns (res:bool^m);
-let
- res = map<<=>,m>>(A,B) ;
-tel
-
------------------------------------------------------------------------------
-node add_int_true(X:int; Y:bool^m) returns (Z:int);
-let
- Z = red<<bool_to_int,m>>(X,Y);
-tel
-
------------------------------------------------------------------------------
-node one_true (tab:bool^m^n) returns (res:bool);
-let
- res = (((red<<add_int_true,n>>(0,tab)))=1);
-tel
-
------------------------------------------------------------------------------
-node all_true (tab_acti:bool^m^n) returns (res:bool);
-let
- res = boolred<<m,m,m>>((red<<map_and,n>>(true^m,tab_acti))) ;
-tel
-
------------------------------------------------------------------------------
-node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
-let
- nb_act = 0 -> pre(nb_act) + (red<<add_int_true,n>>(0,tab_acti));
-tel
-
------------------------------------------------------------------------------
-node is_distributed(acti,enab:bool^m^n) returns (res:bool);
-let
- res = true -> (((red<<add_int_true,n>>(0,acti))>=1) or silent<<m,n>>(enab)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_central(acti:bool^m^n) returns (res:bool);
-let
- res = true -> (one_true(acti)) and pre(res);
-tel
-
------------------------------------------------------------------------------
-node is_synchronous(enab,acti:bool^m^n) returns (res:bool);
-let
- res = true -> all_true(map<<implies_list,n>>(enab,acti)) and pre(res);
-tel
-
diff --git a/test/dijkstra-ring/round.lus b/test/dijkstra-ring/round.lus
new file mode 120000
index 0000000000000000000000000000000000000000..453c4f026c4ca356655dad74ae2d22c1c243aef5
--- /dev/null
+++ b/test/dijkstra-ring/round.lus
@@ -0,0 +1 @@
+../lustre/round.lus
\ No newline at end of file
diff --git a/test/dijkstra-ring/state.ml b/test/dijkstra-ring/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..df1f3e07e93f77c6ebf375dc9d881d06b889a746
--- /dev/null
+++ b/test/dijkstra-ring/state.ml
@@ -0,0 +1,5 @@
+
+type t = int
+let to_string = string_of_int
+let of_string = None
+let copy x = x
diff --git a/test/lustre/oracle_utils.lus b/test/lustre/oracle_utils.lus
index 20eee78ebf5f1b199bb6efbe913c92b2f692f360..bce7fb7ff140afc65e6e57d8a2d22918665910f2 100644
--- a/test/lustre/oracle_utils.lus
+++ b/test/lustre/oracle_utils.lus
@@ -1,16 +1,13 @@
+include "utils.lus"
include "round.lus"
include "demon.lus"
-include "utils.lus"
-----------------------------------------------------------------------------
-- An algo is silent when no action is enable
node silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool);
-var
- enab:bool^pn; -- at least one action is enabled
let
- enab = map<< red<<or, an>>, pn >>(false^pn, Enab);
- ok = not(red<<or, pn>>(false, enab));
+ ok = all_false<<an, pn>>(Enab);
tel
-----------------------------------------------------------------------------
diff --git a/test/lustre/round.lus b/test/lustre/round.lus
index ed7eebd0cad48aefd499f2a3023340e3f3faeaa0..ad7175ebe159a3afe1dd74a5ebb85a4e7ad45e39 100644
--- a/test/lustre/round.lus
+++ b/test/lustre/round.lus
@@ -1,4 +1,4 @@
--- -- Time-stamp: <modified the 08/07/2019 (at 17:04) by Erwan Jahier>
+-- -- Time-stamp: <modified the 18/09/2019 (at 14:29) by Erwan Jahier>
--
-- Computing rounds in Lustre
-- The inputs are 2 arrays Enab and Acti, where:
@@ -11,12 +11,13 @@ node round<<const an : int; const pn: int>> (Enab, Acti: bool^an^pn) returns (re
var
mask: bool^pn;
pres: bool;
+ psilent: bool;
let
pres = true -> pre res;
mask = merge pres (true -> mask_init<<an, pn>> (Enab, Acti) when pres)
(false -> mask_update<<an, pn>>(Enab, Acti, pre mask) when not pres);
-
- res = boolred<<0,0,pn>>(mask); -- when all are false,
+ res = not(psilent) and boolred<<0,0,pn>>(mask) ; -- when all are false,
+ psilent = false fby silent<<an,pn>>(Enab);
tel
function mask_init <<const an:int; const pn:int>> (E,A: bool^an^pn) returns (res : bool^pn);
@@ -40,9 +41,10 @@ var
acti:bool^pn; -- at least one action is active
let
acti = map<< red<<or, an>>, pn >>(false^pn, A);
- res = map<<not_implies, pn>>(pmask,acti);
+ res = map<<and, pn>>(pmask,acti);
tel
node test53=round<< 5,3 >>
node test52=round<< 5,2 >>
+
diff --git a/test/lustre/utils.lus b/test/lustre/utils.lus
index 824aaf1e3dee84496a6bd9d7390f34731456d826..4b3fa973697f047355e702c660a694828f7987ba 100644
--- a/test/lustre/utils.lus
+++ b/test/lustre/utils.lus
@@ -58,3 +58,21 @@ node all_false <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool);
let
res = boolred<<0,0,m>>((red<<map_or<<m>>,n>>(false^m,t))) ;
tel
+-- function all_false <<const n:int; const m:int>> (a: bool^m^n) returns (res : bool);
+-- let
+-- res = not(red << red <<or, m>>, n>>(false, a));
+--tel
+
+
+-----------------------------------------------------------------------------
+node bool_to_int(X:int; Y:bool) returns (Z:int);
+let
+ Z = if(Y) then X+1 else X;
+tel
+
+-----------------------------------------------------------------------------
+node compt_move (tab_acti:bool^m^n) returns (nb_act:int);
+let
+ nb_act = 0 -> pre(nb_act) + (red<<count_true_acc,n>>(0,tab_acti));
+tel
+
diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml
index ea3b775acef18f907daf8adc1260c47d065c4e51..f7fb277b933cfd2e7ae638107510e83181456542 100644
--- a/test/my-rdbg-tuning.ml
+++ b/test/my-rdbg-tuning.ml
@@ -66,6 +66,7 @@ let last_round = ref 0
let round_nodes = ref [] (* nodes we look the activation at *)
let (round : Event.t -> bool) =
fun e ->
+ e.kind = Ltop &&
let (pl : process list) = get_processes e in
let rm_me = get_removable pl in
if !verbose then (
@@ -104,6 +105,14 @@ let next_round e = next_cond e round;;
let nr () = e:=next_round !e; circo p dotfile !e;;
let pr () = e:=goto_last_ckpt !e.nb; circo p dotfile !e;;
+(* Goto to the next oracle violation *)
+let goto_next_false_oracle e =
+ next_cond e (fun e -> e.kind = Exit && e.lang = "lustre" &&
+ e.outputs = [("ok", Bool)] &&
+ not (vb "ok" e))
+
+let viol () = e:=goto_next_false_oracle !e
+
(* checkpoint at rounds! *)
let _ = check_ref := round;;
diff --git a/test/skeleton/Makefile b/test/skeleton/Makefile
index 51c29329ac61a2c56f6c774c6d26ac6e1d4fe79b..8ddfa28d646eaf3bf9373879d6d6cb4d0e7ccf07 100644
--- a/test/skeleton/Makefile
+++ b/test/skeleton/Makefile
@@ -1,21 +1,21 @@
-# Time-stamp: <modified the 05/09/2019 (at 14:48) by Erwan Jahier>
+# Time-stamp: <modified the 13/09/2019 (at 09:03) by Erwan Jahier>
-test: p.cmxs ring.lut
+test: ring.cmxs ring.lut
$(sasa) -l 200 ring.dot
-cmxs: p.cmxs p.cma
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
gnuplot: ring.rif
gnuplot-rif $<
-rdbg: p.cma ring.lut
+rdbg: ring.ml ring.lut
rdbg -o ring.rif \
-env "$(sasa) g.dot -cd"
clean: genclean
+ rm -f ring.ml
-include ../Makefile.inc
diff --git a/test/skeleton/p.ml b/test/skeleton/p.ml
index 42617848e2169e444732193298f4d35175f4d760..ad2b85a4da1e9b15ec84be9e355d0f5775fcb5ca 100644
--- a/test/skeleton/p.ml
+++ b/test/skeleton/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/07/2019 (at 15:41) by Erwan> *)
+(* Time-stamp: <modified the 13/09/2019 (at 09:06) by Erwan Jahier> *)
(* a dumb algo *)
@@ -23,20 +23,6 @@ let (step_f : 'st neighbor list -> 'st -> action -> 'st ) =
| "action2" -> 1
| _ -> e
+let actions = Some ["action1";"action2"];
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "p";
- init_state = init_state;
- actions = Some ["action1";"action2"];
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = (fun s -> Printf.sprintf "i=%i" s);
- state_of_string = Some int_of_string;
- copy_state = (fun x -> x);
- }
diff --git a/test/skeleton/state.ml b/test/skeleton/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2c0037d193265e4b72cefe8b07fa491e36c3fe9b
--- /dev/null
+++ b/test/skeleton/state.ml
@@ -0,0 +1,5 @@
+
+type t = int
+let to_string = (fun s -> Printf.sprintf "i=%i" s)
+let of_string = Some int_of_string
+let copy x = x
diff --git a/test/unison/Makefile b/test/unison/Makefile
index b6b6f914cbf1441964cb0eabcdba15f56321e6eb..42c657db945b33d810344341a18b37cf401d3697 100644
--- a/test/unison/Makefile
+++ b/test/unison/Makefile
@@ -1,27 +1,26 @@
-# Time-stamp: <modified the 05/09/2019 (at 14:49) by Erwan Jahier>
+# Time-stamp: <modified the 13/09/2019 (at 10:08) by Erwan Jahier>
test: test1 test2 lurette0
-test1: unison.cmxs
- $(sasa) -l 5 fig4.1.dot -sd -rif
+test1: fig41.cmxs
+ $(sasa) -l 5 fig41.dot -sd -rif
-test2: unison.cmxs
+test2: ring.cmxs
$(sasa) -l 50 ring.dot -rif
sasaopt=-sd
-cmxs: unison.cmxs unison.cma
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
gnuplot: ring.rif
gnuplot-rif $<
-luciole:
+luciole: ring.cmxs
luciole-rif $(sasa) ring.dot -custd -rif -ifi
-lurette0:cmxs ring.lut ring_oracle.lus
+lurette0: ring.lut ring_oracle.lus
lurette -o lurette.rif \
-env "$(sasa) ring.dot -custd -rif" \
-sut "lutin ring.lut -n synchronous" \
@@ -29,7 +28,7 @@ lurette0:cmxs ring.lut ring_oracle.lus
lurette: lurette0 s g
-rdbg: unison.cma unison.cmxs ring.lut
+rdbg: ring.ml ring.lut
rdbg -o unison.rif \
-env "$(sasa) ring.dot -custd -rif" \
-sut-nd "lutin ring.lut -n synchronous"
@@ -37,4 +36,4 @@ rdbg: unison.cma unison.cmxs ring.lut
-include ../Makefile.inc
clean: genclean
- rm -f ring_oracle.lus
+ rm -f ring_oracle.lus fig41.ml ring.ml
diff --git a/test/unison/fig4.1.dot b/test/unison/fig41.dot
similarity index 100%
rename from test/unison/fig4.1.dot
rename to test/unison/fig41.dot
diff --git a/test/unison/state.ml b/test/unison/state.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d44954246f24d71f8da94be5cf0f4f75306e910d
--- /dev/null
+++ b/test/unison/state.ml
@@ -0,0 +1,5 @@
+
+type t = int
+let to_string = string_of_int
+let of_string = None
+let copy x = x
diff --git a/test/unison/unison.ml b/test/unison/unison.ml
index 3c709010fd574acda46be7db5f336a8b7f0fe6c9..4e2961af1827bcd3dd3f7ca5ded20f8e5ef8ea92 100644
--- a/test/unison/unison.ml
+++ b/test/unison/unison.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/07/2019 (at 17:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/09/2019 (at 09:56) by Erwan Jahier> *)
open Algo
@@ -32,24 +32,6 @@ let (step_f : 'v neighbor list -> 'v -> action -> 'v) =
match a with
| _ -> v
-let (state_to_string: ('v -> string)) = string_of_int
-let (copy_state : ('v -> 'v)) = fun x -> x
-
-
-let () =
- Algo.register {
- algo = [
- {
- algo_id = "unison";
- init_state = init_state;
- actions = Some ["g"];
- enab = enable_f;
- step = step_f;
- }
- ];
- state_to_string = state_to_string;
- state_of_string = None;
- copy_state = copy_state;
- }
+let actions = Some ["g"]