diff --git a/test/alea-coloring/my-rdbg-tuning.ml b/test/alea-coloring/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/alea-coloring/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/alea-coloring/my-rdbg-tuning.ml b/test/alea-coloring/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..9ba333d82207840466e748a80995cb21eab12ec7 --- /dev/null +++ b/test/alea-coloring/my-rdbg-tuning.ml @@ -0,0 +1,6 @@ + +#use "../my-rdbg-tuning.ml";; + + + + diff --git a/test/async-unison/Makefile b/test/async-unison/Makefile index 52da8a2a22ce9d365f685da36e06c2e0c541c716..2765bf8cf7b198930a5f29fcd2763db9b6563fb3 100644 --- a/test/async-unison/Makefile +++ b/test/async-unison/Makefile @@ -1,7 +1,7 @@ -# Time-stamp: <modified the 17/10/2019 (at 17:18) by Erwan Jahier> +# Time-stamp: <modified the 23/10/2019 (at 11:43) by Erwan Jahier> -test: ring.cmxs ring.lut +test: ring.cmxs ring.lut rdbg_test $(sasa) -l 500 ring.dot @@ -16,6 +16,9 @@ lurette: ring.cmxs -sut "sasa -rif ring.dot -cd" \ -oracle "lv6 -2c-exec ring_oracle.lus -n oracle" +rdbg_test: ring.ml + echo "\nnr\nsd\n" | rdbg -o ring.rif -l 10000 -env "$(sasa) -vl 1 ring.dot -cd" + rdbg: ring.ml rdbg -o ring.rif -l 10000 \ -env "$(sasa) -vl 1 ring.dot -cd" diff --git a/test/async-unison/my-rdbg-tuning.ml b/test/async-unison/my-rdbg-tuning.ml index f42644e96dabdd172a901484aeec3fd238f3f5d2..a6e1a16d550248da9b9562150dfc582d86793df1 100644 --- a/test/async-unison/my-rdbg-tuning.ml +++ b/test/async-unison/my-rdbg-tuning.ml @@ -2,7 +2,5 @@ #use "../my-rdbg-tuning.ml";; #use "async_unison_oracle.ml";; -let _ = - ne ();; diff --git a/test/bfs-spanning-tree/my-rdbg-tuning.ml b/test/bfs-spanning-tree/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/bfs-spanning-tree/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/bfs-spanning-tree/my-rdbg-tuning.ml b/test/bfs-spanning-tree/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..82813d6dd7166c61c1d740335f934f70f340988a --- /dev/null +++ b/test/bfs-spanning-tree/my-rdbg-tuning.ml @@ -0,0 +1,8 @@ + +#use "../my-rdbg-tuning.ml";; + +let _ = + dot_view:=ci;; + + + diff --git a/test/coloring/my-rdbg-tuning.ml b/test/coloring/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/coloring/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/coloring/my-rdbg-tuning.ml b/test/coloring/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..9ba333d82207840466e748a80995cb21eab12ec7 --- /dev/null +++ b/test/coloring/my-rdbg-tuning.ml @@ -0,0 +1,6 @@ + +#use "../my-rdbg-tuning.ml";; + + + + diff --git a/test/debug_sasa/my-rdbg-tuning.ml b/test/debug_sasa/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/debug_sasa/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/debug_sasa/my-rdbg-tuning.ml b/test/debug_sasa/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..9ba333d82207840466e748a80995cb21eab12ec7 --- /dev/null +++ b/test/debug_sasa/my-rdbg-tuning.ml @@ -0,0 +1,6 @@ + +#use "../my-rdbg-tuning.ml";; + + + + diff --git a/test/dfs-list/my-rdbg-tuning.ml b/test/dfs-list/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/dfs-list/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/dfs-list/my-rdbg-tuning.ml b/test/dfs-list/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..82813d6dd7166c61c1d740335f934f70f340988a --- /dev/null +++ b/test/dfs-list/my-rdbg-tuning.ml @@ -0,0 +1,8 @@ + +#use "../my-rdbg-tuning.ml";; + +let _ = + dot_view:=ci;; + + + diff --git a/test/dfs/Makefile b/test/dfs/Makefile index bb4d5363fe57c681dc127ebb4d32ace845cbec4e..bc34f0806898f1b52a4eb9e52aacb2ed8472529e 100644 --- a/test/dfs/Makefile +++ b/test/dfs/Makefile @@ -1,7 +1,7 @@ -# Time-stamp: <modified the 14/10/2019 (at 20:55) by Erwan Jahier> +# Time-stamp: <modified the 23/10/2019 (at 12:21) by Erwan Jahier> -test: test0 lurette0 +test: test0 lurette0 rdbg_test test0: g.cmxs g.lut $(sasa) -rif -l 200 g.dot -sd @@ -26,6 +26,11 @@ rdbg: g.lut g.ml -env "$(sasa) g.dot -rif" \ -sut-nd "lutin g.lut -n dummy" +rdbg_test: g.lut g.ml + echo "\nnr\nsd\n" | rdbg -o lurette.rif \ + -env "$(sasa) g.dot -rif" \ + -sut-nd "lutin g.lut -n dummy" + clean: genclean rm -f g_oracle.lus g.ml diff --git a/test/dfs/my-rdbg-tuning.ml b/test/dfs/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/dfs/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/dfs/my-rdbg-tuning.ml b/test/dfs/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..151ab7a3a35c182a660e38f80deb07aa75a5b386 --- /dev/null +++ b/test/dfs/my-rdbg-tuning.ml @@ -0,0 +1,9 @@ + +#use "../my-rdbg-tuning.ml";; + +let _ = + dot_view:=ci; + !dot_view();; + + + diff --git a/test/dijkstra-ring/my-rdbg-tuning.ml b/test/dijkstra-ring/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/dijkstra-ring/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/dijkstra-ring/my-rdbg-tuning.ml b/test/dijkstra-ring/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..9ba333d82207840466e748a80995cb21eab12ec7 --- /dev/null +++ b/test/dijkstra-ring/my-rdbg-tuning.ml @@ -0,0 +1,6 @@ + +#use "../my-rdbg-tuning.ml";; + + + + diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml index 5d7923d550fe13a55e6807fcc7374b4a47347ba2..f0c6fea146b6ab254997b3573294e89c68ee5df5 100644 --- a/test/my-rdbg-tuning.ml +++ b/test/my-rdbg-tuning.ml @@ -3,7 +3,7 @@ let _ = time_travel true;; - +(* Shortcuts for moving around *) let e = ref (RdbgStdLib.run());; let s () = e:=step !e;; let si i = e:=stepi !e i;; @@ -19,15 +19,14 @@ let bt () = print_src !e;; let finish () = loopforever !e;; (**********************************************************************) -(* #require "ocamlgraph";; *) #mod_use "../../lib/algo/algo.ml";; #mod_use "../../lib/sasacore/register.ml";; #mod_use "../../lib/sasacore/topology.ml";; #use "../rdbg-utils/dot.ml";; - - let p = Topology.read dotfile;; + +(* shortcuts for dot viewer *) let d () = dot p dotfile !e;; let ne () = neato p dotfile !e;; let tw () = twopi p dotfile !e;; @@ -37,26 +36,27 @@ let sf () = sfdp p dotfile !e;; let pa () = patchwork p dotfile !e;; let os () = osage p dotfile !e;; -let graph_printer = - ref ( +(* To be able to choose the different default dot viewer on a per directory basis. + To change the graph printer: + dot_view := ci;; +*) +let dot_view : (unit -> unit) ref = + ref ( (* choosing a reasonable default viewer *) if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else if Algo.is_directed () then d else ne) -(** to change the graph printer - graph_printer := ci;; - *) -(* Convergence is reached when data does not change *) +(* Move forward until convergence, i.e., when no data changes *) let rec go () = let data = !e.data in - s(); if data = !e.data then !graph_printer () else go () ;; + s(); if data = !e.data then !dot_view () else go () ;; -let sd () = s();!graph_printer();; -let nd () = n();!graph_printer();; -let bd () = b();!graph_printer();; +let sd () = s();!dot_view();; +let nd () = n();!dot_view();; +let bd () = b();!dot_view();; (**********************************************************************) -(* Computing rounds *) +(** Computing rounds *) (* a process can be removed from the mask if one action of p is triggered or if no action of p is enabled *) @@ -112,12 +112,8 @@ let (round : Event.t -> bool) = (* go to next and previous rounds *) 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;; - -(**********************************************************************) -(* *) - +let nr () = e:=next_round !e; !dot_view ();; +let pr () = e:=goto_last_ckpt !e.nb; !dot_view ();; (**********************************************************************) (* Goto to the next oracle violation *) @@ -128,9 +124,13 @@ let goto_next_false_oracle e = let viol () = e:=goto_next_false_oracle !e -(* checkpoint at rounds! *) +(**********************************************************************) +(* Perform the checkpointing at rounds! *) let _ = check_ref := round;; +(**********************************************************************) +(* Goto to the next event which name contains a string (useful for + navigating inside lustre or lutin programs) *) let next_match str e = next_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0) let nm str = e:= next_match str !e ;; @@ -139,11 +139,23 @@ let prev_match str e = rev_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0) let rm str = e:=next_match str !e ;; +(**********************************************************************) +(* ok, let's start the debugging session! *) + +let pdf_viewer = + if Sys.command "which zathura" = 0 then "zathura" else + if Sys.command "which xpdf" = 0 then "xpdf" else + if Sys.command "which acroread" = 0 then "acroread" else + if Sys.command "which evince" = 0 then "evince" else + failwith "No pdf viewer is found" let _ = - !graph_printer (); - ignore(Sys.command (Printf.sprintf "zathura sasa-%s.pdf&" dotfile)); - round !e + !dot_view (); + let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in + Printf.printf "%s\n!" cmd; + Unix.sleep 1; + ignore(Sys.command cmd); + round !e let _ = print_string " --> type 'man' for online help diff --git a/test/skeleton/my-rdbg-tuning.ml b/test/skeleton/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/skeleton/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/unison/Makefile b/test/unison/Makefile index 4ebc9768c61a44c0d389bdb59aeae5cee9070d15..8c4dda0a069abbcf782c261440474129a929edf6 100644 --- a/test/unison/Makefile +++ b/test/unison/Makefile @@ -1,6 +1,6 @@ -# Time-stamp: <modified the 23/10/2019 (at 09:21) by Erwan Jahier> +# Time-stamp: <modified the 23/10/2019 (at 12:18) by Erwan Jahier> -test: test1 test2 lurette0 lurette1 +test: test1 test2 lurette0 lurette1 rdbg_test test1: fig41.cmxs $(sasa) -l 5 fig41.dot -sd -rif @@ -34,10 +34,13 @@ lurette1: ring.lut ring_oracle.lus lurette: lurette0 s g -rdbg: ring.ml ring.lut +rdbg: ring.ml rdbg -o unison.rif \ - -env "$(sasa) ring.dot -custd -rif" \ - -sut-nd "lutin ring.lut -n synchronous" + -sut "$(sasa) ring.dot -sd -rif" \ + +rdbg_test: ring.ml + echo "\nnr\nsd\n" | rdbg -o unison.rif \ + -sut "$(sasa) ring.dot -sd -rif" \ -include ../Makefile.inc diff --git a/test/unison/my-rdbg-tuning.ml b/test/unison/my-rdbg-tuning.ml deleted file mode 120000 index e83bd7c305302c3c46720aa3e77027eb0867f0c9..0000000000000000000000000000000000000000 --- a/test/unison/my-rdbg-tuning.ml +++ /dev/null @@ -1 +0,0 @@ -../my-rdbg-tuning.ml \ No newline at end of file diff --git a/test/unison/my-rdbg-tuning.ml b/test/unison/my-rdbg-tuning.ml new file mode 100644 index 0000000000000000000000000000000000000000..9ba333d82207840466e748a80995cb21eab12ec7 --- /dev/null +++ b/test/unison/my-rdbg-tuning.ml @@ -0,0 +1,6 @@ + +#use "../my-rdbg-tuning.ml";; + + + +