Interactive sasa simulations with rdbg (advanced users)

Warning: this tutorial describes how to perform interactive sasa session using a CLI (Command Line Interface). It is probably easier to begin with the GUI:

This tutorial focuses on how to use rdbg to

  • perform interactive sasa simulations
  • move forwards, or backwards
  • step by step, or round by round
  • how to define a new rdbg command

Launching an example

Let’s download an example available in the git repository (if you haven’t already done this clone in other vtt posts).

[ -d "sasa" ] || git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test/coloring
make grid10.dot
make grid10.cma

The test/Makefile define rules to generate the grid10.dot, the registration code, and compiles everything (and generate grid10.cm* files that are needed for simulations). So now we can call sasa under the control of rdbg. We will use a synchronous daemon (--central-daemon or -cd for the close friends) that triggers at most one process at a time, so that the simulation does not converge too fast toward a silent configuration where there is nothing interesting to see.

rdbg --sasa -sut "sasa grid10.dot -cd" -l 1000

1
2
3

Enter one of the following key (the first is the default one):
  [] create a fresh session
  [q] quit

rdbg asks whether you want to create a new session (line 2) or quit (line 3). Let’s create a new session and the press [Enter] to choose the default alternative. This rdbg session launches the sasa simulator

The debugger stops at the first simulation event, display a pdf view of the grid10.dot file, where enabled processes are colored in green, and the activated (triggered) processes in orange (at most one here because of the --central-daemon option).

Moving around

Now, you can move one step forward using the s command at the (rdbg) prompt, and update the dot pdf view with d:

(rdbg) s
(rdbg) d

(rdbg) s
[2] p71_c=0
(rdbg) d
(rdbg)

Each time a new simulation event is reached, sasa prints the activated processed (here, p71) state values (here, 0). Note that you can tune this behavior if you wish (cf the rdbg-print-event vtt post).

Equivalently, you can use the sd command that combines s and d. After each move, the values of active processes states are printed (p71_c=0), as well as the step number between square braces ([2]).

Then you can try to move:

  • 13 steps forward: si 13
  • 1 step backward: b
  • 5 steps backwards: bi 5
  • to the first step: g 1
  • 1 round forward: nr
  • 1 round backward: pr

You can also type h to get online helps:

(rdbg) h

(rdbg) h
 rdbg is a Reactive program DeBuGger.
 - web doc  :http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg
 - tutorials:http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/vtt/rdbg
 - online doc:
   + help cat     (* List commands categories *)
   + help <a cat> (* List commands related to a given category *)
   + help <a command>   (* Print the documentation of a command/function *)
   + apropos <a string> (* List functions related a string *)
   + apropos            (* List all functions *)
   + h (* Shortcut for help        *)
   + a (* Shortcut for apropos     *)
   + l (* List of Level 0 commands *)

Extending the set of commands (for advanced users)

One specificity of rdbg is of being programmable. Basically, you need to know ocaml and a little bit of the rdbg API if you want to do it yourself. This objective of the following is to demonstrate how quickly it can be done. If you want to understand everything about what’s really happening here, you may want to read the rdbg Level1 documentation at some point.

By default, rdbg provides a limited set of commands for moving inside the simulation history that are dedicated to sasa. Actually, the sasa specific commands are not defined in rdbg but the test/.my-rdbg-tuning.ml file, that is loaded in the sub-directories of test/.

Here is a part of what is displayed via the l command:

[snip]
Here is the list of rdbg Level 0 commands:
- forward moves:
  n: move forward of one event
  ni i: move forward of i events
  s: move forward of one step
  si i: move forward of n steps
  nm <string>:  move forward until a function which name matches a <string>

- backward moves:
  b: move backward of one event
  bi i: move backward of i events
  pm <string>:  move backward until a function which name matches a <string>
  g i: go to event number i
[snip]

- sasa commands
[snip]
 + Moving commands
   sd: go to the next step and display the network with one of the GraphViz tools
   nd: go to the next event and display the network
   bd: go to the previous event and display the network
   nr: go to the next round and display the network
   pr: go to the previous round and display the network

Suppose now that you want to inspect what happens when a particular process is triggered. For instance the process p38. In other words, you’d like to go the step where the variable p38_conflict is true. To do that, we can use 2 rdbg commands fc and vv:

(rdbg) help fc
(rdbg) help vv

(rdbg) h "fc"
 fc : (unit -> bool) -> unit
 move forward until a predicate (of type unit -> bool) becomes true
(rdbg) h "vv"
 vv : string -> Data.t
 returns the value of a variable attached to the current event (if available)

Hence, if one wants to jump the first step forward where the process named p42 is triggered, one can take advantage of the variable named p42_conflict and stop when it becomes true.

(rdbg) fc (fun () -> vv "p42_conflict"= B true)

One issue with the request above is that we may reach stabilization without having the p42 process triggered. If such a case, the request will stop when the maximal step number is reached1 as p42 will never be enabled. To avoid this, we can take advantage of the stable predicate (which is defined in test/.my-rdbg-tuning.ml), and stop as soon as stablilization is reached (all Enab_* variables in the current configuration are false).

(rdbg) help stable
(rdbg) fc (fun () -> stable () || vv "p42_conflict"= B true)

(rdbg) help stable
 stable : unit -> bool
 is the current configuration stable?
(rdbg) fc (fun () -> stable () || vv "p42_conflict"= B true)
 [28] p42_c=3

On this particular simulation, 42 was triggered at step 28.

If you need to do that kind of search often, on different processes, you can define an ocaml shorthand as follows:

(rdbg) let trig p = fc (fun _ -> stable() || vv (p^"_conflict") = B true); d();;
(rdbg) trig "p23"

The d () at the end of the trig definition is to update the dot graph.

  1. which is controlled by the -l (also named --test-length or --step-number) rdbg option. [return]