diff --git a/test/async-unison/async_unison_oracle.ml b/test/async-unison/async_unison_oracle.ml
index 1806160fe83436e302bc0aab1642b6789ed37266..2bdd77581c81e8810fb1b3daed9196113850dcb8 100644
--- a/test/async-unison/async_unison_oracle.ml
+++ b/test/async-unison/async_unison_oracle.ml
@@ -48,11 +48,11 @@ let move_forward_until_stabilisation e =
aux 0 e
-(* move forward until a legitimate configuration is reached.
+(* Move forward until a legitimate configuration is reached.
-Let's override the silence command.
+nb: it overrides the legitimate commande in ../sasa-rdbg-cmds.ml.
*)
-let silence () =
+let legitimate () =
let rn, ne = move_forward_until_stabilisation !e in
e := ne;
Printf.printf "Stabilisation reached after %i round%s\n" rn
@@ -60,14 +60,19 @@ let silence () =
flush stdout;
d ();;
-let _ = Printf.printf "You can use stab to move forward until"
+let _ = add_doc_entry
+ "legitimate" "unit -> unit"
+ " Move forward until a legitimate configuration is reached (when clocks are close)"
+ "sasa" "async_unison_oracle.ml";;
+
+
let time f x =
let t = Sys.time() in
let fx = f x in
Printf.printf "Execution time: %fs\n" (Sys.time() -. t);
fx
-
+
(* Mimick the work of the lurette oracle (to compare perf): a each
step, compute the round number + check for stabilisation *)
let go () =
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
index 3c5105af867cc37d25f4a7ed98debff90191a9f1..97d66c54cb078b506938e34e09fe2e278a49418d 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/test/coloring/coloring_oracle.lus
@@ -28,8 +28,7 @@ let
res = RoundNb <= 1; -- from theorem 3.17 page 29
tel
-
-node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+node coloring_oracle0<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
returns (res:bool; RoundNb:int);
var res0:bool;
let
@@ -38,4 +37,16 @@ let
tel
+-- Hide the second output of coloring_oracle0
+-- Indeed, the automatically generated oracles (out of the dot files) suppose
+-- that this node has only one output.
+node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (res:bool);
+var RoundNb:int;
+let
+ res, RoundNb = coloring_oracle0<<an,pn>>(Enab,Acti);
+tel
+
+
+
node test=coloring_oracle<< 5,2 >>
diff --git a/test/coloring/ring_oracle.lus b/test/coloring/ring_oracle.lus
index cb8b92ae497e8444fa33d93218a7fd3f83658ddf..0d22238e6499db280c4369c45951b16815083b27 100644
--- a/test/coloring/ring_oracle.lus
+++ b/test/coloring/ring_oracle.lus
@@ -31,7 +31,7 @@ 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, r = coloring_oracle<<an,pn>>(Enab,Acti);
+ ok, r = coloring_oracle0<<an,pn>>(Enab,Acti);
tel
diff --git a/test/rdbg-utils/dot.ml b/test/rdbg-utils/dot.ml
index 6f42430b6bc10adf3a0e37842cc7a8339b04ddac..ce94125c4f7d046e6e2755755a7f996ee8067cbc 100644
--- a/test/rdbg-utils/dot.ml
+++ b/test/rdbg-utils/dot.ml
@@ -213,8 +213,35 @@ let osage = to_pdf "osage" "_par" ;;
sfdp - filter for drawing large undirected graphs
patchwork - filter for squarified tree maps
osage - filter for array-based layouts
+
+let _ =
+ add_doc_entry
+ "dot" "unit -> unit" "Generate a pdf (out of the current) topology with dot"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "neato" "unit -> unit" "Generate a pdf (out of the current) topology with neato"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "twopi" "unit -> unit" "Generate a pdf (out of the current) topology with twopi"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "circo" "unit -> unit" "Generate a pdf (out of the current) topology with circo"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "fdp" "unit -> unit" "Generate a pdf (out of the current) topology with fdp"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "sfdp" "unit -> unit" "Generate a pdf (out of the current) topology with sfdp"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "patchwork" "unit -> unit" "Generate a pdf (out of the current) topology with patchwork"
+ "sasa" "rdbg-utils/dot.ml";
+ add_doc_entry
+ "osage" "unit -> unit" "Generate a pdf (out of the current) topology with osage"
+ "sasa" "rdbg-utils/dot.ml";;
*)
+
(***********************************************************************)
let get_removable pl =
@@ -227,25 +254,3 @@ let get_removable pl =
in
List.map (fun p -> p.name) pl
(***********************************************************************)
-
-let _ = print_string "
-===> Use the read fonction to load the dot file
-===> Use the dot function at Ltop event to generated .dot.pdf files
-
-You migth want to add something along those lines at the end of your rdbg-session.ml file
-(the name of the dot file and the path to the dot.ml file migth need to be adapted
-to your context tough):
-;;
-#require \"ocamlgraph\";;
-#mod_use \"../../lib/algo/algo.ml\";;
-#use \"../../lib/sasacore/topology.ml\";;
-#use \"../rdbg-utils/dot.ml\";;
-let dotfile = \"g.dot\";;
-let p = Topology.read dotfile;;
-let d () = dot (p.nodes, dotfile) !e;;
-let sd () = s();d();;
-let nr () = e:=next_round dotfile !e; d();;
-
-let _ = n (); d (); Sys.command (\"zathura sasa-g.dot.pdf&\")
-
-"
diff --git a/test/sasa-rdbg-cmds.ml b/test/sasa-rdbg-cmds.ml
index 4a41469c8ef58984c8d29812e5567ecec5c00331..02fbfc50e3e9320b531c95b65ebcebc2000aa130 100644
--- a/test/sasa-rdbg-cmds.ml
+++ b/test/sasa-rdbg-cmds.ml
@@ -1,11 +1,10 @@
-(* This file defines sasa specific commands.
-
-It is meant to loaded after the (rdbg-generated) "rdbg-cmds.ml" file.
+(* This file defines sasa specific commands.
+It is meant to be loaded after the (rdbg-generated) "rdbg-cmds.ml" file.
+Look at the sasa/test/*/my-rdbg-commands.ml files for examples
*)
#require "sasa";;
-
(**********************************************************************)
(* Dealing with rounds *)
@@ -15,7 +14,7 @@ let roundtbl = Hashtbl.create 1;;
(**********************************************************************)
-(* The code below is specific to sasa and to the sasa test directory *)
+(* BEWARE: The paths below are specific to sasa and to the sasa test directory *)
#mod_use "../../lib/algo/algo.ml";;
#mod_use "../../lib/sasacore/register.ml";;
@@ -24,7 +23,8 @@ let roundtbl = Hashtbl.create 1;;
let p = Topology.read dotfile;;
-(* shortcuts for dot viewer *)
+
+(* Shortcuts for dot viewers defined in rdbg-utils/dot.ml *)
let d_par () = dot true !roundnb p dotfile !e;;
let dot_par () = dot true !roundnb p dotfile !e;;
let ne_par () = neato true !roundnb p dotfile !e;;
@@ -45,26 +45,20 @@ let pa () = patchwork false !roundnb p dotfile !e;;
let os () = osage false !roundnb p dotfile !e;;
-(* To be able to choose the different default dot viewer on a per directory basis.
- To change the graph printer:
+(* To change the default dot/graph viewer:
dot_view := ci;;
*)
let dot_view : (unit -> unit) ref =
- ref ( (* choosing a reasonable default viewer *)
+ ref ( (* Try to chose the most sensible default viewer *)
if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else
if Algo.is_directed () then dot else ne)
let d () = !dot_view ()
-
-(* Move forward until convergence, i.e., when no data changes *)
-let rec go () =
- let data = !e.data in
- s(); if data = !e.data then !dot_view () else go () ;;
-
let sd () = s();!dot_view();;
let nd () = n();!dot_view();;
let bd () = b();!dot_view();;
+
(**********************************************************************)
(** Computing rounds *)
@@ -244,27 +238,43 @@ let is_silent e =
let goto_silence e = next_cond e is_silent
let silence () = e:=goto_silence !e; !dot_view ();;
+let _ = add_doc_entry
+ "silence" "unit -> unit" "Move forward until is_silent returns true"
+ "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry
+ "is_silent" "RdbgEvent.t -> bool"
+ "is the event correspond to a silent configuration? (i.e., no enable node)"
+ "sasa" "sasa-rdbg-cmds.ml";;
+
+
+let legitimate = silence;;
+let _ = add_doc_entry
+ "legitimate" "unit -> unit"
+ " Move forward until a legitimate configuration is reached (uses 'silence' by default)"
+ "sasa" "sasa-rdbg-cmds.ml";;
+
+
(**********************************************************************)
(* Perform the checkpointing at rounds! *)
let _ = check_ref := round;;
(**********************************************************************)
let _ =
- add_doc_entry "d" "unit -> unit" "display the current network with dot" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "ne" "unit -> unit" "display the current network with neato" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "tw" "unit -> unit" "display the current network with twopi" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "ci" "unit -> unit" "display the current network with circo" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "fd" "unit -> unit" "display the current network with fdp" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "sf" "unit -> unit" "display the current network with sfdp" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "pa" "unit -> unit" "display the current network with patchwork" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "os" "unit -> unit" "display the current network with osage" "sasa" "my-rdbg-tuning.ml";
+ add_doc_entry "d" "unit -> unit" "display the current network with dot" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "ne" "unit -> unit" "display the current network with neato" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "tw" "unit -> unit" "display the current network with twopi" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "ci" "unit -> unit" "display the current network with circo" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "fd" "unit -> unit" "display the current network with fdp" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "sf" "unit -> unit" "display the current network with sfdp" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "pa" "unit -> unit" "display the current network with patchwork" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "os" "unit -> unit" "display the current network with osage" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "sd" "unit -> unit"
- "go to the next step and display the network with one of the GraphViz tools" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "nd" "unit -> unit" "go to the next event and display the network" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "bd" "unit -> unit" "go to the previous event and display the network" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "nr" "unit -> unit" "go to the next round and display the network" "sasa" "my-rdbg-tuning.ml";
- add_doc_entry "pr" "unit -> unit" "go to the previous round and display the network" "sasa" "my-rdbg-tuning.ml"
+ "go to the next step and display the network with one of the GraphViz tools" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "nd" "unit -> unit" "go to the next event and display the network" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "bd" "unit -> unit" "go to the previous event and display the network" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "nr" "unit -> unit" "go to the next round and display the network" "sasa" "sasa-rdbg-cmds.ml";
+ add_doc_entry "pr" "unit -> unit" "go to the previous round and display the network" "sasa" "sasa-rdbg-cmds.ml"
;;
let l () =
@@ -304,20 +314,6 @@ the dot_view command as follows:
dot_view := ci
");;
-(**********************************************************************)
-(* is the current configuration stable? *)
-let count_true l =
- List.fold_left (fun cpt (_,_,v) -> if v=B true then cpt+1 else cpt) 0 l
-
-let stable_event e =
- let enab, _, _ = split_data e.data in
- count_true enab = 0
-let stable () = stable_event !e
-
-let _ = add_doc_entry
- "stable" "unit -> bool" "is the current configuration stable?" "sasa"
- "my-rdbg-tuning.ml"
-
(**********************************************************************)
(* ok, let's start the debugging session! *)
diff --git a/tools/rdbgui/rdbgui.ml b/tools/rdbgui/rdbgui.ml
index 8709ca6643a3a3a40d2f373251a8b6d6b40fae08..69a86a6b96ad5e1978b509add3e406ab3548c1a4 100644
--- a/tools/rdbgui/rdbgui.ml
+++ b/tools/rdbgui/rdbgui.ml
@@ -124,18 +124,18 @@ let gui str =
change_label round_button "_Round";
ignore (round_button#connect#clicked ~callback:(fun () -> p "nr"));
- let silence () =
- let silence_button = GButton.button ~use_mnemonic:true
+ let legitimate () =
+ let legitimate_button = GButton.button ~use_mnemonic:true
~packing:bbox#add () in
- silence_button#misc#set_tooltip_text
- "Move FORWARD until the algorithm is SILENT (i.e., when no action is enabled)";
+ legitimate_button#misc#set_tooltip_text
+ "Move FORWARD until a legitimate configuration is reached (silence by default)";
let image = GMisc.image ~file:"../rdbg-utils/chut_small.svg" () in
- silence_button#set_image image#coerce;
- (* change_label silence_button "Silen_t"; *)
- ignore (silence_button#connect#clicked ~callback:(fun () -> p "silence"))
+ legitimate_button#set_image image#coerce;
+ (* change_label legitimate_button "Silen_t"; *)
+ ignore (legitimate_button#connect#clicked ~callback:(fun () -> p "legitimate"))
in
- silence ();
+ legitimate ();
let graph () =
let graph_button = GButton.button ~use_mnemonic:true ~packing:bbox#add () in