Research / Alloy4Fun dataset
Models tell a story, too.
The Alloy4Fun dataset brings together student submissions from formal methods courses. Explore the published collection and its documentation on Zenodo.
View the dataset ↗ A space for better questions
Make ideas
precise.
Meet Alloy Studio: an interactive learning environment inspired by Alloy4Fun, with next-step hints and behavioral feedback for exploring Alloy models.
AN IDEA, MADE VISIBLE
＋
01 / DEFINEGive ideas shape
02 / RELATEConnect the pieces
03 / EXPLORESee what follows
ALLOY4FUN / 001Think in models✳ Explore relationshipsAsk better questions ↗
A clearer way to think
Big ideas start
with small models.
Alloy is a language for describing structures and exploring their consequences. By making assumptions explicit, a model gives us a way to reason about a system before its details get in the way.
Alloy Studio builds on the original Alloy4Fun experience with edit-distance hints and a behavioral similarity score, helping learners understand what to try next and how a formula behaves.
01 / DEFINE
Frame the idea.
Start with the things that matter and describe the rules that connect them.
02 / EXPLORE
Follow the logic.
Think through possible configurations and discover what your assumptions allow.
03 / LEARN
Refine your thinking.
Use what you find to ask sharper questions and develop a clearer model.
Research in practice
More chances to find a way forward.
In the manuscript Automated Hint Guidance for Alloy Models, both Alloy Studio hint modes produced a nonempty hint for every incorrect submission in the evaluation. The study compares them with TAR and HiGenA using the Alloy4Fun dataset.
Availability measures whether a hint was returned—not whether it was helpful or a verified repair.
ALLOY STUDIO / CANONICAL & AST
100%
42,388 of 42,388 incorrect submissions received a hint.
TAR
44.59%
18,901 incorrect submissions received a hint.
HIGENA / WITH MUTATION
50.42%
21,373 incorrect submissions received a hint.
Study conditions: 42,388 incorrect inputs, five-fold session-based evaluation, and a 60-second deadline. HiGenA history-only returned hints for 34.02%. The manuscript also reports nonempty hints on some held-out correct submissions: 8.68% for Canonical and 21.29% for AST. Results describe this benchmark, not guaranteed performance on every model. Source: Automated Hint Guidance for Alloy Models, research manuscript; see also the project repository.
Built on a history of learning
From an online portal to a shared resource.
The original Alloy4Fun portal was created for editing and sharing Alloy models online, with an emphasis on education. Its stored model versions and derivation histories opened a window into how people learn and work with Alloy.
Read the original paper ↗ Keep exploring
Curiosity looks good on you.
Start with the research, explore the dataset, and see where a model can take you.
Open Alloy Studio ↗