Sequential Training Problems
The problems listed here represent smaller versions of the actual problems used during the RERS Challenge 2020. Problems 1 – 3 resemble problems from the Sequential LTL track. As with the challenge problems, C99 and Java versions are available for each training problem.
This year, we have fine-tuned the depth of LTL counterexamples, meaning the number of steps required to falsify a given property, based on a newly conceived approach for safety properties. Therefore, the new training problems below only feature safety properties. Actual challenge problems might also include other properties. For examples, please consider looking at training problems from previous RERS iterations such as 2019.
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.
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.
- .constraints-... (.txt file): LTL properties that participants of RERS have to check on the given program. See the problem description for details.
- constraints-solution-... (.txt file): Lists the correct "true"/"false" answers for each property, including exemplary counterexample traces for violated properties. This will not be available for actual challenge problems.
plain, small | arithmetic, small | data structures, small |
Problem1 | Problem2 | Problem3 |
Reachability Training Problems
Please use the training problems from previous challenge iterations, for example those from RERS 2019.