|
| 1 | +--- |
| 2 | +title: New Dataset and Metrics for Analyzing Alloy Models |
| 3 | + |
| 4 | +event: ABZ 2025 β 11th International Conference on Rigorous State Based Methods |
| 5 | +event_url: https://abz-conf.org/site/2025/ |
| 6 | + |
| 7 | +location: DΓΌsseldorf, Germany |
| 8 | + |
| 9 | + |
| 10 | +summary: '' |
| 11 | +abstract: '' |
| 12 | + |
| 13 | +date: '2025-06-10T00:00:00Z' |
| 14 | +all_day: true |
| 15 | + |
| 16 | +# Schedule page publish date (NOT talk date). |
| 17 | +publishDate: '2024-06-10T00:00:00Z' |
| 18 | + |
| 19 | +authors: [] |
| 20 | +tags: [] |
| 21 | + |
| 22 | +# Is this a featured talk? (true/false) |
| 23 | +featured: false |
| 24 | + |
| 25 | +image: |
| 26 | + caption: '' |
| 27 | + focal_point: Right |
| 28 | + |
| 29 | +url_code: https://github.com/se-buw/alloy-metrics |
| 30 | +url_pdf: https://soaib.me/publications/resources/ABZ25.pdf |
| 31 | +url_slides: '' |
| 32 | +url_video: '' |
| 33 | + |
| 34 | +# Markdown Slides (optional). |
| 35 | +# Associate this talk with Markdown slides. |
| 36 | +# Simply enter your slide deck's filename without extension. |
| 37 | +# E.g. `slides = "example-slides"` references `content/slides/example-slides.md`. |
| 38 | +# Otherwise, set `slides = ""`. |
| 39 | +slides: |
| 40 | + |
| 41 | +# Projects (optional). |
| 42 | +# Associate this post with one or more of your projects. |
| 43 | +# Simply enter your project's folder or file name without extension. |
| 44 | +# E.g. `projects = ["internal-project"]` references `content/project/deep-learning/index.md`. |
| 45 | +# Otherwise, set `projects = []`. |
| 46 | +projects: FM Playground |
| 47 | +--- |
| 48 | + |
| 49 | +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](https://abz-conf.org/site/2025/) |
| 50 | + |
| 51 | +In this work, we introduce FMPals, a new dataset of Alloy models authored on our Formal Methods Playground. |
| 52 | + |
| 53 | + |
| 54 | +### π What Weβre Releasing |
| 55 | + |
| 56 | +#### **π Paper:** |
| 57 | + |
| 58 | +> 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. |
| 59 | +
|
| 60 | +> [π₯ PDF](https://soaib.me/publications/resources/ABZ25.pdf) |
| 61 | +
|
| 62 | +> π DOI: [10.1007/978-3-031-94533-5_5](https://doi.org/10.1007/978-3-031-94533-5_5) |
| 63 | +
|
| 64 | +#### **ποΈ Dataset:** |
| 65 | + |
| 66 | +> Formal Methods Playground Alloy Dataset |
| 67 | +> [π Zenodo: https://zenodo.org/records/15619393](https://zenodo.org/records/15619393) |
| 68 | +
|
| 69 | +#### **π» Code & Metrics:** |
| 70 | + |
| 71 | +> Includes our Halstead metric implementation and all scripts for edit path analysis and data processing. |
| 72 | +> [π GitHub: https://github.com/se-buw/alloy-metrics](https://github.com/se-buw/alloy-metrics) |
| 73 | +
|
| 74 | + |
| 75 | +### π§ͺ Highlights from the Paper |
| 76 | + |
| 77 | +* A new application of **Halstead difficulty metrics** to Alloy. |
| 78 | +* Comparison with the Alloy4Fun dataset shows: |
| 79 | + |
| 80 | + * Broader modeling behaviors in FMPals. |
| 81 | + * Frequent user edits to all language constructs. |
| 82 | + * Iterative and exploratory modeling styles. |
| 83 | +* Insights into how users fix errors and how model complexity evolves over time. |
0 commit comments