RDBG - a Reactive programs DeBuGger

opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y
opam install -y rdbg

Once this is done, upgrading to the last version of the tools is as simple as:

opam update
opam upgrade

cf the Install section of http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox

You will need:

• make (gnu)
• a set of tools installable via opam
  • dune
  • rdbg
  • lutin (not for compiling actually, but for using sasa with custom demons)

One can mimick the content of the build job in the project Gitlab CI script.

This tutorial is made for people that knows nothing about ocaml, and that are not willing to learn it to take advantage of the programming capability of rdbg.

Although rdbg is built on top of an ocaml toplevel REPL interpreter, it is possible to use it with knowing ocaml at all. Of course you loose the possibility of extending the set of available commands.

Let's illustrate the use of rdbg on a Lustre program. Let's download of such example from the Lustre examples github repository (https://github.com/jahierwan/lustre-examples/blob/master/verimag-v6/).

wget https://raw.githubusercontent.com/jahierwan/lustre-examples/master/core/examples/stopwatch.lus

If you have installed the Synchrone Reactive Tool Box, you should be able to simulate this program.

lv6 stopwatch.lus -n stopwatch -exec

As this program requires 3 Boolean inputs, you are prompted to enter a sequence of Boolean values. Try to enter the following input (that will perform 4 steps):

t f f
t t f
t f f
t f f

As manually entering inputs is boring, we can ask to a Lutin program (env.lut) to generate random ones.

echo "node env(time:int) returns(time_unit:bool;b1:bool;b2:bool) = loop true" > env.lut

You can simulate this Lutin program as follows:

lutin env.lut -n env

Now we can invoke rdbg using those 2 programs plugged onto each other:

rdbg -sut "lv6 stopwatch.lus -n stopwatch -exec" -env "lutin env.lut -n env"

rdbg asks to enter one of the 3 following choices:

[] create a fresh session
[q] quit

The first possibility in the list is the one that is chosen by default if you directly press [Return]. Hence press [Return] to create a fresh session (This will create a rdbg-session.ml file, but let's forget about that for now)

  1   1   call env            ()
(rdbg)

The first integer is the event number, and the second is the step number. Then comes the kind of event (call or exit), the name of the current node, and the variables instanciation.

Here at the first event, we should be able to see the value of the node env input (time:int). But this input comes from the SUT output, and is this not available at the first step. Let's move one step forward to see such a value.

(rdbg) s
120   2   call env            (0)
(rdbg)

Now you can see the value (0) of the =time input of node env at the beginning of the second step. Notice also that the step counter has been incremented by 1, while the event counter has been incremented by 119!

You can list the available commands with 'l'. You may try each of those commands to see what happens.

(rdbg) l
(rdbg) help "n"

(rdbg) n
(rdbg) n
(rdbg) ni 10
(rdbg) b
(rdbg) s
(rdbg) si 5
(rdbg)

If you type [Enter] without any key, the last command will be used.

To leave rdbg, simply type 'q'.

To launch again previous sessions, you don't need to provide any arguments; just launch rdbg. By default the first created session will be used. If you have created several different sessions, you can chose it from a list (session numbers are created in increasing order):

$ rdbg 
Enter one of the following key (the first is the default one):
  [] #use "rdbg-session.ml"
  [1] #use "rdbg-session1.ml"
  [2] #use "rdbg-session2.ml"
  [c] create a fresh session
  [q] quit

[/1/2/c/q/s]:

If you don't want to reuse a previous session, enter the c key. In this case of course, you should have provided some -sut arguments.

If you type [Enter] without any key, the firstly created session will be used. If you want to launch an older session, type the corresponding integer.

If you type (at least) a space (i.e., an empty string) before your command at the rdbg prompt, you will enter a multi-line mode. In this mode, the [Enter] key won't send the command to the rdbg engine. It will do it only once you enter the ";;" string. This is handy to type programs on several lines, which is out of the scope of this tutorial. We mention this here because if by mistake you enter a space, you will be stuck in this multi-line mode.

In order to let rdbg opens emacs buffer and highlights active expressions, one can call rdbg with the --emacs options (you need to install the emacs highligth package available in melpa). In order to turn on or off the emacs mode from rdbg, one can do:

 emacs := true;;
 emacs := false;;

The list of commands can be obtained with the 'l' key:

(rdbg) l

 rdbg --help

rdbg is a Reactive programs debugger. 
rdbg is extensible: debugging commands or functions can be programmed
rdbg is meant to be easily pluggable. Currently, existing plugins are: 
    lutin, lustre-v6, sasa

Examples of usage:
  rdbg -sut "lv6 file.lus -n node" -env "lutin f.lut -n main"
  rdbg -sut "ecexe-rif f.ec node" -env "lutin f.lut -n main"
  lv6 -2c -cc f.lus -n n ;rdbg -sut "./n.exec" -env "lutin f.lut -n main"

Hint: preprend rdbg by 'ledit' (or 'ledit -h rdbg-history -x').

More information: http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/

usage: rdbg [<options>] 
where <options> are:

-sut, --sut <string>
      Add a sut 
-sut-nd, --sut-nd <string>
      Add a sut, but don't debug it
-env, --env <string>
      Add an env
-env-nd, --env-nd <string>
      Add an env, but don't debug it
-oracle, --oracle <string>
      Add an oracle
-oracle-nd, --oracle-nd <string>
      Add an oracle, but don't debug it
-lurette, --lurette
      Use the lurette mode (i.e., runs everything without debugging)
-l, --test-length, --step-number <int>
      in lurette mode only: Set test length (step number)
-o, -output, --output, -rif, --rif <string>
      Set the output file name (currently,  "www.rif")
-e, -emacs, --emacs
      Use emacs to open appropriate buffers while debugging
-h, -help, --help
      Display this help message
-m, -more, --more
      Display more options

 rdbg --more

-ocd, --ocamldebug
      Run in lurette mode, but under the control of ocamldebug
-g, --gnuplot
      in lurette mode only:  Launch gnuplot to visualize the generated rif file
-s, --sim2chro
      in lurette mode only:  Launch sim2chro to visualize the generated rif file
--missing-vars-last
      Launch the missing variables process (luciole or stdin) in last (i.e., after env, and sut)
--luciole
      Launch luciole when variables are missing (stdin is used otherwise)
-norif, --no-rif
      Do not print data in the rif file (useful when there are too many variables)
      nb: inhibits  --sim2chro (which is fine when there are too many variables)
-orf, --overwrite-rif-file
      Overwrite "www.rif" if it exists without trying to invent a new name
-dsoe, --dont-stop-on-oracle-error
      Do not stop if one oracle is violated
-cv, --cov-file <string>
      file name coverage info will be put into
-rcv, --reset-cov-file
      Reset coverage file data
-no-log, --no-log
      Do no generate a rdbg.log file and output everything on stdout
-v, -verbose, --verbose
      Echo the commands sent to rdbg-top
--debug
      set on a verbose mode to (try to) understand what's going on
--ocaml-version
      Print the current ocaml version it was compiled with and exit
-version, --version
      Print the current version and exit

This tutorial is made for people that knows a little bit of ocaml, and that are willing to take advantage of the programming capability of rdbg.

rdbg-top is an ocaml toplevel REPL (Read-Eval-Print-Loop) with some modules pre-loaded (cf the rdbg.log to see the messages generated by rdbg-top during this loading).

rdbg is a wrapper around rdbg-top, which basically performs 3 things:

1. It discharges users from writing () and ;; before rdbg commands. This wrapping can be:
   • turned on/off by the #auto_on / #auto_off directives;
   • locally inhibited for lines beginning with the ' ' character or the "let" string.
2. It generates a rdbg-session-<i>.ml file that is loaded by rdbg-top. Each time rdbg is invoked with some arguments, an new rdbg-session-<i>.ml can be created. When rdbg is invoked (with or without argument), the user is prompted with the possibility to use previously generated sessions (cf Basic usage Section).
3. It generates a default my-rdbg-tuning.ml file, if none exists in the current directory. my-rdbg-tuning.ml is meant to contains user commands that persist across sessions. This file is loaded by from rdbg-session-<i>.ml at the very end of it.

my-rdbg-tuning.ml actually contains all the code that implements the Basic (Level 1) commands, taking advantage of Ocaml modules described in Sections 5, Rdbg6, and 7. We explain how below.

All rdbg commands are built on top of 2 functions only:

run : unit -> RdbgEvent.t
next :  RdbgEvent.t -> RdbgEvent.t

run (Section 5) returns the first event (Section 6). next allows one to access to the next event. Launch rdbg-top, and try to enter the following Ocaml sentences:

let e = run();;
let e = next e;;
let e = next e;;
let e = next e;;
let e = next e;;

e is of type RdbgEvent.t, which is an ocaml structure. You can access to the various fields of that structure as follows:

e.nb;;
e.data;;

If you are an ocaml programmer, you probably understand all the things that you could program using those 2 functions. Anyway, you just can use the ones that are provided in the RdbgStdLib module, which Interface documentation can be found in Section 7. You may also want to look at how they are implemented. Most of most are fairly simple.

Writing let e = next e;; to move one event forward is tedious. A sensible trick is to store the current event in a reference, and to define shortcuts that, by a side-effect, updates the current event.

let e = ref (run());;
let n () = e:=next !e;;

Now, to move one event forward from rdbg-top, you can type n();;. From rdbg, since it automatically adds () and ;;, you can actually just type n. The generated my-rdbg-tuning.ml file contains such kind of short-cuts for most useful functions defined in 7.

An OCaml sentence is any string you type at the ocaml REPL prompt until you type ;; and then the [Return] key. An rdbg sentence is any string you type at the rdbg prompt until you press the [Return] key.

rdbg sends everything you type to an ocaml toplevel REPL (rdbg-top), trying to guess when to add (boring) () and ;; and the end of your rdbg sentence () to build valid ocaml sentences. Hence, when you type at the rdbg prompt:

• help "apropos"[Return] it sends to the ocaml REPL the string help "apropos";;, which calls the help (pre-loaded) function with the ="apropos"= string argument.
• n[Return] it sends n();; to the ocaml REPL (which will do something iff the function n is defined and takes () (unit) as argument).

If you want to be sure that rdbg does not add anything to the sentences you type, just add a leading blank:

• ​ let my_n () = n ();; sends let my_n () = n ();;

but if you type

• ​ n[Return] it sends n and nothing happen as ocaml waits for ;;; so if then you type
• ;;[Return] it sends ;;, which returns the type of n, but without actually calling n as no () has been provided.

In different words n[Return] has the same effect as ​ n();;[Return]

If you want to write a function on several lines, begin your sentence by a space (i.e., an empty string) at the rdbg prompt. To end your sentence and send it to rdbg-top, enter the ";;" string.

https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/rdbg/blob/master/lib/rdbgEvent.ml

https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/lutils/blob/master/lib/data.mli

yes