Add documentation for the instrumentation and monitoring of the sampl…

…e example.

Containerfile

@@ -11,6 +11,7 @@ RUN \
   m4 \
   python3 \
   python3-distutils \
+  dos2unix \
   opam
 
 RUN opam init --disable-sandboxing -ya

doc/general.md

@@ -16,7 +16,7 @@
 - [The Configuration File (optional)](#configuration-file-optional)
 
 
-### Overview of the Command Line Interface of rmtld3synth
+## Overview of the Command Line Interface of rmtld3synth
 
 Here are the options available:
 
@@ -47,121 +47,108 @@ Arg                   | Description
   --help              |Display this list of options
 
 
-### Input Languages
+## Input Languages
 
-DSL syntax available [here](dsl.md).
+The primary language used is the DSL, whose syntax is available [here](dsl.md).
 
+Other input languages are available [here](input-languages.md).
 
-#### Write old style RMTLD3 formulas
 
-RMTLD3 is composed of atomic propositions and logic variables that can be syntactically connected using some temporal operators and the relation '<' for terms. The syntax of RMTLD3 terms `t` and formulas `f` is defined inductively as follows:
-```
-t ::= (Constant `<constant>`) | (Variable `<lvariable>`) | (Plus t t) | (Times t t) | (Duration t formula)
-f ::= (Prop `<proposition>`) | (LessThan t t) | (Or f f) | (Not f) | (Until `<number>` f f)
-```
-where `<constant>` is a real-number (interpreted as float/double), `<lvariable>` is a logic variable (identified by unique strings), `<proposition>` is a proposition (identified by unique strings), and `<number>` is a non-negative real-number (interpreted as float/double). For more details you can read the syntax defined in the paper [[3]](http://link.springer.com/chapter/10.1007%2F978-3-319-23820-3_11).
+## Include Monitors with rtmlib2
 
-Let us now formalize the sentence `"the duration of task A with an arbitrary period greater than 10 and small than 20 is less than 5 units."`
-as a formula in RMTLD3. It can be described as
+Let us assume that we would like to construct a monitor to observe the temporal behaviour and the duration. We define an example property as follows:
 ```
-(And
-  (Not (And (Lessthan (Variable x) (Constant 20)) (Lessthan (Constant 10) (Variable x))))  
-  (LessThan (Duration x (Or task_a_release (Or task_a_start ...))) 5)
-)
-
+(a -> (a || b) until c within 10s) && 
+(duration of c in 0 .. 10) < 4
 ```
-The formula contains `...` meaning the remaining events triggered by the task A, and `x` is a logic variable meaning that the duration can be measured such as the inequality `10 < x < 20`. Note that `(And a b)` is a shortcut for `(Not (Or (Not a) (Not b)))`.
-
-Note that in this example the notion of event is as used in Discrete Event Systems. Events are directly encoded using propositions and each event means an atomic proposition.
-
 
-
-#### Write formulas in latex and know how to use them
-
-Latex equation formulas are much less verbose than symbolic expressions. Due to that, we made available the synthesis of RMTLD3 formulas written as latex equations.
-Consider the formula
+Plain LaTeX serves as an alternative encoding for expressions, and the aforementioned property can be encoded using it.
 ```
 (a \rightarrow ((a \lor b) \until{<10} c)) \land \int^{10} c < 4
 ```
-that intuitively describes that given an event `a`, `b` occurs until `c` and, at the same time, the duration of `b` shall be less than four time units over the next `10` time units.
-For instance, a trace that satisfies this formula is
+
+To construct the monitor and its accompanying functions within the `mon1` folder, we utilize the command 
 ```
-(a,2),(b,2),(a,1),(c,3),(a,3),(c,10)
+./rmtld3synth --synth-cpp11
+--input-dsl "(a -> (a || b) until c within 10s) && (duration of c in 0 .. 10) < 4" --out-src="mon1" 
 ```
-From rmtld3synth tool, we have synthesized the formula's example into the Ocaml language code described in the ![texeq_sample.ml](/examples/texeq_sample.ml?raw=true). For that, we have used the command
+Note that instead of using `--input-dsl`, you can utilize a latex expression by replacing it with `--input-latexeq`.
+The files that should be included in the `mon1` folder are:
 ```
-./rmtld3synth --synth-ocaml --input-latexeq
-"(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" > mon_sample.ml
+Rtm_compute_0746.h     (* The compute file where monitor is defined *)
+Rtm_instrument_0746.h  (* The instrumentation to be included in the software under observation. *)
+Rtm_monitor_0746.h     (* The monitor bindings to deploy the monitor as a thread or task. *)
 ```
-We can also generate cpp11 monitors by replacing the argument `--synth-ocaml` with `--synth-cpp11`.
-The outcome is the monitor illustrated in the ![texeq_sample_mon0.h](/examples/texeq_sample_mon0.h?raw=true) and ![texeq_sample_mon0_compute.h](/examples/texeq_sample_mon0_compute.h?raw=true) files.
-Both monitors can now be coupled to the system under observation using rtmlib.
+Note that `0746` is the hexadecimal indetifier of the monitor. If the monitor structure and behaviour changes, the identifier also changes.
 
-To use those monitors in Ocaml, we need to define a trace for Ocaml reference as follows:
-```
-open Mon_sample
-module OneTrace : Trace = struct let trc = [("a",(0.,2.));("b",(2.,4.));("a",(4.,5.));("c",(5.,8.));
-    ("a",(8.,11.));("c",(11.,21.))] end;;
+### Sample (runs on all architectures supported by rtmlib2)
 
-module MonA = Mon_sample.Mon0(OneTrace);;
-```
+Consider the previous generated monitor, their files in folder `mon1`, and the instrumentation file `sample_instrumentation.cpp` as defined below.
 
+```C++
+// filename sample_instrumentation.cpp
 
-#### Map Event Symbols
+#include "Rtm_instrument_0746.h"
 
-Let us use the previous example containing three propositions `a, b, c` that will be mapped to the SUO in a different way.
-The usage of ASCII characters or strings is not the most efficient way to proceed since they will quickly increase the memory footprint. We will see now how we can avoid it.
+extern int sample(); // the external function to construct the sample monitor
 
-The content of the file `mon0_compute.h` describes where the symbols can appear as simple numbers. Indeed `a`,`b` and `c` were mapped using a hash table to some sort of binary enumeration (i.e., `0x04` for a, `0x03` for `b`, and `0x01` for `c`). To be able to match this encoding when generating events describing `a,b,c`, we have to use the macro definitions `SORT_a,SORT_b,SORT_c`. If we have a symbol `sym` then the respective macro should be `SORT_sym`. Althought a check is performed by the tool, we have to be carefull about the macro variable's names accepted in C++11 when describing the name of the propositions in RMTLD3 specifications.
+int main() {
+  using Writer = Writer_rtm__0746;
 
-The map function `_mapsorttostring` is also available if we do not want to work with sorts and instead use strings.
+  // using the new name
+  Writer w;
 
+  // push symbol 'a' with timestamp 0
+  // Note that all propositions are defined inside the writer.
+  // There is no way to send other symbols that are not defined there.
+  w.push(Writer::a, 0);
+
+  sample(); // run the sample monitor
+}
+```
+
+Now, we are able to compile the instrumentation sample
 ```
-  #define SORT_a 4
-  #define SORT_b 3
-  #define SORT_c 1
-  
-  #include <string>
-  #include <unordered_map>
-  // Create an unordered_map of sorts (that map to integers)
-  std::unordered_map<std::string, int> _mapsorttostring = {
-  {"a",4},
-  {"b",3},
-  {"c",1},
-  };
+gcc -I../rtmlib2/src/ sample_instrumentation.cpp -o test -latomic
 ```
+It will ask for `__buffer_rtm_monitor_3a50` at linkage step and the `sample` function.
 
+We will now establish a sample monitor that incorporates the necessary symbols in the following manner:
 
-### Include Monitors with rtmlib2
+```C++
+// filename sample_monitor.cpp
 
-Let us assume that we would like to construct a monitor to observe the temporal behaviour and the duration. We define an example property as follows:
-```
-(a \rightarrow ((a \lor b) \until{<10} c)) \land \int^{10} c < 4
-```
+#include "Rtm_monitor_3a50.h"
 
-To build the monitor and some auxiliary functions in the folder `mon1`, we utilize the command
-```
-./rmtld3synth --synth-cpp11 --input-latexeq
-"(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" --out-src="mon1"
+RTML_BUFFER0_SETUP(); // defines the buffer here
+
+int sample() {
+  RTML_BUFFER0_TRIGGER_PERIODIC_MONITORS(); // triggers the thread to run the
+                                            // monitor
+
+  while (true) {
+    // do something to wait for threads
+  }
+}
 ```
 
-The output tree should contain the files:
+We perform the compilation of `sample_monitor.cpp` and `sample_instrumentation.cpp` with
+
 ```
-Rtm_compute_XXXX.h     (* The compute file where monitor is defined *)
-Rtm_instrument_XXXX.h  (* The instrumentation to be included in the software under observation. *)
-Rtm_monitor_XXXX.h     (* The monitor bindings to deploy the monitor as a thread or task. *)
+gcc -I../rtmlib2/src/ sample_monitor.cpp sample_instrumentation.cpp -o example -latomic -fno-rtti -fno-exceptions -DRTMLIB_ENABLE_DEBUG_RMTLD3
 ```
-Note that `XXXX` is the hexadecimal indetifier of the monitor. If the monitor changes, the identifier also changes.
+After creating the initial instrumentation and monitoring samples, you can execute them by running `./example`.
 
+Great, you have successfully created and run your first C++ monitor!
 
 
-#### Bare Metal (without OS)
+### Bare Metal (without OS)
 
 To include the monitor as baremetal application we have to deploy it without thread support.
 
 Please refer to [rtmlib2](https://github.com/anmaped/rtmlib) documentation for more details.
 
-#### NuttX OS
+### NuttX OS
 
 In this case, we only have to include the header file `Rtm_monitor_XXXX.h` to include the monitor and the `Rtm_instrument_XXXX.h` to instrument the software under observation.
 Now, we are able to access some symbols such as `__start_periodic_monitors` and `__buffer_mon1`. The `Rtm_monitor_XXXX.h` defines them as follows:
@@ -186,31 +173,80 @@ RTML_buffer<int, 100> __buffer_mon1 __attribute__((used));
 ```
 indicating that `__buffer_mon1` is reused or locally instantiated. The function `__start_periodic_monitors` will enable the task using the POSIX Threads interface defined in rtmlib (see task_compat.h for more details).
 
-##### Compile existing demos
+#### Compile existing demos
 
 After this step, we shall link the monitors as a standalone app or module as provided in [rtmlib2 examples](https://github.com/anmaped/rtmlib) directory.
 
 The monitors to be used with Ardupilot should be included in the external Px4 makefile `px4_common.mk` in the Ardupilot's directory `modules/Px4`. Check [these instructions](nuttx-ardupilot.md) for more details.
 
 
-#### FreeRTOS
+### FreeRTOS
 
 Please refer to [rtmlib2](https://github.com/anmaped/rtmlib) documentation for more details.
 
 
-#### Hardware (FPGA)
+### Hardware (FPGA)
 
-[TBC]
+[TBD]
 
 
-#### Unit Test Generation
 
-rmtld3synth also supports the automatic generation of unit tests for C++ based on the oracle deployed in Ocaml. Based on it, we test the expected evaluation of a set of formulas against the evaluation in the embedded platform.
+### To show the mapping between the propositions and the symbols.
+
+Let us take the previous example with three propositions `a, b, c`, which are mapped to instrumentation and monitor side in a different way.
+Using ASCII characters or strings is not the most efficient way to do this, as they will quickly increase the memory footprint. We will now see how we can avoid this.
+
+The content of the file `Rtm_compute_0746.h` describes where the symbols can appear as simple numbers.
+
+```C++
+// Propositions
+enum _auto_gen_prop
+{
+  PROP_a = 3,
+  PROP_b = 2,
+  PROP_c = 1,
+};
+```
+
+In fact, `a`,`b` and `c` have been mapped to a kind of binary enumeration using a hash table (i.e. `0x03` for a, `0x02` for `b`, and `0x01` for `c`). To match this encoding when generating events describing `a,b,c` we need to use the macro definitions `PROP_a,PROP_b,PROP_c`. If we have a symbol `sym` then the corresponding macro should be `PROP_sym`.
+
+Although the rtmtld3synth tool does a check and all variable names accepted by the DSL are safe, we need to be aware of the macro variable names accepted in C++11 when describing the names of propositions in other RMTLD3 specifications.
+
+```C++
+#ifdef RTMLIB_ENABLE_MAP_SORT
+#include <string>
+#include <unordered_map>
+
+// Create an unordered_map of sorts (that map to integers)
+std::unordered_map<std::string, int> _mapsorttostring = {
+  { "a", PROP_a },
+  { "b", PROP_b },
+  { "c", PROP_c },
+};
 
-There are two flags. The `gen_unit_tests` enables the automatic generation of monitors including the makefiles, and the  `gen_concurrency_tests` that instructs the construction of a set of tests for the performance evaluation of the rmtlib.
+// Create an unordered_map of sorts (that map to strings)
+std::unordered_map<int, std::string> _mapsorttoint = {
+  { PROP_a, "a" },
+  { PROP_b, "b" },
+  { PROP_c, "c" },
+};
+#endif
+```
+The map function `_mapsorttostring' is also available if we do not want to work with sorts and want to use strings instead.
+
+### Intrumentation side
+
+Since version `0.4` all propositions are defined inside the writer. There is no way to send other symbols that are not defined there.
+```C++
+using Writer = Writer_rtm__0746;
+
+Writer::a // means PROP_a
+...
+Writer::c // means PROP_c
+```
 
 
-#### Translate rmtld3 to smtlibv2
+## Translate rmtld3 to smtlibv2
 
 To solve the formula `(LessThan (Constant 0) (Duration (Constant 10) (Prop A)))`, we can follow these steps:
 
@@ -225,7 +261,7 @@ To solve the formula `(LessThan (Constant 0) (Duration (Constant 10) (Prop A)))`
 Please note that step 2 is optional.
 
 
-#### Configuration File (optional)
+## Configuration File (optional)
 
 Settings for RMTLD3 synthesis tool are defined using the syntax `(<setting_id> <bool_type | integer_type | string_type>)`, where '|' indicates the different types of arguments such as Boolean, integer or string, and `setting_id` the setting identifier of the type string.
 
@@ -244,7 +280,7 @@ See [the overall parameters](doc/configparameters.md) for more details.
 
 ~~~~~~~~~~~~~~~~~~~~~
 
-`gen_tests` sets the automatic generations of test cases (to be used as a demo in the described illustration below).
+`gen_tests` sets the automatic generations of test cases (see other options below).
 
 `minimum_inter_arrival_time` establishes the minimum inter-arrival time that the events can have. It is a very pessimistic setting but provides some information for static checking.
 
@@ -253,3 +289,9 @@ See [the overall parameters](doc/configparameters.md) for more details.
 `event_subtype` provides the type for the event data. In that case, it is an identifier that can distinct 255 events. However, if more events are required, the type should be modified to *uint32_t* or greater. The number of different events versus the available size for the identifier is also statically checked.
 
 `cluster_name` identifies the set of monitors. It acts as a label for grouping monitor specifications.
+
+### unit tests flags
+
+rmtld3synth also supports the automatic generation of unit tests for C++ based on the oracle deployed in Ocaml. Based on it, we test the expected evaluation of a set of formulas against the evaluation in the embedded platform.
+
+There are two flags. The `gen_unit_tests` enables the automatic generation of monitors including the makefiles, and the  `gen_concurrency_tests` that instructs the construction of a set of tests for the performance evaluation of the rmtlib.

doc/input-languages.md

@@ -0,0 +1,61 @@
+# Input Languages
+
+rtmtld3synth has three major input languages.
+
+## With DSL (prefered)
+
+Documentation available [here](dsl.md).
+
+## With symbolic expressions (old style)
+
+RMTLD3 is composed of atomic propositions and logic variables that can be syntactically connected using some temporal operators and the relation '<' for terms. The syntax of RMTLD3 terms `t` and formulas `f` is defined inductively as follows:
+```
+t ::= (Constant `<constant>`) | (Variable `<lvariable>`) | (Plus t t) | (Times t t) | (Duration t formula)
+f ::= (Prop `<proposition>`) | (LessThan t t) | (Or f f) | (Not f) | (Until `<number>` f f)
+```
+where `<constant>` is a real-number (interpreted as float/double), `<lvariable>` is a logic variable (identified by unique strings), `<proposition>` is a proposition (identified by unique strings), and `<number>` is a non-negative real-number (interpreted as float/double). For more details you can read the syntax defined in the paper [[3]](http://link.springer.com/chapter/10.1007%2F978-3-319-23820-3_11).
+
+Let us now formalize the sentence `"the duration of task A with an arbitrary period greater than 10 and small than 20 is less than 5 units."`
+as a formula in RMTLD3. It can be described as
+```
+(And
+  (Not (And (Lessthan (Variable x) (Constant 20)) (Lessthan (Constant 10) (Variable x))))  
+  (LessThan (Duration x (Or task_a_release (Or task_a_start ...))) 5)
+)
+
+```
+The formula contains `...` meaning the remaining events triggered by the task A, and `x` is a logic variable meaning that the duration can be measured such as the inequality `10 < x < 20`. Note that `(And a b)` is a shortcut for `(Not (Or (Not a) (Not b)))`.
+
+Note that in this example the notion of event is as used in Discrete Event Systems. Events are directly encoded using propositions and each event means an atomic proposition.
+
+
+
+## LaTex expressions for paper writing purposes
+
+Latex equation formulas are much less verbose than symbolic expressions. Due to that, we made available the synthesis of RMTLD3 formulas written as latex equations.
+Consider the formula
+```
+(a \rightarrow ((a \lor b) \until{<10} c)) \land \int^{10} c < 4
+```
+that intuitively describes that given an event `a`, `b` occurs until `c` and, at the same time, the duration of `b` shall be less than four time units over the next `10` time units.
+For instance, a trace that satisfies this formula is
+```
+(a,2),(b,2),(a,1),(c,3),(a,3),(c,10)
+```
+From rmtld3synth tool, we have synthesized the formula's example into the Ocaml language code described in the ![texeq_sample.ml](/examples/texeq_sample.ml?raw=true). For that, we have used the command
+```
+./rmtld3synth --synth-ocaml --input-latexeq
+"(a \rightarrow ((a \lor b) \until_{<10} c)) \land \int^{10} c < 4" > mon_sample.ml
+```
+We can also generate cpp11 monitors by replacing the argument `--synth-ocaml` with `--synth-cpp11`.
+The outcome is the monitor illustrated in the ![texeq_sample_mon0.h](/examples/texeq_sample_mon0.h?raw=true) and ![texeq_sample_mon0_compute.h](/examples/texeq_sample_mon0_compute.h?raw=true) files.
+Both monitors can now be coupled to the system under observation using rtmlib.
+
+To use those monitors in Ocaml, we need to define a trace for Ocaml reference as follows:
+```
+open Mon_sample
+module OneTrace : Trace = struct let trc = [("a",(0.,2.));("b",(2.,4.));("a",(4.,5.));("c",(5.,8.));
+    ("a",(8.,11.));("c",(11.,21.))] end;;
+
+module MonA = Mon_sample.Mon0(OneTrace);;
+```

src/rmtld3synth.ml

@@ -120,7 +120,7 @@ let default_settings helper =
      (rtm_min_inter_arrival_time 1)\n\
      (rtm_max_period 2000000)\n\
      (rtm_event_type Event)\n\
-     (rtm_event_subtype prop)\n\
+     (rtm_event_subtype _auto_gen_prop)\n\
      (rtm_monitor_name_prefix rtm_#_%)\n\
      (rtm_monitor_time_unit s)\n\
      (gen_tests false)"