The problems listed below are similar to the challenge problems of the industrial tracks of RERS 2019. As with the challenge problems, C99 and Java versions are available for each training problem.

---

Important update (Mar. 13th):

The C99 code of all training problems has been replaced.

---

Within each track (LTL/CTL/Reachability), there are three training problems in the category "arithmetic" and three problems in the category "data structures". In contrast to the challenge problems, both categories are based on the same set of models. LTL and CTL problems are based on the same code/model in a given category whereas reachability problems feature their own version of the code/model.

Reachability properties are encoded in the source code whereas LTL and CTL files are provided as .txt files. In addition to these property specifications, the following files are contained in each problem's directory:

• .java file: Java version of the source code.
• .c file: C99 version of the source code.
• "...alphabet_mapping_C_version.txt" file: Bijection between the integer values in the C99 version and the input/output symbols in the property descriptions.
• .traces file: Execution logs provided by ASML. See the problem description for details.
• .aut file: Reference model based on which the source code was generated. This will not be available for actual challenge problems.
• "solution_..." file: Lists the correct "true"/"false" answers for each property. This will not be available for actual challenge problems.

For further information on these problems, please refer to the problem description and the Java code and C99 code description.

LTL Training Problems

A zip containing the LTL training problems and solutions can be downloaded here.

---

CTL Training Problems

A zip containing the CTL training problems and solutions can be downloaded here.

---

Reachability Training Problems

A zip containing the reachability training problems and solutions can be downloaded here.