Test the behavior under anomalous operating conditions

These are test cases to check the TLA+ Model Checker behavior under anomalous operating conditions. These tests use the same model, but checking of the model is performed under specific conditions, where where computational resources (depending on the test case) are not enough to complete the task successfully. Main objective of these tests is to ensure that the tool is capable to detect and report such situations. Thus expecting outcome is crash for all the cases.

Test Cases

Id	Anomalous Conditions	Model Checking Status	Expected Status	Test Results	Test Model
482473e2fd649da0c4fc2909e877338427052e31	Out of memory	crash	crash	Passed	Model Under Test
b3f15c4cfe9b60515342b1b480a1f55d86e4a9fc	out of space	crash	crash	Passed	Model Under Test
600e647414de312cefad469ab4b57ba4a90b1994	Out of handles	crash	crash	Passed	Model Under Test