Introduction
This report contains test specification and results of their execution. There are several kinds of tests:- Tests obtained by combining pairwise feature combinations. Feature is a TLA+ operator, constant, variable, or other TLA+ language construct, which is required to support the use cases. These cases utilize back-to-back testing approach to evaluate if a test is failed or passed.
- Some feature combinations make not sense (e.g., integer multiplication and boolean constant). Such combinations are "skipped": no test case is generated out of them. All such combinations are listed in the page Skipped feature combinations along with reasons, why they have been skipped
- If during back-to-back testing outcomes of the model-under-test and equivalent model diverge, the test is failed. All failed cases are listed in the page Failed test cases. This report also provides explanation for every failed test case. There must be no failed tests without explanation
- There is a group of SYMMETRY tests, designed to validate important model checker optimization for symmetry sets. These tests also use back-to-back approach, but the only difference between model-under-test and equivalent model is that the latter does not use symmetry set optimization. These cases utilize back-to-back testing approach to evaluate if a test is failed or passed.
- Another group of tests is designed to validate TLA+ Model Checker behavior, when command line switch -workers is provided with a value greater than one. (Note that test cases above use command line option -workers 1). And these test cases check that the number of workers does not affect model checking results.
- The last group of tests checks the behavior of the tool under anomalous operating conditions, where computational resources are not enough to complete the task successfully. Main objective of the tests under anomalous conditions is to ensure that the tool is capable to detect and report such situations. These cases are expected to fail.
Statistics
| Skipped test cases | 22718 |
| Generated test cases | 54591 |
| Passed test cases | 54501 |
| Failed with explanation | 90 |
| Failed without explanation | 0 |