Release version v0.5 of the rmtld3synth tool

v0.5 release features:

• Improve error messages.
• Macro improvements for easy buffer size editing.
• Add .devcontainer.json file.
• Fix enum type mismatch with std::underlying_type.
• Add unique ids for cpp11 monitor generation.
• Add generation of push and push_all functions.
• Add Containerfile.slim file.
• Update rtmlib2 for v2.1.0.
• Fix adjust_base gamma to avoid losing precision.
• Add time_of_s, time_of_ms for base time conversion.
• Refactor helper.ml file.
• Add Szudzik Pairing.
• Add raw input expressions to settings.
• Add cpp11 unbounded mprev explicit conversion.
• Improve dsl-parser error messages.
• Add 'within range' support for dsl-parser.

Full Changelog: v0.4...v0.5

Release version v0.4 of the rmtld3synth tool

v0.4 release features:

• Fix dsl-parser term associativity.
• Add units to dsl-parser terms.
• Remove extensional operator U[<=] from rmtld3.
• Add (~) symbol to dsl-parser.
• Implement unittest for texeqparser.
• Add support for the next operator in the DSL.
• Fix solver version 4.12.3.
• Add support for the Since operator and remove old SMT encoding.
• Update rtmlib2 version.
• Fix typo in string_of_rmtld_fm function.
• Add Since equal operator.
• Add graphical examples.
• Add wave3 examples.
• Add unbounded eventually less operator for cpp11 conversion.
• Enable the usage of --input-dsl in --synth-smtlibv2.
• Add documentation for the instrumentation and monitoring of the sample example.
• Update documentation for v0.4 and rtmlib2 for v2.0.5.

Full Changelog: v0.4-alpha...v0.4

Release version v0.4-alpha of the rmtld3synth tool

v0.4-alpha release features:

• Fix declaration of propositions with C++11 enumerations
• Integration of the new dsl-parser
• Add error tests to dsl-parser by @jantoniobfg in #8
• Add rtm_monitor_time_unit setting
• Improves cpp11 monitor construction and supports new rtmlib2
• Fix z3 store array
• Refactoring of C++11 synthesis with new rtmlib2
• Add simple_monitor HLS example

Release version v0.3-alpha2 of the rtmld3synth tool

v0.3-alpha release features:

• Supports synthesis from latex equations using the argument --input-latexeq
• Supports synthesis from the micro resource DSL using the argument --input-rmdsl (excellent to encode scheduling schemes)
• Ready for solving problems in the SMTLibv2 language using Z3 (--solver-z3) and CVC4 (--solver-cvc4) SMTs
• Enables the recursive unrolling optimization using the argument --recursive-unrolling
• Ready to communicate with Mathematica 10 for simplifying quantified formulas using the argument --simpl-cad
• Ready for generating random RMTLD formulas using the argument --gen-rmtld-formula
• Supports js_of_ocaml

Release version v0.2-alpha of the rtmld3synth tool

v0.2-alpha release features:

• Support for generating monitors in C++ (NuttX OS ready)
• Added support for synthesis of RMTLD3 formulas to SMTLibv2 language (Z3 solver ready)