Unfortunately I got the product wrong; it was not Atlas, it was Realm Sync. All of the test-case generation stuff is in Section 5.