Update documentation for v0.4 and rtmlib2 for v2.0.5.

doc/dsl.md

@@ -51,13 +51,46 @@ The BNF representation of the domain specification language is provided below:
 ## Examples
 
 1)
-![Wave 1](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave1.json)
+    ```
+    always (a until b within 3s) within 10s
+    ```
 
-2)
-![Wave 2](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave2.json)
+    "Always, within a span of 3 seconds, condition 'a' holds true until condition 'b' is met, and this must hold true throughout the entire 10 seconds span."
+
+    This implies that 'a' must always be true until 'b' becomes true, and the transition from 'a' to 'b' must happen within 3 seconds. Furthermore, this entire sequence must also occur within a 10-time-unit window.
+
+2) 
+    ```
+    always ((rise a) -> (eventually b within 3s)) within 10s
+    ```
+
+    "Always, within a span of 10 seconds, if 'a' rises, then 'b' will eventually occur within 3 seconds."
+
+    This means that whenever 'a' rises, it is always followed by 'b' within 3 units of time, and this pattern must hold true throughout the entire 10-time-unit window.
 
 3)
-![Wave 3](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave3.json)
+    ```
+    always ((rise a) -> (b on 3s)) within 10s
+    ```
+
+    or equivalent expression
+
+    ```
+    always ((rise a) -> (eventually b within =3s)) within 10s
+    ```
+
+    "Always, within a span of 10 units of time, if 'a' rises, then 'b' will occur exactly on the 3rd-second."
+
+    This means that whenever 'a' rises, it is always followed by 'b' exactly on the 3rd-time-unit, and this pattern must hold true throughout the entire 10-time-unit window.
+
+    - 3.a
+        ![Wave 1](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave1.json)
+
+    - 3.b
+        ![Wave 2](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave2.json)
+
+    - 3.c
+        ![Wave 3](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave3.json)
 
-4)
-![Wave 4](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave4.json)
+    - 3.d
+        ![Wave 4](https://svg.wavedrom.com/github/anmaped/rmtld3synth/v0.4/doc/waves/wave4.json)

doc/general.md

@@ -2,18 +2,23 @@
 # General Documentation
 
 ## Table of Contents
-- [rmtld3synth's CLI Overview](#overview-of-the-command-line-interface-of-rmtld3synth)
-- [Input Languages](#input-languages)
-  - [Write Formulas in RMTLD3](#write-formulas-in-rmtld3)
-  - [Import Formulas from Latex Equations](#write-formulas-in-latex-and-know-how-to-use-them)
-- [Compile generated Monitors](#compile-the-generated-monitors)
-- [Map Event Symbols](#map-event-symbols)
-- [Integrate Monitors using rtmlib in Bare Metal Platforms](#integrate-monitors-using-rtmlib-in-a-bare-metal-platform)
-  - [NuttX](#nuttx-os)
-  - [FreeRTOS](#freertos)
-- [Unit Test Generation](#unit-test-generation)
-- [Translate rmtld3 to smtlibv2](#translate-rmtld3-to-smtlibv2)
-- [The Configuration File (optional)](#configuration-file-optional)
+- [Overview of the Command Line Interface of rmtld3synth](general.md#overview-of-the-command-line-interface-of-rmtld3synth)
+- [Input Languages](general.md#input-languages)
+  - [With DSL (prefered)](input-languages.md#with-dsl-prefered)
+  - [With symbolic expressions (old style)](input-languages.md#with-symbolic-expressions-old-style)
+  - [LaTex expressions for paper writing purposes](input-languages.md#latex-expressions-for-paper-writing-purposes)
+- [Include Monitors with rtmlib2](general.md#include-monitors-with-rtmlib2)
+  - [Sample](general.md#sample-runs-on-all-architectures-supported-by-rtmlib2)
+  - [Bare Metal (without OS)](general.md#bare-metal-without-os)
+  - Real-time OS
+    - [NuttX](general.md#nuttx-os)
+    - [FreeRTOS](general.md#freertos)
+    - [RTEMS](general.md#rtems)
+  - [Hardware (FPGA)](general.md#hardware-fpga)
+  - [Mapping between propositions and symbols](general.md#to-show-the-mapping-between-the-propositions-and-the-symbols)
+- [Translate rmtld3 to smtlibv2](general.md#translate-rmtld3-to-smtlibv2)
+- [The Configuration File (optional)](general.md#configuration-file-optional)
+  - [Unit Tests flags](general.md#unit-tests-flags)
 
 
 ## Overview of the Command Line Interface of rmtld3synth
@@ -184,6 +189,10 @@ The monitors to be used with Ardupilot should be included in the external Px4 ma
 
 Please refer to [rtmlib2](https://github.com/anmaped/rtmlib) documentation for more details.
 
+### RTEMS
+
+[TBD]
+
 
 ### Hardware (FPGA)
 
@@ -210,7 +219,7 @@ enum _auto_gen_prop
 
 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.
+Although the rmtld3synth 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

readme.md

@@ -2,14 +2,14 @@
 rmtld3synth toolchain: Synthesis from a fragment of MTL with durations
 ======================================================================
 
-The rmtld3synth toolchain is capable of automatically generating cpp11/ocaml monitors and specifications in SMT-LIB v2 standard language from a fragment of metric temporal logic with durations. This logic is a three-valued extension over a restricted fragment of metric temporal logic with durations that allow us to reason about explicit time and temporal order of durations.
+The rmtld3synth toolchain is capable of automatically generating cpp11/ocaml monitors and specifications in the SMT-LIB v2 standard language from a fragment of metric temporal logic with durations. This logic is a three-valued extension of a restricted fragment of metric temporal logic with durations, which allows us to reason about explicit time and temporal order of durations.
 
-Supported by this formalism are polynomial inequalities (using the less relation <) and the common modal operators of temporal logics U (until) and S (since). 
-The existential quantification over these formulas is also possible through the adoption of the cylindrical algebraic decomposition (CAD) method. This method is suitable for converting quantified formulas under various decomposed conditions without these quantifiers.
+Supported by this formalism are polynomial inequalities (using the less relation <) and the common modal operators of temporal logic U (until) and S (since). 
+Existential quantification via these formulae is also possible by adopting the cylindrical algebraic decomposition (CAD) method. This method is suitable for converting quantified formulas under various decomposition conditions without these quantifiers.
 
-To check formula satisfiability, the tool is ready to synthesize the logic fragment in the input language accepted by the z3 SMT solver or any other prover supporting AUFNIRA logic and SMT-LIB v2. It can be used to discard various constraints involving the duration and temporal order of the propositions.
+To check the satisfiability of formulae, the tool is ready to synthesize the logic fragment in the input language accepted by the z3 SMT solver or any other prover supporting AUFNIRA logic and SMT-LIB v2. It can be used to discard various constraints concerning the duration and temporal order of the propositions.
 
-For example, schedulability analysis of hard real-time systems is possible by specifying the complete problem in RMTLD3. First using rmtld3synth to synthesize the problem in SMT-LIB and then using Z3 to solve it. The idea is to know if there exists a trace for which the RMTLD3 problem is satisfiable, or whether the SMT gives us an unsatisfiable answer meaning that is impossible to schedule such a configuration. The latter reinforces the refinement by drawing a counterexample.
+For example, schedulability analysis of hard real-time systems is possible by specifying the complete problem in RMTLD3. First, rmtld3synth is used to synthesize the problem in SMT-LIB, and then Z3 is used to solve it. The idea is to know whether there is a trace for which the RMTLD3 problem is satisfiable, or whether the SMT gives us an unsatisfiable answer, meaning that it is impossible to plan such a configuration. The latter reinforces the refinement by giving a counterexample.
 
 # Contents
 
@@ -21,15 +21,15 @@ For example, schedulability analysis of hard real-time systems is possible by sp
 - [Documentation](#documentation)
 - [License](#license)
 
-### Get started with the online demonstrator :camel:
+## Get started with the online demonstrator :camel:
 
 The stable version is available for testing in the browser [Try it](https://anmaped.github.io/rmtld3synth).
 
-### Get started with Tarball binaries
+## Get started with Tarball binaries
 
-The latest release version is [0.4-alpha](../../releases/tag/v0.4-alpha/).
+The latest release version is [0.4](../../releases).
 
-### Get started with docker :whale:
+## Get started with docker :whale:
 
 ![build workflow](https://github.com/anmaped/rmtld3synth/actions/workflows/build-and-send-images.yml/badge.svg)
 
@@ -60,13 +60,12 @@ For further insights on instrumenting the monitors, please refer to the illustra
 Alternatively, you may explore the [Documentation](#documentation) section of rmtld3synth. This resource provides valuable insights into creating monitors for various targets such as bare metal or operating systems like NuttX and FreeRTOS.
 
 
-### Building from Git
+## Building from Git
 
 ![run tests workflow](https://github.com/anmaped/rmtld3synth/actions/workflows/run-tests.yml/badge.svg)
 
-<!--[![Build Status](https://app.travis-ci.com/anmaped/rmtld3synth.svg?branch=master)](https://app.travis-ci.com/anmaped/rmtld3synth)-->
 
-#### To compile rmtld3synth for Linux and macOS using Opam and Ocaml version >= 4.04.0
+### To compile rmtld3synth for Linux and macOS using Opam and Ocaml version >= 4.04.0
 
 To build rmtld3synth for Linux and macOS using Opam and a minimum Ocaml version of 4.04.0, follow these steps:
 
@@ -96,7 +95,7 @@ sudo make install
 Please ensure that you have at least Python version 2.7 and `g++-5` installed on your system.
 
 
-#### To compile rmtld3synth for Windows using ocaml >= 4.04.0
+### To compile rmtld3synth for Windows using ocaml >= 4.04.0
 
 Get [Andreas Hauptmann's installer](https://fdopen.github.io/opam-repository-mingw/installation/) and switch the Ocaml compiler to version `>= 4.04.0``.
 
@@ -125,31 +124,40 @@ CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar py
 Ensure also that libz3 is properly installed in the current environment.
 If the libz3 is not found then use the copy command to copy the `z3/build/libz3.dll.a` library to the `/lib` or `/home/current-user/.opam/compiler-version/lib` directory.
 
-#### Instructions to use rtmlib2
+## Notes on rtmlib2
 
-The current version is [v2.0.1](https://github.com/anmaped/rtmlib/tags).
+The current version is [v2.0.5](https://github.com/anmaped/rtmlib/tags).
+
+![build workflow](https://github.com/anmaped/rtmlib/actions/workflows/build-and-send-images.yml/badge.svg)
 
 The rtmlib2 is a support library for embedding runtime monitors written in CPP11.
 
-Note that we can skip this compilation step if we do not need to integrate the monitors into the target system or if we just want to synthesize RMTLD3 specifications in SMT-Libv2.
+Note that we can skip this compilation step if we do not need to integrate the monitors into the target system, or if we just want to synthesize the RMTLD3 specifications into SMT-Libv2.
 
-Please ensure that you have the gcc 4.7.0 or greater with the c++0x standard flag enabled. Proper files to support atomics are provided in the GIT repository and do not need to be added afterward (only for GCC 4.7.0 version).
+Please make sure you have gcc 4.7.0 or later with the c++0x standard flag enabled. The appropriate files to support atomics are provided in the GIT repository and do not need to be added afterward (only for GCC 4.7.0 version).
 
-More details are available in the [rtmlib documentation repository](https://anmaped.github.io/rtmlib/doc/).
+See below for more details. See also the [rtmlib documentation repository](https://anmaped.github.io/rtmlib/doc/).
 
 
 ## Documentation
 
-- [rmtld3synth's CLI](doc/general.md#overview-of-the-command-line-interface-of-rmtld3synth)
-  - [The Configuration File](doc/general.md#overview-of-the-configuration-file)
-- [Write Formulas in RMTLD3](doc/general.md#write-formulas-in-rmtld3)
-- [Import Formulas from Latex Equations](doc/general.md#write-formulas-in-latex-and-know-how-to-use-them)
-- [Compile generated Monitors](doc/general.md#compile-the-generated-monitors)
-- [Map Event Symbols](doc/general.md#map-event-symbols)
-- [Integrate Monitors using rtmlib in Bare Metal Platforms](doc/general.md#integrate-monitors-using-rtmlib-in-a-bare-metal-platform)
-  - [NuttX](doc/general.md#nuttx-os)
-  - [FreeRTOS](doc/general.md#freertos)
-- [Unit Test Generation](doc/general.md#unit-test-generation)
+- [Overview of the Command Line Interface of rmtld3synth](doc/general.md#overview-of-the-command-line-interface-of-rmtld3synth)
+- [Input Languages](doc/general.md#input-languages)
+  - [With DSL (prefered)](doc/input-languages.md#with-dsl-prefered)
+  - [With symbolic expressions (old style)](doc/input-languages.md#with-symbolic-expressions-old-style)
+  - [LaTex expressions for paper writing purposes](doc/input-languages.md#latex-expressions-for-paper-writing-purposes)
+- [Include Monitors with rtmlib2](doc/general.md#include-monitors-with-rtmlib2)
+  - [Sample](doc/general.md#sample-runs-on-all-architectures-supported-by-rtmlib2)
+  - [Bare Metal (without OS)](doc/general.md#bare-metal-without-os)
+  - Real-time OS
+    - [NuttX](doc/general.md#nuttx-os)
+    - [FreeRTOS](doc/general.md#freertos)
+    - [RTEMS](doc/general.md#rtems)
+  - [Hardware (FPGA)](doc/general.md#hardware-fpga)
+  - [Mapping between propositions and symbols](doc/general.md#to-show-the-mapping-between-the-propositions-and-the-symbols)
+- [Translate rmtld3 to smtlibv2](doc/general.md#translate-rmtld3-to-smtlibv2)
+- [The Configuration File (optional)](doc/general.md#configuration-file-optional)
+  - [Unit Tests flags](doc/general.md#unit-tests-flags)
 
 
 ## License

unittests/rmtld3/unittest.ml

@@ -160,8 +160,9 @@ let rmtld3_unit_test_generation cluster_name cpp11_compute helper =
       let id = string_of_int (get_counter_test_cases helper) in
       Printf.printf "\x1b[32m[Sucess]\x1b[0m (%s) \n" (b3_to_string t_value);
       (* to generate C++ unit tests *)
-      call_code :=
+      call_code := 
         !call_code
+        ^ "// " ^ lb ^ "\n"
         ^ (rmtld3_unit_test_case_generation trace formula t_value cpp11_compute helper
             cluster_name n);
       Printf.printf "count_until: %i, stack_deep:%i count_full:%d\n" !count
@@ -423,7 +424,7 @@ let rmtld3_unit_test_generation cluster_name cpp11_compute helper =
       ("A", (9., 20.));
     ]
   in
-  pass_test Unknown "usecase1" trc usecase1_formula;
+  pass_test Unknown (string_of_rmtld_fm usecase1_formula) trc usecase1_formula;
 
   let filename = cluster_name ^ "/tests/unit_test_cases.h" in
   let oc = open_out filename in