From 8ccdf9a97ddbb825126d848f3f1dfed90d60fea4 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 09:42:35 +0100
Subject: [PATCH] Update: a little bit more work on the rdbg plugin
Actually, I've just realized that the I/O mode of rdbg already makes
it possible to use sasa from rdbg (exit event only). This plugin would
only be necessary when we would need a finer grained intrumentation, e.g.,
to stop at enable step, or to at each process call/exit.
---
lib/sasalib/sasaRun.ml | 82 +++++++++++++++++++++++++++++++--
lib/sasalib/sasaRun.mli | 9 ++++
test/bfs-spanning-tree/Makefile | 7 ++-
3 files changed, 94 insertions(+), 4 deletions(-)
diff --git a/lib/sasalib/sasaRun.ml b/lib/sasalib/sasaRun.ml
index 180ff64c..e73c3f93 100644
--- a/lib/sasalib/sasaRun.ml
+++ b/lib/sasalib/sasaRun.ml
@@ -1,6 +1,82 @@
-let (make: string array -> RdbgPlugin.t) =
- fun _ ->
-
+open Sasacore
+(* open SasArg *)
+open RdbgPlugin
+
+
+let (to_sasa_value : Data.v -> Algo.value) = function
+ | Data.I i -> Algo.I i
+ | Data.F f -> Algo.F f
+ | Data.B b -> Algo.B b
+ | Data.E(_id,_i) -> assert false (* xxx finishme *)
+ | Data.A _a -> assert false (* xxx finishme *)
+ | Data.S _s -> assert false (* xxx finishme *)
+ | Data.U -> assert false (* xxx finishme *)
+
+
+let (_to_sasa_env : (string * Data.v) list -> string -> Algo.value) =
+ fun sl v ->
+ to_sasa_value (List.assoc v sl)
+let (to_sasa_env : (string * Data.v) list -> Env.t) =
+ fun sl ->
+ (* inputs are actions of the form "pid_ActionName" *)
+ let split_var str =
+ match Str.split (Str.regexp "_") str with
+ | [pid;action] -> pid,action
+ | [] -> assert false
+ | [_] -> assert false
+ | _ -> assert false
+ in
+ let _sl = List.map (fun (var,v) -> split_var var, to_sasa_value v) sl in
assert false
+
+let (make_do: string array -> SasArg.t -> RdbgPlugin.t) =
+ fun argv _opt ->
+
+ let vntl_i = [] in
+ let vntl_o = [] in
+ let step sl_in =
+ let _ins = to_sasa_env sl_in in
+ assert false
+ in
+ let step_dbg _sl_in _ectx _cont = assert false
+ in
+ let (mems_in : Data.subst list) = [] in (* XXX todo *)
+ let (mems_out : Data.subst list) = [] in (* XXX todo *)
+ {
+ id = Printf.sprintf "%s (with sasa Version %s)"
+ (String.concat " " (Array.to_list argv)) SasaVersion.str;
+ inputs = vntl_i;
+ outputs= vntl_o;
+ reset=(fun () -> ());
+ kill=(fun _ -> flush stdout; flush stderr);
+ init_inputs=mems_in;
+ init_outputs=mems_out;
+ step=step;
+ step_dbg=step_dbg;
+ }
+
+
+let (make: string array -> RdbgPlugin.t) =
+ fun argv ->
+ let opt = SasArg.parse argv in
+ try make_do argv opt with
+ | Dynlink.Error e ->
+ Printf.printf "Error: %s\n" (Dynlink.error_message e);
+ flush stdout;
+ exit 2
+ | Failure msg ->
+ Printf.printf "Error: %s\n" msg;
+ flush stdout;
+ exit 2
+
+ | Assert_failure (file, line, col) ->
+ prerr_string (
+ "\nError: oops, sasa internal error\n\tFile \""^ file ^
+ "\", line " ^ (string_of_int line) ^ ", column " ^
+ (string_of_int col) ^ "\n") ;
+ flush stderr;
+ exit 2
+
+
diff --git a/lib/sasalib/sasaRun.mli b/lib/sasalib/sasaRun.mli
index bb870ac8..ee1efe28 100644
--- a/lib/sasalib/sasaRun.mli
+++ b/lib/sasalib/sasaRun.mli
@@ -1,2 +1,11 @@
+(* XXX finishme!
+
+Actually, the I/O mode of rdbg already makes it possible to use sasa
+ from rdbg and see all of its variable values after each step (exit
+ event). This plugin would only be necessary when we would need a
+ finer-grained intrumentation, e.g., to stop at enable step, or to
+ at each process call/exit.
+
+*)
val make: string array -> RdbgPlugin.t
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index 61d2d8df..5240eb92 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 14/03/2019 (at 16:46) by Erwan Jahier>
+# Time-stamp: <modified the 17/03/2019 (at 21:40) by Erwan Jahier>
test: test0 lurette0
@@ -31,6 +31,11 @@ lurette: lurette0
sim2chrogtk -ecran -in lurette.rif > /dev/null
gnuplot-rif lurette.rif
+rdbg:
+ rdbg -o lurette.rif \
+ -env "$(sasa) fig5.1-noinit.dot -custd -rif" \
+ -sut "lutin demon.lut -n distributed"
+
manual:cmxs
lurette -o lurette.rif --sim2chro \
--
GitLab