Alloy is a declarative formal modeling language with syntax derived from notations common to object-oriented design and a first-order relational logic semantics. To better understand the usability of Alloy, the paper presents the results of an empirical study with 30 participants assessing two types of modeling tasks: bug fixing and model building based on natural language specifications. The participants consisted of both novices and non-novices. Besides accuracy and time to complete tasks, we also examined the correlation between the performance of two cognitive tasks (mental rotation and operation span) and task performance. Results indicate that overall non-novices completed the tasks with significantly higher accuracy (54% more accurate) than novices. In the novice group, performing more actions using the Alloy analyzer led to more edits and, eventually higher scores in bug fixing tasks. We found that participants of all levels had much difficulty writing a model from scratch, and they did not utilize the analyzer to improve their models. On average, non-novices completed all the tasks 32 minutes faster than novices. Non-novices who performed better on the Alloy tasks had higher mental rotation scores, which indicates the importance of spatial cognition ability in solving Alloy tasks. Overall, we find that there is a definite need for improving the usability of the visualizations in Alloy Analyzer. We discuss the implications of these findings.