Skip to content
Snippets Groups Projects
Commit f69b093b authored by erwan's avatar erwan
Browse files

Test: add calls to rdbg in the non-reg tests

parent bec863f0
No related branches found
No related tags found
No related merge requests found
Showing
with 155 additions and 51 deletions
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
# 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 $(sasa) -l 500 ring.dot
...@@ -16,6 +16,9 @@ lurette: ring.cmxs ...@@ -16,6 +16,9 @@ lurette: ring.cmxs
-sut "sasa -rif ring.dot -cd" \ -sut "sasa -rif ring.dot -cd" \
-oracle "lv6 -2c-exec ring_oracle.lus -n oracle" -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: ring.ml
rdbg -o ring.rif -l 10000 \ rdbg -o ring.rif -l 10000 \
-env "$(sasa) -vl 1 ring.dot -cd" -env "$(sasa) -vl 1 ring.dot -cd"
......
...@@ -2,7 +2,5 @@ ...@@ -2,7 +2,5 @@
#use "../my-rdbg-tuning.ml";; #use "../my-rdbg-tuning.ml";;
#use "async_unison_oracle.ml";; #use "async_unison_oracle.ml";;
let _ =
ne ();;
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
let _ =
dot_view:=ci;;
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
let _ =
dot_view:=ci;;
# 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 test0: g.cmxs g.lut
$(sasa) -rif -l 200 g.dot -sd $(sasa) -rif -l 200 g.dot -sd
...@@ -26,6 +26,11 @@ rdbg: g.lut g.ml ...@@ -26,6 +26,11 @@ rdbg: g.lut g.ml
-env "$(sasa) g.dot -rif" \ -env "$(sasa) g.dot -rif" \
-sut-nd "lutin g.lut -n dummy" -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 clean: genclean
rm -f g_oracle.lus g.ml rm -f g_oracle.lus g.ml
......
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
let _ =
dot_view:=ci;
!dot_view();;
../my-rdbg-tuning.ml
\ No newline at end of file
#use "../my-rdbg-tuning.ml";;
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
let _ = time_travel true;; let _ = time_travel true;;
(* Shortcuts for moving around *)
let e = ref (RdbgStdLib.run());; let e = ref (RdbgStdLib.run());;
let s () = e:=step !e;; let s () = e:=step !e;;
let si i = e:=stepi !e i;; let si i = e:=stepi !e i;;
...@@ -19,15 +19,14 @@ let bt () = print_src !e;; ...@@ -19,15 +19,14 @@ let bt () = print_src !e;;
let finish () = loopforever !e;; let finish () = loopforever !e;;
(**********************************************************************) (**********************************************************************)
(* #require "ocamlgraph";; *)
#mod_use "../../lib/algo/algo.ml";; #mod_use "../../lib/algo/algo.ml";;
#mod_use "../../lib/sasacore/register.ml";; #mod_use "../../lib/sasacore/register.ml";;
#mod_use "../../lib/sasacore/topology.ml";; #mod_use "../../lib/sasacore/topology.ml";;
#use "../rdbg-utils/dot.ml";; #use "../rdbg-utils/dot.ml";;
let p = Topology.read dotfile;; let p = Topology.read dotfile;;
(* shortcuts for dot viewer *)
let d () = dot p dotfile !e;; let d () = dot p dotfile !e;;
let ne () = neato p dotfile !e;; let ne () = neato p dotfile !e;;
let tw () = twopi p dotfile !e;; let tw () = twopi p dotfile !e;;
...@@ -37,26 +36,27 @@ let sf () = sfdp p dotfile !e;; ...@@ -37,26 +36,27 @@ let sf () = sfdp p dotfile !e;;
let pa () = patchwork p dotfile !e;; let pa () = patchwork p dotfile !e;;
let os () = osage p dotfile !e;; let os () = osage p dotfile !e;;
let graph_printer = (* To be able to choose the different default dot viewer on a per directory basis.
ref ( 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 String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else
if Algo.is_directed () then d else ne) 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 rec go () =
let data = !e.data in 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 sd () = s();!dot_view();;
let nd () = n();!graph_printer();; let nd () = n();!dot_view();;
let bd () = b();!graph_printer();; let bd () = b();!dot_view();;
(**********************************************************************) (**********************************************************************)
(* Computing rounds *) (** Computing rounds *)
(* a process can be removed from the mask if one action of p is triggered (* a process can be removed from the mask if one action of p is triggered
or if no action of p is enabled *) or if no action of p is enabled *)
...@@ -112,12 +112,8 @@ let (round : Event.t -> bool) = ...@@ -112,12 +112,8 @@ let (round : Event.t -> bool) =
(* go to next and previous rounds *) (* go to next and previous rounds *)
let next_round e = next_cond e round;; let next_round e = next_cond e round;;
let nr () = e:=next_round !e; circo p dotfile !e;; let nr () = e:=next_round !e; !dot_view ();;
let pr () = e:=goto_last_ckpt !e.nb; circo p dotfile !e;; let pr () = e:=goto_last_ckpt !e.nb; !dot_view ();;
(**********************************************************************)
(* *)
(**********************************************************************) (**********************************************************************)
(* Goto to the next oracle violation *) (* Goto to the next oracle violation *)
...@@ -128,9 +124,13 @@ let goto_next_false_oracle e = ...@@ -128,9 +124,13 @@ let goto_next_false_oracle e =
let viol () = e:=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;; 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 = let next_match str e =
next_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0) next_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0)
let nm str = e:= next_match str !e ;; let nm str = e:= next_match str !e ;;
...@@ -139,11 +139,23 @@ let prev_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) rev_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0)
let rm str = e:=next_match str !e ;; 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 _ = let _ =
!graph_printer (); !dot_view ();
ignore(Sys.command (Printf.sprintf "zathura sasa-%s.pdf&" dotfile)); let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in
round !e Printf.printf "%s\n!" cmd;
Unix.sleep 1;
ignore(Sys.command cmd);
round !e
let _ = print_string " let _ = print_string "
--> type 'man' for online help --> type 'man' for online help
......
../my-rdbg-tuning.ml
\ No newline at end of file
# 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 test1: fig41.cmxs
$(sasa) -l 5 fig41.dot -sd -rif $(sasa) -l 5 fig41.dot -sd -rif
...@@ -34,10 +34,13 @@ lurette1: ring.lut ring_oracle.lus ...@@ -34,10 +34,13 @@ lurette1: ring.lut ring_oracle.lus
lurette: lurette0 s g lurette: lurette0 s g
rdbg: ring.ml ring.lut rdbg: ring.ml
rdbg -o unison.rif \ rdbg -o unison.rif \
-env "$(sasa) ring.dot -custd -rif" \ -sut "$(sasa) ring.dot -sd -rif" \
-sut-nd "lutin ring.lut -n synchronous"
rdbg_test: ring.ml
echo "\nnr\nsd\n" | rdbg -o unison.rif \
-sut "$(sasa) ring.dot -sd -rif" \
-include ../Makefile.inc -include ../Makefile.inc
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment