DOI: 10.5281/zenodo.17390557
title: Alloy4Fun Dataset for 2024/25

description: This dataset contains models submitted by students in the Alloy4Fun platform to solve the challenge models from various editions of formal methods courses in the University of Minho (UM) and the University of Porto (UP) between the fall of 2019 and the spring of 2025, totalling around 185.000 entries. Participants include those enrolled in the optional MSc course "Specification and Modelling" (EM) and the mandatory MSc course "Formal Methods in Software Engineering" (MFES) in UM, and the optional MSc course "Formal Methods for Critical Systems" (MFS) in UP. Note that since the challenges' permalinks are publicly available, the dataset may contain submissions from other participants outside the classroom context.

The analysis of the 2021 dataset is reported in the Science of Computer Programming paper "Experiences on Teaching Alloy with an Automated Assessment Platform" (extending the ABZ'20 conference version analysing the 2020 dataset).




Name
Permalink
Courses (Students)
Entries




Trash FOL
sDLK7uBCbgZon3znd
EM 19/20 (~20) & 20/21 (~20), MFS 21/22 (~10) & 22/23 (~10)
4333


Classroom FOL
YH3ANm7Y5Qe5dSYem
EM 19/20 (~20) & 20/21 (~20), MFS 21/22 (~10) & 22/23 (~10)
5106


Trash RL
PQAJE67kz8w5NWJuM
EM 19/20 (~20) & 20/21 (~20)
4929


Classroom RL
zRAn69AocpkmxXZnW
EM 19/20 (~20) & 20/21 (~20)
6813


Graphs
gAeD3MTGCCv8YNTaK
EM 19/20 (~20) & 20/21 (~20)
3382


LTS
zoEADeCW2b2suJB2k
EM 19/20 (~20) & 20/21 (~20)
3597


Production line


jyS8Bmceejj9pLbTW

bNCCf9FMRZoxqobfX (v2)

aTwuoJgesSd8hXXEP (v3)

dyj49tEp7j6aWAQQX (v4)



EM 19/20 (~20) & 20/21 (~20)

MFES 21/22 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24. (~10)

MFES 22/23 (~200)

MFES 23/24 (~200) & 24/25 (~200)



2582

6731

3684

13238



CV


JC8Tij8o8GZb99gEJ 

WGdhwKZnCu7aKhXq9 (v2)



EM 19/20 (~20)

EM 20/21 (~20)



1423

393



Trash LTL
9jPK8KBWzjFmBx4Hb
EM 19/20 (~20) & 20/21 (~20)
5910


Train Station


FwCGymHmbqcziisH5

QxGnrFQnXPGh2Lh8C (v2)

cXPP9QBPTYgTX6WJ6 (v3)



EM 20/21 (~20)

MFES 21/22 (~200) & 22/23 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24 (~10)

MFES 23/24 (~200) & 24/25 (~200)



1285

9383

8805



Courses


PSqwzYAfW9dFAa9im

JDKw8yJZF5fiP3jv3 (v2)

iP5JL36afv5KbDKP6 (v3)



MFES 21/22 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24 (~10)

MFES 22/23 (~200)

MFES 23/24 (~200) & 24/25 (~200)



17515

8533

25722



Social network


dkZH6HJNQNLLDX6Aj

x3JXgWhJ3uti5Dzxz (v2)



MFES 21/22 (~200) & 22/23 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24 (~10)

MFES 23/24 (~200) & 24/25 (~200)



24688

27302





Each entry of the dataset registers either an execution (which may have returned a result or an error) or the creation of a permalink for sharing, and contains:



_id: the id of the interaction

time: the timestamp of its creation

derivationOf: the parent entry

original: the first ancestor with secrets (always the same within an exercise)

code: the complete code of the model (excluding the secrets defined in the original entry) (with student comments removed)

sat: whether the command was satisfiable (counter-example found for checks), or -1 when error thrown [only for executions]

cmd_i: the index of the executed command [only for executions]

cmd_n: the name of the executed command [only for successful executions, i.e. no error thrown]

cmd_c: whether the command was a check [only for successful executions, i.e. no error thrown]

msg: the error or warning message [only for successful executions with warnings or when error thrown]

theme: the visualisation theme [only for sharing entries]


User comments were removed from the code to guarantee anonymization.