Identifying the limits of transformers when performing model-checking with natural language