DOI: 10.5281/zenodo.8123547
title: Alloy4Fun Dataset for 2022/23

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 2023, totalling about 100.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) and 20/21 (~20), MFS 21/22 (~10) and 22/23 (~10)
			4092
		
		
			Classroom FOL
			YH3ANm7Y5Qe5dSYem
			EM 19/20 (~20) and 20/21 (~20), MFS 21/22 (~10) and 22/23 (~10)
			5893
		
		
			Trash RL
			PQAJE67kz8w5NWJuM
			EM 19/20 (~20) and 20/21 (~20)
			4361
		
		
			Classroom RL
			zRAn69AocpkmxXZnW
			EM 19/20 (~20) and 20/21 (~20)
			6341
		
		
			Graphs
			gAeD3MTGCCv8YNTaK
			EM 19/20 (~20) and 20/21 (~20)
			3211
		
		
			LTS
			zoEADeCW2b2suJB2k
			EM 19/20 (~20) and 20/21 (~20)
			3382
		
		
			Production line
			
			
jyS8Bmceejj9pLbTW

			
bNCCf9FMRZoxqobfX (v2)

			
aTwuoJgesSd8hXXEP (v3)
			
			
			
EM 19/20 (~20) and 20/21 (~20)

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

			
MFES 22/23 (~200)
			
			
			
898

			
4903

			
3175
			
		
		
			CV
			
			
JC8Tij8o8GZb99gEJ 

			
WGdhwKZnCu7aKhXq9 (v2)
			
			
			
EM 19/20 (~20)

			
EM 20/21 (~20)
			
			
			
1199

			
393
			
		
		
			Trash LTL
			9jPK8KBWzjFmBx4Hb
			EM 19/20 (~20) and 20/21 (~20)
			5279
		
		
			Train Station
			
			
FwCGymHmbqcziisH5

			
QxGnrFQnXPGh2Lh8C (v2)
			
			
			
EM 20/21 (~20)

			
MFES 21/22 (~200) and 22/23 (~200), MFS 21/22 (~10) and 22/23 (~10)
			
			
			
1264

			
8158
			
		
		
			Courses
			
			
PSqwzYAfW9dFAa9im

			
JDKw8yJZF5fiP3jv3 (v2)
			
			
			
MFES 21/22 (~200), MFS 21/22 (~10) and 22/23 (~10)

			
MFES 22/23 (~200)
			
			
			
14884

			
7632
			
		
		
			Social network
			dkZH6HJNQNLLDX6Aj
			MFES 21/22 (~200) and 22/23 (~200), MFS 21/22 (~10) and 22/23 (~10)
			22690
		
	



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.