We are excited to announce the publication of our new paper, dataset, and accompanying code: On Writing Alloy Models: Metrics and a New Dataset presented at ABZ 2025
In this work, we introduce FMPals, a new dataset of Alloy models authored on our Formal Methods Playground.
📁 What We’re Releasing
📄 Paper:
Soaibuzzaman, S. Kalantari, J.O. Ringert. On Writing Alloy Models: Metrics and a new Dataset. Rigorous State-Based Methods. ABZ 2025. LNCS 15728, pp. 1–18, 2025.
📚 DOI: 10.1007/978-3-031-94533-5_5
🗃️ Dataset:
Formal Methods Playground Alloy Dataset 🔗 Zenodo: https://zenodo.org/records/15619393
💻 Code & Metrics:
Includes our Halstead metric implementation and all scripts for edit path analysis and data processing. 🔗 GitHub: https://github.com/se-buw/alloy-metrics
🧪 Highlights from the Paper
A new application of Halstead difficulty metrics to Alloy.
Comparison with the Alloy4Fun dataset shows:
- Broader modeling behaviors in FMPals.
- Frequent user edits to all language constructs.
- Iterative and exploratory modeling styles.
Insights into how users fix errors and how model complexity evolves over time.
