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
b9cfb78c128a4fcd1238faac654c2ca75a9c7f99	Out of memory	crash	crash	Passed	Model Under Test
3c387b798f2f6070037cd956958aeb2947bdac83	out of space	crash	crash	Passed	Model Under Test
67527e7962f2cb339b2b8051ce0df22c97fec3c9	Out of handles	crash	crash	Passed	Model Under Test