On Writing Alloy Models: Metrics and a New Dataset1 minAlloy Formal Methods Model Analysis Formal Specification