ReaX: User Manual

A set of non-controllable variables must be declared within an !input section:

# Declaration of non-controllable variables
<input-decls> ::= "!input" <var-decls>

The declaration of a sequence of controllable variables takes place in !controllable sections, and additionally permits the specification of associated default expressions:

# Declaration of controllable variables
<crtl-decls> ::= "!controllable" <ctrl-decls'> { <ctrl-decls'> }
<ctrl-decls'> ::= <ctrl-id> { ',' <ctrl-id> } ':' <type> ';'
<ctrl-id> ::= <id> [ '?' <expr> ]

U/C groups are declared by alternating !input and !controllable sections.

# Possibly empty sequence of U/C groups
<uc-groups-decl> ::= { <uc-group-decl> } [ <uc-group-final-u> ]
                     | <uc-group-only-c>
<uc-group-decl> ::= <input-decls> <ctrl-decls>
<uc-group-final-u> ::= <input-decls>
<uc-group-only-c> ::= <ctrl-decls>

U/C group sequences must start with the declaration of a set of non-controllable inputs, unless all inputs are controllable.

I/O groups are the counterpart of U/C groups, and typically define the signature of a function resulting from the triangularization of a controller synthesized for a weavable node. I/O groups are declared by alternating !input and !output sections.

# Non-empty sequence of I/O groups
<io-groups-decl> ::= <io-group-decl> [ <io-group-final-i> ]
                   | <io-group-only-o>
<io-group-decl> ::= <io-group-decl'> { <io-group-decl'> }
<io-group-decl'> ::= <input-decls> <output-decls>
<io-group-final-i> ::= <input-decls>
<io-group-only-o> ::= <output-decls>
<output-decls> ::= "!output" <var-decls>

I/O group sequences must start with the declaration of a set of non-controllable inputs, unless all inputs are controllable.

The transition function of nodes are specified as assignments of state variables according to the following syntax:

<trans-func> ::= "!transition" <assign> { <assign> }
<assign> ::= <id> ( ":=" | "'" '=' ) <expr> ';'

Notice that the Boolean synthesis algorithm may compute correct results for nodes involving numerical components in their vector of state variables (even if these state variables do not encode outputs — see Section “A Note on Specifying Outputs” of the Technical References Manual). It may however never terminate and lead to an explosion of memory consumption in this case.

Let the file 2tasks.ctrln exclusively contain the Controllable-Nbac code as listed bellow. It describes a node (almost) equivalent to the one described as Figure 3 in the paper introducting ReaX [Berthier and Marchand(2014)]. In terms of behavior, the main difference lies in the ability of the controller to force entering Idle from Active. Its automaton representation is shown in Figure 1.

!typedef
  S = enum {Idle, Active};

!state
  t1, t2: S;

!input
  r1, r2, s1, s2, _c1: bool;

!controllable
  c1 ? _c1, c2 ? c1: bool;

!transition
  t1' = if t1 = Idle   and r1 and c1  then Active else
        if t1 = Active and (s1 or c1) then Idle   else t1;
  t2' = if t2 = Idle   and r2 and c2  then Active else
        if t2 = Active and (s2 or c2) then Idle   else t2;

!initial
  t1 = Idle and t2 = Idle;

!invariant
  #(t1 = Active, t2 = Active);

Remark that in this example, the default value for controllable input c1 is specified as additional non-controllable input _c1; for illustrative purpose, the default value of c2 is the effective value of c1 (to be chosen by the controller).

To compute a controller for this node using the Boolean synthesis algorithm (sB), to triangularize it (-t), and also to show basic debugging information about the execution of ReaX (--debug D), one can use the following command line:

reax 2tasks.ctrln -a 'sB' -t --debug D

The program reports on its execution using a sequence of log entries as listed bellow. Each log entry starts with a measure of the time it effectively used the processor since the beginning of its execution (in seconds). Following are a character describing the log level: ’E’ for errors, ’W’ for warnings, ’I’ for general information (the default level), and ’D’, ’d’ and ’.’ for three further debugging levels. Then comes the name of an internal module of ReaX and the payload itself.

[0.019 I Main] This is ReaX version 0.10.2-19-ge7f3a3b.
[0.020 I Main] Reading node from `2tasks.ctrln'…
[0.028 I Supra] Variables(bool/num): state=(2/0), i=(7/0), u=(5/0), c=(2/0)
[0.029 I Df2cf] Preprocessing: discrete program
[0.029 I Synth] Boolean synthesis:
[0.029 D sB] ++ φ = t1 = Idle or t1 = Active and t2 = Idle (= ~β)
[0.029 I sB] ++> Invariance:
[0.030] CUDD reordering…
[0.036 I sB] ++<
[0.036 D sB] β = t1 = Active and t2 = Active
[0.036 I sB] I∩β=∅ = true (= success)
[0.036 I sB] Building controller…
[0.036 I sB] Computing boundary transtions…
[0.036 I sB] Simplifying controller…
[0.036 I Synth] Boolean synthesis succeeded.
[0.036 I Main] Extracting generated controller…
[0.036 I Main] Checking generated controller…
[0.037 I Main] Outputting into `2tasks.ctrlr'…
[0.039 I t.] Triangulation…
[0.039] Full synchronous reordering.
[0.041] CUDD reordering…
[0.049 D t.] Triangularized controller:
             c1' = _c1;
             c2' = c1 and not r1 or
                   c1 and r1 and not r2 and t1 = Idle or
                   c1 and r1 and r2 and t1 = Idle and t2 = Active or
                   c1 and r1 and t1 = Active;
[0.049 I Main] Extracting triangularized controller…
[0.049 I Main] Checking triangularized controller…
[0.050 I Main] Outputting into `2tasks.ctrlf'…

The resulting output file 2tasks.ctrlf encodes the triangulated controller. Observe that its inputs are the union of all state and non-controllable inputs of the original node, and its outputs are the two controllable inputs.

(*
Generated by ReaX version 0.10.2-19-ge7f3a3b.
The full command line was:
/users/loco/nberth/bin/reax 2tasks.ctrln -a sB -t --debug D
*)
!typedef
  S = enum {Idle, Active};

!input
  t1: S;
  t2: S;
  r1: bool;
  r2: bool;
  s1: bool;
  s2: bool;
  _c1: bool;

!output
  c1: bool;
  c2: bool;

!local
  l14, l15, l16, l17: bool;

!definition
  c1 = _c1;
  l14 = not ((t2 = Idle));
  l15 = (not r2 or l14);
  l16 = (not ((t1 = Idle)) or l15);
  l17 = (not r1 or l16);
  c2 = c1 and l17;

!assertion true;

Consider an extended version of the previous example finite Controllable-Nbac node, now involving a numerical state variable. In this model, additional state variables x1 and x2 are used to count the number of steps spent in the Active state for each task.

Let 2tasks-counters.ctrln be the file:

!typedef
  S = enum {Idle, Active};

!state
  t1, t2: S;
  x1, x2: int;

!input
  r1, r2, s1, s2, _c1, _c2: bool;

!controllable
  c1 ? _c1, c2 ? _c2: bool;

!transition
  t1' = if t1 = Idle   and r1 and c1  then Active else
        if t1 = Active and (s1 or c1) then Idle   else t1;
  x1' = if t1 = Idle   and r1 and c1  then 0      else
        if t1 = Active                then x1 + 1 else x1;
  t2' = if t2 = Idle   and r2 and c2  then Active else
        if t2 = Active and (s2 or c2) then Idle   else t2;
  x2' = if t2 = Idle   and r2 and c2  then 0      else
        if t2 = Active                then x2 + 1 else x2;

!initial
  t1 = Idle and t2 = Idle and x1 = 0 and x2 = 0;

!invariant
  #(t1 = Active, t2 = Active) and x1 <= 10 and x2 <= 10;

It encodes the parallel composition of two instances of the automaton of Figure 2. Here, the invariant to enforce imposes both the mutual exclusion between the Active states, and an upper-bound on their counters.

To compute a controller for this node using the deadlock-avoiding over-approximating synthesis algorithm (sS:deads) with the disjunctive power domain over intervals (d={I:D}), and then triangularize it (-t), we use the following command line:

reax 2tasks-counters.ctrln -a 'sS:d={I:D},deads' -t --debug D2

The corresponding rather detailed execution trace (--debug D2) shows:

[0.016 I Main] This is ReaX version 0.10.2-19-ge7f3a3b.
[0.016 I Main] Reading node from `2tasks-counters.ctrln'…
[0.024 I Supra] Variables(bool/num): state=(2/2), i=(8/0), u=(6/0), c=(2/0)
[0.024 I Verif] Forcing selection of power domain.
[0.025 I Df2cf] Preprocessing: discrete program
[0.025 I Synth] Standard logico-numerical synthesis with powerset extension of
                power domain over boxes with BDDs and capture of deadlocking
                states:
[0.025 I s.] Computing the guard on inputs.
[0.025 I s.] Computing the original set of deadlocking states.
[0.025 d sS] α(𝔉) = {⟦x1≥11⟧,
                     ⟦t1 = Active and t2 = Active ⟼ x1≤10 ∧ x2≤10⟧,
                     ⟦x2≥11⟧}
[0.026 D s.] Beginning of least fixpoint computation.
[0.026 D sS] Traversing arc 1.
[0.029 D sS] Traversing arc 1.
[0.033 D s.] End of least fixpoint computation.
[0.033 d sS] I'𝔉 = γ({⟦t1 = Active and t2 = Idle ⟼ x1≥10⟧,
                      ⟦t1 = Active and t2 = Active ⟼ x1≥10⟧,
                      ⟦t1 = Active and t2 = Active ⟼ x1≤10 ∧ x2≤10⟧,
                      ⟦x1≥11⟧,
                      ⟦x2≥11⟧,
                      ⟦t1 = Active and t2 = Active ⟼ x2≥10⟧,
                      ⟦t1 = Idle and t2 = Active ⟼ x2≥10⟧})
[0.034 I sB] Building controller…
[0.035 I sB] Computing boundary transtions…
[0.035 I sB] Simplifying controller…
[0.035 d sB]   K  = (35n,72m)
[0.035 I Synth] Standard logico-numerical synthesis with powerset extension of
                power domain over boxes with BDDs and capture of deadlocking
                states succeeded.
[0.035 I Main] Extracting generated controller…
[0.036 I Main] Checking generated controller…
[0.038 I Main] Outputting into `2tasks-counters.ctrlr'…
[0.041 I t.] Triangulation…
[0.041] Full synchronous reordering.
[0.043] CUDD reordering…
[0.048 d t.] #1:   K = t1 = Idle and t2 = Idle and x2<=10 and x1<=10 or
                       t1 = Idle and t2 = Active and x2<=10 and x1<=10
                       and x2<=9 or
                       t1 = Active and t2 = Idle and x2<=10 and x1<=10
                       and x1<=9
[0.048 D t.] Triangularized controller:
             c1' = not _c1 and not s1 and t1 = Active and x1>=9 or _c1;
             c2' = not _c2 and not r1 and not s2 and t2 = Active and x2>=9 or
                   not _c2 and not c1 and r1 and not s2 and t2 = Active
                   and x2>=9 or
                   not _c2 and c1 and r1 and not s2 and t2 = Active or
                   _c2 and not r2 and t1 = Idle and t2 = Idle or
                   _c2 and not r1 and r2 and t1 = Idle and t2 = Idle or
                   _c2 and not c1 and r1 and r2 and t1 = Idle and t2 = Idle or
                   _c2 and t1 = Idle and t2 = Active or
                   _c2 and not r2 and not s1 and t1 = Active or
                   _c2 and c1 and r2 and not s1 and t1 = Active or
                   _c2 and s1 and t1 = Active;
[0.049 I Main] Extracting triangularized controller…
[0.049 I Main] Checking triangularized controller…
[0.051 I Main] Outputting into `2tasks-counters.ctrlf'…

From this trace, one can observe the successive values computed, and notably the set of states to be effectively avoided (\(I(\mathfrak{F})\)). Note that the BDD representation of the controller (\(K\)) is printed in abbreviated form as it is quite large; still, a representation of the triangularized controller (assignments of c1 and c2) is shown at the end of the trace. In Controllable-Nbac format, the resulting triangularized controller 2tasks-counters.ctrlf is:

(*
Generated by ReaX version 0.10.2-19-ge7f3a3b.
The full command line was:
/users/loco/nberth/bin/reax 2tasks-counters.ctrln -a sS:d={I:D},deads -t --debug D2
*)
!typedef
  S = enum {Idle, Active};

!input
  t1: S;
  t2: S;
  x1: int;
  x2: int;
  r1: bool;
  r2: bool;
  s1: bool;
  s2: bool;
  _c1: bool;
  _c2: bool;

!output
  c1: bool;
  c2: bool;

!local
  l35, l36, l37, l38, l39, l40, l41, l42, l43, l44, l45, l46, l47, l48: bool;

!definition
  l35 = (x1 >= 9);
  l38 = (x2 >= 9);
  l36 = not s1 and l35;
  l37 = not ((t1 = Idle)) and l36;
  c1 = (_c1 or l37);
  l39 = (c1 or l38);
  l43 = (not r2 or c1);
  l45 = (not r1 or not c1);
  l40 = (if r1 then l39 else l38);
  l44 = (s1 or l43);
  l46 = (not r2 or l45);
  l41 = not s2 and l40;
  l47 = ((t2 = Active) or l46);
  l42 = not ((t2 = Idle)) and l41;
  l48 = (if (t1 = Idle) then l47 else l44);
  c2 = (if _c2 then l48 else l42);

!assertion true;

From this step, the command

ctrl2lut -o two-tasks-counters.lut 2tasks-counters.ctrln 2tasks-counters.ctrlr

creates a Lutin file two-tasks-counters.lut, that can then be simulated using the appropriate tools2. For instance, one can simulate the above controlled system by executing Luciole to interactively set all inputs of the system at each step (“main” is the name of the main node in the generated Lutin program):

lutin -n main -luciole two-tasks-counters.lut

Although Lutin does not support non-Boolean finite variables (i.e. enumerations) for now, ctrl2lut is able to handle them: it one-hot encodes such variables to keep the input and output signals readable. Note however that finite numerical variables are not supported.

Alternatively, one can also use the ctrl2lut tool to generate a stochastic environment node generating the inputs of the controller (or original) node from the values of its state variables, and by ensuring that its assertion is not violated.

ctrl2lut -o two-tasks-counters.lut 2tasks-counters.ctrln 2tasks-counters.ctrlr \
  -e -eo two-tasks-counters-env.lut

In this case, the simulation can be launched using Lurette3:

lurettetop \
  -rp 'sut:lutin:two-tasks-counters.lut:main' \
  -rp 'env:lutin:two-tasks-counters-env.lut:env'

To perform one-step optimization targeting the minimization of x1 and then of x2, one can use:

reax 2tasks-counters.ctrln -a 'sS:d={I:D},deads' -O 'o1:min x1,min x2'