Add & reorganize syntax tests

[ahelwer]

Also added some failing tests. We can rely on a patch file (also checked in) to modify them to be skipped when syncing tests with the tlaplus-standard repo.